<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.
Definition beq_var (x y : var) := if eq_nat_dec x y then true else false.
Notation "x == y" := (beq_var x y) (at level 70).
Lemma beq_var_refl : forall x, x == x = true.
Proof.
  unfold beq_var.
  intros.
  destruct eq_nat_dec. auto.
  elim n; auto.
Qed.
Lemma beq_var_true : forall x x', x == x' = true -> x = x'.
Proof.
  unfold beq_var.
  intros.
  destruct eq_nat_dec. auto.
  discriminate.
Qed.

(* 定数・関数記号 *)
Notation symbol := String.string.
Definition beq_symbol x y :=
  if String.string_dec x y then true else false.

(* 項は木構造 *)
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.

(* 出現しない変数は代入されない *)
Lemma subs_same : forall v t' t,
  ~In v (vars t) -> subs v t' t = t.
Proof.
  intros.
  induction t; simpl; intros; auto.
  (* Var *)
  unfold beq_var.
  simpl in *.
  destruct eq_nat_dec; 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_dec (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_dec.

Definition occurs x t := if occurs_dec x t then true else false.
Lemma occurs_false : forall x t,
  occurs x t = false -> ~In x (vars t).
Proof.
  unfold occurs. intros.
  destruct occurs_dec. discriminate.
  assumption.
Qed.
Hint Resolve occurs_false.

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).


(* 単一化 *)

(* 等式の大きさの計算 *)
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 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.

Definition measure (l : list (tree * tree)) :=
  (length (vars_pairs l), size_pairs l).

Section Lexico.
Variable A : Type.
Variable lt : A -> A -> Prop.
Hypothesis lt_wf : well_founded lt.

Inductive lt2 : A * A -> A * A -> Prop :=
  | lt2l : forall x1 y1 x2 y2, lt x1 x2 -> lt2 (x1,y1) (x2,y2)
  | lt2r : forall x y1 y2, lt y1 y2 -> lt2 (x,y1) (x,y2).

Theorem lt2_wf : well_founded lt2.
Proof.
  intros [x y].
  generalize (lt_wf x); intros.
  revert y; induction H; intros.
  generalize (lt_wf y); intros.
  induction H1.
  constructor.
  intros [x' y'] H'.
  inversion H'; subst.
    apply H0. assumption.
  apply H2. assumption.
Qed.
End Lexico.

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

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.

Definition lt_pairs a b := lt2 _ lt (measure a) (measure b).

Lemma lt_pairs_wf : well_founded lt_pairs.
Proof.
  unfold lt_pairs, well_founded.
  intros.
  generalize (lt2_wf _ lt lt_wf (measure a)); intros.
  remember (measure a) as x.
  revert a Heqx.
  induction H; intros; subst.
  constructor.
  intros.
  apply (H0 (measure y)); auto.
Qed.

Require Import Recdef Omega.

Lemma lt_pairs_rem : forall a r, lt_pairs r (a :: r).
  unfold lt_pairs, measure.
  simpl.
  intros.
  destruct a as [t1 t2].
  generalize (length_union1 (vars_pairs r) (union (vars t1) (vars t2))); intros.
  inversion H; clear H.
    apply lt2r.
    destruct t1; simpl; auto with arith.
  apply lt2l.
  auto with arith.
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)).
Hint Resolve vars_pairs_decrease.
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)).

Notation unify_subs unify x t r :=
  (if occurs x t then None else may_cons x t (unify (map (subs_pair x t) r))).

