(* 単一化 *)

From mathcomp Require Import all_ssreflect.
Require String.
Import String.StringSyntax.
Open Scope string_scope.

Lemma mem_tail {A:eqType} x a {l : seq A} : x \in l -> x \in a::l.
Proof. rewrite inE => ->; exact/orbT. Qed.
Hint Resolve mem_head mem_tail : core.

(* 変数 *)
Definition var := nat.

(* 定数・関数記号 *)
Notation symbol := String.string.
Definition symbol_dec := String.string_dec.

(* 項は木構造 *)
Inductive tree : Set :=
  | Var : var -> tree
  | Sym : symbol -> tree
  | Fork : tree -> tree -> tree.

(* 自動的に等価性を生成する *)
Scheme Equality for tree. (* 8.9で動かないかも *)

(* Equality が失敗するなら手で定義する *)
Definition tree_eq_dec' (t1 t2 : tree) : {t1 = t2}+{t1 <> t2}.
  revert t2; induction t1; destruct t2; try by right.
  - case /boolP: (v == v0) => /eqP H. by left; rewrite H. by right; case.
  - case (symbol_dec s s0) => H. by left; rewrite H. by right; case.
  - case (IHt1_1 t2_1) => [<-|N]; last by right; case.
    case (IHt1_2 t2_2) => [<-|N']. by left. by right; case.
Defined.

(* tree を eqType として登録する *)
Lemma tree_eq_boolP : Equality.axiom tree_eq_dec.
Proof. move=> x y. case: tree_eq_dec => //= H; by constructor. Qed.
Definition tree_eq_mixin := EqMixin tree_eq_boolP.
Canonical tree_eqType := Eval hnf in EqType _ tree_eq_mixin.

(* [t/x] t' *)
Fixpoint subs (x : var) (t t' : tree) : tree :=
  match t' with
  | Var v => if v == x then t else t'
  | Sym b => Sym b
  | Fork t1 t2 => Fork (subs x t t1) (subs x t t2)
  end.

(* 代入は変数代入の繰り返し *)
Definition subs_list (s : list (var * tree)) t : tree :=
  foldl (fun t (p : var * tree)  => subs p.1 p.2 t) t s.

(* 単一子の定義 *)
Definition unifies s (t1 t2 : tree) := subs_list s t1 = subs_list s t2.

(* 例 : (a, (x, y)) [x := (y, b)] [y := z] = (a, ((z,b), z)) *)
Definition atree := Fork (Sym "a") (Fork (Var 0) (Var 1)).
Definition asubs := (0, Fork (Var 1) (Sym "b")) :: (1, Var 2) :: nil.
Eval compute in subs_list asubs atree.

(* 和集合 *)
Fixpoint union (vl1 vl2 : list var) :=
  if vl1 is v :: vl then
    if v \in vl2 then union vl vl2 else union vl (v :: vl2)
  else vl2.

Lemma in_union_or v vl1 vl2 :
  v \in union vl1 vl2 = (v \in vl1) || (v \in vl2).
Proof.
  elim: vl1 vl2 => //= x vl IH vl2.
  case: ifP => Hx /=.
  - rewrite inE IH.
    case/boolP: (v == x) => // /eqP ->.
    by rewrite Hx orbT.
  - by rewrite IH !inE orbA (orbC (v == x)).
Qed.

(* 完全性のために必要 *)
Lemma uniq_union vl1 vl2 : uniq vl2 -> uniq (union vl1 vl2).
Proof.
  elim: vl1 vl2 => //= v vl IH vl2 H.
  case: ifP => Hv; by rewrite IH //= Hv.
Qed.

(* 出現変数 *)
Fixpoint vars (t : tree) : list var :=
  match t with
  | Var x => [:: x]
  | Sym _ => nil
  | Fork t1 t2 => union (vars t1) (vars t2)
  end.

(* 出現しない変数は代入されない *)
Lemma subs_same v t' t : v \notin (vars t) -> subs v t' t = t.
Proof.
  elim: t => //= [x | t1 IH1 t2 IH2].
  - by rewrite inE eq_sym => /negbTE ->.
  - by rewrite in_union_or negb_or => /andP[] /IH1 -> /IH2 ->.
Qed.

Definition may_cons (x : var) (t : tree) r := omap (cons (x,t)) r.
Definition subs_pair x t (p : tree * tree) := (subs x t p.1, subs x t p.2).

(* 単一化 *)
Section Unify1.

(* 代入を行ったときの再帰呼び出し *)
Variable unify2 : list (tree * tree) -> option (list (var * tree)).

(* 代入して再帰呼び出し. x は t に現れてはいけない *) 
Definition unify_subs x t r :=
  if x \in vars t then None else may_cons x t (unify2 (map (subs_pair x t) r)).

(* 代入をせずに分解 *)
Fixpoint unify1 (h : nat) (l : list (tree * tree))
  : option (list (var * tree)) :=
  if h is h'.+1 then
    match l with
    | nil => Some nil
    | (Var x, Var x') :: r =>
      if x == x' then unify1 h' r else unify_subs x (Var x') r
    | (Var x, t) :: r =>
      unify_subs x t r
    | (t, Var x) :: r =>
      unify_subs x t r
    | (Sym b, Sym b') :: r =>
      if symbol_dec b b' then unify1 h' r else None
    | (Fork t1 t2, Fork t1' t2') :: r =>
      unify1 h' ((t1, t1') :: (t2, t2') :: r)
    | _ => None
    end
  else None.
End Unify1.

(* 等式の大きさの計算 *)
Fixpoint size_tree (t : tree) : nat :=
  if t is Fork t1 t2 then 1 + size_tree t1 + size_tree t2 else 1.

Definition size_pairs (l : list (tree * tree)) :=
  sumn [seq size_tree p.1 + size_tree p.2 | p <- l].

(* 代入したときだけ再帰 *)
Fixpoint unify2 (h : nat) l :=
  if h is h'.+1 then unify1 (unify2 h') (size_pairs l + 1) l else None.

Fixpoint vars_pairs (l : list (tree * tree)) : list var :=
  match l with
  | nil => nil                     (* 集合を後部から作るようにする *)
  | (t1, t2) :: r => union (union (vars t1) (vars t2)) (vars_pairs r)
  end.

(* 変数の数だけ unify2 を繰り返す *)
Definition unify t1 t2 :=
  let l := [:: (t1,t2)] in unify2 (size (vars_pairs l) + 1) l.

(* 例 *)
Eval compute in unify (Sym "a") (Var 1).

Eval compute in
  unify (Fork (Sym "a") (Var 0))
        (Fork (Var 1) (Fork (Var 1) (Var 2))).

(* 全ての等式の単一子 *)
Definition unifies_pairs s (l : list (tree * tree)) :=
  forall t1 t2, (t1,t2) \in l -> unifies s t1 t2.

(* subs_list と Fork が可換 *)
Lemma subs_list_Fork s t1 t2 :
  subs_list s (Fork t1 t2) = Fork (subs_list s t1) (subs_list s t2).
Proof. by elim: s t1 t2 => /=. Qed.

(* unifies_pairs の性質 *)
Lemma unifies_pairs_same s t l :
  unifies_pairs s l -> unifies_pairs s ((t,t) :: l).
Proof.
  move=> H t1 t2; rewrite inE => /orP[].
  - by case/eqP => -> ->.
  - exact/H.
Qed.

Lemma unifies_pairs_swap s t1 t2 l :
  unifies_pairs s ((t1, t2) :: l) -> unifies_pairs s ((t2, t1) :: l).
Proof.
  move=> H x y.
  rewrite inE => /orP[/eqP[-> ->] | Hl].
  - exact/esym/H.
  - exact/H/mem_tail.
Qed.

Lemma unify_subs_sound h v t l s :
  (forall s l, unify2 h l = Some s -> unifies_pairs s l) ->
  unify_subs (unify2 h) v t l = Some s ->
  unifies_pairs s ((Var v, t) :: l).
Proof.
  rewrite /unify_subs.
  case Hocc: (v \in _) => // IH.
  case Hun: (unify2 _ _) => [s'|] //= [] <-.
  move=> t1 t2.
  rewrite /unifies inE => /orP[/eqP[-> ->] | Hin] /=.
    by rewrite eqxx subs_same // Hocc.
  apply (IH _ _ Hun).
  exact: (map_f (subs_pair v t) Hin).
Qed.

(* unify2 の健全性 *)
Theorem unify2_sound h s l :
  unify2 h l = Some s -> unifies_pairs s l.
Proof.
  elim: h s l => //= h IH s l.
  move: (size_pairs l + 1) => h'.
  elim: h' l => //= h' IH' [] //.
  move=> [t1 t2] l.
  destruct t1, t2 => //.
  (* VarVar *)
- case: ifP.
    by move=> /eqP <- /IH' /unifies_pairs_same.
  move=> _ /unify_subs_sound; exact.
  (* VarSym *)
- move/unify_subs_sound; exact.
  (* VarFork *)
- move/unify_subs_sound; exact.
  (* SymVar *)
- move/unify_subs_sound/unifies_pairs_swap; exact.
  (* SymSym *)
- by case: symbol_dec => //= -> /IH'/unifies_pairs_same.
  (* ForkVar *)
- move/unify_subs_sound/unifies_pairs_swap; exact.
  (* ForkFork *)
- move/IH' => Hun t1 t2.
  rewrite inE => /orP[/eqP[-> ->] | Hl].
    rewrite /unifies !subs_list_Fork.
    rewrite (Hun t1_1 t2_1) //.
    rewrite (Hun t1_2 t2_2); by auto.
  apply Hun; by auto.
Qed.

(* 単一化の健全性 *)
Corollary soundness t1 t2 s :
  unify t1 t2 = Some s -> unifies s t1 t2.
Proof. move/unify2_sound; exact. Qed.

(* 完全性 *)

(* 循環的な項が作れない *)
Lemma not_unifies_occur v t s :
  Var v != t -> v \in vars t -> ~unifies s (Var v) t.
Proof.
  rewrite /unifies.
  move=> vt Ht Hun.
  (* size_tree で矛盾を導く *)
  have Hs: size_tree (subs_list s (Var v)) >= size_tree (subs_list s t).
    by rewrite Hun.
  (* 元の仮定を消してから帰納法を使う *)
  elim: t {Hun} vt Ht Hs => //= [v' | t1 IH1 t2 IH2] vt.
  (* Var *)
  rewrite inE => /eqP Hv.
  by rewrite Hv eqxx in vt.
  (* Fork *)
  rewrite subs_list_Fork /= in_union_or => /orP[] Hv Hs.
  - apply IH1 => //.
      case vt1: (Var v == t1) Hs => //.
      by rewrite -(eqP vt1) -addnA add1n ltnNge leq_addr.
    apply/leq_trans: Hs.
    by rewrite (addnC 1) -addnA leq_addr.
  - apply IH2 => //.
      case vt2: (Var v == t2) Hs => //.
      by rewrite -(eqP vt2) -addnA add1n ltnNge leq_addl.
    apply/leq_trans: Hs.
    by rewrite leq_addl.
Qed.

(* 集合の要素の数に関する基礎的な補題 *)
Lemma size_union2 l1 l2 : size (union l1 l2) >= size l2.
Proof.
  elim: l1 l2 => //= v l1 IH l2.
  case: ifP => Hv //.
  refine (leq_trans _ (IH _)); exact: ltnW.
Qed.

(* Sym の代入 *)
Lemma subs_list_Sym s f : subs_list s (Sym f) = Sym f.
Proof. by elim: s => //= -[]. Qed.

(* 代入の合成 *)
Lemma unifies_extend s v t t' :
  unifies s (Var v) t -> unifies s (subs v t t') t'.
Proof.
  elim: t' => //= [v' | t1 IH1 t2 IH2] Hs.
    by case: ifP => // /eqP ->.
  by rewrite /unifies !subs_list_Fork IH1 // IH2.
Qed.

Lemma unifies_pairs_extend s v t l :
  unifies_pairs s ((Var v, t) :: l) -> unifies_pairs s (map (subs_pair v t) l).
Proof.
  move=> H t1 t2 /mapP /= [] [t3 t4] Hl [-> ->].
  have Hv : unifies s (Var v) t by apply H.
  rewrite /unifies !unifies_extend //.
  apply H; by auto.
Qed.

Lemma unifies_pairs_Fork s t1 t2 t'1 t'2 l :
  unifies s (Fork t1 t2) (Fork t'1 t'2) ->
  unifies_pairs s l ->
  unifies_pairs s ((t1,t'1)::(t2,t'2)::l).
Proof.
  rewrite /unifies !subs_list_Fork => -[H1 H2] Hs t3 t4.
  rewrite !inE.
  case/orP => [/eqP[-> ->] // |].
  case/orP => [/eqP[-> ->] // |].
  exact: Hs.
Qed.

(* s が s' より一般的な単一子である *)
Definition moregen s s' :=
  exists s2, forall t, subs_list s' t = subs_list s2 (subs_list s t).

(* 一般性を保ちながら拡張 *)
Lemma moregen_extend s v t s1 :
  unifies s (Var v) t -> moregen s1 s -> moregen ((v, t) :: s1) s.
Proof.
  move=> Hs [s2 Hs2].
  exists s2 => t' /=.
  rewrite -Hs2.
  exact/esym/unifies_extend.
Qed.

(* 変数の数に関する補題 *)
(* 難しいので、証明しなくて良い *)
Lemma subs_del x t t' : x \notin vars t -> x \notin vars (subs x t t').
Proof.
  move=> Hv.
  elim: t' => //= [v | t1 IH1 t2 IH2].
  - case: ifP => //=.
    by rewrite inE eq_sym => ->.
  - by rewrite in_union_or negb_or IH1 IH2.
Qed.

Lemma subs_pairs_del x t l :
  x \notin vars t -> x \notin (vars_pairs (map (subs_pair x t) l)).
Proof.
  move=> Hv.
  elim: l => //= -[t1 t2] l IH.
  by rewrite !in_union_or !negb_or /= IH !subs_del.
Qed.

Lemma subs_sub x t t' : {subset vars (subs x t t') <= union (vars t) (vars t')}.
Proof.
  elim: t' => //= [v | t1 IH1 t2 IH2] y.
  - rewrite in_union_or.
    case: ifP => [/eqP -> | _] -> //=.
    by rewrite orbT.
  - rewrite !in_union_or => /orP[/IH1 | /IH2];
    rewrite in_union_or => /orP[] -> //;
    by rewrite !orbT.
Qed.

Lemma subs_pairs_sub x t l :
  {subset vars_pairs (map (subs_pair x t) l) <= union (vars t) (vars_pairs l)}.
Proof.
  elim: l => //= -[t1 t2] l IH /= y.
  rewrite !in_union_or => /orP[/orP[] /subs_sub| /IH];
  rewrite in_union_or => /orP[] -> //;
  by rewrite !orbT.
Qed.

Lemma uniq_vars_pairs l : uniq (vars_pairs l).
Proof. elim: l => //= -[t1 t2] l IH. exact: uniq_union. Qed.

Lemma vars_pairs_decrease x t l :
  x \notin (vars t) ->
  size (vars_pairs (map (subs_pair x t) l))
    < size (vars_pairs ((Var x, t) :: l)).
Proof.
  move=> Hx.
  apply (@leq_trans (size (x :: vars_pairs (map (subs_pair x t) l)))) => //.
  apply uniq_leq_size.
    by rewrite /= uniq_vars_pairs subs_pairs_del.
  move=> /= y.
  rewrite (negbTE Hx) inE => /orP[/eqP ->|].
    by rewrite in_union_or inE eqxx.
  move/subs_pairs_sub.
  rewrite !in_union_or !inE => /orP[] ->; by rewrite orbT.
Qed.

Lemma size_vars_pairs_swap t1 t2 l :
  size (vars_pairs ((t1,t2) :: l)) = size (vars_pairs ((t2,t1) :: l)).
Proof.
  apply/eqP; rewrite eqn_leq /=.
  apply/andP; split; apply uniq_leq_size;
  rewrite ?(uniq_union, uniq_vars_pairs) //= => y;
  rewrite !in_union_or => /orP[/orP[]|] -> //;
  by rewrite orbT.  
Qed.  

Lemma size_vars_pairs_Fork t1 t2 t'1 t'2 l :
  size (vars_pairs ((Fork t1 t2, Fork t'1 t'2) :: l)) =
  size (vars_pairs ((t1, t'1) :: (t2, t'2) :: l)).
Proof.
  apply/eqP; rewrite eqn_leq /=.
  apply/andP; split; apply uniq_leq_size;
  rewrite ?(uniq_union, uniq_vars_pairs) //= => y;
  rewrite !in_union_or; do !case/orP; move ->;
  by rewrite ?orbT.  
Qed.

Lemma unify_subs_complete s h v t l :
  (forall l,
    h > size (vars_pairs l) -> unifies_pairs s l ->
    exists s1, unify2 h l = Some s1 /\ moregen s1 s) ->
  h.+1 > size (vars_pairs ((Var v, t) :: l)) ->
  unifies_pairs s ((Var v, t) :: l) ->
  Var v != t ->
  exists s1, unify_subs  (unify2 h) v t l = Some s1 /\ moregen s1 s.
Proof.
  move=> IHh Hh Hs Hv.
  rewrite /unify_subs.
  case: ifPn => vt.
    elim: (not_unifies_occur v t s) => //.
    exact: Hs.
  case: (IHh (map (subs_pair v t) l)) => //.
      have Hhv := vars_pairs_decrease v t l vt.
      apply (leq_trans Hhv).
      by rewrite -ltnS.
    exact: unifies_pairs_extend.
  move=> s1 [Hun Hmg].
  rewrite Hun /=.
  exists ((v,t) :: s1); split => //.
  apply moregen_extend => //. exact: Hs.
Qed.

(* 完全性 *)
Theorem unify2_complete s h l :
  h > size (vars_pairs l) ->
  unifies_pairs s l ->
  exists s1, unify2 h l = Some s1 /\ moregen s1 s.
Proof.
  elim: h l => //= h IH l Hh.
  move Hh': (size_pairs l + 1) => h'.
  have {Hh'} : h' > size_pairs l.
    by rewrite -Hh' addn1 ltnS.
  elim: h' l Hh => //= h' IH' [] //=.
    move=>*; exists nil; split => //; by exists s.
  case=> t1 t2 l Hh Hh' Hs.
  destruct t1, t2 => /=.
  (* VarVar *)
- case: ifP => vv0.
    move/eqP in vv0; subst v0.
    apply IH'.
    + apply/leq_trans: Hh.
      rewrite ltnS.
      exact: size_union2.
    + rewrite /size_pairs /= -!addnA !add1n ltnS in Hh'.
      exact: ltnW.
    + move=> t1 t2 Hl; apply Hs; by auto.
  have Hvar : Var v != Var v0.
    apply/negP => /eqP[] /eqP.
    by rewrite vv0.
  exact: unify_subs_complete. 
  (* VarSym *)
- exact: unify_subs_complete.
  (* VarFork *)
- exact: unify_subs_complete.
  (* SymVar *)
- apply unify_subs_complete => //.
  exact: unifies_pairs_swap.
  (* SymSym *)
- destruct symbol_dec.
    subst.
    apply IH' => //.
      rewrite /size_pairs /= -!addnA !add1n ltnS in Hh'.
      exact: ltnW.
    move=> t1 t2 Hl.
    apply Hs; by auto.
  have : unifies s (Sym s0) (Sym s1) by apply Hs.
  by rewrite /unifies !subs_list_Sym => -[].
  (* SymFork *)
  have : unifies s (Sym s0) (Fork t2_1 t2_2) by apply Hs.
  by rewrite /unifies subs_list_Sym subs_list_Fork.
  (* ForkVar *)
  apply unify_subs_complete => //.
    by rewrite size_vars_pairs_swap.
  exact: unifies_pairs_swap.
  (* ForkSym *)
  have : unifies s (Fork t1_1 t1_2) (Sym s0) by apply Hs.
  by rewrite /unifies subs_list_Sym subs_list_Fork.
  (* ForkFork *)
  apply IH'.
      by rewrite -size_vars_pairs_Fork.
    rewrite /size_pairs /= in Hh' *.
    rewrite !add1n !(addnS,addSn) in Hh'.
    rewrite !addnA in Hh' *.
    rewrite (addnAC (size_tree t1_1)) in Hh'.
    exact: ltnW.
  apply unifies_pairs_Fork. exact: Hs.
  move=> t t' Hl. apply Hs; by auto.
Qed.

(* 短い完全性定理 *)
Corollary unify_complete s t1 t2 :
  unifies s t1 t2 ->
  exists s1, unify t1 t2 = Some s1 /\ moregen s1 s.
Proof.
  rewrite /unify addnC => Hs.
  apply unify2_complete => // x y.
  by rewrite inE => /eqP[-> ->].
Qed.