<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* 単一化 *)

Require Import Arith List ListSet.
Require String.
Open Scope string_scope.

Definition var := nat.
Notation "x == y" := (eq_nat_dec x y) (at level 70).

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

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

(* [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.

(* 代入は変数代入の繰り返し *)
Fixpoint subs_list (s : list (var * tree)) t : tree :=
  match s with
  | nil => t
  | (x, t') :: s' => subs_list s' (subs x t' t)
  end.

Lemma subs_list_app : forall s1 s2 t,
  subs_list (s1 ++ s2) t = subs_list s2 (subs_list s1 t).
Proof.
  induction s1; simpl; auto.
  destruct a. congruence.
Qed.

(* 単一子の定義 *)
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.

(* 和集合 *)
Definition union : list var -> list var -> list var := set_union eq_nat_dec.

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

(* 出現しない変数は代入されない *)
Print set_In.
Check set_union_intro.
Lemma subs_same : forall v t' t,
  ~In v (vars t) -> subs v t' t = t.
Proof.
  intros.
  induction t; simpl; intros; auto.
  (* Var *)
  simpl in *.
  destruct (v0 == v); intuition.
  (* Fork *)
  rewrite IHt1, IHt2; auto.
    intro; elim H; simpl.
    apply set_union_intro; auto.
  intro; elim H; simpl.
  apply set_union_intro; auto.
Qed.

(* 出現判定 *)
Definition occurs (x : var) (t : tree) : {In x (vars t)}+{~In x (vars t)}.
  intros.
  case_eq (set_mem eq_nat_dec x (vars t)); intros.
    left; apply (set_mem_correct1 _ _ _ H).
  right; apply (set_mem_complete1 _ _ _ H).
Defined.
Extraction occurs.

Definition may_cons (x : var) (t : tree) r :=
  match r with
  | None => None
  | Some s => Some ((x,t) :: s)
  end.
Definition subs_pair x t (p : tree * tree) :=
  let (t1, t2) := p in (subs x t t1, subs x t t2).

(* 単一化 *)
Section Unify1.

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

(* 代入して再帰呼び出し. x は t に現れてはいけない *) 
Definition unify_subs x t r :=
  if occurs x 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)) :=
  match h with
  | 0 => None
  | S h' =>
    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)
    | l => None
    end
  end.
End Unify1.

(* 等式の大きさの計算 *)
Fixpoint size_tree (t : tree) : nat :=
  match t with
  | Fork t1 t2 => 1 + size_tree t1 + size_tree t2
  | _ => 1
  end.

Fixpoint size_pairs (l : list (tree * tree)) :=
  match l with
  | nil => 0
  | (t1, t2) :: r => size_tree t1 + size_tree t2 + size_pairs r
  end.

(* 代入したときだけ再帰 *)
Fixpoint unify2 (h : nat) l :=
  match h with
  | 0    => None
  | S h' => unify1 (unify2 h') (size_pairs l + 1) l
  end.

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

