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