(* 単一化 *) 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.