(* 変数の数だけ unify2 を繰り返す *)
Definition unify t1 t2 :=
  let l := (t1,t2)::nil in unify2 (length (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 :=
  forall t1 t2, In (t1,t2) l -> unifies s t1 t2.

(* subs_list と Fork が可換 *)
Lemma subs_list_Fork : forall s t1 t2,
  subs_list s (Fork t1 t2) = Fork (subs_list s t1) (subs_list s t2).
Proof.
  induction s; simpl; intros.
    reflexivity.
  destruct a.
  apply IHs.
Qed.

(* unifies_pairs の性質 *)
Lemma unifies_pairs_same : forall s t l,
  unifies_pairs s l -> unifies_pairs s ((t,t) :: l).
Proof.
  intros.
  intros t1 t2 Hin.
  simpl in Hin; destruct Hin; auto.
  inversion H0; reflexivity.
Qed.

Lemma unifies_pairs_swap : forall s t1 t2 l,
  unifies_pairs s ((t1, t2) :: l) -> unifies_pairs s ((t2, t1) :: l).
Proof.
  unfold unifies_pairs; simpl; intros.
  destruct H0.
    inversion H0; subst t0 t3.
    symmetry.
    apply H; auto.
  apply H; auto.
Qed.

(* unify2 の健全性 *)
Theorem unify2_sound : forall h s l,
  unify2 h l = Some s -> unifies_pairs s l.
Proof.
  induction h; simpl; intros.
    discriminate.
  remember (size_pairs l + 1) as h'.
  clear Heqh'.
  revert l H.
  induction h'; simpl; intros.
    discriminate.
  destruct l.
    intros t1 t2 Hin. elim Hin.
  destruct p as [t1 t2].
  destruct t1; destruct t2; try discriminate.
  (* VarVar *)
  destruct (v == v0).
    subst v0.
    apply unifies_pairs_same. auto.
Lemma unify_subs_sound : forall 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.
  intros until s.
  unfold unify_subs.
  destruct occurs. intros; discriminate.
  intros IHh H.
  case_eq (unify2 h (map (subs_pair v t) l)); intros;
    rewrite H0 in H; inversion H; clear H.
  subst.
  specialize (IHh _ _ H0); clear H0.
  unfold unifies_pairs, unifies in *; simpl.
  intros.
  destruct H.
    inversion H; subst; clear -n.
    simpl.
    rewrite subs_same by assumption.
    destruct (v == v); intuition.
  apply IHh.
  apply (in_map (subs_pair v t) _ _ H).
Qed.
  apply (unify_subs_sound h); auto.
  (* VarSym *)
  apply (unify_subs_sound h); auto.
  (* VarFork *)
  apply (unify_subs_sound h); auto.
  (* SymVar *)
  apply unifies_pairs_swap.
  apply (unify_subs_sound h); auto.
  (* SymSym *)
  destruct symbol_dec.
    subst.
    auto using unifies_pairs_same.
  discriminate.
  (* ForkVar *)
  apply unifies_pairs_swap.
  apply (unify_subs_sound h); auto.
  (* ForkFork *)
  specialize (IHh' _ H).
  clear -IHh'.
  intros t1 t2 Hin.
  simpl in Hin; destruct Hin.
    inversion H; subst.
    unfold unifies.
    repeat rewrite subs_list_Fork.
    apply f_equal2.
      apply IHh'; simpl; auto.
    apply IHh'; simpl; auto.
  apply IHh'; simpl; auto.
Qed.

(* 単一化の健全性 *)
Corollary soundness : forall t1 t2 s,
  unify t1 t2 = Some s -> unifies s t1 t2.
Proof.
  unfold unify; intros.
  apply (unify2_sound _ _ _ H).
  simpl; intros; intuition.
Qed.


(* 完全性 *)
Require Import Omega.

(* 循環的な項が作れない *)
Lemma not_unifies_occur : forall v t s,
  Var v <> t -> In v (vars t) -> ~unifies s (Var v) t.
Proof.
  intros.
  unfold unifies; intro Hun.
  (* size_tree で矛盾を導く *)
  assert (Hs: size_tree (subs_list s (Var v)) >= size_tree (subs_list s t)).
    rewrite Hun; auto with arith.
  (* 元の仮定を消してから帰納法を使う *)
  clear Hun. induction t; simpl in *.
  (* Var *)
  destruct H0.
    subst. elim H; auto.
  elim H0.
  (* Sym *)
  elim H0.
  (* Fork *)
  rewrite subs_list_Fork in Hs; simpl in Hs.
  unfold union in H0.
  destruct (set_union_elim _ _ _ _ H0).
    destruct t1.
        simpl in H1.
        destruct H1; subst; auto.
        omega.
      elim H1.
    apply IHt1; auto.
      intro; discriminate.
    omega.
  destruct t2.
      simpl in H1.
      destruct H1; subst; auto.
      omega.
    elim H1.
  apply IHt2; auto.
    intro; discriminate.
  omega.
Qed.

(* 集合の要素の数に関する基礎的な補題 *)
Lemma length_set_add : forall a l,
  length (set_add eq_nat_dec a l) >= length l.
Proof.
  induction l; simpl. auto.
  destruct (a == a0); simpl; auto with arith.
Qed.

Check le_trans.
Check le_lt_trans.
Lemma length_union1 : forall l1 l2, length (union l1 l2) >= length l1.
Proof.
  intros; induction l2; simpl. auto.
  eapply le_trans. apply IHl2.
  apply length_set_add.
Qed.

(* Sym の代入 *)
Lemma subs_list_Sym : forall s f, subs_list s (Sym f) = Sym f.
Proof.
  intros; induction s; simpl. auto.
  destruct a. auto.
Qed.

(* 代入の合成 *)
Lemma unifies_extend : forall s v t t',
  unifies s (Var v) t -> unifies s (subs v t t') t'.
Proof.
  unfold unifies.
  induction t'; simpl; intros; auto.
    destruct (v0 == v); subst; auto.
  specialize (IHt'1 H).
  specialize (IHt'2 H).
  repeat rewrite subs_list_Fork.
  congruence.
Qed.

Check in_map_iff.
Lemma unifies_pairs_extend : forall s v t l,
  unifies_pairs s ((Var v, t) :: l) -> unifies_pairs s (map (subs_pair v t) l).
Proof.
  unfold unifies_pairs, unifies in *.
  intros.
  apply -> in_map_iff in H0.
  destruct H0 as [[t1' t2'] [Hmap Hin]].
  simpl in Hmap.
  inversion Hmap; subst.
  assert (unifies s (Var v) t).
    apply H; simpl; auto.
  repeat rewrite unifies_extend by auto.
  apply H; simpl; auto.
Qed.

Lemma unifies_pairs_Fork : forall 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.
  intros.
  unfold unifies in H.
  repeat rewrite subs_list_Fork in H.
  inversion H; clear H.
  intros t t' Hin.
  simpl in Hin; destruct Hin.
    inversion H; subst.
    auto.
  destruct H.
    inversion H; subst.
    auto.
  apply H0; simpl; auto.
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 : forall s v t s1,
  unifies s (Var v) t -> moregen s1 s -> moregen ((v, t) :: s1) s.
Proof.
  intros.
  destruct H0 as [s2 Hs2].
  exists s2.
  intros.
  simpl.
  rewrite <- subs_list_app.
  rewrite unifies_extend.
    rewrite subs_list_app.
    apply Hs2.
  unfold unifies.
  repeat rewrite subs_list_app, <- Hs2.
  assumption.
Qed.

(* 変数の数に関する補題 *)
(* 難しいので、証明しなくて良い *)
Parameter vars_pairs_decrease : forall x t l,
  ~In x (vars t) ->
  length (vars_pairs (map (subs_pair x t) l))
    < length (vars_pairs ((Var x, t) :: l)).
Parameter length_vars_pairs_swap : forall t1 t2 l,
  length (vars_pairs ((t1,t2) :: l)) = length (vars_pairs ((t2,t1) :: l)).
Parameter length_vars_pairs_Fork : forall t1 t2 t'1 t'2 l,
  length (vars_pairs ((Fork t1 t2, Fork t'1 t'2) :: l)) =
  length (vars_pairs ((t1, t'1) :: (t2, t'2) :: l)).

(* 完全性 *)
Theorem unify2_complete : forall s h l,
  h > length (vars_pairs l) ->
  unifies_pairs s l ->
  exists s1, unify2 h l = Some s1 /\ moregen s1 s.
Proof.
  induction h.
    intros. elimtype False. omega.
  simpl.
  intros l Hh.
  remember (size_pairs l + 1) as h'.
  assert (Hh': h' > size_pairs l) by (subst; omega).
  clear Heqh'.
  revert l Hh Hh'.
  induction h'; intros.
    elimtype False. omega.
  simpl.
  destruct l.
    exists nil; split; auto.
    exists s; reflexivity.
  destruct p.
  destruct t; destruct t0.
  (* VarVar *)
  destruct (v == v0).
    subst v0.
    simpl in *.
    apply IHh'; try omega.
      eapply le_lt_trans; try apply Hh.
      apply length_union1.
    intros t1 t2 Hin. apply H; simpl; auto.
  assert (Var v <> Var v0).
    intro.
    elim n.
    inversion H0; reflexivity.
Lemma unify_subs_complete : forall s h v t l,
  (forall l,
    h > length (vars_pairs l) -> unifies_pairs s l ->
    exists s1, unify2 h l = Some s1 /\ moregen s1 s) ->
  S h > length (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.
  intros until l; intros IHh Hh Hs Hv.
  unfold unify_subs.
  destruct (occurs v t).
    elim (not_unifies_occur _ _ s Hv i).
    apply Hs. simpl; auto.
  destruct (IHh (map (subs_pair v t) l)) as [s1 [Hun Hmg]]; auto.
      generalize (vars_pairs_decrease v t l n); intros.
      omega.
    apply unifies_pairs_extend. assumption.
  rewrite Hun.
  simpl.
  exists ((v,t) :: s1); split; auto.
  apply moregen_extend. apply Hs; simpl; auto. assumption.
Qed.
  apply unify_subs_complete; intuition.
  (* VarSym *)
  apply unify_subs_complete; intuition.
  discriminate.
  (* VarFork *)
  apply unify_subs_complete; intuition.
  discriminate.
  (* SymVar *)
  apply unify_subs_complete; intuition.
    apply unifies_pairs_swap; auto.
  discriminate.
  (* SymSym *)
  destruct symbol_dec.
    subst.
    apply IHh'; auto.
      simpl in Hh'. omega.
    intros t1 t2 Hin.
    apply H; simpl; auto.
  assert (unifies s (Sym s0) (Sym s1)).
    apply H; simpl; auto.
  unfold unifies in H0.
  repeat rewrite subs_list_Sym in H0.
  inversion H0.
  intuition.
  (* SymFork *)
  assert (unifies s (Sym s0) (Fork t0_1 t0_2)).
    apply H; simpl; auto.
  unfold unifies in H0.
  rewrite subs_list_Sym, subs_list_Fork in H0.
  discriminate.
  (* ForkVar *)
  apply unify_subs_complete; intuition.
      rewrite length_vars_pairs_swap.
      auto.
    apply unifies_pairs_swap; auto.
  discriminate.
  (* ForkSym *)
  assert (unifies s (Fork t1 t2) (Sym s0)).
    apply H; simpl; auto.
  unfold unifies in H0.
  rewrite subs_list_Sym, subs_list_Fork in H0.
  discriminate.
  (* ForkFork *)
  apply IHh'.
      rewrite <- length_vars_pairs_Fork.
      auto.
    simpl.
    simpl in Hh'.
    omega.
  apply unifies_pairs_Fork. apply H; simpl; auto.
  intros t t' Hin. apply H; simpl; auto.
Qed.

(* 短い完全性定理 *)
Corollary unify_complete : forall s t1 t2,
  unifies s t1 t2 ->
  exists s1, unify t1 t2 = Some s1 /\ moregen s1 s.
Proof.
  unfold unify.
  intros.
  rewrite plus_comm.
  apply unify2_complete; try omega.
  intros t t' Hin.
  simpl in Hin.
  destruct Hin.
    inversion H0; subst; auto.
  elim H0.
Qed.