From 60c31282930ab8815c8a9d72b1219cd6c5eff7b0 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 30 Jan 2024 10:37:47 +0100 Subject: [PATCH 01/18] All but the function base case. very much WIP --- src/abs.ott | 17 +- theories/abs_defs.v | 11 +- theories/abs_functional_metatheory.v | 404 ++++++++++++++++++++++++++- 3 files changed, 426 insertions(+), 6 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index 35d0211..f30b71a 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -108,8 +108,12 @@ 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 + | 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]]) }} embed {{ coq @@ -142,6 +146,15 @@ 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. }} defns @@ -193,6 +206,6 @@ 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 ) + fresh ( y1 , ... , yn , e , s) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- :: 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..da097cc 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -130,6 +130,15 @@ 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. + (** definitions *) (* defns expression_well_typing *) @@ -164,7 +173,7 @@ 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 ) -> + (fresh_vars (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) e5 s5 ) -> 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_functional_metatheory.v b/theories/abs_functional_metatheory.v index 7bf5619..d8a671a 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -1,26 +1,424 @@ From ABS Require Import abs_defs. -From Coq Require Import List. +From Coq Require Import List + FSets.FMapFacts + Lia. + +Module MapFacts := FSets.FMapFacts.Facts Map. Import ListNotations. (** * ABS Functional Metatheory *) +Notation "G ⊢ e : T" := (typ_e G e T) (at level 5). +Notation "G F⊢ F" := (typ_F G F) (at level 5). +(* Notation "Fs , s ⊢ e ⇝ s' ⊢ e'" := (red_e Fs s e s' e') (at level 10). *) + Definition subG (G1 G2 : G) : Prop := forall (key : string) (elt : ctxv), Map.find key G1 = Some elt -> Map.find key G2 = Some elt. +Notation "G1 ⊆ G2" := (subG G1 G2) (at level 5). + Definition G_vdash_s (G5 : G) (s5 : s) := forall (x5 : x) (t5 : t) (T5 : T), Map.find x5 s5 = Some t5 -> Map.find x5 G5 = Some (ctxv_T T5) -> typ_e G5 (e_t t5) T5. +Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). + +Ltac splits := repeat split. +Ltac inv H :=inversion H ; subst; clear H. +Tactic Notation "intros*" := repeat intro. + +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_ T_ ? ?. + apply H in H2. + pose proof H0 x_ t_ T_ H1 H2. + inv H3;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. + +(* extremely tedious stuff *) +Lemma subst_fst_commutes: forall x0 s e_T_list, + map (fun pat_ : e * T => let (e_, _) := pat_ in e_) + (map (fun pat_ : e * T => let (e_, T_) := pat_ in (e_var_subst e_ [(x0, s)], T_)) e_T_list) = + map (fun e : e => e_var_subst e [(x0, s)]) (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list). +Proof with auto. + induction e_T_list... + destruct a;cbn. + rewrite IHe_T_list... +Qed. + +Lemma combine_fst {X Y: Type} : 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 {X Y: Type} : forall (l1: list X), + @combine X Y l1 [] = []. +Proof. destruct l1; easy. Qed. + +Lemma combine_snd {X Y: Type} : 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 {X Y: Type} : 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 {X Y: Type}: 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_combine_app{X Y:Type}: 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 {X Y: Type} : 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 {X Y: Type}: 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 combine_map {X Y: Type}: 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 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 e_var_subst_empty: forall e0, e_var_subst e0 [] = e0. +Proof. + eapply e_ott_ind with + (P_list_e:= fun es => map (fun e0 => e_var_subst e0 []) es = es);simpl;intros;auto. + { rewrite H. auto. } + induction e_l. + - rewrite H. + reflexivity. + - inv H0. + simpl. + rewrite H. + rewrite 2 H2. + rewrite 2 H3. + reflexivity. +Qed. + +Lemma split_corresponding_list_aux {X Y: Type}: 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. + +Corollary split_corresponding_list {X Y: Type}: 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_aux _ _ _ _ H) + as (left_list' & mid' & right_list' & _ & _ & EQ). + exists left_list', mid', right_list'. + apply EQ. +Qed. + 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. +Proof with try easy. + 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... + inv e0_type. + apply (s_well_typed _ _ _ H H2). + + - (* RED_FUN_EXPR *) + intros. + inv e0_type. + rewrite app_nil_r in H0. + pose proof split_corresponding_list_aux 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... + apply in_combine_app with (2:=eq_refl)... + } + 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... + 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))). + (* by apply combine_fst. *) + 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)... + apply H2. + apply in_map_iff. + exists (e_, T_). + split... + rewrite H3. + rewrite combine_app... { + eapply in_app_iff. + left... + } + rewrite 2 app_length. + simpl. + rewrite H1. + reflexivity. + -- rewrite combine_app in H8... + apply in_app_iff in H8. + destruct H8. + ++ inv H8;[|contradiction]. + inv H9. + apply H7. + ++ apply subG_type with (G1:=G5)... + apply H2. + apply in_map_iff. + exists (e_, T_). + split... + rewrite H3. + rewrite combine_app... { + 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. + -- 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... + ** 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... + rewrite map_length. + rewrite H3. + rewrite combine_length. + repeat (rewrite app_length). + rewrite H, H1. + simpl. + lia. + + - (* RED_FUN_CALL *) + admit. Admitted. From bf7d5d74fff44fa3dd56ac59570f29f1d15a3af4 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Wed, 31 Jan 2024 14:49:49 +0100 Subject: [PATCH 02/18] Factoring out list utilities --- _CoqProject | 1 + theories/abs_functional_metatheory.v | 218 +-------------------------- theories/utils.v | 217 ++++++++++++++++++++++++++ 3 files changed, 224 insertions(+), 212 deletions(-) create mode 100644 theories/utils.v diff --git a/_CoqProject b/_CoqProject index 3e6d0d6..0edf932 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,3 +4,4 @@ theories/abs_defs.v theories/abs_functional_metatheory.v +theories/utils.v diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index d8a671a..2226112 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -1,4 +1,6 @@ -From ABS Require Import abs_defs. +From ABS Require Import abs_defs + utils. + From Coq Require Import List FSets.FMapFacts Lia. @@ -27,10 +29,6 @@ Definition G_vdash_s (G5 : G) (s5 : s) := Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). -Ltac splits := repeat split. -Ltac inv H :=inversion H ; subst; clear H. -Tactic Notation "intros*" := repeat intro. - Lemma subG_consistent: forall G1 G2 s0, subG G1 G2 -> G_vdash_s G2 s0 -> G_vdash_s G1 s0. Proof. @@ -58,148 +56,18 @@ Proof. apply H2. Qed. -(* extremely tedious stuff *) +(* some slightly ad-hoc equalities *) Lemma subst_fst_commutes: forall x0 s e_T_list, map (fun pat_ : e * T => let (e_, _) := pat_ in e_) (map (fun pat_ : e * T => let (e_, T_) := pat_ in (e_var_subst e_ [(x0, s)], T_)) e_T_list) = map (fun e : e => e_var_subst e [(x0, s)]) (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list). Proof with auto. + intros. induction e_T_list... destruct a;cbn. rewrite IHe_T_list... Qed. -Lemma combine_fst {X Y: Type} : 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 {X Y: Type} : forall (l1: list X), - @combine X Y l1 [] = []. -Proof. destruct l1; easy. Qed. - -Lemma combine_snd {X Y: Type} : 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 {X Y: Type} : 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 {X Y: Type}: 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_combine_app{X Y:Type}: 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 {X Y: Type} : 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 {X Y: Type}: 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 combine_map {X Y: Type}: 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 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))) @@ -228,79 +96,6 @@ Proof. reflexivity. Qed. -Lemma split_corresponding_list_aux {X Y: Type}: 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. - -Corollary split_corresponding_list {X Y: Type}: 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_aux _ _ _ _ H) - as (left_list' & mid' & right_list' & _ & _ & EQ). - exists left_list', mid', right_list'. - apply EQ. -Qed. - Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), G_vdash_s G5 s5 -> Forall (typ_F G5) Flist -> @@ -323,7 +118,7 @@ Proof with try easy. intros. inv e0_type. rewrite app_nil_r in H0. - pose proof split_corresponding_list_aux e_T_list e_list e_5 e'_list 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. @@ -339,7 +134,6 @@ Proof with try 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))). - (* by apply combine_fst. *) apply typ_func_expr... * intros. rewrite pat2_id in H8. diff --git a/theories/utils.v b/theories/utils.v new file mode 100644 index 0000000..bf34fb6 --- /dev/null +++ b/theories/utils.v @@ -0,0 +1,217 @@ +From Coq Require Import List + Lia. + +Import ListNotations. + +Ltac splits := repeat split. +Ltac inv H :=inversion H ; subst; clear H. +Tactic Notation "intros*" := repeat intro. + +Section ListLemmas. + Context {X Y: Type}. + + 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_combine_app: 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 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. From bc697596962616161ea346db73f1b02ebced1e4f Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 6 Feb 2024 19:45:37 +0100 Subject: [PATCH 03/18] Some cleanup and minor progress --- src/abs.ott | 34 +++---- theories/abs_defs.v | 34 +++---- theories/abs_functional_metatheory.v | 140 +++++++++++++++++++++++---- theories/utils.v | 21 +++- 4 files changed, 168 insertions(+), 61 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index f30b71a..384ed91 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -117,27 +117,19 @@ formula :: formula_ ::= 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. +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_ +}. + +(* I would prefer not doing this, but sometimes I need it to compute *) +Global Transparent e_var_subst_one. + +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; diff --git a/theories/abs_defs.v b/theories/abs_defs.v index da097cc..d643636 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -100,27 +100,19 @@ 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. +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_ +}. + +(* I would prefer not doing this, but sometimes I need it to compute *) +Global Transparent e_var_subst_one. + +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; diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index 2226112..d25cd25 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -10,6 +10,10 @@ Import ListNotations. (** * ABS Functional Metatheory *) +Section FunctionalMetatheory. + +Hypothesis (vars_fs_distinct: forall (x_:x) (fn_:fn), x_ <> fn_). + Notation "G ⊢ e : T" := (typ_e G e T) (at level 5). Notation "G F⊢ F" := (typ_F G F) (at level 5). (* Notation "Fs , s ⊢ e ⇝ s' ⊢ e'" := (red_e Fs s e s' e') (at level 10). *) @@ -27,6 +31,14 @@ Definition G_vdash_s (G5 : G) (s5 : s) := Map.find x5 G5 = Some (ctxv_T T5) -> typ_e G5 (e_t t5) T5. +(* sanity check *) +Lemma empty_G_consistent: forall s0, + G_vdash_s (Map.empty ctxv) s0. +Proof. + intros*. + inv H0. +Qed. + Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). Lemma subG_consistent: forall G1 G2 s0, @@ -57,14 +69,29 @@ Proof. Qed. (* some slightly ad-hoc equalities *) -Lemma subst_fst_commutes: forall x0 s e_T_list, - map (fun pat_ : e * T => let (e_, _) := pat_ in e_) - (map (fun pat_ : e * T => let (e_, T_) := pat_ in (e_var_subst e_ [(x0, s)], T_)) e_T_list) = - map (fun e : e => e_var_subst e [(x0, s)]) (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list). +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 with auto. intros. induction e_T_list... - destruct a;cbn. + destruct a;cbn in *. rewrite IHe_T_list... Qed. @@ -80,20 +107,73 @@ Proof. reflexivity. Qed. -Lemma e_var_subst_empty: forall e0, e_var_subst e0 [] = e0. +(* this is 9.3.8 from Types and Programming Languages *) +(* it has not yet proven useful *) +Lemma subst_lemma_aux: 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 - (P_list_e:= fun es => map (fun e0 => e_var_subst e0 []) es = es);simpl;intros;auto. - { rewrite H. auto. } - induction e_l. - - rewrite H. - reflexivity. - - inv H0. + (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; constructor. + - inv H. simpl. - rewrite H. - rewrite 2 H2. - rewrite 2 H3. - reflexivity. + 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. + 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 type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), @@ -125,7 +205,7 @@ Proof with try easy. apply in_map_iff. exists (e_5, T_5). split... - apply in_combine_app with (2:=eq_refl)... + apply in_combine_split with (2:=eq_refl)... } pose proof H2 e_5 T_5 H5. destruct (IHreduction G5 s_well_typed F_well_typed _ H6) as (G' & G'extends & G'consistent & ?). @@ -214,5 +294,29 @@ Proof with try easy. lia. - (* RED_FUN_CALL *) - admit. + 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 H1 F_well_typed fn_def H0 as fn_typed. + inv e0_type. + inv fn_typed. + rewrite H8 in H7. + inv H7. + assert (map (fun '(_,T_) => T_) e_T_list = map (fun '(T_, _, _, _) => T_) T_x_t_y_list). { + rewrite <- H4. + rewrite map_map. + apply map_eq. + intros [[[? ?] ?] ?]. + reflexivity. + } + clear H4. + set (G':=(fold_right (fun '(T_, _, _, y) G0 => Map.add y (ctxv_T T_) G0) G5 T_x_t_y_list)). + exists G'. + splits. + + admit. + + admit. + + admit. Admitted. +End FunctionalMetatheory. diff --git a/theories/utils.v b/theories/utils.v index bf34fb6..acfd687 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -10,6 +10,16 @@ Tactic Notation "intros*" := repeat intro. 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 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. @@ -77,7 +87,16 @@ Section ListLemmas. rewrite IHl1; easy. Qed. - Lemma in_combine_app: forall (l: list (X*Y)) l1 l1' l2 l2' x y, + 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. From 934ac816eeb829e2f65f36f8812747d4fb9c6ee3 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Mon, 12 Feb 2024 15:58:12 +0100 Subject: [PATCH 04/18] Some reorganizing, but not much progress --- theories/abs_functional_metatheory.v | 79 +++++++++++++++++++++------- theories/utils.v | 12 +++++ 2 files changed, 73 insertions(+), 18 deletions(-) diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index d25cd25..1bfe231 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -41,6 +41,24 @@ Qed. Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). +(* the proof in the original ABS paper appeals to the following two properties in the RED_FUN_GROUND case*) +(* however, I am not sure either holds without some extra assumptions *) +(* (in particular uniqueness of the substituted variables and freshness wrt the typing context) *) +Lemma fresh_subG: forall G0 s0 (sub_list: list (T*x*t*x)), + (* this should really be fresh wrt G0, but we don't actually have that so maybe these suffice? *) + G_vdash_s G0 s0 -> + fresh_vars_s (map (fun '(_,_,_,y)=>y) sub_list) s0 -> + subG G0 (fold_right (fun '(T_,_,_,y_) G0 => Map.add y_ (ctxv_T T_) G0) G0 sub_list). +Admitted. + +Lemma fresh_consistent: 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 -> + 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. +Admitted. + Lemma subG_consistent: forall G1 G2 s0, subG G1 G2 -> G_vdash_s G2 s0 -> G_vdash_s G1 s0. Proof. @@ -109,7 +127,7 @@ Qed. (* this is 9.3.8 from Types and Programming Languages *) (* it has not yet proven useful *) -Lemma subst_lemma_aux: forall (x0 x1:x) G0 e0 T0 T1, +Lemma subst_lemma_one: 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. @@ -176,6 +194,39 @@ Proof. + eapply H0; eauto. Qed. +Lemma subst_lemma: forall G0 e0 T0 (sub_list: list (T*x*t*x)), + (* idea: some wellformedness condition that ensures the two admits *) + typ_e (fold_right (fun '(T1, x0, _, _) G' => Map.add x0 (ctxv_T T1) G') G0 sub_list) e0 T0 -> + (forall x1 T1, + In (T1, x1) (map (fun '(T1, _, _, x1) => (T1, x1)) sub_list) -> + typ_e G0 (e_var x1) T1) -> + typ_e G0 (e_var_subst e0 (map (fun '(_, x0, _, x1) => (x0, x1)) sub_list)) T0. +Proof. + intros. + generalize dependent G0. + induction sub_list; intros; auto. + destruct a as (((?T_&?x_)&?t_)&?y_). + simpl. + replace ((T_, x_, t_, y_) :: sub_list) with (sub_list ++ [(T_, x_, t_, y_)]) + in H by admit. + (* if all the x0s are unique, then order does not matter *) + setoid_rewrite fold_right_app in H. + eapply subst_lemma_one. + - eapply IHsub_list; eauto. + intros. + assert (In (T1, x1) (map (fun '(T2, _, _, x2) => (T2, x2)) ((T_, x_, t_, y_)::sub_list))). + {right; auto. } + pose proof H0 x1 T1 H2. + inv H3. + constructor. + apply Map.find_1. + apply Map.add_2. + { admit. } (* not sure how to get rid of this *) + apply Map.find_2 in H6; auto. + - apply H0. + left; eauto. +Admitted. + Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), G_vdash_s G5 s5 -> Forall (typ_F G5) Flist -> @@ -293,30 +344,22 @@ Proof with try easy. simpl. lia. - - (* RED_FUN_CALL *) + - (* 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 H1 F_well_typed fn_def H0 as fn_typed. - inv e0_type. inv fn_typed. - rewrite H8 in H7. - inv H7. - assert (map (fun '(_,T_) => T_) e_T_list = map (fun '(T_, _, _, _) => T_) T_x_t_y_list). { - rewrite <- H4. - rewrite map_map. - apply map_eq. - intros [[[? ?] ?] ?]. - reflexivity. - } - clear H4. - set (G':=(fold_right (fun '(T_, _, _, y) G0 => Map.add y (ctxv_T T_) G0) G5 T_x_t_y_list)). - exists G'. + inv e0_type. + exists (fold_right (fun '(T_, _, _, y) G0 => Map.add y (ctxv_T T_) G0) G5 T_x_t_y_list). splits. - + admit. - + admit. - + admit. + + eapply fresh_subG; eauto. + apply H. + + rewrite <- fold_map. + apply fresh_consistent; eauto. + apply H. + + (* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) Admitted. End FunctionalMetatheory. diff --git a/theories/utils.v b/theories/utils.v index acfd687..74bbd17 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -151,6 +151,17 @@ Section ListLemmas. 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 combine_map: forall (l: list (X*Y)), combine (map fst l) (map snd l) = l. Proof. @@ -233,4 +244,5 @@ Section ListLemmas. exists left_list', mid', right_list'. apply EQ. Qed. + End ListLemmas. From dce8f1bb03dcd29e6f79d3583a80b2b302184711 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Mon, 19 Feb 2024 20:34:37 +0100 Subject: [PATCH 05/18] Almost there with type preservation, tho still missing the actual type (substitution lemma) --- src/abs.ott | 13 +- theories/abs_defs.v | 11 +- theories/abs_functional_metatheory.v | 231 ++++++++++++++++++++------- theories/utils.v | 39 +++++ 4 files changed, 235 insertions(+), 59 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index 384ed91..e09ac85 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -114,6 +114,8 @@ formula :: formula_ ::= {{ coq (fresh_vars_s [[x1 ... xn]] [[s]]) }} | fresh ( x1 , ... , xn , e , s ) :: M :: fresh {{ coq (fresh_vars [[x1 ... xn]] [[e]] [[s]]) }} + | well_formed ( x1 , ... , xn , e , s ) :: M :: well_formed + {{ coq (well_formed [[e]] [[s]] [[x1 ... xn]]) }} embed {{ coq @@ -147,6 +149,15 @@ Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := fresh_vars_s l s0 /\ fresh_vars_e l e0. + +Inductive distinct: list x -> Prop := + | distinct_nil: distinct nil + | distinct_cons: forall y ys, + ~ In y ys -> + distinct ys -> + distinct (y::ys). + +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l. }} defns @@ -198,6 +209,6 @@ 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 , s) + well_formed (y1 , ... , yn , e, s) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- :: 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 d643636..c90d835 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -131,6 +131,15 @@ Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := fresh_vars_s l s0 /\ fresh_vars_e l e0. +Inductive distinct: list x -> Prop := + | distinct_nil: distinct nil + | distinct_cons: forall y ys, + ~ In y ys -> + distinct ys -> + distinct (y::ys). + +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l. + (** definitions *) (* defns expression_well_typing *) @@ -165,7 +174,7 @@ 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 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) e5 s5 ) -> + (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) ) -> 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_functional_metatheory.v b/theories/abs_functional_metatheory.v index 1bfe231..e461816 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -13,6 +13,9 @@ Import ListNotations. 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_). Notation "G ⊢ e : T" := (typ_e G e T) (at level 5). Notation "G F⊢ F" := (typ_F G F) (at level 5). @@ -25,48 +28,150 @@ Definition subG (G1 G2 : G) : Prop := Notation "G1 ⊆ G2" := (subG G1 G2) (at level 5). -Definition G_vdash_s (G5 : G) (s5 : s) := - forall (x5 : x) (t5 : t) (T5 : T), - Map.find x5 s5 = Some t5 -> - Map.find x5 G5 = Some (ctxv_T T5) -> - typ_e G5 (e_t t5) T5. +Lemma subG_refl: forall G0, + subG G0 G0. +Proof. easy. Qed. -(* sanity check *) -Lemma empty_G_consistent: forall s0, - G_vdash_s (Map.empty ctxv) s0. +Lemma subG_add: forall G0 G1 y T_, + subG G0 G1 -> + ~ Map.In y G0 -> + subG G0 (Map.add y T_ G1). Proof. - intros*. - inv H0. + 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. +(* 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), + Map.find x5 G5 = Some (ctxv_T 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). -(* the proof in the original ABS paper appeals to the following two properties in the RED_FUN_GROUND case*) -(* however, I am not sure either holds without some extra assumptions *) -(* (in particular uniqueness of the substituted variables and freshness wrt the typing context) *) +(* how is this not in MapFacts? *) +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 fresh_subG: forall G0 s0 (sub_list: list (T*x*t*x)), - (* this should really be fresh wrt G0, but we don't actually have that so maybe these suffice? *) G_vdash_s G0 s0 -> fresh_vars_s (map (fun '(_,_,_,y)=>y) sub_list) s0 -> + distinct (map (fun '(_,_,_,y)=>y) sub_list) -> subG G0 (fold_right (fun '(T_,_,_,y_) G0 => Map.add y_ (ctxv_T T_) G0) G0 sub_list). -Admitted. +Proof with try easy. + intros. + induction sub_list... + 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 -> + distinct (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. -Admitted. +Proof with try easy. + intros. + induction sub_list... + 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_ T_ ? ?. - apply H in H2. - pose proof H0 x_ t_ T_ H1 H2. - inv H3;constructor. + 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, @@ -194,37 +299,12 @@ Proof. + eapply H0; eauto. Qed. -Lemma subst_lemma: forall G0 e0 T0 (sub_list: list (T*x*t*x)), - (* idea: some wellformedness condition that ensures the two admits *) - typ_e (fold_right (fun '(T1, x0, _, _) G' => Map.add x0 (ctxv_T T1) G') G0 sub_list) e0 T0 -> - (forall x1 T1, - In (T1, x1) (map (fun '(T1, _, _, x1) => (T1, x1)) sub_list) -> - typ_e G0 (e_var x1) T1) -> - typ_e G0 (e_var_subst e0 (map (fun '(_, x0, _, x1) => (x0, x1)) sub_list)) T0. -Proof. - intros. - generalize dependent G0. - induction sub_list; intros; auto. - destruct a as (((?T_&?x_)&?t_)&?y_). - simpl. - replace ((T_, x_, t_, y_) :: sub_list) with (sub_list ++ [(T_, x_, t_, y_)]) - in H by admit. - (* if all the x0s are unique, then order does not matter *) - setoid_rewrite fold_right_app in H. - eapply subst_lemma_one. - - eapply IHsub_list; eauto. - intros. - assert (In (T1, x1) (map (fun '(T2, _, _, x2) => (T2, x2)) ((T_, x_, t_, y_)::sub_list))). - {right; auto. } - pose proof H0 x1 T1 H2. - inv H3. - constructor. - apply Map.find_1. - apply Map.add_2. - { admit. } (* not sure how to get rid of this *) - apply Map.find_2 in H6; auto. - - apply H0. - left; eauto. +(* pipe dream: might need some stronger assumptions*) +Lemma subst_lemma: forall (T_x_t_y_list:list (T*x*t*x)) G0 e0 T0, + typ_e (fold_right (fun '(T_, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T T_) G0) G0 T_x_t_y_list) e0 T0 -> + typ_e (fold_right (fun '(T_, _, _, y) (G0 : G) => Map.add y (ctxv_T T_) G0) G0 T_x_t_y_list) + (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) + T0. Admitted. Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), @@ -243,7 +323,10 @@ Proof with try easy. - intros. exists G5; splits... inv e0_type. - apply (s_well_typed _ _ _ H H2). + destruct (s_well_typed x5 T0 H2) as (?, (?, ?)). + rewrite H in H0. + inv H0. + assumption. - (* RED_FUN_EXPR *) intros. @@ -353,13 +436,47 @@ Proof with try easy. pose proof H1 F_well_typed fn_def H0 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). + { + rewrite H5 in H9. + inv H9. + 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 H3. + 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 <- H10. + 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. - apply H. + rewrite <- fold_map. apply fresh_consistent; eauto. - apply H. - + (* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) -Admitted. + (* some slightly silly reshuffling *) + intros. + apply in_map_iff in H10. + destruct H10 as (Txty, (?, ?)). + apply H6. + rewrite H7. + rewrite map_map. + apply in_map_iff. + exists Txty. + split... + destruct Txty as (((?, ?), ?), ?). + now inv H10. + +(* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) + + rewrite H5 in H9. + inv H9. + apply subst_lemma. + rewrite <- fold_map_reshuffle. + apply H8. +Qed. + End FunctionalMetatheory. diff --git a/theories/utils.v b/theories/utils.v index 74bbd17..1264f3b 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -20,6 +20,45 @@ Section ListLemmas. 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. + + (* extremely ad-hoc*) + 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. From 61215409b59ab0c427e24a0366df242f937484ae Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Tue, 20 Feb 2024 13:13:39 +0100 Subject: [PATCH 06/18] add coq-stdpp as dependency, add abs_examples module --- README.md | 3 ++- _CoqProject | 1 + coq-abs-metatheory.opam | 1 + meta.yml | 8 ++++++-- theories/abs_examples.v | 22 ++++++++++++++++++++++ 5 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 theories/abs_examples.v diff --git a/README.md b/README.md index e5302f2..6651ce7 100644 --- a/README.md +++ b/README.md @@ -23,6 +23,7 @@ Formal metatheory in Coq for the ABS language. - Additional dependencies: - [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later - [Equations Coq library](https://github.com/mattam82/Coq-Equations) 1.3 or later + - [Coq-Std++](https://gitlab.mpi-sws.org/iris/stdpp) 1.9.0 or later - Coq namespace: `ABS` - Related publication(s): - [ABS: A Core Language for Abstract Behavioral Specification](https://link.springer.com/chapter/10.1007/978-3-642-25271-6_8) doi:[10.1007/978-3-642-25271-6_8](https://doi.org/10.1007/978-3-642-25271-6_8) @@ -33,7 +34,7 @@ To install all dependencies, do: ```shell opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq.8.18.0 coq-ott +opam install coq.8.18.0 coq-ott coq-equations coq-stdpp ``` To build when dependencies are installed, do: diff --git a/_CoqProject b/_CoqProject index 3e6d0d6..62c7654 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3,4 +3,5 @@ -arg -w -arg -deprecated-hint-without-locality theories/abs_defs.v +theories/abs_examples.v theories/abs_functional_metatheory.v diff --git a/coq-abs-metatheory.opam b/coq-abs-metatheory.opam index 5168bf6..903e6b3 100644 --- a/coq-abs-metatheory.opam +++ b/coq-abs-metatheory.opam @@ -20,6 +20,7 @@ depends: [ "coq" {>= "8.16"} "coq-ott" {>= "0.33"} "coq-equations" {>= "1.3"} + "coq-stdpp" {>= "1.9.0"} ] tags: [ diff --git a/meta.yml b/meta.yml index 45c5eac..4661988 100644 --- a/meta.yml +++ b/meta.yml @@ -33,12 +33,16 @@ dependencies: version: '{>= "0.33"}' description: |- [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later - - opam: name: coq-equations version: '{>= "1.3"}' description: |- [Equations Coq library](https://github.com/mattam82/Coq-Equations) 1.3 or later +- opam: + name: coq-stdpp + version: '{>= "1.9.0"}' + description: |- + [Coq-Std++](https://gitlab.mpi-sws.org/iris/stdpp) 1.9.0 or later tested_coq_opam_versions: - version: '8.18' @@ -60,7 +64,7 @@ build: |- ```shell opam repo add coq-released https://coq.inria.fr/opam/released - opam install coq.8.18.0 coq-ott + opam install coq.8.18.0 coq-ott coq-equations coq-stdpp ``` To build when dependencies are installed, do: diff --git a/theories/abs_examples.v b/theories/abs_examples.v new file mode 100644 index 0000000..af0c048 --- /dev/null +++ b/theories/abs_examples.v @@ -0,0 +1,22 @@ +From ABS Require Import abs_defs. +From stdpp Require Import prelude. + +(** * ABS Examples *) + +Definition e_const_5 : e := + e_t (t_int 5%Z). + +Definition func_const_5 : F := + F_fn T_int "const_5"%string [] e_const_5. + +Definition e_call_const_5 : e := + e_fn_call "const_5"%string []. + +Lemma e_const_5_T_int : + typ_e (Map.empty ctxv) e_const_5 T_int. +Proof. by apply typ_int. Qed. + +Lemma e_call_const_5_T_int : + typ_e (Map.empty ctxv) e_call_const_5 T_int. +Proof. +Admitted. From e6738f2a70f2e2eeb7c3f764a74fd27638d04783 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 27 Feb 2024 11:04:23 +0100 Subject: [PATCH 07/18] =?UTF-8?q?Some=20more=20lemmas=20=E2=80=93=20still?= =?UTF-8?q?=20stuck?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/abs.ott | 12 +- theories/abs_defs.v | 12 +- theories/abs_functional_metatheory.v | 439 ++++++++++++++++++++++++++- theories/utils.v | 8 + 4 files changed, 439 insertions(+), 32 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index e09ac85..f39551c 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -128,9 +128,6 @@ where e_list_subst_one (es:list e) (x_ y_: x) : list e := { e_list_subst_one (e0::es) x_ y_ := e_var_subst_one e0 x_ y_ :: e_list_subst_one es x_ y_ }. -(* I would prefer not doing this, but sometimes I need it to compute *) -Global Transparent e_var_subst_one. - 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 := { @@ -150,14 +147,7 @@ Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := fresh_vars_s l s0 /\ fresh_vars_e l e0. -Inductive distinct: list x -> Prop := - | distinct_nil: distinct nil - | distinct_cons: forall y ys, - ~ In y ys -> - distinct ys -> - distinct (y::ys). - -Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l. +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ NoDup l. }} defns diff --git a/theories/abs_defs.v b/theories/abs_defs.v index c90d835..59cb328 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -109,9 +109,6 @@ where e_list_subst_one (es:list e) (x_ y_: x) : list e := { e_list_subst_one (e0::es) x_ y_ := e_var_subst_one e0 x_ y_ :: e_list_subst_one es x_ y_ }. -(* I would prefer not doing this, but sometimes I need it to compute *) -Global Transparent e_var_subst_one. - 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 := { @@ -131,14 +128,7 @@ Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := fresh_vars_s l s0 /\ fresh_vars_e l e0. -Inductive distinct: list x -> Prop := - | distinct_nil: distinct nil - | distinct_cons: forall y ys, - ~ In y ys -> - distinct ys -> - distinct (y::ys). - -Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l. +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ NoDup l. (** definitions *) diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index e461816..767fe53 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -5,6 +5,9 @@ From Coq Require Import List FSets.FMapFacts Lia. +From Equations Require Import Equations. + +Require Import FMapList. Module MapFacts := FSets.FMapFacts.Facts Map. Import ListNotations. @@ -54,6 +57,26 @@ Proof. 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) := @@ -83,7 +106,7 @@ Qed. 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 -> - distinct (map (fun '(_,_,_,y)=>y) sub_list) -> + 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 with try easy. intros. @@ -110,7 +133,7 @@ Lemma fresh_consistent: forall G0 s0 (sub_list: list (T*x*t*x)), (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 -> - distinct (map (fun '(_,_,_,y)=>y) sub_list) -> + 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 with try easy. @@ -250,9 +273,9 @@ Proof. typ_e G0 (e_var x1) T1 -> typ_e G0 (e_var_subst e0 [(x0, x1)]) T0) ;cbn; intros. - - inv H; constructor. + - inv H; simp e_var_subst_one; constructor. - inv H. - simpl. + simp e_var_subst_one. destruct (eq_x x5 x0); subst. + apply Map.find_2 in H3. apply MapFacts.add_mapsto_iff in H3. @@ -268,6 +291,7 @@ Proof. * 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 @@ -299,14 +323,409 @@ Proof. + eapply H0; eauto. Qed. +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. + +Lemma fresh_vars_first: 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 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. + inv H0. + apply Heqo. + exists x. + eapply Map.add_3; eauto. + eapply Map.add_3; eauto. + * symmetry. + apply MapFacts.not_find_in_iff in Heqo. + apply MapFacts.not_find_in_iff. + intro. + inv H0. + apply Heqo. + exists x. + eapply Map.add_3; eauto. + eapply Map.add_3; eauto. +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*t*x)), + ~ In y (map (fun '(_,_,_, y) => y) upd) -> + 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). +Admitted. + +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_alt: 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 fresh_subst_NoDup: forall e0 y sub, + fresh_vars_e [y] e0 -> + ~ In y (map (fun '(_, y) => y) sub) -> + fresh_vars_e [y] (e_var_subst e0 sub). +Admitted. + (* pipe dream: might need some stronger assumptions*) -Lemma subst_lemma: forall (T_x_t_y_list:list (T*x*t*x)) G0 e0 T0, - typ_e (fold_right (fun '(T_, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T T_) G0) G0 T_x_t_y_list) e0 T0 -> - typ_e (fold_right (fun '(T_, _, _, y) (G0 : G) => Map.add y (ctxv_T T_) G0) G0 T_x_t_y_list) - (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) - T0. +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) -> + (* needed? *) + fresh_vars_e (map (fun '(_, _, _, y) => y) T_x_t_y_list) e0 -> + 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. + induction T_x_t_y_list; intros. + - easy. + - destruct a as (((?T_,?x_),?t_),?y). + unfold e_var_subst. + simpl. + inv H0. + apply subst_lemma_one_alt. + + replace (fold_right (fun '(x', y') (e' : e) => e_var_subst_one e' x' y') e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) + with (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) by auto. + simpl in H, H1. + apply fresh_monotone_e in H1. + admit. + + + apply fresh_vars_first in H1. + apply fresh_subst_NoDup; eauto. + intro. + apply H4. + rewrite map_map in H0. + apply in_map_iff in H0. + destruct H0 as ((((?,?),?), ?), (?, ?)); subst. + apply in_map_iff. + eexists. + split; now eauto. Admitted. + Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), G_vdash_s G5 s5 -> Forall (typ_F G5) Flist -> @@ -474,7 +893,7 @@ Proof with try easy. (* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) + rewrite H5 in H9. inv H9. - apply subst_lemma. + apply subst_lemma; auto. rewrite <- fold_map_reshuffle. apply H8. Qed. diff --git a/theories/utils.v b/theories/utils.v index 1264f3b..5c8f2d6 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -7,6 +7,14 @@ 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}. From d14b13842f57e9de7a1dc2d874cf8c13155bb9b2 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 27 Feb 2024 11:22:04 +0100 Subject: [PATCH 08/18] Typing examples --- theories/abs_examples.v | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/theories/abs_examples.v b/theories/abs_examples.v index af0c048..bd27b4c 100644 --- a/theories/abs_examples.v +++ b/theories/abs_examples.v @@ -1,5 +1,5 @@ From ABS Require Import abs_defs. -From stdpp Require Import prelude. +From stdpp Require Import prelude base. (** * ABS Examples *) @@ -12,11 +12,27 @@ Definition func_const_5 : F := Definition e_call_const_5 : e := e_fn_call "const_5"%string []. +Definition Ctx : G := + Map.add ("const_5"%string) (ctxv_sig (sig_sig [] T_int)) (Map.empty ctxv). + Lemma e_const_5_T_int : - typ_e (Map.empty ctxv) e_const_5 T_int. + typ_e Ctx e_const_5 T_int. Proof. by apply typ_int. Qed. +Lemma e_call_const_typ_F : + typ_F Ctx func_const_5. +Proof. + apply typ_func_decl. + - easy. + - apply e_const_5_T_int. +Qed. + Lemma e_call_const_5_T_int : - typ_e (Map.empty ctxv) e_call_const_5 T_int. + typ_e Ctx e_call_const_5 T_int. Proof. -Admitted. + unfold e_call_const_5. + replace [] with (map (fun (pat_:(e*T)) => match pat_ with (e_,T_) => e_ end ) []) + by auto. + apply typ_func_expr; + easy. +Qed. From ec013522951aae429af9d192bdf4de4c0dc62a53 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 27 Feb 2024 11:27:07 +0100 Subject: [PATCH 09/18] nits --- theories/abs_examples.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/abs_examples.v b/theories/abs_examples.v index bd27b4c..c21ed60 100644 --- a/theories/abs_examples.v +++ b/theories/abs_examples.v @@ -33,6 +33,5 @@ Proof. unfold e_call_const_5. replace [] with (map (fun (pat_:(e*T)) => match pat_ with (e_,T_) => e_ end ) []) by auto. - apply typ_func_expr; - easy. + by apply typ_func_expr. Qed. From 21f67b044d4c6764cc113536bfe80d232034d52c Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 27 Feb 2024 11:41:57 +0100 Subject: [PATCH 10/18] Cleanup Proof with... --- theories/abs_functional_metatheory.v | 95 +++++++++++++++------------- 1 file changed, 51 insertions(+), 44 deletions(-) diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index 767fe53..7049a6b 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -108,24 +108,25 @@ Lemma fresh_subG: forall G0 s0 (sub_list: list (T*x*t*x)), 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 with try easy. +Proof. intros. - induction sub_list... - destruct a as (((?T_, ?x_), ?t_), y). - inv H1. - inv H0. - pose proof IHsub_list H2 H5. - cbn. - apply subG_add; auto. - intro. + 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. + 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)), @@ -136,16 +137,17 @@ Lemma fresh_consistent: forall G0 s0 (sub_list: list (T*x*t*x)), 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 with try easy. +Proof. intros. - induction sub_list... - destruct a as (((?T_, ?x_), ?t_), y). - inv H1. - inv H2. + 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. + cbn. + intros ?y ?T_ ?. + destruct (eq_x y y0); subst. - exists t_. split... + apply Map.find_1. @@ -234,11 +236,11 @@ 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 with auto. +Proof. intros. - induction e_T_list... + induction e_T_list; auto. destruct a;cbn in *. - rewrite IHe_T_list... + now rewrite IHe_T_list. Qed. Lemma fold_map_reshuffle: forall (l: list (T*x*t*x)) G0, @@ -733,14 +735,15 @@ Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), 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 with try easy. +Proof. 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... + exists G5; splits. + 1,2: easy. inv e0_type. destruct (s_well_typed x5 T0 H2) as (?, (?, ?)). rewrite H in H0. @@ -757,17 +760,18 @@ Proof with try easy. rewrite H3. apply in_map_iff. exists (e_5, T_5). - split... - apply in_combine_split with (2:=eq_refl)... + 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... + 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... + apply typ_func_expr. * intros. rewrite pat2_id in H8. rewrite H3 in H8. @@ -775,33 +779,35 @@ Proof with try easy. rewrite combine_app in H8... apply in_app_iff in H8. destruct H8. - -- apply subG_type with (G1:=G5)... + -- apply subG_type with (G1:=G5); auto. apply H2. apply in_map_iff. exists (e_, T_). - split... + split; auto. rewrite H3. - rewrite combine_app... { + rewrite combine_app; auto. + { eapply in_app_iff. - left... + now left. } rewrite 2 app_length. simpl. rewrite H1. reflexivity. - -- rewrite combine_app in H8... + -- 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)... + ++ apply subG_type with (G1:=G5); auto. apply H2. apply in_map_iff. exists (e_, T_). - split... + split; auto. rewrite H3. - rewrite combine_app... { + rewrite combine_app; auto. + { eapply in_app_iff. right. right. @@ -814,6 +820,7 @@ Proof with try easy. reflexivity. ++ rewrite app_nil_r. apply H1. + -- auto. -- rewrite app_nil_r. simpl. rewrite H1. @@ -826,7 +833,7 @@ Proof with try easy. apply H4. ++ rewrite map_length. rewrite H3. - rewrite 2 combine_app... + rewrite 2 combine_app; auto. ** repeat (rewrite app_length). rewrite 3 combine_length. simpl. @@ -837,7 +844,7 @@ Proof with try easy. rewrite H1. reflexivity. * rewrite app_nil_r. - rewrite combine_fst... + rewrite combine_fst; auto. rewrite map_length. rewrite H3. rewrite combine_length. @@ -886,7 +893,7 @@ Proof with try easy. rewrite map_map. apply in_map_iff. exists Txty. - split... + split; auto. destruct Txty as (((?, ?), ?), ?). now inv H10. From 4f627f2210db4c91ffc6a8e3f127321d0ce1e098 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 30 Jan 2024 10:37:47 +0100 Subject: [PATCH 11/18] All but the function base case. very much WIP --- src/abs.ott | 17 +- theories/abs_defs.v | 11 +- theories/abs_functional_metatheory.v | 404 ++++++++++++++++++++++++++- 3 files changed, 426 insertions(+), 6 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index 35d0211..f30b71a 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -108,8 +108,12 @@ 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 + | 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]]) }} embed {{ coq @@ -142,6 +146,15 @@ 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. }} defns @@ -193,6 +206,6 @@ 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 ) + fresh ( y1 , ... , yn , e , s) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- :: 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..da097cc 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -130,6 +130,15 @@ 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. + (** definitions *) (* defns expression_well_typing *) @@ -164,7 +173,7 @@ 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 ) -> + (fresh_vars (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) e5 s5 ) -> 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_functional_metatheory.v b/theories/abs_functional_metatheory.v index 7bf5619..d8a671a 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -1,26 +1,424 @@ From ABS Require Import abs_defs. -From Coq Require Import List. +From Coq Require Import List + FSets.FMapFacts + Lia. + +Module MapFacts := FSets.FMapFacts.Facts Map. Import ListNotations. (** * ABS Functional Metatheory *) +Notation "G ⊢ e : T" := (typ_e G e T) (at level 5). +Notation "G F⊢ F" := (typ_F G F) (at level 5). +(* Notation "Fs , s ⊢ e ⇝ s' ⊢ e'" := (red_e Fs s e s' e') (at level 10). *) + Definition subG (G1 G2 : G) : Prop := forall (key : string) (elt : ctxv), Map.find key G1 = Some elt -> Map.find key G2 = Some elt. +Notation "G1 ⊆ G2" := (subG G1 G2) (at level 5). + Definition G_vdash_s (G5 : G) (s5 : s) := forall (x5 : x) (t5 : t) (T5 : T), Map.find x5 s5 = Some t5 -> Map.find x5 G5 = Some (ctxv_T T5) -> typ_e G5 (e_t t5) T5. +Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). + +Ltac splits := repeat split. +Ltac inv H :=inversion H ; subst; clear H. +Tactic Notation "intros*" := repeat intro. + +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_ T_ ? ?. + apply H in H2. + pose proof H0 x_ t_ T_ H1 H2. + inv H3;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. + +(* extremely tedious stuff *) +Lemma subst_fst_commutes: forall x0 s e_T_list, + map (fun pat_ : e * T => let (e_, _) := pat_ in e_) + (map (fun pat_ : e * T => let (e_, T_) := pat_ in (e_var_subst e_ [(x0, s)], T_)) e_T_list) = + map (fun e : e => e_var_subst e [(x0, s)]) (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list). +Proof with auto. + induction e_T_list... + destruct a;cbn. + rewrite IHe_T_list... +Qed. + +Lemma combine_fst {X Y: Type} : 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 {X Y: Type} : forall (l1: list X), + @combine X Y l1 [] = []. +Proof. destruct l1; easy. Qed. + +Lemma combine_snd {X Y: Type} : 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 {X Y: Type} : 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 {X Y: Type}: 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_combine_app{X Y:Type}: 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 {X Y: Type} : 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 {X Y: Type}: 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 combine_map {X Y: Type}: 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 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 e_var_subst_empty: forall e0, e_var_subst e0 [] = e0. +Proof. + eapply e_ott_ind with + (P_list_e:= fun es => map (fun e0 => e_var_subst e0 []) es = es);simpl;intros;auto. + { rewrite H. auto. } + induction e_l. + - rewrite H. + reflexivity. + - inv H0. + simpl. + rewrite H. + rewrite 2 H2. + rewrite 2 H3. + reflexivity. +Qed. + +Lemma split_corresponding_list_aux {X Y: Type}: 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. + +Corollary split_corresponding_list {X Y: Type}: 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_aux _ _ _ _ H) + as (left_list' & mid' & right_list' & _ & _ & EQ). + exists left_list', mid', right_list'. + apply EQ. +Qed. + 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. +Proof with try easy. + 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... + inv e0_type. + apply (s_well_typed _ _ _ H H2). + + - (* RED_FUN_EXPR *) + intros. + inv e0_type. + rewrite app_nil_r in H0. + pose proof split_corresponding_list_aux 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... + apply in_combine_app with (2:=eq_refl)... + } + 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... + 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))). + (* by apply combine_fst. *) + 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)... + apply H2. + apply in_map_iff. + exists (e_, T_). + split... + rewrite H3. + rewrite combine_app... { + eapply in_app_iff. + left... + } + rewrite 2 app_length. + simpl. + rewrite H1. + reflexivity. + -- rewrite combine_app in H8... + apply in_app_iff in H8. + destruct H8. + ++ inv H8;[|contradiction]. + inv H9. + apply H7. + ++ apply subG_type with (G1:=G5)... + apply H2. + apply in_map_iff. + exists (e_, T_). + split... + rewrite H3. + rewrite combine_app... { + 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. + -- 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... + ** 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... + rewrite map_length. + rewrite H3. + rewrite combine_length. + repeat (rewrite app_length). + rewrite H, H1. + simpl. + lia. + + - (* RED_FUN_CALL *) + admit. Admitted. From d0278b2f6a465ed60bd8eee5a506210efd282e3d Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Wed, 31 Jan 2024 14:49:49 +0100 Subject: [PATCH 12/18] Factoring out list utilities --- _CoqProject | 1 + theories/abs_functional_metatheory.v | 218 +-------------------------- theories/utils.v | 217 ++++++++++++++++++++++++++ 3 files changed, 224 insertions(+), 212 deletions(-) create mode 100644 theories/utils.v 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/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index d8a671a..2226112 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -1,4 +1,6 @@ -From ABS Require Import abs_defs. +From ABS Require Import abs_defs + utils. + From Coq Require Import List FSets.FMapFacts Lia. @@ -27,10 +29,6 @@ Definition G_vdash_s (G5 : G) (s5 : s) := Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). -Ltac splits := repeat split. -Ltac inv H :=inversion H ; subst; clear H. -Tactic Notation "intros*" := repeat intro. - Lemma subG_consistent: forall G1 G2 s0, subG G1 G2 -> G_vdash_s G2 s0 -> G_vdash_s G1 s0. Proof. @@ -58,148 +56,18 @@ Proof. apply H2. Qed. -(* extremely tedious stuff *) +(* some slightly ad-hoc equalities *) Lemma subst_fst_commutes: forall x0 s e_T_list, map (fun pat_ : e * T => let (e_, _) := pat_ in e_) (map (fun pat_ : e * T => let (e_, T_) := pat_ in (e_var_subst e_ [(x0, s)], T_)) e_T_list) = map (fun e : e => e_var_subst e [(x0, s)]) (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list). Proof with auto. + intros. induction e_T_list... destruct a;cbn. rewrite IHe_T_list... Qed. -Lemma combine_fst {X Y: Type} : 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 {X Y: Type} : forall (l1: list X), - @combine X Y l1 [] = []. -Proof. destruct l1; easy. Qed. - -Lemma combine_snd {X Y: Type} : 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 {X Y: Type} : 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 {X Y: Type}: 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_combine_app{X Y:Type}: 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 {X Y: Type} : 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 {X Y: Type}: 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 combine_map {X Y: Type}: 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 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))) @@ -228,79 +96,6 @@ Proof. reflexivity. Qed. -Lemma split_corresponding_list_aux {X Y: Type}: 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. - -Corollary split_corresponding_list {X Y: Type}: 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_aux _ _ _ _ H) - as (left_list' & mid' & right_list' & _ & _ & EQ). - exists left_list', mid', right_list'. - apply EQ. -Qed. - Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), G_vdash_s G5 s5 -> Forall (typ_F G5) Flist -> @@ -323,7 +118,7 @@ Proof with try easy. intros. inv e0_type. rewrite app_nil_r in H0. - pose proof split_corresponding_list_aux e_T_list e_list e_5 e'_list 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. @@ -339,7 +134,6 @@ Proof with try 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))). - (* by apply combine_fst. *) apply typ_func_expr... * intros. rewrite pat2_id in H8. diff --git a/theories/utils.v b/theories/utils.v new file mode 100644 index 0000000..bf34fb6 --- /dev/null +++ b/theories/utils.v @@ -0,0 +1,217 @@ +From Coq Require Import List + Lia. + +Import ListNotations. + +Ltac splits := repeat split. +Ltac inv H :=inversion H ; subst; clear H. +Tactic Notation "intros*" := repeat intro. + +Section ListLemmas. + Context {X Y: Type}. + + 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_combine_app: 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 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. From 391e679b2c047e02e78fbc01533377c27672d291 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 6 Feb 2024 19:45:37 +0100 Subject: [PATCH 13/18] Some cleanup and minor progress --- src/abs.ott | 34 +++---- theories/abs_defs.v | 34 +++---- theories/abs_functional_metatheory.v | 140 +++++++++++++++++++++++---- theories/utils.v | 21 +++- 4 files changed, 168 insertions(+), 61 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index f30b71a..384ed91 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -117,27 +117,19 @@ formula :: formula_ ::= 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. +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_ +}. + +(* I would prefer not doing this, but sometimes I need it to compute *) +Global Transparent e_var_subst_one. + +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; diff --git a/theories/abs_defs.v b/theories/abs_defs.v index da097cc..d643636 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -100,27 +100,19 @@ 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. +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_ +}. + +(* I would prefer not doing this, but sometimes I need it to compute *) +Global Transparent e_var_subst_one. + +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; diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index 2226112..d25cd25 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -10,6 +10,10 @@ Import ListNotations. (** * ABS Functional Metatheory *) +Section FunctionalMetatheory. + +Hypothesis (vars_fs_distinct: forall (x_:x) (fn_:fn), x_ <> fn_). + Notation "G ⊢ e : T" := (typ_e G e T) (at level 5). Notation "G F⊢ F" := (typ_F G F) (at level 5). (* Notation "Fs , s ⊢ e ⇝ s' ⊢ e'" := (red_e Fs s e s' e') (at level 10). *) @@ -27,6 +31,14 @@ Definition G_vdash_s (G5 : G) (s5 : s) := Map.find x5 G5 = Some (ctxv_T T5) -> typ_e G5 (e_t t5) T5. +(* sanity check *) +Lemma empty_G_consistent: forall s0, + G_vdash_s (Map.empty ctxv) s0. +Proof. + intros*. + inv H0. +Qed. + Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). Lemma subG_consistent: forall G1 G2 s0, @@ -57,14 +69,29 @@ Proof. Qed. (* some slightly ad-hoc equalities *) -Lemma subst_fst_commutes: forall x0 s e_T_list, - map (fun pat_ : e * T => let (e_, _) := pat_ in e_) - (map (fun pat_ : e * T => let (e_, T_) := pat_ in (e_var_subst e_ [(x0, s)], T_)) e_T_list) = - map (fun e : e => e_var_subst e [(x0, s)]) (map (fun pat_ : e * T => let (e_, _) := pat_ in e_) e_T_list). +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 with auto. intros. induction e_T_list... - destruct a;cbn. + destruct a;cbn in *. rewrite IHe_T_list... Qed. @@ -80,20 +107,73 @@ Proof. reflexivity. Qed. -Lemma e_var_subst_empty: forall e0, e_var_subst e0 [] = e0. +(* this is 9.3.8 from Types and Programming Languages *) +(* it has not yet proven useful *) +Lemma subst_lemma_aux: 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 - (P_list_e:= fun es => map (fun e0 => e_var_subst e0 []) es = es);simpl;intros;auto. - { rewrite H. auto. } - induction e_l. - - rewrite H. - reflexivity. - - inv H0. + (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; constructor. + - inv H. simpl. - rewrite H. - rewrite 2 H2. - rewrite 2 H3. - reflexivity. + 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. + 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 type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), @@ -125,7 +205,7 @@ Proof with try easy. apply in_map_iff. exists (e_5, T_5). split... - apply in_combine_app with (2:=eq_refl)... + apply in_combine_split with (2:=eq_refl)... } pose proof H2 e_5 T_5 H5. destruct (IHreduction G5 s_well_typed F_well_typed _ H6) as (G' & G'extends & G'consistent & ?). @@ -214,5 +294,29 @@ Proof with try easy. lia. - (* RED_FUN_CALL *) - admit. + 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 H1 F_well_typed fn_def H0 as fn_typed. + inv e0_type. + inv fn_typed. + rewrite H8 in H7. + inv H7. + assert (map (fun '(_,T_) => T_) e_T_list = map (fun '(T_, _, _, _) => T_) T_x_t_y_list). { + rewrite <- H4. + rewrite map_map. + apply map_eq. + intros [[[? ?] ?] ?]. + reflexivity. + } + clear H4. + set (G':=(fold_right (fun '(T_, _, _, y) G0 => Map.add y (ctxv_T T_) G0) G5 T_x_t_y_list)). + exists G'. + splits. + + admit. + + admit. + + admit. Admitted. +End FunctionalMetatheory. diff --git a/theories/utils.v b/theories/utils.v index bf34fb6..acfd687 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -10,6 +10,16 @@ Tactic Notation "intros*" := repeat intro. 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 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. @@ -77,7 +87,16 @@ Section ListLemmas. rewrite IHl1; easy. Qed. - Lemma in_combine_app: forall (l: list (X*Y)) l1 l1' l2 l2' x y, + 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. From 70dafdb528b6c90acf5969a946754741bf97a538 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Mon, 12 Feb 2024 15:58:12 +0100 Subject: [PATCH 14/18] Some reorganizing, but not much progress --- theories/abs_functional_metatheory.v | 79 +++++++++++++++++++++------- theories/utils.v | 12 +++++ 2 files changed, 73 insertions(+), 18 deletions(-) diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index d25cd25..1bfe231 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -41,6 +41,24 @@ Qed. Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). +(* the proof in the original ABS paper appeals to the following two properties in the RED_FUN_GROUND case*) +(* however, I am not sure either holds without some extra assumptions *) +(* (in particular uniqueness of the substituted variables and freshness wrt the typing context) *) +Lemma fresh_subG: forall G0 s0 (sub_list: list (T*x*t*x)), + (* this should really be fresh wrt G0, but we don't actually have that so maybe these suffice? *) + G_vdash_s G0 s0 -> + fresh_vars_s (map (fun '(_,_,_,y)=>y) sub_list) s0 -> + subG G0 (fold_right (fun '(T_,_,_,y_) G0 => Map.add y_ (ctxv_T T_) G0) G0 sub_list). +Admitted. + +Lemma fresh_consistent: 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 -> + 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. +Admitted. + Lemma subG_consistent: forall G1 G2 s0, subG G1 G2 -> G_vdash_s G2 s0 -> G_vdash_s G1 s0. Proof. @@ -109,7 +127,7 @@ Qed. (* this is 9.3.8 from Types and Programming Languages *) (* it has not yet proven useful *) -Lemma subst_lemma_aux: forall (x0 x1:x) G0 e0 T0 T1, +Lemma subst_lemma_one: 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. @@ -176,6 +194,39 @@ Proof. + eapply H0; eauto. Qed. +Lemma subst_lemma: forall G0 e0 T0 (sub_list: list (T*x*t*x)), + (* idea: some wellformedness condition that ensures the two admits *) + typ_e (fold_right (fun '(T1, x0, _, _) G' => Map.add x0 (ctxv_T T1) G') G0 sub_list) e0 T0 -> + (forall x1 T1, + In (T1, x1) (map (fun '(T1, _, _, x1) => (T1, x1)) sub_list) -> + typ_e G0 (e_var x1) T1) -> + typ_e G0 (e_var_subst e0 (map (fun '(_, x0, _, x1) => (x0, x1)) sub_list)) T0. +Proof. + intros. + generalize dependent G0. + induction sub_list; intros; auto. + destruct a as (((?T_&?x_)&?t_)&?y_). + simpl. + replace ((T_, x_, t_, y_) :: sub_list) with (sub_list ++ [(T_, x_, t_, y_)]) + in H by admit. + (* if all the x0s are unique, then order does not matter *) + setoid_rewrite fold_right_app in H. + eapply subst_lemma_one. + - eapply IHsub_list; eauto. + intros. + assert (In (T1, x1) (map (fun '(T2, _, _, x2) => (T2, x2)) ((T_, x_, t_, y_)::sub_list))). + {right; auto. } + pose proof H0 x1 T1 H2. + inv H3. + constructor. + apply Map.find_1. + apply Map.add_2. + { admit. } (* not sure how to get rid of this *) + apply Map.find_2 in H6; auto. + - apply H0. + left; eauto. +Admitted. + Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), G_vdash_s G5 s5 -> Forall (typ_F G5) Flist -> @@ -293,30 +344,22 @@ Proof with try easy. simpl. lia. - - (* RED_FUN_CALL *) + - (* 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 H1 F_well_typed fn_def H0 as fn_typed. - inv e0_type. inv fn_typed. - rewrite H8 in H7. - inv H7. - assert (map (fun '(_,T_) => T_) e_T_list = map (fun '(T_, _, _, _) => T_) T_x_t_y_list). { - rewrite <- H4. - rewrite map_map. - apply map_eq. - intros [[[? ?] ?] ?]. - reflexivity. - } - clear H4. - set (G':=(fold_right (fun '(T_, _, _, y) G0 => Map.add y (ctxv_T T_) G0) G5 T_x_t_y_list)). - exists G'. + inv e0_type. + exists (fold_right (fun '(T_, _, _, y) G0 => Map.add y (ctxv_T T_) G0) G5 T_x_t_y_list). splits. - + admit. - + admit. - + admit. + + eapply fresh_subG; eauto. + apply H. + + rewrite <- fold_map. + apply fresh_consistent; eauto. + apply H. + + (* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) Admitted. End FunctionalMetatheory. diff --git a/theories/utils.v b/theories/utils.v index acfd687..74bbd17 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -151,6 +151,17 @@ Section ListLemmas. 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 combine_map: forall (l: list (X*Y)), combine (map fst l) (map snd l) = l. Proof. @@ -233,4 +244,5 @@ Section ListLemmas. exists left_list', mid', right_list'. apply EQ. Qed. + End ListLemmas. From 4ad9b1940c68f1b1dc4e8a45169d6009d960ef07 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Mon, 19 Feb 2024 20:34:37 +0100 Subject: [PATCH 15/18] Almost there with type preservation, tho still missing the actual type (substitution lemma) --- src/abs.ott | 13 +- theories/abs_defs.v | 11 +- theories/abs_functional_metatheory.v | 231 ++++++++++++++++++++------- theories/utils.v | 39 +++++ 4 files changed, 235 insertions(+), 59 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index 384ed91..e09ac85 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -114,6 +114,8 @@ formula :: formula_ ::= {{ coq (fresh_vars_s [[x1 ... xn]] [[s]]) }} | fresh ( x1 , ... , xn , e , s ) :: M :: fresh {{ coq (fresh_vars [[x1 ... xn]] [[e]] [[s]]) }} + | well_formed ( x1 , ... , xn , e , s ) :: M :: well_formed + {{ coq (well_formed [[e]] [[s]] [[x1 ... xn]]) }} embed {{ coq @@ -147,6 +149,15 @@ Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := fresh_vars_s l s0 /\ fresh_vars_e l e0. + +Inductive distinct: list x -> Prop := + | distinct_nil: distinct nil + | distinct_cons: forall y ys, + ~ In y ys -> + distinct ys -> + distinct (y::ys). + +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l. }} defns @@ -198,6 +209,6 @@ 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 , s) + well_formed (y1 , ... , yn , e, s) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- :: 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 d643636..c90d835 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -131,6 +131,15 @@ Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := fresh_vars_s l s0 /\ fresh_vars_e l e0. +Inductive distinct: list x -> Prop := + | distinct_nil: distinct nil + | distinct_cons: forall y ys, + ~ In y ys -> + distinct ys -> + distinct (y::ys). + +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l. + (** definitions *) (* defns expression_well_typing *) @@ -165,7 +174,7 @@ 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 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list) e5 s5 ) -> + (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) ) -> 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_functional_metatheory.v b/theories/abs_functional_metatheory.v index 1bfe231..e461816 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -13,6 +13,9 @@ Import ListNotations. 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_). Notation "G ⊢ e : T" := (typ_e G e T) (at level 5). Notation "G F⊢ F" := (typ_F G F) (at level 5). @@ -25,48 +28,150 @@ Definition subG (G1 G2 : G) : Prop := Notation "G1 ⊆ G2" := (subG G1 G2) (at level 5). -Definition G_vdash_s (G5 : G) (s5 : s) := - forall (x5 : x) (t5 : t) (T5 : T), - Map.find x5 s5 = Some t5 -> - Map.find x5 G5 = Some (ctxv_T T5) -> - typ_e G5 (e_t t5) T5. +Lemma subG_refl: forall G0, + subG G0 G0. +Proof. easy. Qed. -(* sanity check *) -Lemma empty_G_consistent: forall s0, - G_vdash_s (Map.empty ctxv) s0. +Lemma subG_add: forall G0 G1 y T_, + subG G0 G1 -> + ~ Map.In y G0 -> + subG G0 (Map.add y T_ G1). Proof. - intros*. - inv H0. + 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. +(* 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), + Map.find x5 G5 = Some (ctxv_T 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). -(* the proof in the original ABS paper appeals to the following two properties in the RED_FUN_GROUND case*) -(* however, I am not sure either holds without some extra assumptions *) -(* (in particular uniqueness of the substituted variables and freshness wrt the typing context) *) +(* how is this not in MapFacts? *) +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 fresh_subG: forall G0 s0 (sub_list: list (T*x*t*x)), - (* this should really be fresh wrt G0, but we don't actually have that so maybe these suffice? *) G_vdash_s G0 s0 -> fresh_vars_s (map (fun '(_,_,_,y)=>y) sub_list) s0 -> + distinct (map (fun '(_,_,_,y)=>y) sub_list) -> subG G0 (fold_right (fun '(T_,_,_,y_) G0 => Map.add y_ (ctxv_T T_) G0) G0 sub_list). -Admitted. +Proof with try easy. + intros. + induction sub_list... + 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 -> + distinct (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. -Admitted. +Proof with try easy. + intros. + induction sub_list... + 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_ T_ ? ?. - apply H in H2. - pose proof H0 x_ t_ T_ H1 H2. - inv H3;constructor. + 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, @@ -194,37 +299,12 @@ Proof. + eapply H0; eauto. Qed. -Lemma subst_lemma: forall G0 e0 T0 (sub_list: list (T*x*t*x)), - (* idea: some wellformedness condition that ensures the two admits *) - typ_e (fold_right (fun '(T1, x0, _, _) G' => Map.add x0 (ctxv_T T1) G') G0 sub_list) e0 T0 -> - (forall x1 T1, - In (T1, x1) (map (fun '(T1, _, _, x1) => (T1, x1)) sub_list) -> - typ_e G0 (e_var x1) T1) -> - typ_e G0 (e_var_subst e0 (map (fun '(_, x0, _, x1) => (x0, x1)) sub_list)) T0. -Proof. - intros. - generalize dependent G0. - induction sub_list; intros; auto. - destruct a as (((?T_&?x_)&?t_)&?y_). - simpl. - replace ((T_, x_, t_, y_) :: sub_list) with (sub_list ++ [(T_, x_, t_, y_)]) - in H by admit. - (* if all the x0s are unique, then order does not matter *) - setoid_rewrite fold_right_app in H. - eapply subst_lemma_one. - - eapply IHsub_list; eauto. - intros. - assert (In (T1, x1) (map (fun '(T2, _, _, x2) => (T2, x2)) ((T_, x_, t_, y_)::sub_list))). - {right; auto. } - pose proof H0 x1 T1 H2. - inv H3. - constructor. - apply Map.find_1. - apply Map.add_2. - { admit. } (* not sure how to get rid of this *) - apply Map.find_2 in H6; auto. - - apply H0. - left; eauto. +(* pipe dream: might need some stronger assumptions*) +Lemma subst_lemma: forall (T_x_t_y_list:list (T*x*t*x)) G0 e0 T0, + typ_e (fold_right (fun '(T_, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T T_) G0) G0 T_x_t_y_list) e0 T0 -> + typ_e (fold_right (fun '(T_, _, _, y) (G0 : G) => Map.add y (ctxv_T T_) G0) G0 T_x_t_y_list) + (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) + T0. Admitted. Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), @@ -243,7 +323,10 @@ Proof with try easy. - intros. exists G5; splits... inv e0_type. - apply (s_well_typed _ _ _ H H2). + destruct (s_well_typed x5 T0 H2) as (?, (?, ?)). + rewrite H in H0. + inv H0. + assumption. - (* RED_FUN_EXPR *) intros. @@ -353,13 +436,47 @@ Proof with try easy. pose proof H1 F_well_typed fn_def H0 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). + { + rewrite H5 in H9. + inv H9. + 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 H3. + 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 <- H10. + 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. - apply H. + rewrite <- fold_map. apply fresh_consistent; eauto. - apply H. - + (* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) -Admitted. + (* some slightly silly reshuffling *) + intros. + apply in_map_iff in H10. + destruct H10 as (Txty, (?, ?)). + apply H6. + rewrite H7. + rewrite map_map. + apply in_map_iff. + exists Txty. + split... + destruct Txty as (((?, ?), ?), ?). + now inv H10. + +(* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) + + rewrite H5 in H9. + inv H9. + apply subst_lemma. + rewrite <- fold_map_reshuffle. + apply H8. +Qed. + End FunctionalMetatheory. diff --git a/theories/utils.v b/theories/utils.v index 74bbd17..1264f3b 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -20,6 +20,45 @@ Section ListLemmas. 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. + + (* extremely ad-hoc*) + 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. From 1ed7a07af9bc7ffb542bd350269cb7385746542b Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 27 Feb 2024 11:04:23 +0100 Subject: [PATCH 16/18] =?UTF-8?q?Some=20more=20lemmas=20=E2=80=93=20still?= =?UTF-8?q?=20stuck?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/abs.ott | 12 +- theories/abs_defs.v | 12 +- theories/abs_functional_metatheory.v | 439 ++++++++++++++++++++++++++- theories/utils.v | 8 + 4 files changed, 439 insertions(+), 32 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index e09ac85..f39551c 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -128,9 +128,6 @@ where e_list_subst_one (es:list e) (x_ y_: x) : list e := { e_list_subst_one (e0::es) x_ y_ := e_var_subst_one e0 x_ y_ :: e_list_subst_one es x_ y_ }. -(* I would prefer not doing this, but sometimes I need it to compute *) -Global Transparent e_var_subst_one. - 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 := { @@ -150,14 +147,7 @@ Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := fresh_vars_s l s0 /\ fresh_vars_e l e0. -Inductive distinct: list x -> Prop := - | distinct_nil: distinct nil - | distinct_cons: forall y ys, - ~ In y ys -> - distinct ys -> - distinct (y::ys). - -Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l. +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ NoDup l. }} defns diff --git a/theories/abs_defs.v b/theories/abs_defs.v index c90d835..59cb328 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -109,9 +109,6 @@ where e_list_subst_one (es:list e) (x_ y_: x) : list e := { e_list_subst_one (e0::es) x_ y_ := e_var_subst_one e0 x_ y_ :: e_list_subst_one es x_ y_ }. -(* I would prefer not doing this, but sometimes I need it to compute *) -Global Transparent e_var_subst_one. - 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 := { @@ -131,14 +128,7 @@ Fixpoint fresh_vars_s (l : list x) (s0 : s): Prop := Definition fresh_vars (l : list x) (e0: e) (s0: s) : Prop := fresh_vars_s l s0 /\ fresh_vars_e l e0. -Inductive distinct: list x -> Prop := - | distinct_nil: distinct nil - | distinct_cons: forall y ys, - ~ In y ys -> - distinct ys -> - distinct (y::ys). - -Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ distinct l. +Definition well_formed (e0: e) (s0: s) (l:list x) : Prop := fresh_vars l e0 s0 /\ NoDup l. (** definitions *) diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index e461816..767fe53 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -5,6 +5,9 @@ From Coq Require Import List FSets.FMapFacts Lia. +From Equations Require Import Equations. + +Require Import FMapList. Module MapFacts := FSets.FMapFacts.Facts Map. Import ListNotations. @@ -54,6 +57,26 @@ Proof. 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) := @@ -83,7 +106,7 @@ Qed. 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 -> - distinct (map (fun '(_,_,_,y)=>y) sub_list) -> + 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 with try easy. intros. @@ -110,7 +133,7 @@ Lemma fresh_consistent: forall G0 s0 (sub_list: list (T*x*t*x)), (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 -> - distinct (map (fun '(_,_,_,y)=>y) sub_list) -> + 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 with try easy. @@ -250,9 +273,9 @@ Proof. typ_e G0 (e_var x1) T1 -> typ_e G0 (e_var_subst e0 [(x0, x1)]) T0) ;cbn; intros. - - inv H; constructor. + - inv H; simp e_var_subst_one; constructor. - inv H. - simpl. + simp e_var_subst_one. destruct (eq_x x5 x0); subst. + apply Map.find_2 in H3. apply MapFacts.add_mapsto_iff in H3. @@ -268,6 +291,7 @@ Proof. * 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 @@ -299,14 +323,409 @@ Proof. + eapply H0; eauto. Qed. +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. + +Lemma fresh_vars_first: 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 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. + inv H0. + apply Heqo. + exists x. + eapply Map.add_3; eauto. + eapply Map.add_3; eauto. + * symmetry. + apply MapFacts.not_find_in_iff in Heqo. + apply MapFacts.not_find_in_iff. + intro. + inv H0. + apply Heqo. + exists x. + eapply Map.add_3; eauto. + eapply Map.add_3; eauto. +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*t*x)), + ~ In y (map (fun '(_,_,_, y) => y) upd) -> + 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). +Admitted. + +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_alt: 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 fresh_subst_NoDup: forall e0 y sub, + fresh_vars_e [y] e0 -> + ~ In y (map (fun '(_, y) => y) sub) -> + fresh_vars_e [y] (e_var_subst e0 sub). +Admitted. + (* pipe dream: might need some stronger assumptions*) -Lemma subst_lemma: forall (T_x_t_y_list:list (T*x*t*x)) G0 e0 T0, - typ_e (fold_right (fun '(T_, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T T_) G0) G0 T_x_t_y_list) e0 T0 -> - typ_e (fold_right (fun '(T_, _, _, y) (G0 : G) => Map.add y (ctxv_T T_) G0) G0 T_x_t_y_list) - (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) - T0. +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) -> + (* needed? *) + fresh_vars_e (map (fun '(_, _, _, y) => y) T_x_t_y_list) e0 -> + 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. + induction T_x_t_y_list; intros. + - easy. + - destruct a as (((?T_,?x_),?t_),?y). + unfold e_var_subst. + simpl. + inv H0. + apply subst_lemma_one_alt. + + replace (fold_right (fun '(x', y') (e' : e) => e_var_subst_one e' x' y') e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) + with (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) by auto. + simpl in H, H1. + apply fresh_monotone_e in H1. + admit. + + + apply fresh_vars_first in H1. + apply fresh_subst_NoDup; eauto. + intro. + apply H4. + rewrite map_map in H0. + apply in_map_iff in H0. + destruct H0 as ((((?,?),?), ?), (?, ?)); subst. + apply in_map_iff. + eexists. + split; now eauto. Admitted. + Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), G_vdash_s G5 s5 -> Forall (typ_F G5) Flist -> @@ -474,7 +893,7 @@ Proof with try easy. (* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) + rewrite H5 in H9. inv H9. - apply subst_lemma. + apply subst_lemma; auto. rewrite <- fold_map_reshuffle. apply H8. Qed. diff --git a/theories/utils.v b/theories/utils.v index 1264f3b..5c8f2d6 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -7,6 +7,14 @@ 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}. From 20c6c6955038fb39d6a21246caa247c09c17f385 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Tue, 27 Feb 2024 11:41:57 +0100 Subject: [PATCH 17/18] Cleanup Proof with... --- theories/abs_functional_metatheory.v | 95 +++++++++++++++------------- 1 file changed, 51 insertions(+), 44 deletions(-) diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v index 767fe53..7049a6b 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -108,24 +108,25 @@ Lemma fresh_subG: forall G0 s0 (sub_list: list (T*x*t*x)), 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 with try easy. +Proof. intros. - induction sub_list... - destruct a as (((?T_, ?x_), ?t_), y). - inv H1. - inv H0. - pose proof IHsub_list H2 H5. - cbn. - apply subG_add; auto. - intro. + 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. + 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)), @@ -136,16 +137,17 @@ Lemma fresh_consistent: forall G0 s0 (sub_list: list (T*x*t*x)), 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 with try easy. +Proof. intros. - induction sub_list... - destruct a as (((?T_, ?x_), ?t_), y). - inv H1. - inv H2. + 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. + cbn. + intros ?y ?T_ ?. + destruct (eq_x y y0); subst. - exists t_. split... + apply Map.find_1. @@ -234,11 +236,11 @@ 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 with auto. +Proof. intros. - induction e_T_list... + induction e_T_list; auto. destruct a;cbn in *. - rewrite IHe_T_list... + now rewrite IHe_T_list. Qed. Lemma fold_map_reshuffle: forall (l: list (T*x*t*x)) G0, @@ -733,14 +735,15 @@ Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s), 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 with try easy. +Proof. 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... + exists G5; splits. + 1,2: easy. inv e0_type. destruct (s_well_typed x5 T0 H2) as (?, (?, ?)). rewrite H in H0. @@ -757,17 +760,18 @@ Proof with try easy. rewrite H3. apply in_map_iff. exists (e_5, T_5). - split... - apply in_combine_split with (2:=eq_refl)... + 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... + 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... + apply typ_func_expr. * intros. rewrite pat2_id in H8. rewrite H3 in H8. @@ -775,33 +779,35 @@ Proof with try easy. rewrite combine_app in H8... apply in_app_iff in H8. destruct H8. - -- apply subG_type with (G1:=G5)... + -- apply subG_type with (G1:=G5); auto. apply H2. apply in_map_iff. exists (e_, T_). - split... + split; auto. rewrite H3. - rewrite combine_app... { + rewrite combine_app; auto. + { eapply in_app_iff. - left... + now left. } rewrite 2 app_length. simpl. rewrite H1. reflexivity. - -- rewrite combine_app in H8... + -- 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)... + ++ apply subG_type with (G1:=G5); auto. apply H2. apply in_map_iff. exists (e_, T_). - split... + split; auto. rewrite H3. - rewrite combine_app... { + rewrite combine_app; auto. + { eapply in_app_iff. right. right. @@ -814,6 +820,7 @@ Proof with try easy. reflexivity. ++ rewrite app_nil_r. apply H1. + -- auto. -- rewrite app_nil_r. simpl. rewrite H1. @@ -826,7 +833,7 @@ Proof with try easy. apply H4. ++ rewrite map_length. rewrite H3. - rewrite 2 combine_app... + rewrite 2 combine_app; auto. ** repeat (rewrite app_length). rewrite 3 combine_length. simpl. @@ -837,7 +844,7 @@ Proof with try easy. rewrite H1. reflexivity. * rewrite app_nil_r. - rewrite combine_fst... + rewrite combine_fst; auto. rewrite map_length. rewrite H3. rewrite combine_length. @@ -886,7 +893,7 @@ Proof with try easy. rewrite map_map. apply in_map_iff. exists Txty. - split... + split; auto. destruct Txty as (((?, ?), ?), ?). now inv H10. From 951cbf1f7ed73c81a2a6ddb633150fe4176b8a2d Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Mon, 11 Mar 2024 14:22:43 +0100 Subject: [PATCH 18/18] Qed! (Kinda) --- src/abs.ott | 10 + theories/abs_defs.v | 6 + theories/abs_examples.v | 1 + theories/abs_functional_metatheory.v | 377 +++++-------------------- theories/utils.v | 395 ++++++++++++++++++++++++++- 5 files changed, 484 insertions(+), 305 deletions(-) diff --git a/src/abs.ott b/src/abs.ott index f39551c..b207231 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -108,17 +108,25 @@ 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]])) }} + | 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 + +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); @@ -181,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 ; @@ -200,5 +209,6 @@ defn F1 ... Fn , s |- fn ( e1 , ... , ei , e , e'1 , ... , e'j ) ~> s' |- fn ( e1 , ... , ei , e' , e'1 , ... , e'j ) 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 59cb328..54b6526 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -100,6 +100,10 @@ Fixpoint e_ott_ind (n:e) : P_e n := end. End e_rect. + +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); @@ -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 *) @@ -165,6 +170,7 @@ Inductive red_e : list F -> s -> e -> s -> e -> Prop := (* defn 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), (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 7049a6b..95de7b0 100644 --- a/theories/abs_functional_metatheory.v +++ b/theories/abs_functional_metatheory.v @@ -20,15 +20,13 @@ Hypothesis (vars_well_typed: forall (x_:x) (G0: G) T0, Map.find x_ G0 = Some T0 -> exists T_, T0 = ctxv_T T_). -Notation "G ⊢ e : T" := (typ_e G e T) (at level 5). -Notation "G F⊢ F" := (typ_F G F) (at level 5). -(* Notation "Fs , s ⊢ e ⇝ s' ⊢ e'" := (red_e Fs s e s' e') (at level 10). *) - 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, @@ -87,22 +85,6 @@ Definition G_vdash_s (G5 : G) (s5 : s) := Notation "G1 G⊢ s1" := (G_vdash_s G1 s1) (at level 5). -(* how is this not in MapFacts? *) -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 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 -> @@ -216,48 +198,9 @@ Proof. apply H2. Qed. -(* 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. - -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. - (* this is 9.3.8 from Types and Programming Languages *) (* it has not yet proven useful *) -Lemma subst_lemma_one: forall (x0 x1:x) G0 e0 T0 T1, +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. @@ -325,205 +268,6 @@ Proof. + eapply H0; eauto. Qed. -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. - -Lemma fresh_vars_first: 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 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. - inv H0. - apply Heqo. - exists x. - eapply Map.add_3; eauto. - eapply Map.add_3; eauto. - * symmetry. - apply MapFacts.not_find_in_iff in Heqo. - apply MapFacts.not_find_in_iff. - intro. - inv H0. - apply Heqo. - exists x. - eapply Map.add_3; eauto. - eapply Map.add_3; eauto. -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*t*x)), - ~ In y (map (fun '(_,_,_, y) => y) upd) -> - 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). -Admitted. - Lemma same_type_sub: forall (sub_list: list (x*x)) G0 e0 T0, typ_e G0 e0 T0 -> (forall x0 y0 T0, @@ -595,7 +339,7 @@ Proof. Qed. -Lemma subst_lemma_one_alt: forall G0 x0 y0 e0 Ai A, +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. @@ -681,53 +425,80 @@ Proof. - destruct H1; subst. + apply H; eauto. + apply H0; eauto. - } Qed. -Lemma fresh_subst_NoDup: forall e0 y sub, - fresh_vars_e [y] e0 -> - ~ In y (map (fun '(_, y) => y) sub) -> - fresh_vars_e [y] (e_var_subst e0 sub). -Admitted. - -(* pipe dream: might need some stronger assumptions*) 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) -> - (* needed? *) + 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. + simpl in *. inv H0. - apply subst_lemma_one_alt. - + replace (fold_right (fun '(x', y') (e' : e) => e_var_subst_one e' x' y') e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) - with (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list)) by auto. - simpl in H, H1. - apply fresh_monotone_e in H1. - admit. + 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). - + apply fresh_vars_first in H1. - apply fresh_subst_NoDup; eauto. - intro. - apply H4. - rewrite map_map in H0. - apply in_map_iff in H0. - destruct H0 as ((((?,?),?), ?), (?, ?)); subst. - apply in_map_iff. - eexists. - split; now eauto. + (* 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), G_vdash_s G5 s5 -> Forall (typ_F G5) Flist -> @@ -859,21 +630,21 @@ Proof. 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 H1 F_well_typed fn_def H0 as fn_typed. + 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). { - rewrite H5 in H9. - inv H9. + (* 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 H3. + 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 <- H10. + rewrite H7 in H11. + inv H11. rewrite map_map. apply map_ext. intros. @@ -884,25 +655,23 @@ Proof. + eapply fresh_subG; eauto. + rewrite <- fold_map. apply fresh_consistent; eauto. - (* some slightly silly reshuffling *) intros. - apply in_map_iff in H10. - destruct H10 as (Txty, (?, ?)). + apply in_map_iff in H12. + destruct H12 as (Txty, (?, ?)). apply H6. - rewrite H7. + inv H12. rewrite map_map. apply in_map_iff. exists Txty. split; auto. destruct Txty as (((?, ?), ?), ?). - now inv H10. + now inv H15. -(* here the ABS paper appeals to type preservation under substitutions, but that seems like overkill*) - + rewrite H5 in H9. - inv H9. + + rewrite H7 in H11. + inv H11. apply subst_lemma; auto. - rewrite <- fold_map_reshuffle. - apply H8. + * 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 index 5c8f2d6..5d4674f 100644 --- a/theories/utils.v +++ b/theories/utils.v @@ -1,4 +1,5 @@ From Coq Require Import List + FSets.FMapFacts Lia. Import ListNotations. @@ -47,7 +48,17 @@ Section ListLemmas. rewrite (IHl l2); auto. Qed. - (* extremely ad-hoc*) + 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 -> @@ -209,6 +220,39 @@ Section ListLemmas. 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. @@ -293,3 +337,352 @@ Section ListLemmas. 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.