(* This program is free software; you can redistribute it and/or *) (* modify it under the terms of the GNU Lesser General Public License *) (* as published by the Free Software Foundation; either version 2.1 *) (* of the License, or (at your option) any later version. *) (* *) (* This program is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU General Public License for more details. *) (* *) (* You should have received a copy of the GNU Lesser General Public *) (* License along with this program; if not, write to the Free *) (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) (****************************************************************************) (* This proof script is part of the paper titled *) (* "A machine checked model of MGU axioms: applications of finite maps *) (* and functional induction" *) (* *) (****************************************************************************) (* *) (* Coq V8.1.pl3 *) (* *) (* *) (* MGU-axioms *) (* *) (* Sunil Kothari *) (* *) (* May 31, 2008 *) (* *) (****************************************************************************) (* mgu_axiom.v *) (****************************************************************************) (* NOTE: this code requires NoDup.v for CoqIDE to run. *) Require Import List. Require Import Arith. Require Import ZArith. Require Import String. Require Import Int. Require Import Bool. Require Import Recdef. Require Import Coq.Arith.EqNat. Require Import Coq.Arith.Max. Require Import Decidable. Require Import Coq.Bool.Sumbool. Require Import OrderedType. Require Import Omega. Require Import NArith Ndec. Require Import Compare_dec. Require Import Pnat. Require Import OrderedTypeEx. Require Import Wf_nat. Require Import Relation_Operators. Require Import Wf. Require Import Le. Require Import Inverse_Image. (*Require Import LexOrder *) Require Import FMapInterface. Load NoDup. Inductive type:Set := TyVar : nat -> type | Arrow : type -> type -> type . Inductive constr : Set := EqCons: type -> type -> constr. Module Nat_as_MyOT <: UsualOrderedType := Nat_as_OT. Module MyStuff (M:FMapInterface.S with Module E := Nat_as_MyOT). Section Unify_Axioms. Variable elt:type. Lemma eq_type: forall (ty1 ty2: type), {ty1 = ty2} + {ty1 <> ty2}. Proof. intros ty1 ty2. decide equality. decide equality. Qed. Fixpoint FTV(ty:type) := match ty with | TyVar x => x::nil | Arrow ty1 ty2 => (FTV ty1) ++ (FTV ty2) end. Fixpoint FVC(c:list constr) := match c with nil => nil | h::t => match h with | EqCons ty1 ty2 => (FTV ty1) ++ (FTV ty2) ++(FVC t) end end. (* Equality on stamps is decidable *) Lemma eq_dec_stamp : forall (x y : nat), {x = y} + {x <> y}. Proof. intros x y. decide equality. Qed. Fixpoint apply_subst_type (s:M.t type)(ty:type) {struct ty} := match ty with TyVar a => match (M.find a s) with None => ty | Some t => t end | Arrow ty1 ty2 => Arrow (apply_subst_type s ty1) (apply_subst_type s ty2) end. Definition apply_subst_to_subst (s1: M.t type) (s2: M.t type) := M.map (apply_subst_type s2) s1. Definition choose_subst (t1: option type) (t2:option type) := match (t1,t2) with (Some t3, Some t4) => Some t3 | (Some t3, None) => Some t3 | (None, Some t3) => Some t3 | (None, None) => None end. Definition subst_diff (s1:M.t type) (s2:M.t type) := M.map2 choose_subst s1 s2. Definition compose_subst (s1:M.t type) (s2: M.t type) := subst_diff (apply_subst_to_subst s1 s2) s2. Definition dom_subst (s: M.t type): list nat := map (fun p => fst p) (M.elements s). Definition range_subst (s: M.t type): list nat := flat_map (fun x => FTV (snd x)) (M.elements s). Definition FTV_subst (s :M.t type): list nat := range_subst s ++ dom_subst s. Definition apply_subst_constr (s:M.t type) (c:constr) := match c with EqCons ty1 ty2 => EqCons (apply_subst_type s ty1) (apply_subst_type s ty2) end. Fixpoint apply_subst_to_constr_list (s: M.t type) (c:list constr) {struct c}:= match c with nil => nil | h::t => (apply_subst_constr s h)::(apply_subst_to_constr_list s t) end. Fixpoint member (st:nat)(l: list nat) {struct l} := match l with nil => false | h::t => if eq_dec_stamp h st then true else member st t end. Definition satisfies (s:M.t type) (e :constr) := match e with EqCons ty1 ty2 => (apply_subst_type s ty1 = apply_subst_type s ty2) end. Fixpoint satisfies_all (s:M.t type) (c:list constr) {struct c} := match c with nil => True | (h::c) => (satisfies s h /\ satisfies_all s c) end. Fixpoint arrowCount(t:type) : nat := match t with TyVar s => 0 | Arrow ty1 ty2 => 1 + arrowCount ty1 + arrowCount ty2 end. Fixpoint arrowC(l : list constr) : nat := match l with nil => 0 | h ::t => match h with EqCons (TyVar x) (TyVar y) => (arrowC t) | EqCons (TyVar x)(Arrow ty3 ty4) => (arrowCount ty3) + (arrowCount ty4) + 1 + (arrowC t) | EqCons (Arrow ty3 ty4) (TyVar x) => (arrowCount ty3) + (arrowCount ty4) + 1 + (arrowC t) | EqCons (Arrow ty1 ty2) (Arrow ty3 ty4) => (arrowCount ty1) + (arrowCount ty2)+ (arrowCount ty3) + (arrowCount ty4) + 2 + (arrowC t) end end. Function arrowCMea(l : list constr) : nat := match l with nil => 0 | (EqCons ty1 ty2)::t => 1 + (arrowCount ty1) + (arrowCount ty2) + (arrowCMea t) end. Theorem In_nat_dec: forall h:nat, forall t : list nat, { In h t} + {~In h t}. intros. apply In_dec. decide equality. Qed. Fixpoint unique (c: list nat): list nat := match c with nil => nil | h::t => if (In_nat_dec h t) then unique t else h::unique t end. Function arrowComplexMea(l : list constr){measure arrowCMea l}: nat := match l with nil => 0 | h::t => match h with | EqCons (TyVar x) (TyVar y) => 1 + (arrowComplexMea t) | EqCons (TyVar x) (Arrow ty3 ty4) => (arrowCount ty3) + (arrowCount ty4) + 1 + (arrowComplexMea t) | EqCons (Arrow ty3 ty4) (TyVar x) => (arrowCount ty3) + (arrowCount ty4) + 1 + (arrowComplexMea t) | EqCons (Arrow ty1 ty2) (Arrow ty3 ty4) => 2 + (arrowComplexMea ((EqCons ty1 ty3):: (EqCons ty2 ty4)::t) ) end end. Proof. intros. simpl. omega. intros. simpl. omega. intros. simpl. omega. intros. simpl. omega. Defined. Definition meaC (c: list constr): nat * nat * nat:= (List.length (unique (FVC c) ), arrowC c, List.length c). Lemma length_unchanged_by_var_subst : forall c: list constr, forall x y :nat, List.length (apply_subst_to_constr_list (M.add x (TyVar y) (M.empty type)) c) = List.length c. Proof. intros. induction c. simpl. reflexivity. simpl. f_equal. apply IHc. Qed. Lemma length_unchanged_by_arrow_subst : forall c: list constr, forall ty1 ty2: type, forall x:nat, List.length (apply_subst_to_constr_list (M.add x (Arrow ty1 ty2) (M.empty type)) c) = List.length c. Proof. intros. induction c. simpl. reflexivity. simpl. f_equal. apply IHc. Qed. Lemma empty_map_maps_to_nothing: forall ty: type, forall n:nat, M.MapsTo n ty (M.empty type) -> False. Proof. intros. assert (M.Empty (M.empty type)). apply M.empty_1. unfold M.Empty in H0. unfold not in H0. apply H0 in H. assumption. Qed. Lemma arrowC_unchanged_by_type_subst : forall x y :nat, forall t: type, arrowCount (apply_subst_type (M.add x (TyVar y) (M.empty type)) t) = arrowCount t. Proof. intros x y. induction t. simpl. case_eq (M.find n (M.add x (TyVar y) (M.empty type))) . intros. destruct t. simpl. auto. apply M.find_2 in H. apply M.add_3 in H. apply empty_map_maps_to_nothing in H. contradiction H. unfold not; intros. unfold M.E.eq in H0. subst. assert (n = n). reflexivity. apply M.add_1 with (elt := type) (m:= M.empty type)(e:= TyVar y) in H0. apply M.find_1 in H. apply M.find_1 in H0. rewrite H0 in H. discriminate H. intros. simpl. auto. simpl. rewrite IHt1. rewrite IHt2. reflexivity. Qed. Theorem mem_unique_list : forall l:list nat, forall a:nat, In a l -> In a (unique l). Proof. induction l. intros. simpl in H. contradiction H. intros. simpl. simpl in H. destruct H. subst. destruct (In_nat_dec a0 l). apply IHl. assumption. simpl. left; reflexivity. destruct (In_nat_dec a l). apply IHl in H. assumption. simpl. right. apply IHl in H. assumption. Qed. Theorem mem_unique_list_converse : forall l:list nat, forall a:nat, In a (unique l) ->In a l. Proof. induction l. intros. simpl in H. contradiction H. intros. simpl in H. destruct (In_nat_dec a l). simpl. right. apply IHl. assumption. simpl in H. destruct H. subst. simpl. left; reflexivity. simpl. right. apply IHl. assumption. Qed. Theorem unique_and_ulist: forall l:list nat, NoDup (unique l). Proof. simpl. induction l. simpl. apply NoDup_nil. simpl. destruct (In_nat_dec a l). apply IHl. apply NoDup_cons. unfold not in *. intros. elim n. apply mem_unique_list_converse. assumption. assumption. Qed. Set Implicit Arguments. Section Lexicographic_Product. Variables A B : Type. Variable leA : A -> A -> Prop. Variable leB : B -> B -> Prop. Inductive lexprod : A * B -> A * B -> Prop := | left_lex : forall (x1 x2:A) (y1 y2:B), leA x1 x2 -> lexprod (x1, y1) (x2, y2) | right_lex : forall (x1 x2:A) (y1 y2:B), leB y1 y2 -> x1 = x2 -> lexprod (x1, y1) (x2, y2). Lemma acc_A_B_lexprod : well_founded leB -> forall x, Acc leA x -> forall y, Acc leB y -> Acc lexprod (x, y). Proof. intros H x Hx. induction Hx as [x _ IHacc]. intros y Hy. induction Hy as [y _ IHacc0]. apply Acc_intro. intros (x1, y1). inversion 1; subst; auto. Qed. Theorem wf_lexprod : well_founded leA -> well_founded leB -> well_founded lexprod. Proof. intros wfA wfB; unfold well_founded. intros (x, y); auto using acc_A_B_lexprod. Qed. End Lexicographic_Product. Definition lt3 := lexprod (lexprod lt lt) lt. Definition meaPairM (c1: list constr) (c2: list constr ) := lt3 (meaC c1) (meaC c2). Lemma lt3_wf : well_founded lt3. Proof. unfold lt3. auto using wf_lexprod with arith. Qed. Definition meaPairMLt : list constr -> list constr -> Prop := meaPairM. Hint Constructors lexprod. Lemma termination_helper1: forall y:nat, forall t0:type, apply_subst_type (M.add y (TyVar y) (M.empty type)) t0 = t0. Proof. intros y. induction t0. simpl. case_eq(M.find n (M.add y (TyVar y)(M.empty type))). intros. case_eq (eq_nat_dec n y). intros H1. intros H2. rewrite H1 in H. rewrite H1. apply M.find_2 in H. assert (y = y). reflexivity. apply M.add_1 with (e:=TyVar y) (m := M.empty type) in H0. apply M.find_1 in H. apply M.find_1 in H0. rewrite H in H0. injection H0; intros ; assumption. intros. apply M.find_2 in H. apply M.add_3 in H. apply empty_map_maps_to_nothing in H. contradiction H. auto. intros. reflexivity. simpl. rewrite IHt0_1. rewrite IHt0_2. reflexivity. Qed. Lemma termination_helper3: forall ty1 ty2:type, forall x:nat, member x (FTV ty1) || member x (FTV ty2) = false -> member x (FTV (Arrow ty1 ty2)) = false . Proof. intros. simpl. unfold orb in H. unfold ifb in H. case_eq (member x (FTV ty1)). intros. rewrite H0 in H. inversion H. intros. rewrite H0 in H. induction (FTV ty1). simpl. assumption. simpl. simpl in H0. destruct (eq_dec_stamp a x). inversion H0. apply IHl. assumption. Qed. Lemma termination_helper4: forall ty1 ty2:type, forall x:nat, member x (FTV (Arrow ty1 ty2)) = false -> member x (FTV ty1) || member x (FTV ty2) = false. Proof. intros. unfold orb,ifb. case_eq (member x (FTV ty1)). intros. simpl in H. induction (FTV ty1). simpl in H0. inversion H0. simpl in H0. destruct (eq_dec_stamp a x). subst. simpl in H. destruct (eq_dec_stamp x x). inversion H. elim n; reflexivity. apply IHl. simpl in H. destruct (eq_dec_stamp a x). inversion H. assumption. assumption. simpl in H. induction (FTV ty1). intros. simpl in H. assumption. intros. simpl in *. destruct(eq_dec_stamp a x). inversion H. apply IHl in H. assumption. assumption. Qed. Lemma termination_helper5: forall x :nat, forall ty:type, member x (FTV ty) = false -> not (In x (FTV ty)). Proof. intros. unfold not; intros. induction ty. simpl in H0. destruct H0. subst. simpl in H. destruct (eq_dec_stamp x x). inversion H. elim n; reflexivity. contradiction H0. apply termination_helper4 in H. simpl in *. apply in_app_or in H0. unfold orb in H. unfold ifb in H. case_eq (member x (FTV ty1)). intros. rewrite H1 in H. inversion H. intros. rewrite H1 in H. destruct H0. apply IHty1; assumption. apply IHty2; assumption. Qed. Lemma termination_helper6: forall x :nat, forall ty:type, not (In x (FTV ty)) -> member x (FTV ty) = false . Proof. intros. induction ty. simpl in H. simpl. destruct (eq_dec_stamp n x). elim H. left. assumption. reflexivity. apply termination_helper3. unfold orb, ifb. case_eq (member x (FTV ty1)). intros. simpl in H. unfold not in H. rewrite H0 in IHty1. unfold not in IHty1. elim IHty1. reflexivity. intros. elim H. apply in_or_app. left. assumption. intros. apply IHty2. unfold not. intros. elim H. simpl. apply in_or_app. right. assumption. Qed. Lemma not_member_app: forall a b:list nat, forall x:nat, not (In x (a ++ b)) -> (not (In x a)) /\ (not (In x b)). Proof. intros. split. unfold not. intros. unfold not in H. apply H. apply in_or_app. left. assumption. unfold not. intros. unfold not in H. elim H. apply in_or_app. right. assumption. Qed. Lemma not_member_app_converse: forall a b:list nat, forall x:nat,(not (In x a)) /\ (not (In x b)) -> not (In x (a ++ b)). Proof. intros. unfold not. intros. destruct H. apply in_app_or in H0. destruct H0. elim H. assumption. elim H1. assumption. Qed. Lemma termination_helper7: forall x y:nat, forall t : type, x <> y -> not (In x (FTV (apply_subst_type (M.add x (TyVar y)(M.empty type)) t))). Proof. intros x y. intros t. intros H. induction t. simpl. case (eq_dec_stamp n x). intros; subst. case_eq (M.find x (M.add x (TyVar y)(M.empty type))). intros. unfold not; intros. apply M.find_2 in H0. assert (x =x). reflexivity. apply M.add_1 with (m:= M.empty type)(e:=(TyVar y)) in H2. apply M.find_1 in H0. apply M.find_1 in H2. rewrite H0 in H2. injection H2; intros;subst. simpl in H1. destruct H1. elim H. symmetry. assumption. contradiction H1. intros. assert (x=x). reflexivity. apply M.add_1 with (m:=M.empty type)(e:=(TyVar y)) in H1. apply M.find_1 in H1. rewrite H0 in H1. inversion H1. intros. unfold not; intros. case_eq (M.find n (M.add x (TyVar y)(M.empty type))). intros. rewrite H1 in H0. apply M.find_2 in H1. apply M.add_3 in H1. apply empty_map_maps_to_nothing in H1. auto. auto. intros. rewrite H1 in H0. simpl in H0. destruct H0; auto. simpl FTV. apply not_member_app_converse. auto. Qed. Lemma termination_helper8: forall x y:nat, forall t : list constr, x <> y -> not (In x (FVC (apply_subst_to_constr_list (M.add x (TyVar y)(M.empty type)) t))). Proof. intros. induction t. simpl. auto. destruct a. simpl. apply not_member_app_converse. split. apply termination_helper7. assumption. apply not_member_app_converse. split. apply termination_helper7. assumption. assumption. Qed. Lemma termination_helper9 : forall x x0:nat, forall t ty: type, x <> x0 -> In x0 (FTV t) -> (In x0 (FTV (apply_subst_type (M.add x ty (M.empty type)) t))). Proof. intros. intros. induction t. simpl. simpl in H0. destruct H0. subst. case_eq (M.find x0 (M.add x ty (M.empty type))). intros. apply M.find_2 in H0. apply M.add_3 in H0. apply empty_map_maps_to_nothing in H0. contradiction H0. unfold M.E.eq. auto. intros. simpl. left; reflexivity. contradiction H0. simpl. apply in_or_app. simpl in H0. apply in_app_or in H0. destruct H0. apply IHt1 in H0. left; assumption. apply IHt2 in H0. right; assumption. Qed. Lemma termination_helper10 : forall x x0:nat, forall ty:type, forall t : list constr, x <> x0 -> In x0 (unique (FVC t)) -> (In x0 (unique (FVC (apply_subst_to_constr_list (M.add x ty (M.empty type)) t)))). Proof. intros. apply mem_unique_list_converse in H0. apply mem_unique_list. induction t. simpl in H0. contradiction H0. destruct a. simpl in H0. simpl. apply in_or_app. apply in_app_or in H0. destruct H0. left. apply termination_helper9 with (ty:= ty)(t:= t0) in H. auto. auto. apply in_app_or in H0. destruct H0. right. apply in_or_app. left. apply termination_helper9. auto. auto. right. apply in_or_app; right. apply IHt. auto. Qed. Lemma termination_helper11 : forall x x0:nat, forall ty t: type, not (In x0 (FTV ty) ) -> (In x0 (FTV (apply_subst_type (M.add x ty (M.empty type)) t))) -> In x0 (FTV t). Proof. intros. induction t. simpl in *. case_eq (M.find n (M.add x ty (M.empty type))). intros. rewrite H1 in H0. case (eq_dec_stamp n x). intros. subst. assert (x=x). reflexivity. apply M.add_1 with (e:= ty) (m:= M.empty type) in H2. apply M.find_1 in H2. rewrite H2 in H1. injection H1; intros; subst. elim H. auto. intros. apply M.find_2 in H1. apply M.add_3 in H1. apply empty_map_maps_to_nothing in H1. contradiction H1. auto. intros. rewrite H1 in H0. simpl in H0. assumption. simpl. simpl in H0. apply in_app_or in H0. destruct H0. apply IHt1 in H0. apply in_or_app. left. assumption. apply IHt2 in H0. apply in_or_app. right. auto. Qed. Lemma termination_helper12: forall x x0:nat, forall ty:type, forall t : list constr, not (In x0 (FTV ty)) -> (In x0 (FVC (apply_subst_to_constr_list (M.add x ty (M.empty type)) t))) ->In x0 (FVC t) . Proof. intros. induction t. simpl in H0; contradiction H0. destruct a. simpl. simpl in H0. apply in_or_app. apply in_app_or in H0. destruct H0. left. apply termination_helper11 with (ty:=ty)(x:=x). auto. auto. apply in_app_or in H0. destruct H0. right. apply in_or_app. left. apply termination_helper11 with (ty:=ty)(x:=x). auto. auto. right. apply in_or_app. right. apply IHt. auto. Qed. Lemma termination_helper14:forall x y:nat, forall t: list constr, x<>y -> In x (FVC t) -> In y (FVC t) -> (List.length (x::unique (FVC (apply_subst_to_constr_list (M.add x (TyVar y)(M.empty type)) t)))) = List.length (unique (FVC t)). Proof. intros. apply Permutation_length. apply NoDup_Permutation. apply NoDup_cons. unfold not; intros. apply mem_unique_list_converse in H2. apply termination_helper8 with (t:= t) in H. elim H; assumption. apply unique_and_ulist. apply unique_and_ulist. intros. unfold iff. split. intros. simpl in H2. destruct H2. subst. apply mem_unique_list. auto. apply mem_unique_list. apply mem_unique_list_converse in H2. case (eq_dec_stamp x x0);intros. subst; auto. case (eq_dec_stamp x0 y); intros. subst. auto. apply termination_helper12 in H2. auto. simpl. omega. intros. simpl. case (eq_dec_stamp x x0); intros. left; auto. right. apply termination_helper10; auto. Qed. Lemma termination_helper15:forall x x0:nat, forall t: type, x <> x0 -> In x (FTV t) -> In x0 (FTV (apply_subst_type (M.add x (TyVar x0)(M.empty type)) t)). Proof. intros. induction t. simpl in *. destruct H0. subst. case_eq (M.find x (M.add x (TyVar x0)(M.empty type))). intros. assert (x = x). reflexivity. apply M.add_1 with (e:= TyVar x0)(m:=M.empty type) in H1. apply M.find_1 in H1. rewrite H1 in H0. injection H0; intros; subst. simpl. left; reflexivity. intros. assert (x = x). reflexivity. apply M.add_1 with (e:= TyVar x0)(m:=M.empty type) in H1. apply M.find_1 in H1. rewrite H1 in H0. inversion H0. contradiction H0. simpl. simpl in H0. apply in_app_or in H0. apply in_or_app. destruct H0. apply IHt1 in H0. left; auto. apply IHt2 in H0. right; auto. Qed. Lemma termination_helper16:forall x x0:nat, forall t: list constr, x <> x0 -> In x (FVC t) -> In x0 (FVC (apply_subst_to_constr_list (M.add x (TyVar x0)(M.empty type)) t)). Proof. intros. induction t. simpl in H0; contradiction H0. destruct a. simpl in H0. simpl. apply in_app_or in H0. apply in_or_app. destruct H0. left. apply termination_helper15; auto. apply in_app_or in H0. right. apply in_or_app. destruct H0. left. apply termination_helper15; auto. apply IHt in H0. right; auto. Qed. Lemma termination_helper17: forall x y:nat, forall t: list constr, x<>y -> In x (FVC t) -> ~In y (FVC t) -> (List.length (x::unique (FVC (apply_subst_to_constr_list (M.add x (TyVar y)(M.empty type)) t)))) = List.length (y::unique (FVC t)). Proof. intros. apply Permutation_length. apply NoDup_Permutation. apply NoDup_cons. unfold not; intros. apply mem_unique_list_converse in H2. apply termination_helper8 with (t:=t) in H. elim H; auto. apply unique_and_ulist. apply NoDup_cons. unfold not; intros. apply mem_unique_list_converse in H2. elim H1. auto. apply unique_and_ulist. intros. unfold iff. split. intros. simpl in H2. simpl. destruct H2. right. subst. apply mem_unique_list. auto. case (eq_dec_stamp x0 y); intros. left; auto. right. apply mem_unique_list. apply mem_unique_list_converse in H2. eapply termination_helper12. instantiate (1:= (TyVar y)). simpl; omega. apply H2. simpl ; intros. destruct H2. subst. right. apply mem_unique_list. apply termination_helper16. auto. auto. case (eq_dec_stamp x x0); intros. left; auto. right. apply termination_helper10; auto. Qed. Lemma termination_helper18: forall x :nat, forall ty:type, forall t:type, not (In x (FTV t)) -> (FTV (apply_subst_type (M.add x ty (M.empty type)) t)) = (FTV t). Proof. intros. simpl. induction t. simpl FTV in H. simpl in H. f_equal. simpl. case_eq (M.find n (M.add x ty (M.empty type))). intros. apply M.find_2 in H0. apply M.add_3 in H0. apply empty_map_maps_to_nothing in H0. contradiction H0. unfold not,M.E.eq. intros. subst. elim H. left; reflexivity. intros. reflexivity. simpl in H. simpl. case_eq (In_nat_dec x (FTV t1)). intros. elim H. apply in_or_app. left. assumption. intros. clear H0. apply IHt1 in n. rewrite n. case_eq (In_nat_dec x (FTV t2)). intros. elim H. apply in_or_app. right; assumption. intros. clear H0. apply IHt2 in n0. rewrite n0. reflexivity. Qed. Lemma termination_helper19:forall x:nat, forall t: list constr, forall ty:type, not (In x (FVC t)) -> (FVC (apply_subst_to_constr_list (M.add x ty (M.empty type)) t)) = (FVC t). Proof. Proof. intros. induction t. simpl. reflexivity. destruct a. simpl in H. case (In_nat_dec x (FVC t)). intros. elim H. apply in_or_app. right. apply in_or_app. right. assumption. intros. simpl. apply IHt in n. rewrite n. case (In_nat_dec x (FTV t1)). intros. elim H. apply in_or_app. right; apply in_or_app. left;assumption. intros. rewrite termination_helper18. rewrite termination_helper18. reflexivity. assumption. unfold not; intros. elim H. apply in_or_app. left; assumption. Qed. Lemma termination_helper20:forall x y:nat, forall t: list constr, not (In x (FVC t)) -> List.length (unique (FVC (apply_subst_to_constr_list (M.add x (TyVar y)(M.empty type)) t))) = List.length (unique (FVC t)). intros. f_equal. rewrite termination_helper19. reflexivity. assumption. Qed. Lemma termination_helper21: forall x :nat, forall ty3 ty4:type, forall t :list constr, not (In x (FVC t)) -> member x (FTV ty3) || member x (FTV ty4) = false -> List.length (unique (FVC t)) < List.length (unique (x::(FTV ty3 ++FTV ty4)++FVC t)). Proof. intros. case (In_nat_dec x (FTV ty3 ++ FTV ty4 ++ FVC t)). intros H1. apply in_app_or in H1. unfold orb,ifb in H0. case_eq (member x (FTV ty3)). intros H2. rewrite H2 in H0. inversion H0. intros H2; rewrite H2 in H0. apply termination_helper5 in H0. apply termination_helper5 in H2. destruct H1; elim H2; auto. apply in_app_or in H1. destruct H1. elim H0; auto. elim H; auto. intros. apply ulist_incl_length_strict. apply unique_and_ulist. unfold incl. intros. apply mem_unique_list. apply mem_unique_list_converse in H1. assert ( incl (FVC t) (x:: (FTV ty3 ++ FTV ty4) ++ FVC t)). apply incl_tl. unfold incl. intros. apply in_or_app. right. auto. unfold incl in H2. apply H2 in H1. auto. unfold not; intros. elim H. apply mem_unique_list_converse. unfold incl in H1. apply H1. apply mem_unique_list. simpl. left. reflexivity. Qed. Lemma member_apply_subst: forall x:nat, forall ty1 ty2 ty: type, member x (FTV (Arrow ty1 ty2)) = false -> In x (FTV (apply_subst_type (M.add x (Arrow ty1 ty2)(M.empty type)) ty)) -> False. Proof. intros. induction ty. simpl in H0. case_eq (M.find n (M.add x (Arrow ty1 ty2) (M.empty type))). intros. rewrite H1 in H0. apply M.find_2 in H1. apply M.add_3 in H1. apply empty_map_maps_to_nothing in H1. contradiction H1. unfold not ;intros. unfold M.E.eq in H2; intros. subst. assert (n = n). reflexivity. apply M.add_1 with (e := (Arrow ty1 ty2)) (m:= M.empty type) in H2. apply M.find_1 in H2. apply M.find_1 in H1. rewrite H1 in H2. injection H2; intros; subst. apply termination_helper5 in H. elim H ; auto. intros. rewrite H1 in H0. simpl in H0. destruct H0. subst. assert (x=x). reflexivity. apply M.add_1 with (e:= (Arrow ty1 ty2)) (m:= M.empty type) in H0. apply M.find_1 in H0. rewrite H1 in H0. inversion H0. auto. simpl in H0. apply in_app_or in H0. destruct H0. apply IHty1 in H0. auto. apply IHty2 in H0. auto. Qed. Lemma member_apply_subst_constr:forall x:nat, forall ty1 ty2 : type, forall t: list constr, member x (FTV (Arrow ty1 ty2)) = false -> In x (FVC (apply_subst_to_constr_list (M.add x (Arrow ty1 ty2)(M.empty type)) t )) -> False. Proof. intros. induction t. simpl in H0. auto. destruct a. simpl in *. apply in_app_or in H0. destruct H0. apply member_apply_subst in H0; auto. apply in_app_or in H0. destruct H0. apply member_apply_subst in H0; auto. apply IHt. auto. Qed. Lemma ftv_and_apply_subst_type: forall x x0 :nat, forall t ty: type, x<> x0 -> In x (FTV t) -> In x0 (FTV ty) -> In x0 (FTV (apply_subst_type (M.add x ty (M.empty type)) t)). Proof. intros. induction t. simpl in H0. destruct H0. subst. simpl apply_subst_type. case_eq (M.find x (M.add x ty (M.empty type))). intros. assert (x=x). reflexivity. apply M.add_1 with (e:= ty)(m:= M.empty type) in H2. apply M.find_1 in H2. rewrite H0 in H2. injection H2; intros; subst. auto. intros. assert (x=x). reflexivity. apply M.add_1 with (e:= ty)(m:= M.empty type) in H2. apply M.find_1 in H2. rewrite H0 in H2. inversion H2. contradiction H0. simpl. apply in_or_app. simpl in H0. apply in_app_or in H0. destruct H0. left. apply IHt1 in H0. auto. right. apply IHt2 in H0. auto. Qed. Lemma fvc_and_apply_subst_constr: forall x x0 :nat, forall ty: type, forall t:list constr, x<> x0 -> In x (FVC t) -> In x0 (FTV ty) -> In x0 (FVC (apply_subst_to_constr_list (M.add x ty (M.empty type)) t)). Proof. intros. induction t. simpl in H0. contradiction H0. destruct a. simpl in *. apply in_app_or in H0. destruct H0. apply in_or_app. left. apply ftv_and_apply_subst_type. auto. auto. auto. apply in_app_or in H0. destruct H0. apply in_or_app. right. apply in_or_app. left. apply ftv_and_apply_subst_type. auto. auto. auto. apply IHt in H0. apply in_or_app. right; apply in_or_app. right. auto. Qed. Lemma termination_helper22: forall x:nat, forall ty1 ty2: type, forall t :list constr, In x (FVC t) -> member x (FTV (Arrow ty1 ty2)) = false -> List.length (x::unique (FVC (apply_subst_to_constr_list (M.add x (Arrow ty1 ty2) (M.empty type)) t))) = List.length (unique ( (FTV ty1 ++ FTV ty2) ++ FVC t)). Proof. intros. apply Permutation_length. apply NoDup_Permutation. apply NoDup_cons. unfold not; intros. apply mem_unique_list_converse in H1. induction t. simpl in H; contradiction H. destruct a. simpl in *. apply in_app_or in H1. destruct H1. apply member_apply_subst in H1. auto. auto. apply in_app_or in H1. destruct H1. apply member_apply_subst in H1. auto. auto. apply member_apply_subst_constr in H1. auto. auto. apply unique_and_ulist. apply unique_and_ulist. intros. unfold iff. split. intros. simpl in H1. destruct H1. subst. apply mem_unique_list. apply in_or_app. right; auto. apply mem_unique_list. apply mem_unique_list_converse in H1. case (eq_dec_stamp x x0). intros. subst. apply member_apply_subst_constr with (t:= t) in H0. contradiction H0. auto. intros. apply in_or_app. case (In_nat_dec x0 (FTV (Arrow ty1 ty2))). intros. left; simpl in i;auto. intros. right. apply termination_helper12 with (ty:= Arrow ty1 ty2)(x:=x). auto. auto. intros. simpl. case (eq_dec_stamp x x0); intros. left; auto. right. apply mem_unique_list. apply mem_unique_list_converse in H1. apply in_app_or in H1. destruct H1. apply fvc_and_apply_subst_constr. auto. auto. auto. apply mem_unique_list in H1. apply mem_unique_list_converse. apply termination_helper10 with (ty:= Arrow ty1 ty2). auto. auto. Qed. Lemma length_invariant_order : forall x :nat, forall ty3 ty4: type, forall t:list constr, length (unique (x:: (FTV ty3 ++ FTV ty4) ++ FVC t)) = length (unique ((FTV ty3 ++ FTV ty4) ++x:: FVC t)). Proof. intros. apply Permutation_length. apply NoDup_Permutation. apply unique_and_ulist. apply unique_and_ulist. intros. unfold iff. split. intros. apply mem_unique_list. apply mem_unique_list_converse in H. simpl in H. destruct H. subst. apply in_or_app. right. simpl. left; reflexivity. apply in_or_app. apply in_app_or in H. destruct H. left. auto. right. simpl. right. auto. intros. apply mem_unique_list_converse in H. apply mem_unique_list. apply in_app_or in H. destruct H. simpl. right. apply in_or_app. left. auto. simpl in H. destruct H. simpl. left. auto. simpl. right; apply in_or_app. right; auto. Qed. Lemma member_and_append : forall l l' :list nat, forall n:nat, member n (l++ l') = false -> member n l = false /\ member n l' = false. Proof. intros list1. induction list1. intros. simpl in H. simpl. split. reflexivity. assumption. (* induction case *) intros. split. simpl. destruct (eq_dec_stamp a n). subst. simpl in H. destruct (eq_dec_stamp n n). assumption. elim n0. reflexivity. simpl in H. destruct (eq_dec_stamp a n). inversion H. apply IHlist1 in H. destruct H. assumption. simpl in H. destruct (eq_dec_stamp a n). inversion H. apply IHlist1 in H. destruct H. assumption. Qed. Lemma member_and_append_converse : forall l l' :list nat, forall n:nat, member n l = false /\ member n l' = false -> member n (l++ l') = false. Proof. intros. induction l. destruct H; simpl in *. auto. destruct H. simpl in *. destruct (eq_dec_stamp a n). inversion H. auto. Qed. Function unify (c:list constr){wf meaPairMLt} :(option (M.t type)) := match c with nil => Some (M.empty type) | h:: t => (match h with EqCons (TyVar x) (TyVar y) => if eq_dec_stamp x y then unify t else (match unify (apply_subst_to_constr_list (M.add x (TyVar y) (M.empty type)) t) with Some p => Some (compose_subst (M.add x (TyVar y) (M.empty type)) p) | None => None end) | EqCons (TyVar x) (Arrow ty3 ty4) => if (member x (FTV ty3)) || (member x (FTV ty4) ) then None else (match (unify (apply_subst_to_constr_list (M.add x (Arrow ty3 ty4) (M.empty type)) t) ) with Some p => Some (compose_subst (M.add x (Arrow ty3 ty4) (M.empty type)) p) | None => None end ) | EqCons (Arrow ty3 ty4)(TyVar x) => if (member x (FTV ty3)) || (member x (FTV ty4)) then None else (match (unify (apply_subst_to_constr_list (M.add x (Arrow ty3 ty4) (M.empty type)) t) ) with Some p => Some (compose_subst (M.add x (Arrow ty3 ty4) (M.empty type)) p) | None => None end ) | EqCons (Arrow ty3 ty4) (Arrow ty5 ty6) => unify ((EqCons ty3 ty5)::((EqCons ty4 ty6)::t)) end ) end. Proof. intros. unfold meaPairMLt. unfold meaPairM. unfold meaC. rewrite anonymous. simpl FVC. simpl arrowC. unfold lt3. simpl. case (In_nat_dec y (FVC t)). intros. apply right_lex. auto. f_equal. destruct (In_nat_dec y (y::FVC t)). reflexivity. simpl in n. elim n. left; reflexivity. intros. apply left_lex. apply left_lex. simpl. destruct (In_nat_dec y (y::FVC t)). simpl. omega. simpl. omega. (* case when x and y are different *) intros. unfold meaPairMLt. unfold meaPairM. unfold lt3. unfold meaC. apply left_lex. apply left_lex. simpl. destruct (In_nat_dec x (y::FVC t)). simpl in i. destruct i. elim anonymous. symmetry; auto. destruct (In_nat_dec y (FVC t)). rewrite <- termination_helper14 with (x:=x)(y:=y)(t:=t). simpl. omega. assumption. assumption. assumption. rewrite <- termination_helper17 with (x:=x)(y:=y)(t:=t). simpl. omega. assumption. assumption. assumption. simpl. destruct (In_nat_dec y (FVC t)). simpl in n. apply not_or in n. destruct n. rewrite termination_helper20. omega. assumption. simpl. rewrite termination_helper20. omega. simpl in n. apply not_or in n. destruct n. assumption. (* third case constraint of type x =c t*) intros. unfold meaPairMLt. unfold meaPairM. unfold meaC. unfold lt3. apply left_lex. apply left_lex. (* new code *) case (In_nat_dec x (FVC t)). intros. simpl FVC. simpl. destruct (In_nat_dec x ((FTV ty3 ++ FTV ty4) ++ FVC t)). rewrite <- termination_helper22 with (ty1 := ty3) (ty2:= ty4) (t:=t) (x:=x). simpl. omega. auto. simpl. unfold orb,ifb in teq3. case_eq (member x (FTV ty3)). intros. rewrite H in teq3. inversion teq3. intros. rewrite H in teq3. apply member_and_append_converse. split; auto. apply not_member_app in n. destruct n. elim H0. auto. intros. simpl FVC. rewrite termination_helper19. apply termination_helper21 with (t:=t) (x:=x)(ty3:=ty3)(ty4:=ty4). assumption. assumption. assumption. (* third case constraint of type x =c t*) intros. unfold meaPairMLt. unfold meaPairM. unfold meaC. unfold lt3. apply left_lex. apply left_lex. case (In_nat_dec x (FVC t)). intros. simpl FVC. rewrite <- length_invariant_order. simpl. destruct (In_nat_dec x ((FTV ty3 ++ FTV ty4) ++ FVC t)). rewrite <- termination_helper22 with (ty1 := ty3) (ty2:= ty4) (t:=t) (x:=x). simpl. omega. auto. simpl. unfold orb,ifb in teq3. case_eq (member x (FTV ty3)). intros. rewrite H in teq3. inversion teq3. intros. rewrite H in teq3. apply member_and_append_converse. split; auto. apply not_member_app in n. destruct n. elim H0. auto. intros. simpl FVC. rewrite <- length_invariant_order. rewrite termination_helper19. apply termination_helper21 with (t:=t) (x:=x)(ty3:=ty3)(ty4:=ty4). assumption. assumption. assumption. (* last case *) intros. unfold meaPairMLt. unfold meaPairM. unfold meaC. unfold lt3. apply left_lex. apply right_lex. simpl arrowC. destruct ty3; destruct ty5; destruct ty4 ; destruct ty6;simpl;auto with arith;omega. simpl FVC. apply Permutation_length. apply NoDup_Permutation. apply unique_and_ulist. apply unique_and_ulist. intros. unfold iff. split. intros. apply mem_unique_list_converse in H. apply mem_unique_list. apply in_app_or in H. destruct H. apply in_or_app. left; apply in_or_app. left. assumption. apply in_app_or in H. destruct H. apply in_or_app. right; apply in_or_app. left; apply in_or_app. left; assumption. apply in_app_or in H. destruct H. apply in_or_app. left; apply in_or_app. right; assumption. apply in_app_or in H. destruct H. apply in_or_app. right; apply in_or_app. left; apply in_or_app. right; assumption. apply in_or_app. right; apply in_or_app. right; assumption. intros. apply mem_unique_list_converse in H. apply mem_unique_list. apply in_app_or in H. destruct H. apply in_app_or in H. destruct H. apply in_or_app. left; assumption. apply in_or_app. right; apply in_or_app. right; apply in_or_app. left; assumption. apply in_app_or in H. destruct H. apply in_app_or in H. destruct H. apply in_or_app. right; apply in_or_app. left;assumption. apply in_or_app. right; apply in_or_app. right; apply in_or_app. right; apply in_or_app. left; assumption. apply in_or_app. right; apply in_or_app. right; apply in_or_app. right; apply in_or_app. right; assumption. (* show well founded meaPairM *) unfold meaPairMLt. unfold meaPairM. apply wf_inverse_image with (A:= list constr)(B:= prod (prod nat nat) nat). apply lt3_wf. Defined. Check unify_ind. Lemma membership_and_apply_subst_to_subst: forall s1 s2:(M.t type), forall n:nat, M.In n s1 /\ M.In n (compose_subst s1 s2) -> M.In n (apply_subst_to_subst s1 s2). Proof. intros s1 s2 n. intros. destruct H. unfold compose_subst in H0. unfold subst_diff in H0. apply M.map2_2 in H0. destruct H0. exact H0. unfold apply_subst_to_subst. unfold M.In. unfold M.In in H. elim H. intros. exists (apply_subst_type s2 x). apply M.map_1. exact H1. Qed. Lemma map_and_mapsto : forall s1 s2 :M.t type, forall n:nat, forall t t0:type, M.MapsTo n t0 s1 /\ M.MapsTo n t (compose_subst s1 s2) -> t = apply_subst_type s2 t0. Proof. intros. inversion H. apply M.map_1 with (f:= apply_subst_type s2) in H0. unfold compose_subst,subst_diff in H1. apply M.find_1 in H1. rewrite M.map2_1 in H1. unfold apply_subst_to_subst in H1. apply M.find_1 in H0. rewrite H0 in H1. unfold choose_subst in H1. destruct (M.find n s2). injection H1. intros. symmetry; auto. injection H1; intros; symmetry ;auto. left. apply membership_and_apply_subst_to_subst. split. apply M.map_2 with (f:= apply_subst_type s2). unfold M.In. exists (apply_subst_type s2 t0); auto. apply M.find_2 in H1. unfold compose_subst, subst_diff. unfold M.In; exists t; auto. Qed. Lemma find_and_map_apply : forall s1 s2:M.t type, forall n:nat, M.find n s1 = None -> M.find n (M.map (apply_subst_type s2) s1) = None. Proof. intros. assert (not (M.In n s1)). unfold not. intros. unfold M.In in H0. elim H0; intros. apply M.find_1 in H1. rewrite H in H1. inversion H1. case_eq (M.find n (M.map (apply_subst_type s2) s1)). intros. apply M.find_2 in H1. assert ((M.In n (M.map (apply_subst_type s2) s1)) ). unfold M.In. exists t. assumption. apply M.map_2 in H2. unfold M.In in H2. elim H2. intros. apply M.find_1 in H3. rewrite H3 in H. inversion H. intros; reflexivity. Qed. Lemma membership_and_apply_subst_to_subst_with_map: forall s1 s2:(M.t type), forall n:nat, M.In n s1 -> M.In n (compose_subst s1 s2). Proof. intros. unfold compose_subst. unfold subst_diff. unfold apply_subst_to_subst. unfold M.In in *. elim H; intros. exists (apply_subst_type s2 x). apply M.find_2. rewrite M.map2_1. unfold choose_subst. case_eq (M.find n (M.map (apply_subst_type s2) s1)). intros. case_eq (M.find n s2). intros. f_equal. apply M.find_2 in H1. apply M.map_1 with (f:= apply_subst_type s2) in H0. apply M.find_1 in H0. apply M.find_1 in H1. rewrite H1 in H0. injection H0; intros; auto. intros. f_equal. apply M.find_2 in H1. apply M.map_1 with (f:= apply_subst_type s2) in H0. apply M.find_1 in H0. apply M.find_1 in H1. rewrite H1 in H0. injection H0; intros; auto. intros. apply M.map_1 with (f:= apply_subst_type s2) in H0. apply M.find_1 in H0. rewrite H1 in H0. inversion H0. left. apply M.map_1 with (f:= apply_subst_type s2) in H0. unfold M.In. exists (apply_subst_type s2 x). auto. Qed. Theorem composition_apply: forall s1 s2 : (M.t type), forall ty:type, apply_subst_type (compose_subst s1 s2) ty = apply_subst_type s2 (apply_subst_type s1 ty). Proof. intros s1. induction ty. simpl. case_eq (M.find n (compose_subst s1 s2)). intros. case_eq (M.find n s1). intros. apply M.find_2 in H0. apply M.find_2 in H. eapply map_and_mapsto. instantiate (1:= s1). instantiate (1:= n). split ; auto. intros. simpl. case_eq (M.find n s2). intros. unfold compose_subst in H. unfold subst_diff in H. unfold apply_subst_to_subst in H. rewrite M.map2_1 in H. rewrite H1 in H. unfold choose_subst in H. apply find_and_map_apply with (s2:= s2) in H0. rewrite H0 in H. injection H. intros. subst; auto. right. apply M.find_2 in H1. unfold M.In. exists t0. auto. intros. unfold compose_subst in H. unfold subst_diff in H. assert (not (M.In n s1)). unfold not. intros. unfold M.In in H2. elim H2. intros. apply M.find_1 in H3. rewrite H0 in H3. inversion H3. apply M.find_2 in H. assert (M.In n (M.map2 choose_subst (apply_subst_to_subst s1 s2) s2)). unfold M.In. exists t; auto. apply M.map2_2 in H3. destruct H3. unfold apply_subst_to_subst in H3. apply M.map_2 in H3. elim H2. auto. unfold M.In in H3. elim H3. intros. apply M.find_1 in H4. rewrite H4 in H1. inversion H1. intros. case_eq (M.find n s1). intros. apply M.find_2 in H0. assert (M.In n s1). unfold M.In; exists t; auto. apply membership_and_apply_subst_to_subst_with_map with (s2:=s2) in H1. unfold M.In in H1. elim H1. intros. apply M.find_1 in H2. rewrite H2 in H. inversion H. intros. simpl. case_eq (M.find n s2). intros. apply find_and_map_apply with (s2:=s2) in H0. unfold compose_subst in H. unfold apply_subst_to_subst in H. unfold subst_diff in H. rewrite M.map2_1 in H. unfold choose_subst in H. rewrite H0 in H. rewrite H1 in H. inversion H. right. unfold M.In. exists t. apply M.find_2. exact H1. intros; reflexivity. simpl. rewrite IHty1. rewrite IHty2. reflexivity. Qed. Lemma apply_subst_type_and_add: forall n n0:nat, n <> n0 -> apply_subst_type (M.add n (TyVar n0) (M.empty type)) (TyVar n) = apply_subst_type (M.add n (TyVar n0) (M.empty type)) (TyVar n0). Proof. intros. simpl. case_eq (M.find n (M.add n (TyVar n0)(M.empty type))). intros. case_eq (M.find n0 (M.add n (TyVar n0)(M.empty type))). intros. apply M.find_2 in H1. apply M.find_2 in H0. assert (H2:n<> n0). auto. apply M.add_3 with (elt := type)(m:= M.empty type)(e:=t0)(e' := TyVar n0) in H. assert (M.Empty (M.empty type)). apply M.empty_1. unfold M.Empty in H3. unfold not in H3. apply H3 in H. contradiction H. assumption. intros. assert (n<>n0);auto. assert (n = n). reflexivity. apply M.add_1 with (e:= (TyVar n0)) (m:= M.empty type) in H3. apply M.find_1 in H3. rewrite H0 in H3. injection H3; intros; auto. intros. case_eq (M.find n0 (M.add n (TyVar n0) (M.empty type))). intros. assert ( n = n). reflexivity. apply M.add_1 with (elt := type) (m:=M.empty type) (e:= TyVar n0) in H2. apply M.find_1 in H2. rewrite H0 in H2; inversion H2. intros. assert ( n = n). reflexivity. apply M.add_1 with (elt := type) (m:=M.empty type) (e:= TyVar n0) in H2. apply M.find_1 in H2. rewrite H0 in H2; inversion H2. Qed. Lemma apply_subst_type_and_membership: forall ty1 ty2:type, forall n:nat, member n (FTV ty1) = false -> ty1 = apply_subst_type (M.add n ty2 (M.empty type)) ty1. intros. induction ty1. simpl in H. simpl. case_eq (eq_dec_stamp n0 n). intros. rewrite H0 in H. inversion H. intros. case_eq (M.find n0 (M.add n ty2 (M.empty type))). intros. apply M.find_2 in H1. apply M.add_3 in H1. assert(M.Empty (M.empty type)). apply M.empty_1. unfold M.Empty in H2. unfold not in H2. apply H2 in H1. inversion H1. unfold not. intros. elim n1. unfold M.E.eq in H2. symmetry. assumption. intros. reflexivity. simpl. f_equal. simpl in H. apply IHty1_1. apply member_and_append in H. destruct H. assumption. apply IHty1_2. simpl in H. apply member_and_append in H. destruct H. assumption. Qed. Lemma compos_subst_and_apply_on_arrow: forall ty1 ty2:type, forall n:nat, member n (FTV ty1) || member n (FTV ty2) = false -> apply_subst_type (M.add n (Arrow ty1 ty2) (M.empty type))(TyVar n) = apply_subst_type (M.add n (Arrow ty1 ty2)(M.empty type)) (Arrow ty1 ty2). Proof. intros. unfold orb in H. unfold ifb in H. case_eq (member n (FTV ty1)). intros. rewrite H0 in H. inversion H. intros. rewrite H0 in H. simpl. case_eq (M.find n (M.add n (Arrow ty1 ty2) (M.empty type))). intros. apply M.find_2 in H1. assert (n = n). reflexivity. apply M.add_1 with (elt := type)(m:= M.empty type)(e:=Arrow ty1 ty2) in H2 . apply M.find_1 in H1. apply M.find_1 in H2. rewrite H1 in H2. injection H2. intros. subst. f_equal. simpl. apply apply_subst_type_and_membership. assumption. apply apply_subst_type_and_membership; assumption. intros. assert (n = n). reflexivity. apply M.add_1 with (elt := type)(m:= M.empty type)(e:=Arrow ty1 ty2) in H2. apply M.find_1 in H2. rewrite H1 in H2. inversion H2. Qed. Lemma empty_subst_on_type: forall ty : type, apply_subst_type (M.empty type) ty = ty. Proof. induction ty. simpl. case_eq (M.find n (M.empty type)). intros. apply M.find_2 in H. apply empty_map_maps_to_nothing in H. contradiction H. intros; reflexivity. simpl. f_equal; auto. Qed. Lemma member_and_constraint_subst_apply_helper: forall x: nat, forall ty ty1 ty2:type, forall t:list constr, In (EqCons ty1 ty2) t -> In (EqCons (apply_subst_type (M.add x ty (M.empty type)) ty1) (apply_subst_type (M.add x ty (M.empty type)) ty2)) (apply_subst_to_constr_list (M.add x ty (M.empty type)) t). Proof. intros. induction t. simpl in H; contradiction H. simpl. simpl in H. destruct H. subst. left. simpl. reflexivity. right. apply IHt. auto. Qed. Lemma solve_single_constraint : forall c:list constr, forall ty ty1:type, forall s :(M.t type), In (EqCons ty ty1) c -> Some s = unify c -> apply_subst_type s ty = apply_subst_type s ty1. Proof. intros c. functional induction (unify c). intros. simpl in H. contradiction H. intros. rewrite _x in H. simpl in H. destruct H. clear e1. injection H; intros; subst. reflexivity. apply IHo; auto. intros. simpl in H. destruct H. injection H; intros; subst. injection H0 ; intros; subst. rewrite composition_apply. rewrite composition_apply. f_equal. apply apply_subst_type_and_add. auto. injection H0; intros; subst. rewrite composition_apply. rewrite composition_apply. apply IHo. apply member_and_constraint_subst_apply_helper. auto. symmetry; auto. intros. inversion H0. intros. inversion H0. intros. simpl in H. destruct H. injection H ; intros; subst. injection H0; intros; subst. rewrite composition_apply. rewrite composition_apply. f_equal. apply compos_subst_and_apply_on_arrow. auto. injection H0; intros; subst. rewrite composition_apply. rewrite composition_apply. apply IHo. apply member_and_constraint_subst_apply_helper. auto. symmetry; auto. intros. inversion H0. intros. inversion H0. intros. simpl in H. destruct H. injection H ; intros; subst. injection H0; intros; subst. rewrite composition_apply. rewrite composition_apply. symmetry. f_equal. apply compos_subst_and_apply_on_arrow. auto. injection H0; intros; subst. rewrite composition_apply. rewrite composition_apply. apply IHo. apply member_and_constraint_subst_apply_helper. auto. symmetry; auto. intros. inversion H0. intros. simpl in H. destruct H. injection H; intros; subst. simpl. f_equal. apply IHo; auto. simpl. left. auto. apply IHo; auto. simpl. right;left. auto. apply IHo; auto. simpl. right. auto. Qed. Lemma satisfies_and_compose_subst: forall x:nat, forall ty:type, forall t:list constr, forall p:M.t type, satisfies_all p (apply_subst_to_constr_list (M.add x ty (M.empty type)) t) -> satisfies_all (compose_subst (M.add x ty (M.empty type)) p) t . Proof. intros. induction t. simpl. auto. simpl in *. destruct H. destruct a. split. unfold satisfies. simpl in H. rewrite composition_apply. rewrite composition_apply. auto. apply IHt. apply H0. Qed. Lemma mgu_axiom1: forall c2: list constr, forall s:(M.t type), Some s = unify c2 -> satisfies_all s c2. Proof. intros c2. functional induction (unify c2). Show 2. Show 3. intros. simpl; auto. rewrite _x. intros. unfold satisfies_all. fold satisfies_all. split. unfold satisfies; auto. apply IHo;auto. intros. unfold satisfies_all. fold satisfies_all. split. unfold satisfies. injection H; intros; subst. rewrite composition_apply. rewrite composition_apply. f_equal. apply apply_subst_type_and_add; auto. injection H; intros; subst. symmetry in e2. apply satisfies_and_compose_subst. apply IHo; auto. intros. inversion H. intros. inversion H. intros. injection H; intros; subst. unfold satisfies_all. fold satisfies_all. split. unfold satisfies. rewrite composition_apply. rewrite composition_apply. f_equal. apply compos_subst_and_apply_on_arrow. exact e1. apply satisfies_and_compose_subst. apply IHo; auto. intros. inversion H. intros. inversion H. intros. injection H; intros; subst. unfold satisfies_all. fold satisfies_all. split. unfold satisfies. rewrite composition_apply. rewrite composition_apply. f_equal. symmetry. apply compos_subst_and_apply_on_arrow. exact e1. apply satisfies_and_compose_subst. apply IHo; auto. intros. inversion H. intros. unfold satisfies_all. fold satisfies_all. split. unfold satisfies. simpl. f_equal. apply solve_single_constraint with (c:= (EqCons ty3 ty5:: EqCons ty4 ty6:: t)). simpl; left; auto. auto. apply solve_single_constraint with (c:= (EqCons ty3 ty5:: EqCons ty4 ty6:: t)). simpl. right. left; auto. auto. apply IHo in H. unfold satisfies_all in H. fold satisfies_all in H. destruct H. destruct H0. auto. Qed. Lemma squiggle_extensionality_lifted_to_types : forall s' s'':M.t type, (forall x : nat, apply_subst_type s' (TyVar x) = apply_subst_type s'' (TyVar x)) -> forall ty : type, apply_subst_type s' ty = apply_subst_type s'' ty. Proof. intros. induction ty. apply H; auto. simpl; auto. f_equal. auto. auto. Qed. Lemma squiggle_extensionality_pushed_to_type_variables : forall s' s'':M.t type, (forall ty : type, apply_subst_type s' ty = apply_subst_type s'' ty) -> forall x : nat, apply_subst_type s' (TyVar x) = apply_subst_type s'' (TyVar x). Proof. intros. apply H; auto. Qed. Lemma fresh_type_and_member_converse: forall ty ty1:type, forall st:nat, ~In st (FTV ty) -> apply_subst_type (M.add st ty1 (M.empty type)) ty = ty. Proof. intros ty. intros ty1. induction ty. intros. simpl. simpl in H. case_eq (M.find n (M.add st ty1 (M.empty type))). intros. apply not_or in H. destruct H. apply M.find_2 in H0. apply M.add_3 in H0. apply empty_map_maps_to_nothing in H0; contradiction H0. auto. intros. reflexivity. intros. simpl in H. apply not_member_app in H. destruct H. simpl. apply IHty1 in H. f_equal. auto. apply IHty2 in H0. auto. Qed. Lemma equal_substitution_instance_for_singleton_subst: forall s':M.t type, forall x: nat, forall ty ty1 :type, ~In x (FTV ty) /\ apply_subst_type s' (TyVar x) = apply_subst_type s' ty -> apply_subst_type s' ty1 = apply_subst_type s' (apply_subst_type (M.add x ty (M.empty type)) ty1). Proof. intros. induction ty1. case (eq_nat_dec x n). intros. subst. destruct H. simpl apply_subst_type at 2. case_eq (M.find n (M.add n ty (M.empty type))). intros. assert (n= n). reflexivity. apply M.add_1 with (e:= ty) (m:= M.empty type) in H2. apply M.find_1 in H2. rewrite H1 in H2. injection H2; intros; subst. auto. intros. assert (n= n). reflexivity. apply M.add_1 with (e:= ty) (m:= M.empty type) in H2. apply M.find_1 in H2. rewrite H1 in H2. inversion H2. intros. rewrite fresh_type_and_member_converse. auto. simpl. omega. simpl. f_equal; auto. Qed. Lemma constraint_satisfaction_and_substitution_instance : forall t:list constr, forall s':M.t type, forall x: nat, forall ty:type, satisfies_all s' t /\ ~In x (FTV ty) /\ apply_subst_type s' (TyVar x) = apply_subst_type s' ty -> satisfies_all s' (apply_subst_to_constr_list (M.add x ty (M.empty type)) t). Proof. intros t. induction t. (*base case *) simpl; auto. (* induction case *) destruct a. intros. destruct H. simpl in H. destruct H. destruct H0. simpl. split. clear H1. clear IHt. induction t0. case (eq_nat_dec x n). intros; subst. simpl. case_eq (M.find n (M.add n ty (M.empty type))). intros. apply M.find_2 in H1. assert (n =n ). auto. apply M.add_1 with (e:= ty) (m:= M.empty type) in H3. apply M.find_1 in H1. apply M.find_1 in H3. rewrite H1 in H3. injection H3; intros; subst. rewrite <- H2. rewrite H. apply equal_substitution_instance_for_singleton_subst. split; auto. intros. assert (n =n ). auto. apply M.add_1 with (e:= ty) (m:= M.empty type) in H3. apply M.find_1 in H3. rewrite H1 in H3. inversion H3. intros. simpl apply_subst_type at 2. case_eq (M.find n (M.add x ty (M.empty type))). intros. apply M.find_2 in H1. apply M.add_3 in H1. apply empty_map_maps_to_nothing in H1. contradiction H1. unfold M.E.eq. omega. intros. rewrite H. apply equal_substitution_instance_for_singleton_subst. split; auto. rewrite equal_substitution_instance_for_singleton_subst with (x:=x)(ty :=ty) in H. rewrite H. apply equal_substitution_instance_for_singleton_subst. split; auto. split; auto. apply IHt. split; auto. Qed. Lemma mgu_axiom2: forall c: list constr, forall s s': M.t type, unify c = Some s -> satisfies_all s' c -> exists s'':(M.t type), forall x:nat, apply_subst_type s' (TyVar x) = apply_subst_type (compose_subst s s'') (TyVar x). Proof. intros c. functional induction (unify c). intros. (* case 1 *) injection H; intros; subst. exists s'. intros. rewrite composition_apply. rewrite empty_subst_on_type. reflexivity. (* case 2*) rewrite _x in *. intros. unfold satisfies_all in H0. fold satisfies_all in H0. destruct H0. apply IHo. auto. auto. (* case 3*) intros. unfold satisfies_all in H0. fold satisfies_all in H0. destruct H0. unfold satisfies in H0. injection H; intros; subst. clear H. apply IHo with (s':=s') in e2. elim e2; intros s'''. intros. exists s'''. intros. rewrite composition_apply. rewrite composition_apply. simpl apply_subst_type at 4. case (eq_nat_dec x x0). intros. subst. case_eq (M.find x0 (M.add x0 (TyVar y)(M.empty type))). intros. assert (x0 = x0). auto. apply M.add_1 with (e:= TyVar y)(m:=M.empty type) in H3. apply M.find_1 in H3. rewrite H2 in H3. injection H3; intros. subst. rewrite <- composition_apply. rewrite H0. apply H. intros. assert (x0 = x0). auto. apply M.add_1 with (e:= TyVar y)(m:=M.empty type) in H3. apply M.find_1 in H3. rewrite H2 in H3. inversion H3. intros. case_eq (M.find x0 (M.add x (TyVar y) (M.empty type))). intros. apply M.find_2 in H2. apply M.add_3 in H2. apply empty_map_maps_to_nothing in H2. contradiction H2. unfold M.E.eq; omega. intros. rewrite <- composition_apply. apply H. apply constraint_satisfaction_and_substitution_instance. split; auto. split; simpl; auto. omega. intros. inversion H. intros. inversion H. Focus 2. intros; inversion H. Focus 2. intros; inversion H. Focus 3. intros; inversion H. (* both arrows *) Focus 3. intros. apply IHo with (s':= s') in H. auto. unfold satisfies_all in H0. fold satisfies_all in H0. unfold satisfies in H0. destruct H0. simpl. simpl in H0. injection H0; intros; subst. rewrite H2. rewrite H3. split; auto. (* arrow case *) intros. injection H; intros; subst. unfold satisfies_all in H0. fold satisfies_all in H0. destruct H0. unfold satisfies in H0. apply IHo with (s':=s') in e2. elim e2. intros s'''. intros. exists s'''. intros. rewrite composition_apply. rewrite composition_apply. case(eq_nat_dec x x0) ;intros. simpl apply_subst_type at 4. subst. case_eq (M.find x0 (M.add x0 (Arrow ty3 ty4)(M.empty type))). intros. assert (x0 = x0). auto. apply M.add_1 with (e:= Arrow ty3 ty4)(m:=M.empty type) in H4. apply M.find_1 in H4. rewrite H3 in H4. injection H4; intros;subst. clear H. clear IHo. rewrite H0. simpl. f_equal. rewrite <- composition_apply. apply squiggle_extensionality_lifted_to_types. auto. rewrite <- composition_apply. apply squiggle_extensionality_lifted_to_types. auto. intros. rewrite <- composition_apply. auto. simpl apply_subst_type at 4. case_eq (M.find x0 (M.add x (Arrow ty3 ty4)(M.empty type))). intros. apply M.find_2 in H3. apply M.add_3 in H3. apply empty_map_maps_to_nothing in H3. contradiction H3. unfold M.E.eq; omega. intros. rewrite H2. rewrite composition_apply. auto. apply constraint_satisfaction_and_substitution_instance. split; auto. split; auto. unfold not; intros. simpl in H2. apply in_app_or in H2. unfold orb,ifb in e1. case_eq (member x (FTV ty3)). intros. rewrite H3 in e1. inversion e1. intros. rewrite H3 in e1. apply termination_helper5 in H3. apply termination_helper5 in e1. destruct H2; tauto. (* the orther arrow case *) intros. injection H; intros; subst. unfold satisfies_all in H0. fold satisfies_all in H0. destruct H0. unfold satisfies in H0. symmetry in H0. apply IHo with (s':=s') in e2. elim e2. intros s'''. intros. exists s'''. intros. rewrite composition_apply. rewrite composition_apply. case(eq_nat_dec x x0) ;intros. simpl apply_subst_type at 4. subst. case_eq (M.find x0 (M.add x0 (Arrow ty3 ty4)(M.empty type))). intros. assert (x0 = x0). auto. apply M.add_1 with (e:= Arrow ty3 ty4)(m:=M.empty type) in H4. apply M.find_1 in H4. rewrite H3 in H4. injection H4; intros;subst. clear H. clear IHo. rewrite H0. simpl. f_equal. rewrite <- composition_apply. apply squiggle_extensionality_lifted_to_types. auto. rewrite <- composition_apply. apply squiggle_extensionality_lifted_to_types. auto. intros. rewrite <- composition_apply. auto. simpl apply_subst_type at 4. case_eq (M.find x0 (M.add x (Arrow ty3 ty4)(M.empty type))). intros. apply M.find_2 in H3. apply M.add_3 in H3. apply empty_map_maps_to_nothing in H3. contradiction H3. unfold M.E.eq; omega. intros. rewrite H2. rewrite composition_apply. auto. apply constraint_satisfaction_and_substitution_instance. split; auto. split; auto. unfold not; intros. simpl in H2. apply in_app_or in H2. unfold orb,ifb in e1. case_eq (member x (FTV ty3)). intros. rewrite H3 in e1. inversion e1. intros. rewrite H3 in e1. apply termination_helper5 in H3. apply termination_helper5 in e1. destruct H2; tauto. Qed. Lemma empty_map_and_elements: M.elements (M.empty type) = nil. Proof. assert (M.Empty (M.empty type)). apply M.empty_1. assert (exists m:list (nat* type), m = (M.elements (M.empty type))). exists (M.elements (M.empty type)). auto. elim H0. intros l. intros. induction l. auto. destruct a. unfold M.Empty in H . elim H with (a:=n)(e:=t) . apply M.elements_2. rewrite <- H1. simpl. apply InA_cons_hd. unfold M.eq_key_elt. unfold M.E.eq. auto. Qed. Lemma subst_and_list_member: forall s:(M.t type), forall n:nat, M.In n s -> exists ty:type,In (n,ty) (M.elements s). Proof. intros. unfold M.In in H. elim H. intros. apply M.elements_1 in H0. apply InA_split in H0. elim H0; intros. elim H1; intros. elim H2; intros. destruct H3. rewrite H4. destruct x1. exists x. simpl. unfold M.eq_key_elt in H3. unfold M.E.eq in H3. destruct H3. injection H3. intros; subst. injection H5; intros; subst. apply in_or_app. right; simpl. left; auto. Qed. Lemma subst_and_list_member_converse: forall s:(M.t type), forall n:nat, forall ty:type , In (n,ty) (M.elements s) -> M.In n s. Proof. intros. unfold M.In. exists ty. apply M.elements_2. apply In_InA. intros. unfold M.eq_key_elt. unfold M.E.eq. split;auto. auto. Qed. Lemma maps_to_and_list_member_elements: forall s:(M.t type), forall n:nat, forall ty:type , In (n,ty) (M.elements s) -> M.MapsTo n ty s. Proof. intros. apply M.elements_2. induction (M.elements s). simpl in H; contradiction H. apply In_InA. intros. unfold M.eq_key_elt. unfold M.E.eq. split;auto. auto. Qed. Lemma maps_to_and_list_member_elements_converse: forall s:(M.t type), forall n:nat, forall ty:type, M.MapsTo n ty s -> In (n,ty) (M.elements s) . Proof. intros. apply M.elements_1 in H. induction (M.elements s). inversion H. inversion H. subst. simpl. left. unfold M.eq_key_elt in H1. destruct H1. destruct a; auto. unfold M.E.eq in H0. simpl in H0, H1. subst; auto. subst. simpl; right. auto. Qed. Lemma mgu_axiom3_helperA : forall (ty0 : type) (a0 x0 : nat), In a0 (FTV ty0) -> In a0 (range_subst (M.add x0 ty0 (M.empty type))). Proof. intros. induction ty0. simpl in *. destruct H. subst; auto. unfold range_subst. rewrite in_flat_map. exists (x0,TyVar a0). simpl; auto. split. apply maps_to_and_list_member_elements_converse. apply M.add_1. unfold M.E.eq ; auto. left; reflexivity. contradiction H. simpl in H. apply in_app_or in H. destruct H. apply IHty0_1 in H. clear IHty0_1. clear IHty0_2. unfold range_subst in *. rewrite in_flat_map in *. elim H; intros. destruct x. destruct H0. simpl in H1. exists (x0, Arrow ty0_1 ty0_2). simpl. apply maps_to_and_list_member_elements in H0. case (eq_nat_dec k x0). intros; subst. assert (x0 = x0); intros. reflexivity. apply M.add_1 with (e:= ty0_1) (m:=M.empty type) in H2. apply M.find_1 in H0. apply M.find_1 in H2. rewrite H0 in H2. injection H2; intros. subst. split. apply maps_to_and_list_member_elements_converse. apply M.add_1. auto. unfold M.E.eq ; auto. apply in_or_app. left; auto. intros. apply M.add_3 in H0. apply empty_map_maps_to_nothing in H0. contradiction H0. unfold not; intros. elim n; auto. apply IHty0_2 in H. clear IHty0_1. clear IHty0_2. unfold range_subst in *. rewrite in_flat_map in *. elim H; intros. destruct x. destruct H0. simpl in H1. exists (x0, Arrow ty0_1 ty0_2). simpl. apply maps_to_and_list_member_elements in H0. case (eq_nat_dec k x0). intros; subst. assert (x0 = x0); intros. reflexivity. apply M.add_1 with (e:= ty0_2) (m:=M.empty type) in H2. apply M.find_1 in H0. apply M.find_1 in H2. rewrite H0 in H2. injection H2; intros. subst. split. apply maps_to_and_list_member_elements_converse. apply M.add_1. auto. unfold M.E.eq ; auto. apply in_or_app. right; auto. intros. apply M.add_3 in H0. apply empty_map_maps_to_nothing in H0. contradiction H0. unfold not; intros. elim n; auto. Qed. Lemma mgu_axiom3_helperA_converse : forall (ty0 : type) (a0 x0 : nat), In a0 (range_subst (M.add x0 ty0 (M.empty type)))-> In a0 (FTV ty0). Proof. intros. unfold range_subst in H. rewrite in_flat_map in H. elim H. intros. destruct H0. destruct x. simpl in *. apply maps_to_and_list_member_elements in H0. case (eq_nat_dec k x0). intros. subst. assert (x0 = x0). reflexivity. apply M.add_1 with (m:= M.empty type)(e:= ty0) in H2. apply M.find_1 in H0. apply M.find_1 in H2. rewrite H2 in H0. injection H0; intros; subst; auto. intros. assert (~M.E.eq x0 k). unfold M.E.eq ; auto. apply M.add_3 with (e:= t)(e':=ty0)(m:=M.empty type) in H2. apply empty_map_maps_to_nothing in H2. contradiction H2. auto. Qed. Lemma mgu_axiom3_helperB: forall (a0 : nat) (p0 : M.t type) (ty0 : type), In a0 (FTV (apply_subst_type p0 ty0)) -> ~ In a0 (range_subst p0) -> In a0 (FTV ty0). Proof. intros. induction ty0. simpl in *. case_eq (M.find n p0). intros. rewrite H1 in H. elim H0. unfold range_subst. rewrite in_flat_map. exists (n,t). simpl. split; auto. apply maps_to_and_list_member_elements_converse. apply M.find_2. auto. intros. rewrite H1 in H. simpl in *. auto. simpl in *. apply in_or_app. apply in_app_or in H. destruct H. apply IHty0_1 in H. left; auto. apply IHty0_2 in H. right; auto. Qed. Lemma alt_def_range: forall x:nat, forall p:M.t type, In x (range_subst p) -> (exists y, (In y (dom_subst p)) /\ In x (FTV (apply_subst_type p (TyVar y)))). Proof. intros x p. intros H1. unfold range_subst in H1. rewrite in_flat_map in H1. elim H1; intros. destruct x0. exists k. simpl in *. split. unfold dom_subst. destruct H. rewrite in_map_iff. exists (k,t). simpl; split;auto. case_eq (M.find k p); intros. destruct H. apply maps_to_and_list_member_elements in H. apply M.find_1 in H. rewrite H in H0. injection H0; intros; subst. auto. simpl. destruct H. apply maps_to_and_list_member_elements in H. apply M.find_1 in H. rewrite H in H0. inversion H0. Qed. Lemma alt_def_range_converse: forall x:nat, forall p:M.t type, (exists y, (In y (dom_subst p)) /\ In x (FTV (apply_subst_type p (TyVar y)))) -> In x (range_subst p). Proof. intros. elim H; intros. unfold range_subst. rewrite in_flat_map. destruct H0. clear H. simpl in H1. case_eq (M.find x0 p). intros. rewrite H in H1. exists (x0,t). split; simpl; auto. apply maps_to_and_list_member_elements_converse. apply M.find_2. auto. intros. rewrite H in H1. simpl in H1. destruct H1; auto. subst. unfold dom_subst in H0. rewrite in_map_iff in H0. elim H0;intros. destruct H1. destruct x0. simpl in H1; subst. apply maps_to_and_list_member_elements in H2. apply M.find_1 in H2. rewrite H in H2. inversion H2. contradiction H1; auto. Qed. Lemma mgu_axiom3_helperC: forall a x : nat, forall ty:type, forall p:M.t type, In a (dom_subst (compose_subst (M.add x ty (M.empty type)) p)) -> In a (dom_subst (M.add x ty (M.empty type))) \/ In a (dom_subst p). Proof. intros. unfold dom_subst in H. case (In_nat_dec a (dom_subst p)). intros. right; auto. intros. left. unfold dom_subst. rewrite in_map_iff. rewrite in_map_iff in H. elim H. intros. destruct x0. simpl in H0. destruct H0. subst. apply subst_and_list_member_converse in H1. unfold compose_subst, subst_diff in H1. apply M.map2_2 in H1. destruct H1. unfold apply_subst_to_subst in H0. apply M.map_2 in H0. unfold M.In in H0. elim H0; intros. case (eq_nat_dec x a). intros; subst. assert (a = a). reflexivity. apply M.add_1 with (e:=ty) (m:= M.empty type) in H2. apply M.find_1 in H2. apply M.find_1 in H1. exists (a,ty). simpl; auto. split; auto. apply maps_to_and_list_member_elements_converse. eapply M.add_1. unfold M.E.eq; auto. intros. exists (a,x0). simpl; split; auto. apply maps_to_and_list_member_elements_converse. auto. elim n. unfold dom_subst. rewrite in_map_iff. unfold M.In in H0. elim H0; intros. exists (a,x0). split; simpl; auto. apply maps_to_and_list_member_elements_converse. auto. Qed. Lemma membership_in_domain_for_singleton_maps: forall x x0:nat, forall ty:type, In x0 (dom_subst (M.add x ty (M.empty type))) -> x = x0. Proof. intros. case(eq_nat_dec x x0). intros; auto. intros. unfold dom_subst in H. rewrite in_map_iff in H. elim H; intros. destruct x1. simpl in H0. destruct H0; subst. apply maps_to_and_list_member_elements in H1. apply M.add_3 in H1. apply empty_map_maps_to_nothing in H1. contradiction H1. unfold not; intros. unfold M.E.eq in H0; omega. Qed. Definition idempotent (s1:M.t type) := (forall a:nat, In a (dom_subst s1) -> not (In a (range_subst s1)) )/\ forall a:nat, In a (range_subst s1) -> not (In a (dom_subst s1)). Lemma occurs_check_and_idempotency: forall x:nat, forall ty:type, member x (FTV ty) = false -> idempotent (M.add x ty (M.empty type)). Proof. intros. apply termination_helper5 in H. unfold idempotent. split; intros. apply membership_in_domain_for_singleton_maps in H0. subst. unfold not; intros. apply mgu_axiom3_helperA_converse in H0. elim H; auto. unfold not; intros. apply membership_in_domain_for_singleton_maps in H1. subst. apply mgu_axiom3_helperA_converse in H0. elim H; auto. Qed. Lemma mgu_axiom3_helperD: forall a x:nat, forall ty:type, forall p:M.t type, member x (FTV ty) = false -> In a (range_subst (compose_subst (M.add x ty (M.empty type)) p)) -> In a (range_subst (M.add x ty (M.empty type))) \/ In a (range_subst p). Proof. intros. apply occurs_check_and_idempotency in H. unfold idempotent in H. destruct H. apply alt_def_range in H0. elim H0; auto. intros x0 H4. destruct H4. rewrite composition_apply in H3. case (eq_type (apply_subst_type (M.add x ty (M.empty type)) (TyVar x0)) (TyVar x0)). intros. rewrite e in H3. right. apply alt_def_range_converse. apply mgu_axiom3_helperC in H2. exists x0. destruct H2. simpl in e. case_eq (M.find x0 (M.add x ty (M.empty type))); intros. rewrite H4 in e. subst. apply H in H2. elim H2. unfold range_subst. rewrite in_flat_map. exists (x0, (TyVar x0)). simpl; split; auto. apply maps_to_and_list_member_elements_converse. apply M.find_2. auto. rewrite H4 in e. unfold dom_subst in H2. rewrite in_map_iff in H2. elim H2; intros. destruct x1. destruct H5. simpl in H5. subst. apply maps_to_and_list_member_elements in H6. apply M.find_1 in H6. rewrite H4 in H6. inversion H6. split; auto. intros. apply mgu_axiom3_helperC in H2. destruct H2. case ( In_nat_dec a (range_subst p)); intros. right; auto. left. apply membership_in_domain_for_singleton_maps in H2. subst. simpl in H3. case_eq (M.find x0 (M.add x0 ty (M.empty type))). intros. rewrite H2 in H3. assert (x0 = x0). reflexivity. apply M.add_1 with (e:= ty) (m:=M.empty type) in H4. apply M.find_1 in H4. rewrite H2 in H4. injection H4; auto. intros; subst. apply mgu_axiom3_helperA. eapply mgu_axiom3_helperB. apply H3. auto. intros. rewrite H2 in H3. assert (x0 = x0). reflexivity. apply M.add_1 with (e:= ty) (m:=M.empty type) in H4. apply M.find_1 in H4. rewrite H2 in H4. inversion H4. simpl in H3. case_eq (M.find x0 (M.add x ty (M.empty type))); intros. rewrite H4 in H3. case (eq_nat_dec x x0). intros. subst. assert (x0 = x0). reflexivity. apply M.add_1 with (e:= ty)(m:=M.empty type) in H5. apply M.find_1 in H5. rewrite H4 in H5. injection H5; intros; subst. case (In_nat_dec a (range_subst p)); intros. right; auto. left. apply mgu_axiom3_helperA. eapply mgu_axiom3_helperB. apply H3. auto. intros. apply M.find_2 in H4. apply M.add_3 in H4. apply empty_map_maps_to_nothing in H4. contradiction H4. unfold not; intros. unfold M.E.eq in H5. elim n0; auto. rewrite H4 in H3. simpl in H3. case_eq (M.find x0 p). intros. rewrite H5 in H3. right. unfold range_subst. rewrite in_flat_map. exists (x0,t). simpl. split; auto. apply maps_to_and_list_member_elements_converse. apply M.find_2. auto. intros. rewrite H5 in H3. case (eq_nat_dec x x0). intros; subst. assert (x0 = x0). reflexivity. apply M.add_1 with (e:= ty)(m:=M.empty type) in H6. apply M.find_1 in H6. rewrite H4 in H6. inversion H6. intros. simpl in H3. destruct H3. subst. unfold dom_subst in H2. rewrite in_map_iff in H2. elim H2; intros. destruct x0. simpl in H3. destruct H3; subst. apply maps_to_and_list_member_elements in H6. apply M.find_1 in H6. rewrite H5 in H6. inversion H6. contradiction H3. Qed. Lemma mgu_axiom3_helper1: forall c:list constr, forall s:M.t type, unify c = Some s -> incl (range_subst s) (FVC c). Proof. intros c. functional induction (unify c). intros. injection H; intros. rewrite <- H0. simpl. unfold range_subst. rewrite empty_map_and_elements. simpl. unfold incl. intros; auto. (* case (TyVar x) = c (TyVar y) *) intros. rewrite _x in *. apply IHo in H. simpl. unfold incl in *. clear IHo. intros. apply H in H0. simpl. right; auto. (* case (TyVar x) =c (TyVar y) and x<> y *) intros. injection H; intros. clear H. apply IHo in e2. rewrite <- H0 in *. clear IHo. clear H0. unfold incl in *. intros; simpl in *. case ( eq_nat_dec x a); intros. left; auto. case ( eq_nat_dec y a); intros. right;left; auto. right. right. case (In_nat_dec a (range_subst p)). intros H1. apply e2 in H1. apply termination_helper12 with (ty:= TyVar y)(x:=x). simpl. unfold not; intros. destruct H0. elim n0;auto. auto. auto. intros. clear e2. elim n1. clear n1. apply mgu_axiom3_helperD in H. destruct H. apply mgu_axiom3_helperA_converse in H. simpl in H. destruct H. elim n0; auto. contradiction H. auto. apply termination_helper6. unfold not; intros. simpl in H0; destruct H0. omega. contradiction H0. intros H H1. discriminate H1. intros H H1. discriminate H1. (* case tyvar x = arrow ty3 ty4 *) intros. injection H ; intros. rewrite <- H0 in *. apply IHo in e2. simpl. simpl in e2. clear IHo. unfold incl in *. intros. simpl. case (eq_nat_dec x a). intros. left;auto. intros. right. apply in_or_app. case (In_nat_dec a (FTV ty3 ++ FTV ty4)); intros. left; auto. right. apply termination_helper12 with (ty:= Arrow ty3 ty4)(x:=x). auto. case (In_nat_dec a (range_subst p)); intros. apply e2 in i; auto. elim n1. clear n1. apply mgu_axiom3_helperD in H1. destruct H1. apply mgu_axiom3_helperA_converse in H1. simpl in H1. elim n0; auto. auto. apply termination_helper6. unfold orb,ifb in e1. simpl. unfold not; intros. apply in_app_or in H2. case_eq (member x (FTV ty3)). intros. rewrite H3 in e1. inversion e1. intros. rewrite H3 in e1. destruct H2. apply termination_helper5 in H3. elim H3; auto. apply termination_helper5 in e1. elim e1; auto. (** **) intros. inversion H. intros. inversion H. (* case 4 *) intros. injection H ; intros. rewrite <- H0 in *. apply IHo in e2. simpl. simpl in e2. clear IHo. unfold incl in *. intros. simpl. apply in_or_app. case (In_nat_dec a (FTV ty3 ++ FTV ty4)); intros. left; auto. right. simpl. case (eq_nat_dec x a). intros. left;auto. intros. right. apply termination_helper12 with (ty:= Arrow ty3 ty4)(x:=x). simpl; auto. case (In_nat_dec a (range_subst p)); intros. apply e2 in i; auto. elim n1. clear n1. apply mgu_axiom3_helperD in H1. destruct H1. apply mgu_axiom3_helperA_converse in H1. simpl in H1. elim n; auto. auto. apply termination_helper6. unfold orb,ifb in e1. simpl. unfold not; intros. apply in_app_or in H2. case_eq (member x (FTV ty3)). intros. rewrite H3 in e1. inversion e1. intros. rewrite H3 in e1. destruct H2. apply termination_helper5 in H3. elim H3; auto. apply termination_helper5 in e1. elim e1; auto. intros. inversion H. intros; auto. apply IHo in H. auto. simpl. simpl in H. unfold incl in *. intros. apply H in H0. apply in_app_or in H0. destruct H0. apply in_or_app. left; apply in_or_app. left; auto. apply in_app_or in H0. destruct H0. apply in_or_app. right; apply in_or_app. left; apply in_or_app. left; auto. apply in_app_or in H0. destruct H0. apply in_or_app. left; apply in_or_app. right; auto. apply in_app_or in H0. destruct H0. apply in_or_app. right; apply in_or_app. left; apply in_or_app. right; auto. apply in_or_app. right; apply in_or_app. right; auto. Qed. Lemma mgu_axiom3_helper2: forall c:list constr, forall s:M.t type, unify c = Some s -> incl (dom_subst s) (FVC c). Proof. intros c. functional induction (unify c). (* case 1*) intros. injection H; intros. rewrite <- H0. simpl. unfold dom_subst. unfold incl. (* case 2*) intros a. intros. rewrite in_map_iff in H1. elim H1. intros. destruct H2. rewrite empty_map_and_elements in H3. simpl in H3. contradiction H3. (* case x =c y and x<>y*) intros. simpl. unfold incl. intros. apply IHo in H. unfold incl in H. simpl. right; right. apply H; auto. (* case 2*) intros. injection H; intros. rewrite <- H0 in *. clear H. apply IHo in e2. intros. unfold incl in e2. unfold incl. intros. clear IHo. clear H0. simpl. unfold dom_subst in H. rewrite in_map_iff in H. elim H. intros. destruct H0. clear H. destruct x0. apply subst_and_list_member_converse in H1. simpl in H0. subst. case (eq_nat_dec a x). intros. subst. left. auto. intros. right. case(eq_nat_dec a y). intros. subst. left; reflexivity. intros. right. apply termination_helper12 with (ty:= TyVar y)(x:=x). simpl. unfold not; intros. destruct H. subst; omega. auto. apply e2. unfold dom_subst. rewrite in_map_iff. unfold compose_subst in H1. unfold subst_diff in H1. unfold apply_subst_to_subst in H1. simpl. apply M.map2_2 in H1. destruct H1. apply M.map_2 in H. unfold M.In in H. elim H;intros. apply M.add_3 in H0. apply empty_map_maps_to_nothing in H0. contradiction H0. unfold not; intros;unfold M.E.eq in H1. auto. unfold M.In in H. elim H; intros. apply M.elements_1 in H0. apply InA_split in H0. elim H0; intros. elim H1; intros. elim H2; intros. destruct x2. destruct H3. rewrite H4. unfold M.eq_key_elt in H3. unfold M.E.eq in H3. destruct H3; simpl in H3. simpl in H5. subst. exists (k,t1). simpl. split; auto. apply in_or_app. right. simpl. left. auto. intros. discriminate H. intros. discriminate H. (* case (Tyvar x) =c Arrow ty3 ty4 *) intros. simpl. injection H; intros. clear H. apply IHo in e2. rewrite <- H0 in *. clear IHo. unfold incl in *. intros. unfold dom_subst in H. rewrite in_map_iff in H. elim H. intros. clear H. destruct x0. simpl in H1. destruct H1. subst. simpl. case (eq_nat_dec x a). intros. left. auto. intros. right. apply in_or_app. case (In_nat_dec a (FTV (Arrow ty3 ty4))). intros. left. simpl in i. auto. intros. right. case (In_nat_dec a (dom_subst p)). intros H2. apply e2 in H2. eapply termination_helper12. instantiate (1:= Arrow ty3 ty4). auto. apply H2. intros. elim n1. unfold dom_subst. rewrite in_map_iff. exists (a,t0). intros. simpl. split. reflexivity. apply subst_and_list_member_converse in H1. unfold compose_subst in H1. unfold subst_diff in H1. unfold apply_subst_to_subst in H1. apply M.map2_2 in H1. destruct H1. apply M.map_2 in H. unfold M.In in H. elim H; intros. apply M.add_3 in H0. apply empty_map_maps_to_nothing in H0; contradiction H0. unfold not; intros; unfold M.E.eq in *; auto. assert (M.In a p). auto. unfold M.In in H. elim H. intros. elim n1. unfold dom_subst. rewrite in_map_iff. exists (a,x0). simpl. split. reflexivity. apply M.elements_1 in H1. apply InA_split in H1. elim H1; intros. elim H2; intros. elim H3; intros. destruct H4. rewrite H5. simpl. unfold M.eq_key_elt in H4. simpl in H4. destruct x2. simpl in *. destruct H4. unfold M.E.eq in H4. subst. apply in_or_app. right. simpl. left; auto. intros. discriminate H. intros. discriminate H. (* case 4 *) intros. simpl. injection H; intros. clear H. apply IHo in e2. rewrite <- H0 in *. clear IHo. unfold incl in *. intros. unfold dom_subst in H. rewrite in_map_iff in H. elim H. intros. clear H. destruct x0. simpl in H1. destruct H1. subst. case (In_nat_dec a (FTV (Arrow ty3 ty4))). intros. apply in_or_app. left. auto. intros. apply in_or_app. right. simpl. case (eq_nat_dec x a). intros. left. auto. intros. right. case (In_nat_dec a (dom_subst p)). intros H2. apply e2 in H2. eapply termination_helper12. instantiate (1:= Arrow ty3 ty4). auto. apply H2. intros. elim n1. unfold dom_subst. rewrite in_map_iff. exists (a,t0). intros. simpl. split. reflexivity. apply subst_and_list_member_converse in H1. unfold compose_subst in H1. unfold subst_diff in H1. unfold apply_subst_to_subst in H1. apply M.map2_2 in H1. destruct H1. apply M.map_2 in H. unfold M.In in H. elim H; intros. apply M.add_3 in H0. apply empty_map_maps_to_nothing in H0; contradiction H0. unfold not; intros; unfold M.E.eq in *; auto. assert (M.In a p). auto. unfold M.In in H. elim H. intros. elim n1. unfold dom_subst. rewrite in_map_iff. exists (a,x0). simpl. split. reflexivity. apply M.elements_1 in H1. apply InA_split in H1. elim H1; intros. elim H2; intros. elim H3; intros. destruct H4. rewrite H5. simpl. unfold M.eq_key_elt in H4. simpl in H4. destruct x2. simpl in *. destruct H4. unfold M.E.eq in H4. subst. apply in_or_app. right. simpl. left; auto. intros. discriminate H. (* case ty3 -> ty4 =c ty5 = c ty6 *) intros. apply IHo in H. simpl. simpl in H. unfold incl in *. intros. apply H in H0. apply in_or_app. apply in_app_or in H0. destruct H0. left. apply in_or_app. left. auto. apply in_app_or in H0. destruct H0. right. apply in_or_app. left. apply in_or_app. left; auto. apply in_app_or in H0. destruct H0. left. apply in_or_app. right;auto. apply in_app_or in H0. destruct H0. right. apply in_or_app. left. apply in_or_app. right; auto. right. apply in_or_app. right; auto. Qed. Lemma mgu_axiom3: forall c:list constr, forall s:M.t type, unify c = Some s -> incl (FTV_subst s) (FVC c). Proof. intros. unfold FTV_subst. apply incl_app. apply mgu_axiom3_helper1. auto. apply mgu_axiom3_helper2. auto. Qed. Lemma member_and_or: forall x:nat, forall ty1 ty2 : type, member x (FTV ty1 ++ FTV ty2) = true -> member x (FTV ty1) = true \/ member x (FTV ty2) = true. Proof. intros. induction (FTV ty1). simpl in *. right; auto. simpl in *. destruct (eq_dec_stamp a x). subst. left; auto. auto. Qed. Lemma type_and_left_arrow: forall ty1 ty2:type, ty1 = Arrow ty1 ty2 -> False. Proof. intros ty1. induction ty1. intros. inversion H. intros. injection H; intros. apply IHty1_1 in H1. auto. Qed. Lemma type_and_right_arrow: forall ty1 ty2:type, ty2 = Arrow ty1 ty2 -> False. Proof. intros ty1. induction ty2. intros. inversion H. intros. injection H; intros. rewrite <- H1 in *. apply IHty2_2 in H0. auto. Qed. Fixpoint subterms (t:type) := match t with TyVar x => nil | Arrow ty1 ty2 => ty1 :: ty2 :: subterms ty1 ++ subterms ty2 end. Lemma containtment: forall ty1 ty2 : type, In ty1 (subterms ty2) -> forall ty:type, In ty (subterms ty1) -> In ty (subterms ty2). Proof. intros. induction ty2. simpl in *. auto. simpl in *. destruct H. subst. right; right. apply in_or_app. left; auto. destruct H; subst. right; right. apply in_or_app. right; auto. apply in_app_or in H. right; right; apply in_or_app. destruct H. apply IHty2_1 in H. left; auto. right; auto. Qed. Lemma well_foundedness_for_types: forall ty, In ty (subterms ty) -> False. Proof. intros ty. induction ty. simpl. auto. simpl. unfold not; intros. destruct H. apply type_and_left_arrow in H. contradiction H. destruct H. apply type_and_right_arrow in H. contradiction H. simpl in H. apply in_app_or in H. destruct H. simpl in H. apply containtment with (ty1 := Arrow ty1 ty2) (ty2:= ty1)(ty:= ty1) in H. auto. simpl; auto. apply containtment with (ty1:= Arrow ty1 ty2) (ty2 := ty2)(ty:= ty2) in H. auto. simpl; auto. Qed. Lemma member_subterms_unequal: forall ty1 ty2: type, In ty1 (subterms ty2) -> ty1 <> ty2. Proof. intros. case (eq_type ty1 ty2). intros. subst. apply well_foundedness_for_types in H. contradiction H. intros. auto. Qed. Lemma member_subterms_and_apply_subst: forall (ty:type) (x0 : nat) (s' : M.t type), In (TyVar x0) (subterms ty) -> apply_subst_type s' (TyVar x0) <> apply_subst_type s' ty. Proof. intros. apply member_subterms_unequal. induction ty. simpl in H. contradiction H. simpl apply_subst_type at 2. simpl subterms. simpl in H. destruct H. subst. simpl. left; auto. destruct H. subst. simpl; right; left; auto. apply in_app_or in H. destruct H. apply IHty1 in H. simpl; right; right; apply in_or_app; left. auto. simpl; right; right; apply in_or_app; right; auto. Qed. Lemma member_arrow_and_subterms: forall (ty1 ty2 : type) (x0 : nat), member x0 (FTV ty1) || member x0 (FTV ty2) = true -> In (TyVar x0) (subterms (Arrow ty1 ty2)). Proof. intros. unfold orb, ifb in *. intros. induction ty1. simpl in *. destruct (eq_dec_stamp n x0). left; f_equal; auto. induction ty2. simpl in *. destruct (eq_dec_stamp n1 x0). right;left; f_equal; auto. inversion H. simpl in H. apply member_and_or in H. destruct H. apply IHty2_1 in H. simpl. destruct H. left; auto. destruct H. right; right; left; auto. right; right; right. right; apply in_or_app. left; auto. apply IHty2_2 in H. simpl. destruct H. left; auto. destruct H. right; right; right; left; auto. right; right; right. right; apply in_or_app. right; auto. simpl in *. case_eq (member x0 (FTV ty1_1 ++ FTV ty1_2)). intros. rewrite H0 in H. apply member_and_or in H0. destruct H0. rewrite H0 in IHty1_1. apply IHty1_1 in H. destruct H. right; right; left; auto. destruct H. right; left; auto. apply in_app_or in H. destruct H. right; right; right;right. apply in_or_app. left; apply in_or_app. left; auto. right; right; right;right. apply in_or_app. right. auto. case_eq (member x0 (FTV ty1_1)). intros. rewrite H0 in IHty1_2. apply IHty1_2 in H. destruct H. right; right; right;left; auto. destruct H. right;left; auto. apply in_app_or in H. destruct H. right; right; right; right. apply in_or_app. left; apply in_or_app. right; auto. right; right; right; right. apply in_or_app. right; auto. intros. rewrite H1 in IHty1_1. rewrite H0 in IHty1_2. apply IHty1_2 in H. destruct H. right; right; right. left; auto. destruct H. right; left; auto. apply in_app_or in H. right;right;right. right. apply in_or_app. destruct H. left; apply in_or_app. right; auto. right; auto. intros. rewrite H0 in H. apply member_and_append in H0. destruct H0. rewrite H0 in IHty1_1. apply IHty1_1 in H. destruct H. right;right;left; auto. destruct H. right; left; auto. apply in_app_or in H. destruct H. right; right;right;right; auto. apply in_or_app. left; apply in_or_app. left; auto. right; right;right;right; auto. apply in_or_app; right; auto. Qed. Lemma member_apply_subst_unequal: forall (ty1 ty2 : type) (x0 : nat) (s' : M.t type), member x0 (FTV ty1) || member x0 (FTV ty2) = true -> apply_subst_type s' (TyVar x0) = apply_subst_type s' (Arrow ty1 ty2) -> False. Proof. intros. apply member_arrow_and_subterms in H. apply member_subterms_and_apply_subst with (s':=s') in H. elim H; auto. Qed. Lemma mgu_axiom4: forall c: list constr, forall s': M.t type, satisfies_all s' c -> exists s:(M.t type), unify c = Some s. Proof. intros c. intros s'. functional induction (unify c). exists (M.empty type). reflexivity. rewrite _x in *. intros. unfold satisfies_all in H. fold satisfies_all in H. destruct H. apply IHo in H0. auto. intros. exists (compose_subst (M.add x (TyVar y) (M.empty type)) p). reflexivity. rewrite e2 in IHo. intros. eapply IHo. unfold satisfies_all in H. fold satisfies_all in H. destruct H. subst. unfold satisfies in H. apply constraint_satisfaction_and_substitution_instance. split; auto. split; auto. simpl; omega. intros. unfold satisfies_all in H. fold satisfies_all in H. destruct H. unfold satisfies in H. apply member_apply_subst_unequal in H. contradiction H. auto. intros. exists (compose_subst (M.add x (Arrow ty3 ty4) (M.empty type)) p). auto. rewrite e2 in IHo. intros. apply IHo. apply constraint_satisfaction_and_substitution_instance. unfold satisfies_all in H. fold satisfies_all in H. destruct H. unfold satisfies in H. split; auto. split; auto. simpl. unfold orb,ifb in e1. case_eq (member x (FTV ty3)). intros. rewrite H1 in e1. inversion e1. intros. rewrite H1 in e1. apply termination_helper5 in H1. apply termination_helper5 in e1. unfold not; intros. apply in_app_or in H2. tauto. intros. unfold satisfies_all in H. fold satisfies_all in H. destruct H. unfold satisfies in H. symmetry in H. apply member_apply_subst_unequal in H. contradiction H. auto. exists (compose_subst (M.add x (Arrow ty3 ty4) (M.empty type)) p). auto. rewrite e2 in IHo. intros. apply IHo. apply constraint_satisfaction_and_substitution_instance. unfold satisfies_all in H. fold satisfies_all in H. destruct H. unfold satisfies in H. split; auto. split; auto. simpl. unfold orb,ifb in e1. case_eq (member x (FTV ty3)). intros. rewrite H1 in e1. inversion e1. intros. rewrite H1 in e1. apply termination_helper5 in H1. apply termination_helper5 in e1. unfold not; intros. apply in_app_or in H2. tauto. auto. intros. apply IHo. clear IHo. unfold satisfies_all in *. fold satisfies_all in *. destruct H. simpl in H. injection H; intros; subst. unfold satisfies; split; auto. Qed. End Unify_Axioms. End MyStuff.