diff --git a/_CoqProject b/_CoqProject index 62c7654..f342861 100644 --- a/_CoqProject +++ b/_CoqProject @@ -5,3 +5,4 @@ theories/abs_defs.v theories/abs_examples.v theories/abs_functional_metatheory.v +theories/utils.v diff --git a/src/abs.ott b/src/abs.ott index 35d0211..b207231 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -108,32 +108,35 @@ formula :: formula_ ::= {{ coq (Map.find [[x]] [[s]] = Some ([[t]])) }} | G ( fn ) = sig :: M :: G_fn_eq_sig {{ coq (Map.find [[fn]] [[G]] = Some (ctxv_sig [[sig]])) }} - | fresh ( x1 , ... , xn , e ) :: M :: fresh + | distinct ( x1 , ... , xn ) :: M :: distinct_vars + {{ coq (NoDup [[x1 ... xn]]) }} + | fresh ( x1 , ... , xn , e ) :: M :: fresh_e {{ coq (fresh_vars_e [[x1 ... xn]] [[e]]) }} + | fresh ( x1 , ... , xn , s ) :: M :: fresh_s + {{ coq (fresh_vars_s [[x1 ... xn]] [[s]]) }} + | fresh ( x1 , ... , xn , e , s ) :: M :: fresh + {{ coq (fresh_vars [[x1 ... xn]] [[e]] [[s]]) }} + | disjoint ( ( x1 , ... , xi ) , ( y1 , ... , yj ) ) :: M :: disjoint + {{ coq (disjoint [[x1 ... xi]] [[y1 ... yj]]) }} + | well_formed ( x1 , ... , xn , e , s ) :: M :: well_formed + {{ coq (well_formed [[e]] [[s]] [[x1 ... xn]]) }} embed {{ coq -Fixpoint get_val (k:x) (l:list(x*x)): option x := - match l with - | nil => None - | (k', v) :: l' => - match eq_x k k' with - | left _ => Some v - | _ => get_val k l' - end - end. -Fixpoint e_var_subst (e5:e) (l:list (x*x)) : e := - match e5 with - | e_t t => e_t t - | e_var x => - match get_val x l with - | None => e_var x - | Some y => e_var y - end - | e_fn_call fn e_list => - e_fn_call fn (map (fun e => e_var_subst e l) e_list) - end. +Definition disjoint {A:Type} (l1 l2: list A): Prop := + forall a, In a l1 -> ~ In a l2. + +Equations e_var_subst_one (e5:e) (x_ y_: x) : e := { + e_var_subst_one (e_t t) _ _ := e_t t; + e_var_subst_one (e_var x0) x_ y_ := if (eq_x x0 x_) then (e_var y_) else (e_var x0); + e_var_subst_one (e_fn_call fn0 arg_list) x_ y_ := e_fn_call fn0 (e_list_subst_one arg_list x_ y_) } +where e_list_subst_one (es:list e) (x_ y_: x) : list e := { + e_list_subst_one nil _ _ := nil; + e_list_subst_one (e0::es) x_ y_ := e_var_subst_one e0 x_ y_ :: e_list_subst_one es x_ y_ +}. + +Definition e_var_subst (e5:e) (l:list (x*x)) : e := fold_right (fun '(x', y') e' => e_var_subst_one e' x' y') e5 l. Equations fresh_vars_e (l : list x) (e0 : e) : Prop := { fresh_vars_e _ (e_t _) := True; @@ -142,6 +145,17 @@ Equations fresh_vars_e (l : list x) (e0 : e) : Prop := { where fresh_vars_el (l : list x) (el0 : list e) : Prop := { fresh_vars_el l nil := True; fresh_vars_el l (e1::el0) := fresh_vars_e l e1 /\ fresh_vars_el l el0 }. + +Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := + match l with + | nil => True + | (y::ys) => ~ Map.In y s0 /\ fresh_vars_s ys s0 + end. + +Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := + fresh_vars_s l s0 /\ fresh_vars_e l e0. + +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ NoDup l. }} defns @@ -175,6 +189,7 @@ defn G ( fn ) = T1 , ... , Tn -> T G [ x1 |-> T1 , ... , xn |-> Tn ] |- e : T + distinct (x1 , ... , xn) ------------------------------------------- :: func_decl G |- def T fn ( T1 x1 , ... , Tn xn ) = e ; @@ -193,6 +208,7 @@ defn ------------------------------------------------------------------------------------------------------------- :: fun_exp F1 ... Fn , s |- fn ( e1 , ... , ei , e , e'1 , ... , e'j ) ~> s' |- fn ( e1 , ... , ei , e' , e'1 , ... , e'j ) - fresh ( y1 , ... , yn , e ) + well_formed (y1 , ... , yn , e, s) + disjoint ((y1 , ... , yn) , (x1 , ... , xn)) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- :: fun_ground F1 ... Fi def T fn ( T1 x1 , ... , Tn xn ) = e ; F'1 ... F'j , s |- fn ( t1 , ... , tn ) ~> s [ y1 |-> t1 , ... , yn |-> tn ] |- e [ x1 |-> y1 , ... , xn |-> yn ] diff --git a/theories/abs_defs.v b/theories/abs_defs.v index 4388839..54b6526 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -100,27 +100,20 @@ Fixpoint e_ott_ind (n:e) : P_e n := end. End e_rect. -Fixpoint get_val (k:x) (l:list(x*x)): option x := - match l with - | nil => None - | (k', v) :: l' => - match eq_x k k' with - | left _ => Some v - | _ => get_val k l' - end - end. -Fixpoint e_var_subst (e5:e) (l:list (x*x)) : e := - match e5 with - | e_t t => e_t t - | e_var x => - match get_val x l with - | None => e_var x - | Some y => e_var y - end - | e_fn_call fn e_list => - e_fn_call fn (map (fun e => e_var_subst e l) e_list) - end. +Definition disjoint {A:Type} (l1 l2: list A): Prop := + forall a, In a l1 -> ~ In a l2. + +Equations e_var_subst_one (e5:e) (x_ y_: x) : e := { + e_var_subst_one (e_t t) _ _ := e_t t; + e_var_subst_one (e_var x0) x_ y_ := if (eq_x x0 x_) then (e_var y_) else (e_var x0); + e_var_subst_one (e_fn_call fn0 arg_list) x_ y_ := e_fn_call fn0 (e_list_subst_one arg_list x_ y_) } +where e_list_subst_one (es:list e) (x_ y_: x) : list e := { + e_list_subst_one nil _ _ := nil; + e_list_subst_one (e0::es) x_ y_ := e_var_subst_one e0 x_ y_ :: e_list_subst_one es x_ y_ +}. + +Definition e_var_subst (e5:e) (l:list (x*x)) : e := fold_right (fun '(x', y') e' => e_var_subst_one e' x' y') e5 l. Equations fresh_vars_e (l : list x) (e0 : e) : Prop := { fresh_vars_e _ (e_t _) := True; @@ -130,6 +123,17 @@ where fresh_vars_el (l : list x) (el0 : list e) : Prop := { fresh_vars_el l nil := True; fresh_vars_el l (e1::el0) := fresh_vars_e l e1 /\ fresh_vars_el l el0 }. +Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := + match l with + | nil => True + | (y::ys) => ~ Map.In y s0 /\ fresh_vars_s ys s0 + end. + +Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := + fresh_vars_s l s0 /\ fresh_vars_e l e0. + +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ NoDup l. + (** definitions *) (* defns expression_well_typing *) @@ -152,6 +156,7 @@ Inductive typ_F : G -> F -> Prop := (* defn F *) | typ_func_decl : forall (T_x_list:list (T*x)) (G5:G) (T_5:T) (fn5:fn) (e5:e), (Map.find fn5 G5 = Some (ctxv_sig (sig_sig (map (fun (pat_:(T*x)) => match pat_ with (T_,x_) => T_ end ) T_x_list) T_5) )) -> typ_e (fold_right (fun (ax : x * T) (G5 : G) => Map.add (fst ax) (ctxv_T (snd ax)) G5) G5 (map (fun (pat_:(T*x)) => match pat_ with (T_,x_) => (x_,T_) end ) T_x_list) ) e5 T_5 -> + (NoDup (map (fun (pat_:(T*x)) => match pat_ with (T_,x_) => x_ end ) T_x_list) ) -> typ_F G5 (F_fn T_5 fn5 T_x_list e5). (** definitions *) @@ -164,7 +169,8 @@ Inductive red_e : list F -> s -> e -> s -> e -> Prop := (* defn e *) red_e F_list s5 e_5 s' e' -> red_e F_list s5 (e_fn_call fn5 ((app e_list (app (cons e_5 nil) (app e'_list nil))))) s' (e_fn_call fn5 ((app e_list (app (cons e' nil) (app e'_list nil))))) | red_fun_ground : forall (T_x_t_y_list:list (T*x*t*x)) (F'_list F_list:list F) (T_5:T) (fn5:fn) (e5:e) (s5:s), - (fresh_vars_e (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) e5 ) -> + (well_formed e5 s5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) ) -> + (disjoint (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => x_ end ) T_x_t_y_list) ) -> red_e ((app F_list (app (cons (F_fn T_5 fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (T_,x_) end ) T_x_t_y_list) e5) nil) (app F'_list nil)))) s5 (e_fn_call fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (e_t t_) end ) T_x_t_y_list)) (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5) s5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (y_,t_) end ) T_x_t_y_list) ) (e_var_subst e5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (x_,y_) end ) T_x_t_y_list) ) . diff --git a/theories/abs_examples.v b/theories/abs_examples.v index c21ed60..97e196d 100644 --- a/theories/abs_examples.v +++ b/theories/abs_examples.v @@ -25,6 +25,7 @@ Proof. apply typ_func_decl. - easy. - apply e_const_5_T_int. + - simpl; constructor. Qed. Lemma e_call_const_5_T_int : diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index 7bf5619..95de7b0 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -1,26 +1,677 @@ -From ABS Require Import abs_defs. -From Coq Require Import List. +From ABS Require Import abs_defs + utils. + +From Coq Require Import List + FSets.FMapFacts + Lia. + +From Equations Require Import Equations. + +Require Import FMapList. +Module MapFacts := FSets.FMapFacts.Facts Map. Import ListNotations. (** * ABS Functional Metatheory *) +Section FunctionalMetatheory. + +Hypothesis (vars_fs_distinct: forall (x_:x) (fn_:fn), x_ <> fn_). +Hypothesis (vars_well_typed: forall (x_:x) (G0: G) T0, + Map.find x_ G0 = Some T0 -> + exists T_, T0 = ctxv_T T_). + Definition subG (G1 G2 : G) : Prop := - forall (key : string) (elt : ctxv), + forall (key : string) (elt : ctxv), Map.find key G1 = Some elt -> Map.find key G2 = Some elt. +Notation "G ⊢ e : T" := (typ_e G e T) (at level 5). +Notation "G F⊢ F" := (typ_F G F) (at level 5). +Notation "G1 ⊆ G2" := (subG G1 G2) (at level 5). + +Lemma subG_refl: forall G0, + subG G0 G0. +Proof. easy. Qed. + +Lemma subG_add: forall G0 G1 y T_, + subG G0 G1 -> + ~ Map.In y G0 -> + subG G0 (Map.add y T_ G1). +Proof. + intros. + intros ?x_ ?T_ ?. + + destruct (eq_x y x_); subst. + - exfalso. + apply H0. + apply MapFacts.in_find_iff. + intro. + rewrite H1 in H2. + discriminate. + - apply Map.find_1. + apply MapFacts.add_neq_mapsto_iff; auto. + pose proof H x_ T_0 H1. + apply Map.find_2. + assumption. +Qed. + +Lemma subG_add_2: forall G0 G1 y T_, + subG G0 G1 -> + Map.find y G0 = Some T_ -> + subG G0 (Map.add y T_ G1). +Proof. + intros. + intros ?x_ ?T_ ?. + + destruct (eq_x y x_); subst. + - rewrite H0 in H1. + inv H1. + apply Map.find_1. + now apply Map.add_1. + - apply Map.find_1. + apply MapFacts.add_neq_mapsto_iff; auto. + pose proof H x_ T_0 H1. + apply Map.find_2. + assumption. +Qed. + +(* this is stricter than the ABS paper *) +(* we require that any variables in the typing context also exist in the state *) Definition G_vdash_s (G5 : G) (s5 : s) := - forall (x5 : x) (t5 : t) (T5 : T), - Map.find x5 s5 = Some t5 -> + forall (x5 : x) (T5 : T), Map.find x5 G5 = Some (ctxv_T T5) -> - typ_e G5 (e_t t5) T5. + exists t5, + Map.find x5 s5 = Some t5 /\ typ_e G5 (e_t t5) T5. + +Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). + +Lemma fresh_subG: forall G0 s0 (sub_list: list (T*x*t*x)), + G_vdash_s G0 s0 -> + fresh_vars_s (map (fun '(_,_,_,y)=>y) sub_list) s0 -> + NoDup (map (fun '(_,_,_,y)=>y) sub_list) -> + subG G0 (fold_right (fun '(T_,_,_,y_) G0 => Map.add y_ (ctxv_T T_) G0) G0 sub_list). +Proof. + intros. + induction sub_list. + - easy. + - destruct a as (((?T_, ?x_), ?t_), y). + inv H1. + inv H0. + pose proof IHsub_list H2 H5. + cbn. + apply subG_add; auto. + intro. + + apply MapFacts.in_find_iff in H3. + apply MapFacts.not_find_in_iff in H1. + pose proof map_neq_none_is_some _ _ H3 as (?T_, ?). + pose proof vars_well_typed _ _ _ H6 as (?T_, ->). + pose proof H _ _ H6 as (?t_, (?, _)). + rewrite H1 in H7. + discriminate. +Qed. + +Lemma fresh_consistent: forall G0 s0 (sub_list: list (T*x*t*x)), + G_vdash_s G0 s0 -> + (forall T_ t_, In (T_, t_) (map (fun '(T_, _, t_, _) => (T_, t_)) sub_list) -> + typ_e G0 (e_t t_) T_) -> + fresh_vars_s (map (fun '(_,_,_,y)=>y) sub_list) s0 -> + NoDup (map (fun '(_,_,_,y)=>y) sub_list) -> + G_vdash_s (fold_right (fun '(T_,_,_,y_) G0 => Map.add y_ (ctxv_T T_) G0) G0 sub_list) + (fold_right (fun '(_,_,t_,y_) s0 => Map.add y_ t_ s0) s0 sub_list). +Proof. + intros. + induction sub_list. + * easy. + * destruct a as (((?T_, ?x_), ?t_), y). + inv H1. + inv H2. + + cbn. + intros ?y ?T_ ?. + destruct (eq_x y y0); subst. + - exists t_. + split... + + apply Map.find_1. + now apply Map.add_1. + + assert (T_ = T_0). + { + apply Map.find_2 in H1. + apply MapFacts.add_mapsto_iff in H1. + destruct H1 as [(_, ?) | (?, ?)]. + + now inv H1. + + exfalso. + now apply H1. + } + assert (In (T_0, t_) (map (fun '(T_, _, t_, _) => (T_, t_)) ((T_, x_, t_, y0) :: sub_list))) + by (left; now rewrite H2). + specialize (H0 _ _ H5). + inv H0; constructor. + - apply Map.find_2 in H1. + apply Map.add_3 in H1; auto. + apply Map.find_1 in H1. + assert (forall (T_ : T) (t_ : t), + In (T_, t_) (map (fun '(T_0, _, t_0, _) => (T_0, t_0)) sub_list) -> + typ_e G0 (e_t t_) T_). + { + intros. + apply H0. + right. + assumption. + } + pose proof IHsub_list H2 H4 H7 _ _ H1 as (?t_, (?, ?)). + exists t_0. + split... + + apply Map.find_1. + apply Map.add_2; auto. + apply Map.find_2; assumption. + + inv H8; constructor. +Qed. + +Lemma subG_consistent: forall G1 G2 s0, + subG G1 G2 -> G_vdash_s G2 s0 -> G_vdash_s G1 s0. +Proof. + intros. + intros x_ t_ ?. + + pose proof H _ _ H1. + pose proof H0 _ _ H2 as (?t, (?, ?)). + exists t. + split; auto. + inv H4;constructor. +Qed. + +Lemma subG_type: forall G1 G2 e0 T0, + subG G1 G2 -> typ_e G1 e0 T0 -> typ_e G2 e0 T0. +Proof. + intros. + induction H0. + - constructor. + - constructor. + - apply H in H0. + constructor. + apply H0. + - constructor. + + intros. + apply H1; auto. + + apply H in H2. + apply H2. +Qed. + +(* this is 9.3.8 from Types and Programming Languages *) +(* it has not yet proven useful *) +Lemma subst_lemma_one_alt: forall (x0 x1:x) G0 e0 T0 T1, + typ_e (Map.add x0 (ctxv_T T1) G0) e0 T0 -> + typ_e G0 (e_var x1) T1 -> + typ_e G0 (e_var_subst_one e0 x0 x1) T0. +Proof. + intros. + generalize dependent T0. + generalize dependent T1. + generalize dependent G0. + eapply e_ott_ind with + (n:=e0) + (P_list_e:= fun e_list => forall e0, + In e0 e_list -> + forall G0 T0 T1, + typ_e (Map.add x0 (ctxv_T T1) G0) e0 T0 -> + typ_e G0 (e_var x1) T1 -> + typ_e G0 (e_var_subst e0 [(x0, x1)]) T0) + ;cbn; intros. + - inv H; simp e_var_subst_one; constructor. + - inv H. + simp e_var_subst_one. + destruct (eq_x x5 x0); subst. + + apply Map.find_2 in H3. + apply MapFacts.add_mapsto_iff in H3. + destruct H3 as [(?&?) | (?&?)]; subst. + * inv H1. + assumption. + * contradiction. + + constructor. + apply Map.find_1. + eapply Map.add_3. + * apply not_eq_sym. + apply n. + * apply Map.find_2 in H3. + apply H3. + - inv H1. + simp e_var_subst_one. + rewrite <- subst_fst_commute. + replace (map (fun x : e * T => let (e_, _) := let '(e_, T_) := x in (e_var_subst_one e_ x0 x1, T_) in e_) e_T_list) + with + (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) + (map (fun '(e_, T_) => (e_var_subst_one e_ x0 x1, T_)) e_T_list)) + by apply map_map. + constructor. + + rewrite map_map. + intros. + apply in_map_iff in H1. + destruct H1 as ((?e_&?T_) & ? & ?). + inv H1. + eapply H. + * apply in_map_iff. + exists (e_0, T_). + split; eauto. + * apply H5. + apply in_map_iff. + exists (e_0, T_). + split; auto. + * apply H0. + + apply Map.find_1. + apply Map.find_2 in H7. + rewrite subst_snd_commutes. + eapply Map.add_3; eauto. + - inv H. + - inv H1. + + eapply H; eauto. + + eapply H0; eauto. +Qed. + +Lemma same_type_sub: forall (sub_list: list (x*x)) G0 e0 T0, + typ_e G0 e0 T0 -> + (forall x0 y0 T0, + In (x0, y0) sub_list -> + Map.find x0 G0 = Some T0 -> + Map.find y0 G0 = Some T0) -> + typ_e G0 (e_var_subst e0 sub_list) T0. +Proof. + { + intros. + generalize dependent T0. + eapply e_ott_ind with + (n:= e0) + (P_list_e:= fun e_list => forall e0 T0, + In e0 e_list -> + typ_e G0 e0 T0 -> + typ_e G0 (e_var_subst e0 sub_list) T0) + ; intros. + - rewrite subst_term. + simp e_var_subst_one. + - rewrite subst_var. + constructor. + induction sub_list. + + inv H. + now simpl. + + destruct a. + simpl. + destruct (eq_x (replace_var x5 sub_list) x); subst. + * eapply H0; eauto. + -- now left. + -- apply IHsub_list; eauto. + intros. + eapply H0; eauto. + now right. + * eapply IHsub_list; eauto. + intros. + eapply H0; eauto. + now right. + - inv H1. + rewrite subst_fn. + rewrite map_map. + replace (map (fun x : e * T => e_var_subst (let (e_, _) := x in e_) sub_list) e_T_list) + with (map (fun pat_:e*T => let (e, _) := pat_ in e) (map (fun '(e, T) => (e_var_subst e sub_list, T)) e_T_list)) + by (rewrite map_map; apply map_ext; now intros (?, ?)). + constructor. + + intros. + apply in_map_iff in H1. + destruct H1 as ((?e, ?T), (?, ?)). + inv H1. + apply in_map_iff in H2. + destruct H2 as ((?e_, ?T_), (?, ?)). + inv H1. + apply H. + * apply in_map_iff. + exists (e_0, T_). + split; eauto. + * apply H5. + apply in_map_iff. + exists (e_0, T_). + split; eauto. + + now replace (map (fun pat_ : e * T => let (_, T_) := pat_ in T_) (map (fun '(e, T) => (e_var_subst e sub_list, T)) e_T_list)) + with(map (fun pat_ : e * T => let (_, T_) := pat_ in T_) e_T_list) + by (rewrite map_map; apply map_ext; now intros (?, ?)). + - inv H. + - inv H2. + + now apply H. + + now apply H1. + } + +Qed. + +Lemma subst_lemma_one: forall G0 x0 y0 e0 Ai A, + typ_e (Map.add x0 Ai G0) e0 A -> + fresh_vars_e [y0] e0 -> + typ_e (Map.add y0 Ai G0) (e_var_subst_one e0 x0 y0) A. +Proof. + { + intros. + generalize dependent A. + revert H0. + apply e_ott_ind with + (n:=e0) + (P_list_e:= fun e_list => + forall e0 A, + In e0 e_list -> + fresh_vars_e [y0] e0 -> + typ_e (Map.add x0 Ai G0) e0 A -> + typ_e (Map.add y0 Ai G0) (e_var_subst_one e0 x0 y0) A); + intros. + - simp e_var_subst_one. + inv H; constructor. + - simp e_var_subst_one. + inv H. + apply Map.find_2 in H3. + apply MapFacts.add_mapsto_iff in H3. + destruct H3 as [(?,?)|(?,?)]; subst. + + destruct (eq_x x5 x5); subst. + * constructor. + apply Map.find_1. + now apply Map.add_1. + * contradiction. + + + destruct (eq_x x5 x0); subst. + * contradiction. + * destruct (eq_x x5 y0); subst. + -- simp fresh_vars_e in H0. + exfalso. + apply H0. + now left. + -- constructor. + apply Map.find_1. + apply Map.add_2; eauto. + - simp e_var_subst_one. + inv H1. + replace (e_list_subst_one (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list) x0 y0) + with (map (fun pat_:e*T => let (e, _) := pat_ in e) (map (fun '(e, T) => (e_var_subst_one e x0 y0, T)) e_T_list)) + by (rewrite e_list_subst_map; + rewrite 2 map_map; + apply map_ext; + now intros (?,?)). + constructor. + + intros. + apply in_map_iff in H1. + destruct H1 as ((?e, ?T), (?, ?)). + inv H1. + apply in_map_iff in H2. + destruct H2 as ((?e_, ?T_), (?, ?)). + inv H1. + apply H. + * apply in_map_iff. + exists (e_0, T_). + split; eauto. + * simp fresh_vars_e in H0. + eapply e_list_fresh. + apply H0. + apply in_map_iff. + eexists (e_0, T_). + split; auto. + * apply H5. + apply in_map_iff. + exists (e_0, T_). + split; eauto. + + replace (map (fun pat_ : e * T => let (_, T_) := pat_ in T_) (map (fun '(e, T) => (e_var_subst_one e x0 y0, T)) e_T_list)) + with(map (fun pat_ : e * T => let (_, T_) := pat_ in T_) e_T_list) + by (rewrite map_map; apply map_ext; now intros (?, ?)). + + apply Map.find_2 in H7. + apply MapFacts.add_mapsto_iff in H7. + destruct H7 as [(?,?)|(?,?)]. + * exfalso. + apply (vars_fs_distinct _ _ H1). + * apply Map.find_1. + apply Map.add_2; eauto. + - inv H. + - destruct H1; subst. + + apply H; eauto. + + apply H0; eauto. + } +Qed. + +Lemma subst_lemma: forall (T_x_t_y_list:list (T*x*t*x)) G0 e0 A, + typ_e (fold_right (fun '(Ai, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T Ai) G0) G0 T_x_t_y_list) e0 A -> + NoDup (map (fun '(_, _, _, y) => y) T_x_t_y_list) -> + NoDup (map (fun '(_, x, _, _) => x) T_x_t_y_list) -> + fresh_vars_e (map (fun '(_, _, _, y) => y) T_x_t_y_list) e0 -> + disjoint (map (fun '(_, _, _, y) => y) T_x_t_y_list) (map (fun '(_, x, _, _) => x) T_x_t_y_list) -> + typ_e (fold_right (fun '(Ai, _, _, y) (G0 : G) => Map.add y (ctxv_T Ai) G0) G0 T_x_t_y_list) + (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) A. +Proof. + intros. + generalize dependent G0. + generalize dependent e0. + induction T_x_t_y_list; intros. + - easy. + - destruct a as (((?T_,?x_),?t_),?y). + unfold e_var_subst. + simpl in *. + inv H0. + inv H1. + pose proof fresh_first_e _ _ _ H2. + pose proof fresh_monotone_e _ _ _ H2. + epose proof disjoint_monotone _ _ _ _ H3. + assert (~ In x_ (map (fun '(_, y) => y) (map (fun '(Ai, _, _, y1) => (Ai, y1)) T_x_t_y_list))). + { intro. + apply (H3 x_). + - right. + rewrite map_map in H9. + replace (map (fun '(_, _, _, y1) => y1) T_x_t_y_list) + with + (map (fun x0 : T * x * t * x => let '(_, y) := let '(Ai, _, _, y1) := x0 in (Ai, y1) in y) T_x_t_y_list). + apply H9. + apply map_eq. + now intros (((?, ?), ?), ?). + - now left. + } + replace (Map.add x_ (ctxv_T T_) (fold_right (fun '(Ai, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T Ai) G0) G0 T_x_t_y_list)) + with (fold_right (fun '(Ai, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T Ai) G0) (Map.add x_ (ctxv_T T_) G0) T_x_t_y_list) + in H. + pose proof IHT_x_t_y_list H7 H8 H4 _ H1 _ H as IH. + replace (fold_right (fun '(Ai, _, _, y) (G0 : G) => Map.add y (ctxv_T Ai) G0) (Map.add x_ (ctxv_T T_) G0) T_x_t_y_list) + with (Map.add x_ (ctxv_T T_) (fold_right (fun '(Ai, _, _, y) (G0 : G) => Map.add y (ctxv_T Ai) G0) G0 T_x_t_y_list)) + in IH. + assert (fresh_vars_e [y] (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list))). + { + assert (map snd (map (fun '(_, x_0, _, y_) => (x_0, y_)) T_x_t_y_list) = map (fun '(_, _, _, y) => y) T_x_t_y_list). + { + rewrite map_map. + apply map_eq. + now intros (((?, ?), ?), ?). + } + apply fresh_var_subst; try rewrite H10; auto. + } + now apply (subst_lemma_one _ _ _ _ _ _ IH H10). + + (* resolving those replaces from earlier *) + { + epose proof fold_add_comm G0 x_ T_ (map (fun '(Ai, _, _, y1) => (Ai, y1)) T_x_t_y_list) H9. + rewrite 2 fold_map1. + Fail apply H10. + (* why? *) + admit. + } + { + epose proof fold_add_comm G0 x_ T_ (map (fun '(Ai, _, _, y1) => (Ai, y1)) T_x_t_y_list) H9. + rewrite 2 fold_map2. + Fail rewrite <- H10. + (* why? *) + admit. + } +Admitted. Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), - (* FIXME: add well-typing of all function definitions here *) G_vdash_s G5 s5 -> + Forall (typ_F G5) Flist -> forall (e5 : e) (T5 : T) (s' : s) (e' : e), typ_e G5 e5 T5 -> red_e Flist s5 e5 s' e' -> exists G', subG G5 G' /\ G_vdash_s G' s' /\ typ_e G' e' T5. Proof. -Admitted. + intros Fs G5 s0 s_well_typed F_well_typed. + intros e0 T0 s' e' e0_type reduction. + generalize dependent T0. + generalize dependent G5. + induction reduction. + - intros. + exists G5; splits. + 1,2: easy. + inv e0_type. + destruct (s_well_typed x5 T0 H2) as (?, (?, ?)). + rewrite H in H0. + inv H0. + assumption. + + - (* RED_FUN_EXPR *) + intros. + inv e0_type. + rewrite app_nil_r in H0. + pose proof split_corresponding_list e_T_list e_list e_5 e'_list H0 + as (T_list & T_5 & T'_list & ? & ? & ?). + assert (In (e_5, T_5) (map (fun pat_ : e * T => let (e_0, T_0) := pat_ in (e_0, T_0)) e_T_list)). { + rewrite H3. + apply in_map_iff. + exists (e_5, T_5). + split; auto. + apply in_combine_split with (2:=eq_refl); auto. + } + pose proof H2 e_5 T_5 H5. + destruct (IHreduction G5 s_well_typed F_well_typed _ H6) as (G' & G'extends & G'consistent & ?). + exists G'. + splits. + 1,2: easy. + replace (e_list ++ [e'] ++ e'_list ++ []) with + (map (fun (pat_:(e*T)) => match pat_ with (e_,T_) => e_ end ) + (combine (e_list ++ [e'] ++ e'_list ++[]) (map (fun pat_ : e * T => let (_, T_) := pat_ in T_) e_T_list))). + apply typ_func_expr. + * intros. + rewrite pat2_id in H8. + rewrite H3 in H8. + rewrite combine_snd in H8. + rewrite combine_app in H8... + apply in_app_iff in H8. + destruct H8. + -- apply subG_type with (G1:=G5); auto. + apply H2. + apply in_map_iff. + exists (e_, T_). + split; auto. + rewrite H3. + rewrite combine_app; auto. + { + eapply in_app_iff. + now left. + } + rewrite 2 app_length. + simpl. + rewrite H1. + reflexivity. + -- rewrite combine_app in H8; auto. + apply in_app_iff in H8. + destruct H8. + ++ inv H8;[|contradiction]. + inv H9. + apply H7. + ++ apply subG_type with (G1:=G5); auto. + apply H2. + apply in_map_iff. + exists (e_, T_). + split; auto. + rewrite H3. + rewrite combine_app; auto. + { + eapply in_app_iff. + right. + right. + rewrite app_nil_r in H8. + apply H8. + } + rewrite 2 app_length. + simpl. + rewrite H1. + reflexivity. + ++ rewrite app_nil_r. + apply H1. + -- auto. + -- rewrite app_nil_r. + simpl. + rewrite H1. + reflexivity. + -- rewrite 4 app_length. + simpl. + lia. + * rewrite combine_snd. + ++ apply G'extends. + apply H4. + ++ rewrite map_length. + rewrite H3. + rewrite 2 combine_app; auto. + ** repeat (rewrite app_length). + rewrite 3 combine_length. + simpl. + rewrite H, H1. + lia. + ** rewrite 2 app_length. + simpl. + rewrite H1. + reflexivity. + * rewrite app_nil_r. + rewrite combine_fst; auto. + rewrite map_length. + rewrite H3. + rewrite combine_length. + repeat (rewrite app_length). + rewrite H, H1. + simpl. + lia. + + - (* RED_FUN_GROUND *) + intros. + set (fn_def:=(F_fn T_5 fn5 (map (fun '(T_, x_, _, _) => (T_, x_)) T_x_t_y_list) e5)). + pose proof utils.in_split F_list F'_list fn_def . + rewrite app_nil_r in *. + pose proof Forall_forall (typ_F G5) (F_list ++ [fn_def] ++ F'_list) as (? & _). + pose proof H2 F_well_typed fn_def H1 as fn_typed. + inv fn_typed. + inv e0_type. + destruct H as ((?, ?), ?). + assert (e_T_list = map (fun '(T_, _, t_, _) => (e_t t_, T_)) T_x_t_y_list). + { + (* inv H11. *) + eapply map_split'. + - replace (map fst e_T_list) with (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list) by easy. + rewrite H4. + apply map_ext. + easy. + - replace (map snd e_T_list) with (map (fun pat_ : e * T => let (_, T_) := pat_ in T_) e_T_list) by easy. + rewrite H7 in H11. + inv H11. + rewrite map_map. + apply map_ext. + intros. + now destruct a as (((?, ?), ?), ?). + } + exists (fold_right (fun '(T_, _, _, y) G0 => Map.add y (ctxv_T T_) G0) G5 T_x_t_y_list). + splits. + + eapply fresh_subG; eauto. + + rewrite <- fold_map. + apply fresh_consistent; eauto. + intros. + apply in_map_iff in H12. + destruct H12 as (Txty, (?, ?)). + apply H6. + inv H12. + rewrite map_map. + apply in_map_iff. + exists Txty. + split; auto. + destruct Txty as (((?, ?), ?), ?). + now inv H15. + + + rewrite H7 in H11. + inv H11. + apply subst_lemma; auto. + * rewrite <- fold_map_reshuffle; eauto. + * rewrite map_xs in H10. + apply H10. +Qed. +End FunctionalMetatheory. diff --git a/theories/utils.v b/theories/utils.v new file mode 100644 index 0000000..5d4674f --- /dev/null +++ b/theories/utils.v @@ -0,0 +1,688 @@ +From Coq Require Import List + FSets.FMapFacts + Lia. + +Import ListNotations. + +Ltac splits := repeat split. +Ltac inv H :=inversion H ; subst; clear H. +Tactic Notation "intros*" := repeat intro. + +Ltac forward H := + match type of H with + | ?x -> _ => + let name := fresh in assert x as name; [| specialize (H name); clear name] + end. +Tactic Notation "forward" ident(H) := + forward H. + +Section ListLemmas. + Context {X Y: Type}. + + Lemma map_eq: forall (l: list X) (f g: X -> Y), + (forall x, f x = g x) -> + map f l = map g l. + Proof. + induction l; intros; auto. + simpl. + rewrite (H a). + erewrite (IHl); eauto. + Qed. + + Lemma map_split {Z W: Type}: forall (l: list (Z*X)) (l2: list (X*Y*Z*W)), + map fst l = map (fun '(_, _, z, _) => z) l2 -> + map snd l = map (fun '(x, _, _, _) => x) l2 -> + l = map (fun '(x, _, z,_) => (z, x)) l2. + Proof. + induction l; intros. + - inv H. + symmetry in H2. + apply map_eq_nil in H2. + now subst. + - destruct a. + destruct l2. + + inv H. + + destruct p as (((?, ?), ?), ?). + inv H. + inv H0. + rewrite (IHl l2); auto. + Qed. + + Lemma map_xs {Z W: Type}: forall (T_x_t_y_list: list (X*Y*Z*W)), + map (fun pat_ : X * Y => let (_, x_) := pat_ in x_) (map (fun '(T_, x_, _, _) => (T_, x_)) T_x_t_y_list) = + map (fun '(_, x, _, _) => x) T_x_t_y_list. + Proof. + induction T_x_t_y_list. + - easy. + - destruct a as (((?, ?), ?), ?). + simpl. + now rewrite IHT_x_t_y_list. + Qed. + + Lemma map_split' {Z Z' W: Type}: forall (l: list (Z'*X)) (l2: list (X*Y*Z*W)) (f: Z -> Z'), + map fst l = map (fun '(_, _, z, _) => f z) l2 -> + map snd l = map (fun '(x, _, _, _) => x) l2 -> + l = map (fun '(x, _, z,_) => (f z, x)) l2. + Proof. + induction l; intros. + - inv H. + symmetry in H2. + apply map_eq_nil in H2. + now subst. + - destruct a. + destruct l2. + + inv H. + + destruct p as (((?, ?), ?), ?). + inv H. + inv H0. + rewrite (IHl l2 f); auto. + Qed. + + Lemma combine_fst: forall (l1: list X) (l2: list Y), + length l1 = length l2 -> + map (fun pat_: (X*Y) => let (e_, _) := pat_ in e_) (combine l1 l2) = l1. + Proof. + induction l1;intros. + - easy. + - destruct l2. + + inv H. + + inv H. + simpl. + rewrite (IHl1 l2 H1). + reflexivity. + Qed. + + Lemma combine_nil: forall (l1: list X), + @combine X Y l1 [] = []. + Proof. destruct l1; easy. Qed. + + Lemma combine_snd: forall (l1: list X) (l2: list Y), + length l1 = length l2 -> + map (fun pat_: (X*Y) => let (_, e_) := pat_ in e_) (combine l1 l2) = l2. + Proof. + intros. + generalize dependent l1. + induction l2; intros. + - rewrite combine_nil. + auto. + - destruct l1. + + inv H. + + inv H. + simpl. + rewrite (IHl2 l1 H1). + reflexivity. + Qed. + + Lemma in_combine: forall (l1: list X) (l2: list Y) x y, + In (x,y) (combine l1 l2) -> In x l1 /\ In y l2. + Proof. + induction l1;intros. + - inv H. + - destruct l2. + + inv H. + + destruct H. + * inv H. + split; left; auto. + * destruct (IHl1 l2 x y H). + split; right; auto. + Qed. + + Lemma combine_app: forall (l1 l2: list X) (l1' l2': list Y), + length l1 = length l1' -> + length l2 = length l2' -> + combine (l1 ++ l2) (l1' ++ l2') = combine l1 l1' ++ combine l2 l2'. + Proof. + induction l1; intros. + - inv H. + symmetry in H2. + apply length_zero_iff_nil in H2. + rewrite H2. + easy. + - destruct l1'. + + inv H. + + inv H. + simpl. + rewrite IHl1; easy. + Qed. + + Lemma in_split: forall (l1 l2: list X) x, + In x (l1 ++ [x] ++ l2). + Proof. + induction l1; intros. + - left; auto. + - right. + apply IHl1. + Qed. + + Lemma in_combine_split: forall (l: list (X*Y)) l1 l1' l2 l2' x y, + length l1 = length l2 -> + l = combine (l1 ++ [x] ++ l1') (l2 ++ [y] ++ l2') -> + In (x, y) l. + Proof. + induction l; intros; subst. + - destruct l1, l2; easy. + - destruct a. + destruct l1,l2. + + inv H0. + left;auto. + + inv H. + + inv H. + + inv H. + right. + inv H0. + eapply IHl. + apply H2. + reflexivity. + Qed. + + Lemma in_fst_iff: forall (l : list (X*Y)) x, + (exists y, In (x, y) l) <-> In x (map (fun pat_ : X * Y => let (e_, _) := pat_ in e_) l). + Proof. + split; intros. + - induction l. + + destruct H. + inv H. + + destruct H as (?y & H). + inv H. + * left; auto. + * right. + apply IHl. + exists y; auto. + - induction l. + + inv H. + + destruct a as (?x & ?y). + inv H. + * exists y. + left;auto. + * destruct (IHl H0) as (?y & ?). + exists y0. + right. + apply H. + Qed. + + Lemma pat2_id: forall l: list (X*Y), + map (fun pat_ : X*Y => let (x_, y_) := pat_ in (x_,y_)) l = l. + Proof. + induction l;auto. + destruct a; cbn. + rewrite IHl. + reflexivity. + Qed. + + Lemma fold_map {A Z W: Type}: forall (f: W -> Z -> A -> A) (l: list (X*Y*Z*W)) a0, + fold_right (fun '(_, _, z, w) a => f w z a) a0 l = + fold_right (fun (xt : W * Z) a => f (fst xt) (snd xt) a) a0 + (map (fun pat_ : X*Y*Z*W => let (p, y_) := pat_ in let (p0, t_) := p in let (_, _) := p0 in (y_, t_)) l). + Proof. + induction l; intros; eauto. + destruct a as [[[? ?] ?] ?]. + simpl. + now rewrite IHl. + Qed. + + Lemma fold_map1 {A Z W: Type}: forall (f: W -> X -> A -> A) (l: list (X*Y*Z*W)) a0, + fold_right (fun '(z, _, _, w) a => f w z a) a0 l = + fold_right (fun '(z, w) a => f z w a) a0 + (map (fun '(z, _, _, w) => (w, z)) l). + Proof. + induction l; intros; eauto. + destruct a as [[[? ?] ?] ?]. + simpl. + now rewrite IHl. + Qed. + + Lemma fold_map2 {A Z W: Type}: forall (f: Y -> X -> A -> A) (l: list (X*Y*Z*W)) a0, + fold_right (fun '(z, w, _, _) a => f w z a) a0 l = + fold_right (fun '(z, w) a => f z w a) a0 + (map (fun '(z, w, _, _) => (w, z)) l). + Proof. + induction l; intros; eauto. + destruct a as [[[? ?] ?] ?]. + simpl. + now rewrite IHl. + Qed. + + Lemma fold_map3 {A Z W: Type}: forall (f: W -> Y -> A -> A) (l: list (X*Y*Z*W)) a0, + fold_right (fun '(_, z, _, w) a => f w z a) a0 l = + fold_right (fun '(z, w) a => f z w a) a0 + (map (fun '(_, z, _, w) => (w, z)) l). + Proof. + induction l; intros; eauto. + destruct a as [[[? ?] ?] ?]. + simpl. + now rewrite IHl. + Qed. + + Lemma combine_map: forall (l: list (X*Y)), + combine (map fst l) (map snd l) = l. + Proof. + induction l; auto. + destruct a; simpl. + rewrite IHl. + reflexivity. + Qed. + + Lemma split_corresponding_list: forall (l: list (X*Y)) left_list mid right_list, + map (fun '(x, _) => x) l = left_list ++ [mid] ++ right_list -> + exists left_list' mid' right_list', + length left_list = length left_list' + /\ length right_list = length right_list' + /\ l = combine (left_list ++ [mid] ++ right_list) (left_list' ++ [mid'] ++ right_list'). + Proof with auto. + induction l;intros. + - apply app_cons_not_nil in H. + contradiction. + - destruct a. + destruct left_list, right_list; + inv H. + + exists [], y, []. + apply map_eq_nil in H2. + rewrite H2. + splits... + + destruct (IHl [] x0 right_list H2) + as (left_list' & mid' & right_list' & ? & ? & ?). + exists [], y, (left_list' ++ [mid'] ++ right_list'). + splits... + * inv H. + symmetry in H4. + apply length_zero_iff_nil in H4. + rewrite H4. + rewrite 2 app_nil_l. + rewrite map_length. + rewrite combine_length. + rewrite 2 app_length. + simpl. + rewrite H0. + lia. + * simpl. + rewrite H1. + rewrite combine_fst. + { easy. } + rewrite app_nil_l. + rewrite 3 app_length. + rewrite <- H. + rewrite H0. + easy. + + destruct (IHl left_list mid [] H2) + as (left_list' & mid' & right_list' & ? & ? & ?). + exists (y::left_list'), mid', right_list'. + splits... + * inv H0. + simpl. + rewrite H. + easy. + * rewrite H1. + easy. + + destruct (IHl left_list mid (x1::right_list) H2) + as (left_list' & mid' & right_list' & ? & ? & ?). + exists (y::left_list'), mid', (right_list'). + splits... + * simpl. + rewrite H. + easy. + * rewrite H1. + easy. + Qed. + + (* I thought this would be useful, but turns out we usually need the length *) + Corollary split_corresponding_list_no_length: forall (l: list (X*Y)) left_list mid right_list, + map (fun '(x, _) => x) l = left_list ++ [mid] ++ right_list -> + exists left_list' mid' right_list', l = combine (left_list ++ [mid] ++ right_list) (left_list' ++ [mid'] ++ right_list'). + Proof. + intros. + destruct (split_corresponding_list _ _ _ _ H) + as (left_list' & mid' & right_list' & _ & _ & EQ). + exists left_list', mid', right_list'. + apply EQ. + Qed. + +End ListLemmas. + +Require Import FMapList OrderedTypeEx. +From ABS Require Import abs_defs. +From Equations Require Import Equations. + +Module MapFacts := FSets.FMapFacts.Facts Map. + + +(* some slightly ad-hoc equalities *) +Lemma subst_fst_commute: forall x0 x1 e_T_list, + map (fun x : e * T => let (e_, _) := let '(e_, T_) := x in (e_var_subst_one e_ x0 x1, T_) in e_) e_T_list = + (fix e_list_subst_one (es : list e) (x_ y_ : x) {struct es} : list e := + match es with + | [] => fun _ _ : x => [] + | e :: l => fun x_0 y_0 : x => e_var_subst_one e x_0 y_0 :: e_list_subst_one l x_0 y_0 + end x_ y_) (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list) x0 x1. +Proof. + induction e_T_list; auto. + destruct a. + simpl. + rewrite <- IHe_T_list. + reflexivity. +Qed. + +Lemma subst_snd_commutes: forall x0 s e_T_list, + map (fun pat_ : e * T => let (_, T_) := pat_ in T_) + (map (fun pat_ : e * T => let (e_, T_) := pat_ in (e_var_subst_one e_ x0 s, T_)) e_T_list) = + map (fun pat_ : e * T => let (_, T_) := pat_ in T_) e_T_list. +Proof. + intros. + induction e_T_list; auto. + destruct a;cbn in *. + now rewrite IHe_T_list. +Qed. + +(* Characterizing substitution *) + +Lemma subst_term: forall t sub, + e_var_subst (e_t t) sub = (e_t t). +Proof. + induction sub. + - trivial. + - destruct a. + simpl. + rewrite IHsub. + now simp e_var_subst_one. +Qed. + +Definition replace_var (x0:x) (sub:list(x*x)) := + fold_right (fun '(x_, y_) x0 => if (eq_x x0 x_) then y_ else x0) x0 sub. + +Lemma subst_var: forall x0 sub, + e_var_subst (e_var x0) sub = e_var (replace_var x0 sub). +Proof. + induction sub. + - trivial. + - destruct a; simpl. + rewrite IHsub. + simp e_var_subst_one. + destruct (eq_x (replace_var x0 sub)); subst; eauto. +Qed. + +Lemma e_list_subst_map: forall x0 y0 e_list, + e_list_subst_one e_list x0 y0 = map (fun e_ => e_var_subst_one e_ x0 y0) e_list. +Proof. + induction e_list; [easy|]; + destruct a; + simpl; + now rewrite IHe_list. +Qed. + +Lemma subst_fn: forall fn0 sub e_list, + e_var_subst (e_fn_call fn0 e_list) sub = (e_fn_call fn0 (map (fun e' => e_var_subst e' sub) e_list)). +Proof. + induction sub; intros. + - simpl. + now rewrite map_id. + - destruct a. + simpl. + rewrite IHsub. + simp e_var_subst_one. + now rewrite e_list_subst_map, map_map. +Qed. + +Lemma e_list_subst: forall el x0 y0, + e_list_subst_one el x0 y0 = map (fun e => e_var_subst_one e x0 y0) el. +Proof. + induction el; intros. + - trivial. + - simpl. + now rewrite IHel. +Qed. + +Lemma e_list_fresh: forall e0 ys el, + fresh_vars_el ys el -> + In e0 el -> + fresh_vars_e ys e0. +Proof. + induction el. + - easy. + - simpl; intros. + destruct H0; subst. + + now destruct H. + + destruct H. + apply IHel; eauto. +Qed. + +(* Properties of fresh_e*) +Lemma fresh_first_e: forall e0 y ys, + fresh_vars_e (y::ys) e0 -> fresh_vars_e [y] e0. +Proof. + induction e0 using e_ott_ind + with (P_list_e := fun e_list => + forall e0 y ys, + In e0 e_list -> + fresh_vars_e (y::ys) e0 -> fresh_vars_e [y] e0); + intros; try easy. + - simp fresh_vars_e in *. + intro. + inv H0. + + apply H. + now left. + + inv H1. + - simp fresh_vars_e in *. + induction e_list. + + easy. + + inv H. + split. + * eapply IHe0; eauto. + now left. + * eapply IHe_list; eauto. + intros; eapply IHe0; eauto. + now right. + - inv H. + + eapply IHe0; eauto. + + eapply IHe1; eauto. +Qed. + +Lemma fresh_monotone_e: forall e0 y ys, + fresh_vars_e (y::ys) e0 -> fresh_vars_e ys e0. +Proof. + induction e0 using e_ott_ind + with (P_list_e := fun e_list => + forall e0 y ys, + In e0 e_list -> + fresh_vars_e (y::ys) e0 -> fresh_vars_e ys e0); + intros; try easy. + - simp fresh_vars_e in *. + intro. + apply H. + right. + assumption. + - simp fresh_vars_e in *. + induction e_list. + + easy. + + inv H. + split. + * eapply IHe0; eauto. + now left. + * apply IHe_list; eauto. + intros; eapply IHe0; eauto. + now right. + - inv H. + + eapply IHe0; eauto. + + eapply IHe1; eauto. +Qed. + +Lemma fresh_first_el: forall el y ys, + fresh_vars_el (y::ys) el -> fresh_vars_el [y] el. +Proof. + induction el; intros. + - now inv H. + - inv H. + split. + + now apply fresh_first_e in H0. + + eapply IHel; eauto. +Qed. + +Lemma fresh_monotone_el: forall el y ys, + fresh_vars_el (y::ys) el -> fresh_vars_el ys el. +Proof. + induction el; intros. + - now inv H. + - inv H. + split. + + now apply fresh_monotone_e in H0. + + eapply IHel; eauto. +Qed. + +Lemma fresh_var_subst: forall e0 y sub, + fresh_vars_e (map snd sub) e0 -> + fresh_vars_e [y] e0 -> + ~ In y (map snd sub) -> + fresh_vars_e [y] (e_var_subst e0 sub). +Proof. + intros. + generalize dependent y. + generalize dependent e0. + induction e0 using e_ott_ind + with + (P_list_e := fun e_list => forall y, + fresh_vars_el (map snd sub) e_list -> + fresh_vars_el [y] e_list -> + ~ In y (map snd sub) -> + fresh_vars_el [y] (map (fun e' => e_var_subst e' sub) e_list)) + ; intros; auto. + - rewrite subst_term. + now simp e_var_subst_one. + - induction sub; auto. + destruct a as (?x_, ?y); simpl. + rewrite subst_var. + simp e_var_subst_one. + destruct (eq_x (replace_var x5 sub) x_). + + simp fresh_vars_e. + intro. + apply H1. + left. + now inv H2. + + rewrite <- subst_var. + apply Decidable.not_or in H1. + destruct H1. + apply fresh_monotone_e in H. + eapply IHsub; auto. + - rewrite subst_fn. + simp fresh_vars_e in *. + - destruct H,H0. + split. + + apply IHe0; auto. + + apply IHe1; eauto. +Qed. + +Fact disjoint_empty{A:Type}: @disjoint A [] []. +Proof. easy. Qed. + +Lemma disjoint_monotone {A:Type}: forall (l1 l2: list A) a1 a2, + disjoint (a1::l1) (a2::l2) -> disjoint l1 l2. +Proof. + intros. + intros ? ? ?. + specialize (H a). + apply H; now right. +Qed. + +Section MapLemmas. + + Lemma map_neq_none_is_some{elt:Type}: forall m x, + Map.find x m <> None -> + exists y, Map.find (elt:=elt) x m = Some y. + Proof. + intros. + destruct (MapFacts.In_dec m x). + - inv i. + exists x0. + apply Map.find_1. + apply H0. + - apply MapFacts.not_find_in_iff in n. + rewrite n in H. + contradiction. + Qed. + + Lemma fold_map_reshuffle: forall (l: list (T*x*t*x)) G0, + (fold_right (fun (ax : x * T) (G' : G) => Map.add (fst ax) (ctxv_T (snd ax)) G') G0 + (map (fun pat_ : T * x => let (T_, x_) := pat_ in (x_, T_)) (map (fun '(T_0, x_, _, _) => (T_0, x_)) l))) + = (fold_right (fun '(T1, x_, _, _) (G' : G) => Map.add x_ (ctxv_T T1) G') G0 l). + Proof. + induction l;intros;auto. + destruct a as (((?T_ & ?x_) & ?t_) & ?y). + simpl. + rewrite IHl. + reflexivity. + Qed. + + Lemma map_add_comm{E:Type}: forall m key key' elt elt', + key <> key' -> Map.Equal (Map.add (elt:=E) key elt (Map.add key' elt' m)) (Map.add key' elt' (Map.add key elt m)). + Proof. + intros. + intro. + destruct (Map.find y m) eqn:?. + - destruct (eq_x y key), (eq_x y key'); subst; + erewrite 2 Map.find_1; eauto; + (* this should just be "eauto with map", but I can't seem to import the hint database *) + try (apply Map.add_2; eauto; now apply Map.add_1); + try (now apply Map.add_1; eauto); + try (repeat (apply Map.add_2; eauto); now apply Map.find_2; eauto). + - destruct (eq_x y key), (eq_x y key'); subst. + + contradiction. + + erewrite 2 Map.find_1; eauto. + * apply Map.add_2; eauto. + now apply Map.add_1. + * now apply Map.add_1. + + erewrite 2 Map.find_1; eauto. + * now apply Map.add_1. + * apply Map.add_2; eauto. + now apply Map.add_1. + + (* there has to be a cleaner way to do this case?? *) + + replace (Map.find (elt:=E) y (Map.add key elt (Map.add key' elt' m))) with (@None E). + replace (Map.find (elt:=E) y (Map.add key' elt' (Map.add key elt m))) with (@None E). + reflexivity. + * symmetry. + apply MapFacts.not_find_in_iff in Heqo. + apply MapFacts.not_find_in_iff. + intro. + apply Heqo. + inv H0. + exists x. + apply Map.add_3 with (x:= key) (e':=elt); auto. + apply Map.add_3 with (x:=key') (e':=elt'); auto. + * symmetry. + apply MapFacts.not_find_in_iff in Heqo. + apply MapFacts.not_find_in_iff. + intro. + inv H0. + apply Heqo. + exists x. + apply Map.add_3 with (x:=key') (e':=elt'); auto. + apply Map.add_3 with (x:= key) (e':=elt); auto. + Qed. + + Lemma fold_not_in: forall G0 y (T_x_t_y_list: list (T*x*t*x)), + ~ Map.In y G0 -> + ~ In y (map (fun '(_, _, _, y') => y') T_x_t_y_list) -> + ~ Map.In y (fold_right (fun '(T_, _, _, y) (G0 : G) => Map.add y (ctxv_T T_) G0) G0 T_x_t_y_list). + Proof. + induction T_x_t_y_list as [ | (((?T_, ?x_), ?t_), ?y) T_x_t_y_list IH ]; [easy|]. + simpl; intros ? ? ?. + destruct (eq_x y y0); subst. + - apply H0. + now left. + - apply MapFacts.add_in_iff in H1. + inv H1. + + apply H0. + now left. + + apply IH; eauto. + Qed. + + Lemma fold_add_comm: forall G0 y T_ (upd: list (T*x)), + ~ In y (map (fun '(_, y) => y) upd) -> + Map.Equal (Map.add y (ctxv_T T_) (fold_right (fun '(T_, y) G0 => Map.add y (ctxv_T T_) G0) G0 upd)) + (fold_right (fun '(T_, y) G0 => Map.add y (ctxv_T T_) G0) (Map.add y (ctxv_T T_) G0) upd). + Proof. + induction upd; intros. + - easy. + - destruct a; simpl in *. + apply Decidable.not_or in H. + destruct H. + now rewrite map_add_comm, IHupd; auto. + Qed. +End MapLemmas.