Function unify (l : list (tree * tree)) {wf lt_pairs l}
  : option (list (var * tree)) :=
  match l with
  | nil => Some nil
  | (Var x, Var x') :: r =>
    if x == x' then unify r else unify_subs unify x (Var x') r
  | (Var x, t) :: r =>
    unify_subs unify x t r
  | (t, Var x) :: r =>
    unify_subs unify x t r
  | (Sym b, Sym b') :: r =>
    if beq_symbol b b' then unify r else None
  | (Fork t1 t2, Fork t1' t2') :: r =>
    unify ((t1, t1') :: (t2, t2') :: r)
  | l => None
  end.
Proof.
  (* (x, x) *)
  intros; subst.
  apply lt_pairs_rem.
  (* (x, y) *)
  intros; subst.
  apply lt2l.
  apply vars_pairs_decrease.
  simpl. intro H. destruct H; subst; auto.
  rewrite beq_var_refl in teq3.
  discriminate.
  (* (x, s) *)
  intros; subst.
  apply lt2l; auto.
  (* (x, (t1, t2)) *)
  intros; subst.
  apply lt2l; auto.
  (* (s, x) *)
  intros; subst.
  apply lt2l.
  apply vars_pairs_decrease.
  auto.
  (* (s, s) *)
  intros; subst.
  apply lt_pairs_rem.
  (* ((t1, t2), x) *)
  intros; subst.
  apply lt2l.
  rewrite length_vars_pairs_swap.
  auto.
  (* (Fork, Fork) *)
  intros; subst.
  unfold lt_pairs, measure.
  rewrite length_vars_pairs_Fork.
  apply lt2r.
  simpl.
  omega.
  (* well_founded *)
  apply lt_pairs_wf.
Defined.

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

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.

(* unify の健全性 *)
Theorem unify_sound : forall l s,
  unify l = Some s -> unifies_pairs s l.
Proof.
  intros l.
  functional induction (unify l); intros; try discriminate.
  (* nil *)
  intros t1 t2 Hin. elim Hin.
  (* VarVar *)
  rewrite <- (beq_var_true _ _ e0).
  apply unifies_pairs_same. apply IHo. auto.
Lemma unify_subs_sound : forall v t r s,
  let l := map (subs_pair v t) r in
  occurs v t = false ->
  (forall s, unify l = Some s -> unifies_pairs s l) ->
  may_cons v t (unify l) = Some s ->
  unifies_pairs s ((Var v, t) :: r).
Proof.
  intros until l.
  intros e IHh H.
  case_eq (unify l); intros;
    rewrite H0 in H; inversion H; clear H.
  subst.
  apply IHh in H0; clear IHh.
  unfold unifies_pairs, unifies in *; simpl.
  intros.
  destruct H.
    inversion H; subst t1 t2; clear -e.
    simpl.
    rewrite subs_same by auto.
    rewrite beq_var_refl; reflexivity.
  apply H0.
  apply (in_map (subs_pair v t) _ _ H).
Qed.
  apply unify_subs_sound; auto.
  (* VarSymFork *)
  apply unify_subs_sound; auto.
  (* SymForkVar *)
  apply unifies_pairs_swap.
  apply unify_subs_sound; auto.
  (* SymSym *)
  unfold beq_symbol in e0.
  destruct String.string_dec.
    subst.
    auto using unifies_pairs_same.
  discriminate.
  (* ForkFork *)
  specialize (IHo _ H).
  clear -IHo.
  intros t3 t4 Hin.
  simpl in Hin; destruct Hin.
    inversion H; subst.
    unfold unifies.
    repeat rewrite subs_list_Fork.
    apply f_equal2.
      apply IHo; simpl; auto.
    apply IHo; simpl; auto.
  apply IHo; simpl; auto.
Qed.


(* 完全性 *)

(* 循環的な項が作れない *)
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.

(* 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.
    unfold beq_var.
    destruct eq_nat_dec; subst; auto.
  specialize (IHt'1 H).
  specialize (IHt'2 H).
  repeat rewrite subs_list_Fork.
  congruence.
Qed.

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.

(* 完全性 *)
Theorem unify_complete : forall s l,
  unifies_pairs s l ->
  exists s1, unify l = Some s1 /\ moregen s1 s.
Proof.
  intros s l.
  functional induction (unify l); intros.
  (* nil *)
  exists nil; split; auto.
  exists s; reflexivity.
  (* (x,x) *)
  simpl in *.
  apply IHo.
  intros t1 t2 Hin. apply H; simpl; auto.
  (* occurs *)
  elim (not_unifies_occur x (Var x') s).
      unfold beq_var in e0.
      destruct eq_nat_dec; try discriminate.
      intro Hx; inversion Hx; intuition.
    unfold occurs in e1.
    destruct occurs_dec. auto. discriminate.
  apply H; simpl; auto.
  (* (x,x') *)
  assert (Var x <> Var x').
    intro.
    unfold beq_var in e0.
    destruct eq_nat_dec; try discriminate.
    elim n.
    inversion H0; reflexivity.
Lemma unify_subs_complete : forall s v t r,
  let l := map (subs_pair v t) r in
  (unifies_pairs s l -> exists s1,  unify l = Some s1 /\ moregen s1 s) ->
  unifies_pairs s ((Var v, t) :: r) ->
  Var v <> t ->
  exists s1, may_cons v t (unify l) = Some s1 /\ moregen s1 s.
Proof.
  intros until l; intros Hl Hs Hv.
  (* elim (not_unifies_occur _ _ s Hv i). *)
  destruct Hl as [s1 [Hun Hmg]]; auto.
    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.
  (* occurs *)
  elim (not_unifies_occur x t s).
      intro. subst. elim y.
    unfold occurs in e0.
    destruct occurs_dec. auto. discriminate.
  apply H; simpl; auto.
  (* VarSymFork *)
  apply unify_subs_complete; intuition.
  subst. elim y.
  (* occurs *)
  elim (not_unifies_occur x t s).
      intro. subst. elim y.
    unfold occurs in e0.
    destruct occurs_dec. auto. discriminate.
  symmetry.
  apply H; simpl; auto.
  (* SymForkVar *)
  apply unify_subs_complete; intuition.
    apply unifies_pairs_swap; auto.
  subst. elim y.
  (* SymSym *)
  unfold beq_symbol in e0.
  destruct String.string_dec.
    subst.
    apply IHo.
    intros t1 t2 Hin.
    apply H; simpl; auto.
  discriminate.
  (* SymSym' *)
  unfold beq_symbol in e0.
  destruct String.string_dec. discriminate.
  assert (unifies s (Sym b) (Sym b')).
    apply H; simpl; auto.
  unfold unifies in H0.
  repeat rewrite subs_list_Sym in H0.
  inversion H0.
  intuition.
  (* ForkFork *)
  apply IHo.
  apply unifies_pairs_Fork. apply H; simpl; auto.
  intros t t' Hin. apply H; simpl; auto.
  (* Fail *)
  elimtype False.
  destruct l; auto.
  destruct p.
  assert (unifies s t t0).
    apply H; simpl; auto.
  unfold unifies in H0.
  destruct t; destruct t0; auto.
    rewrite subs_list_Sym, subs_list_Fork in H0. discriminate.
  rewrite subs_list_Sym, subs_list_Fork in H0. discriminate.
Qed.