From b7d9359800425aa918413c98e849b1361e3ce872 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 26 Jun 2017 20:45:23 -0400 Subject: [PATCH 01/26] defined Barendredgt's convention as function to bool --- substitution.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/substitution.v b/substitution.v index 88a38c8..46efac9 100644 --- a/substitution.v +++ b/substitution.v @@ -1078,6 +1078,23 @@ match bt with bterm lvn (ssubst_aux bnt' (var_ren blv lvn)) end. +Fixpoint checkBC {NVar: Type} +`{Deq NVar} +{Opid} (lv : list NVar) (t : (@NTerm NVar Opid)) +: bool := +match t with +| vterm v => true +| oterm o lbt => ball (map (checkBC_bt lv) lbt) +end +with checkBC_bt {NVar: Type} + `{Deq NVar} + {Opid} (lv : list NVar) +(bt: @BTerm NVar Opid) +: bool := +match bt with +| bterm blv bnt => (checkBC (blv++lv) bnt) && decide (disjoint blv lv) +end. + Fixpoint uniq_change_bvars_alpha {NVar VarCl : Type} `{Deq NVar} {fv : FreshVars NVar VarCl} @@ -1223,8 +1240,11 @@ match b with bterm lvRemaining (apply_bterm b lt) end. + Hint Rewrite @sub_filter_nil_r : SquiggleEq. +Definition inBarendredgtConvention (t:NTerm) : bool := + checkBC (free_vars t) t. Lemma ssubst_ssubst_aux_nb : (forall (t:NTerm) sub, From 16f64501b3c133467b7d2566af76869d340028d6 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Tue, 27 Jun 2017 08:17:32 -0400 Subject: [PATCH 02/26] notes about maintaining BC (Barendredgt convention). --- substitution.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/substitution.v b/substitution.v index 46efac9..cf03320 100644 --- a/substitution.v +++ b/substitution.v @@ -6618,7 +6618,37 @@ Proof using varcl freshv. destruct scs; auto. contradiction. Qed. +(** +This doesn't hold. consider the substitution in the beta reduction of +(\x.\y.x) (\y.y) --> (\y.(\y.y)) +The input was in barendredgt form, but the output is not. +We need the boundvars of [lamBody] to be distinct from [bound_vars appArg] (to maintain BC) +and [free_vars appArg] (to avoid capture) +*) +Lemma betaPreservesBC (appOpid:Opid) (lamBody appArg:NTerm) (lamVar:NVar): + let lam := bterm [lamVar] lamBody in + inBarendredgtConvention (oterm appOpid [lam ; bterm [] appArg])=true + -> inBarendredgtConvention (apply_bterm lam [appArg]) = true. +Proof using. + Local Opaque decide. + simpl. unfold inBarendredgtConvention. simpl. unfold apply_bterm. + simpl. + rwsimplC. intros Hyp. + setoid_rewrite decide_true in Hyp at 2;[| disjoint_reasoningv]. + simpl. ring_simplify in Hyp. repeat rewrite andb_true_iff in Hyp. + repnd. + dands. +Abort. +(* +Section Test. + Variable l:Opid. + Let f := (oterm l [bterm [nvarx] (oterm l [bterm [nvary] (vterm nvarx)])]). + Let arg := (oterm l [bterm [nvary] (vterm nvary)]). + Eval compute in (checkBC [] f). (* vars need to be concrete for this to run *) +End Test. + *) + End SubstGeneric2. From ce675c6402cce69a15ba1c8639e3916509736673 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Tue, 27 Jun 2017 19:50:28 -0400 Subject: [PATCH 03/26] preservation of barandredgt convention --- substitution.v | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/substitution.v b/substitution.v index cf03320..544f684 100644 --- a/substitution.v +++ b/substitution.v @@ -6640,6 +6640,7 @@ Proof using. repnd. dands. Abort. + (* Section Test. Variable l:Opid. @@ -6649,6 +6650,54 @@ Section Test. End Test. *) +Definition bcSubst (t:NTerm) (sub: Substitution) : NTerm := + let fvSub := flat_map free_vars (range sub) in + let tp := change_bvars_alpha fvSub t in + ssubst_aux tp sub. + +Lemma betaPreservesBC (lamVar:NVar) (appArg lamBody:NTerm) lv: + disjoint (all_vars appArg) (bound_vars lamBody) + -> checkBC lv appArg = true + -> checkBC lv lamBody = true + -> checkBC lv (ssubst_aux lamBody [(lamVar, appArg)]) = true. +Proof using. + revert lv. + induction lamBody using NTerm_better_ind; + [intros; simpl; cases_if; auto; fail|]. + simpl. intros lv Hdis Hca Hcl. + rewrite map_map. unfold compose. simpl. +Abort. + +Lemma betaPreservesBC (lamVar:NVar) (appArg:NTerm): + (forall (lamBody:NTerm) lv, + disjoint (all_vars appArg) (bound_vars lamBody) + -> checkBC lv appArg = true + -> checkBC lv lamBody = true + -> checkBC lv (ssubst_aux lamBody [(lamVar, appArg)]) = true) + * + (forall (lamBody:BTerm) lv, + disjoint (all_vars appArg) (bound_vars_bterm lamBody) + -> checkBC lv appArg = true + -> checkBC_bt lv lamBody = true + -> checkBC_bt lv (ssubst_bterm_aux lamBody [(lamVar, appArg)]) = true). +Proof using. + apply NTerm_BTerm_ind; + [intros; simpl; cases_if; auto; fail| |]. +- simpl. intros o lbt Hind lv Hdis Hca Hcl. + rewrite map_map. unfold compose. simpl. + apply ball_map_true. + rewrite ball_map_true in Hcl. + intros ? Hin. specialize (Hind _ Hin lv). + rewrite disjoint_flat_map_r in Hdis. + apply Hind; auto; fail. +- intros blv bnt Hind lv Hdis Hca Hcl. + simpl in *. + apply andb_true. + apply andb_true in Hcl. repnd. + dands;[| assumption]. + cases_if;[rewrite ssubst_aux_nil; assumption|]. + apply Hind; auto;[disjoint_reasoningv|]. +Abort. End SubstGeneric2. @@ -6658,6 +6707,7 @@ Proof using. induction sub; auto. simpl. f_equal. auto. Qed. + Lemma map_sub_range_combine {NVar} {gtsi} {gtso} : forall (f : @NTerm NVar gtsi -> @NTerm NVar gtso) lv nt, map_sub_range f (combine lv nt) = combine lv (map f nt). Proof using. From fe63cc3441ab0ca968f8c625c9f1a012b9087172 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Tue, 27 Jun 2017 23:48:13 -0400 Subject: [PATCH 04/26] lemmas about barendredgt convention. towards preservation by beta. also removed unnecessary assumptions in some var lemmas. the firstorder tactic unnecessarily uses everything. --- substitution.v | 48 +++++++++++++++++++++++++++++++++++++++++++++++- varInterface.v | 14 +++++++++----- 2 files changed, 56 insertions(+), 6 deletions(-) diff --git a/substitution.v b/substitution.v index 544f684..66249a9 100644 --- a/substitution.v +++ b/substitution.v @@ -6668,6 +6668,48 @@ Proof using. rewrite map_map. unfold compose. simpl. Abort. +Lemma checkBCEqset : + (forall (appArg:NTerm) lv1 lv2, + eq_set lv1 lv2 -> checkBC lv1 appArg = checkBC lv2 appArg) + * + (forall (appArg:BTerm) lv1 lv2, + eq_set lv1 lv2 -> checkBC_bt lv1 appArg = checkBC_bt lv2 appArg). +Proof using. + apply NTerm_BTerm_ind; + [refl| |]. +- intros ? ? Hind ? ? Heq. simpl in *. f_equal. + apply eq_maps. eauto. +- intros blv ? Hind ? ? Heq. simpl in *. + f_equal; + [| eapply proper_decider2;[| apply eq_set_refl | apply Heq]; + eauto with typeclass_instances]. + apply Hind. rewrite Heq. reflexivity. +Qed. + +Lemma checkBCStrengthen blv : + (forall (appArg:NTerm) lv, + disjoint (all_vars appArg) blv -> checkBC lv appArg = true -> checkBC (blv ++ lv) appArg = true) + * + (forall (appArg:BTerm) lv, + disjoint (all_vars_bt appArg) blv -> checkBC_bt lv appArg = true -> checkBC_bt (blv ++ lv) appArg = true). +Proof using. + clear dependent varcl. clear freshv. + apply NTerm_BTerm_ind; + [refl| |]. +- intros ? ? Hind lv Hdis. simpl in *. rewrite all_vars_ot in Hdis. + do 2 rewrite ball_map_true. rewrite disjoint_flat_map_l in Hdis. eauto. +- intros bblv bnt Hind lv Hdis. simpl. rewrite allvars_bterm in Hdis. + specialize (Hind (bblv++lv)). do 2 rewrite andb_true. + do 2 rewrite Decidable_spec. + intros Hc. repnd. + dands;[| disjoint_reasoningv2];[]. + rewrite <- Hind; auto;[| disjoint_reasoningv2];[]. + apply checkBCEqset. + do 2 rewrite app_assoc. + apply eqsetv_app; [| refl]. + apply eqset_app_comm. +Qed. + Lemma betaPreservesBC (lamVar:NVar) (appArg:NTerm): (forall (lamBody:NTerm) lv, disjoint (all_vars appArg) (bound_vars lamBody) @@ -6697,8 +6739,12 @@ Proof using. dands;[| assumption]. cases_if;[rewrite ssubst_aux_nil; assumption|]. apply Hind; auto;[disjoint_reasoningv|]. -Abort. + disjoint_reasoning. + revert Hca. revert Hdis0. clear. + apply checkBCStrengthen. +Qed. + End SubstGeneric2. Lemma dom_sub_map_range {NVar} {gtsi} {gtso} : forall (f : @NTerm NVar gtsi -> @NTerm NVar gtso) sub, diff --git a/varInterface.v b/varInterface.v index f93c84e..8504fbc 100644 --- a/varInterface.v +++ b/varInterface.v @@ -358,7 +358,7 @@ Lemma eqsetv_cons_l_iff : forall v vs1 vs2, eq_set (v :: vs1) vs2 <=> (LIn v vs2 # eqsetv (remove_nvar vs1 v) (remove_nvar vs2 v)). -Proof. +Proof using. sp. do 2 (rewrite eqsetv_prop). split; intro i; sp; allrw in_remove_nvar; allsimpl. rw <- i; sp. @@ -368,9 +368,10 @@ Proof. split; sp; subst; sp. destruct (eq_var_dec v x); subst; sp. gen_some x; allrw in_remove_nvar. - discover; sp. firstorder. + discover; sp. clear dependent VClass. firstorder. destruct (eq_var_dec v x); subst; sp. gen_some x; allrw in_remove_nvar. + clear dependent VClass. discover; sp; firstorder. Qed. @@ -1008,8 +1009,9 @@ Lemma eqsetv_remove_nvars : eqsetv la lb -> eqsetv ra rb -> eqsetv (remove_nvars la ra) (remove_nvars lb rb). -Proof. +Proof using. unfold eq_set, subset. setoid_rewrite in_remove_nvars. + clear dependent VClass. firstorder. Qed. @@ -1018,9 +1020,10 @@ Lemma eqsetv_app {A}: eqsetv la lb -> eqsetv ra rb -> eqsetv (app la ra) (app lb rb). -Proof. +Proof using. introv Ha Hb. unfold eq_set, subset. setoid_rewrite in_app_iff. + clear dependent VClass. firstorder. Qed. @@ -1071,10 +1074,11 @@ Proof. sp. Qed. Lemma subsetv_eqsetv {A}: forall s1 s2 s3, subsetv s1 s2 -> eqsetv s1 s3 -> @subsetv A s3 s2. -Proof. +Proof using. introv s e. unfold eq_set in *. unfold subset in *. + clear dependent VClass. firstorder. Qed. From f53f7bd226f43657f18e38d82902038b39acdf66 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Wed, 28 Jun 2017 08:28:48 -0400 Subject: [PATCH 05/26] fixes, strengthened some lemmas --- substitution.v | 27 +++++++++++++++++++-------- 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/substitution.v b/substitution.v index 66249a9..1e1c062 100644 --- a/substitution.v +++ b/substitution.v @@ -6651,7 +6651,7 @@ End Test. *) Definition bcSubst (t:NTerm) (sub: Substitution) : NTerm := - let fvSub := flat_map free_vars (range sub) in + let fvSub := flat_map all_vars (range sub) in let tp := change_bvars_alpha fvSub t in ssubst_aux tp sub. @@ -6688,17 +6688,17 @@ Qed. Lemma checkBCStrengthen blv : (forall (appArg:NTerm) lv, - disjoint (all_vars appArg) blv -> checkBC lv appArg = true -> checkBC (blv ++ lv) appArg = true) + disjoint (bound_vars appArg) blv -> checkBC lv appArg = true -> checkBC (blv ++ lv) appArg = true) * (forall (appArg:BTerm) lv, - disjoint (all_vars_bt appArg) blv -> checkBC_bt lv appArg = true -> checkBC_bt (blv ++ lv) appArg = true). + disjoint (bound_vars_bterm appArg) blv -> checkBC_bt lv appArg = true -> checkBC_bt (blv ++ lv) appArg = true). Proof using. clear dependent varcl. clear freshv. apply NTerm_BTerm_ind; [refl| |]. -- intros ? ? Hind lv Hdis. simpl in *. rewrite all_vars_ot in Hdis. +- intros ? ? Hind lv Hdis. simpl in *. do 2 rewrite ball_map_true. rewrite disjoint_flat_map_l in Hdis. eauto. -- intros bblv bnt Hind lv Hdis. simpl. rewrite allvars_bterm in Hdis. +- intros bblv bnt Hind lv Hdis. simpl in *. specialize (Hind (bblv++lv)). do 2 rewrite andb_true. do 2 rewrite Decidable_spec. intros Hc. repnd. @@ -6712,13 +6712,13 @@ Qed. Lemma betaPreservesBC (lamVar:NVar) (appArg:NTerm): (forall (lamBody:NTerm) lv, - disjoint (all_vars appArg) (bound_vars lamBody) + disjoint (bound_vars appArg) (bound_vars lamBody) -> checkBC lv appArg = true -> checkBC lv lamBody = true -> checkBC lv (ssubst_aux lamBody [(lamVar, appArg)]) = true) * (forall (lamBody:BTerm) lv, - disjoint (all_vars appArg) (bound_vars_bterm lamBody) + disjoint (bound_vars appArg) (bound_vars_bterm lamBody) -> checkBC lv appArg = true -> checkBC_bt lv lamBody = true -> checkBC_bt lv (ssubst_bterm_aux lamBody [(lamVar, appArg)]) = true). @@ -6744,7 +6744,18 @@ Proof using. apply checkBCStrengthen. Qed. - + +Lemma betaPreservesBC2 (lamVar:NVar) (appArg:NTerm): + forall (lamBody:NTerm) lv, + checkBC lv appArg = true + -> checkBC lv lamBody = true + -> checkBC lv (bcSubst lamBody [(lamVar, appArg)]) = true. +Proof using. + unfold bcSubst. + intros. simpl. rewrite app_nil_r. + apply betaPreservesBC; auto. +Abort. + End SubstGeneric2. Lemma dom_sub_map_range {NVar} {gtsi} {gtso} : forall (f : @NTerm NVar gtsi -> @NTerm NVar gtso) sub, From a657ac6ea8dd953eabd71d7caf1d63e43c1cf700 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Wed, 28 Jun 2017 16:39:23 -0400 Subject: [PATCH 06/26] lemmas about app of remove, checkBC --- list.v | 18 +++++++++++++++++- substitution.v | 50 +++++++++++++++++++++++++++++++++++++++----------- 2 files changed, 56 insertions(+), 12 deletions(-) diff --git a/list.v b/list.v index a265b23..2256f10 100644 --- a/list.v +++ b/list.v @@ -4026,4 +4026,20 @@ Proof using. rewrite IHla. split; intros; repnd; dands; auto; noRepDis1. constructor; noRepDis1. -Qed. +Qed. + + +Lemma diffAddCancel {A:Type} {deq: Deq A} (lr lv : list A): +subset lv (lr ++ (lremove lr lv)). +Proof using. + unfold eq_set, subset. + setoid_rewrite in_app_iff. + setoid_rewrite in_diff. firstorder. + destruct (decideP (In x lr)); firstorder. +Qed. + +Lemma removeConsCancel {A:Type} {deq: Deq A} (r:A)(lv : list A): + subset lv (r::(remove r lv)). +Proof using. + apply (diffAddCancel [r]). +Qed. diff --git a/substitution.v b/substitution.v index 1e1c062..af1c413 100644 --- a/substitution.v +++ b/substitution.v @@ -6655,18 +6655,46 @@ Definition bcSubst (t:NTerm) (sub: Substitution) : NTerm := let tp := change_bvars_alpha fvSub t in ssubst_aux tp sub. -Lemma betaPreservesBC (lamVar:NVar) (appArg lamBody:NTerm) lv: - disjoint (all_vars appArg) (bound_vars lamBody) - -> checkBC lv appArg = true - -> checkBC lv lamBody = true - -> checkBC lv (ssubst_aux lamBody [(lamVar, appArg)]) = true. + +Lemma checkBCSubset : + (forall (appArg:NTerm) lvBig lv, + subset lv lvBig -> checkBC lvBig appArg = true -> checkBC lv appArg =true) + * + (forall (appArg:BTerm) lvBig lv, + subset lv lvBig -> checkBC_bt lvBig appArg = true -> checkBC_bt lv appArg = true). Proof using. - revert lv. - induction lamBody using NTerm_better_ind; - [intros; simpl; cases_if; auto; fail|]. - simpl. intros lv Hdis Hca Hcl. - rewrite map_map. unfold compose. simpl. -Abort. + apply NTerm_BTerm_ind; + [refl| |]. +- intros ? ? Hind ? ? Hsub Hc. simpl in *. + rewrite ball_map_true in *. eauto. +- intros blv ? Hind ? ? Hsub Hc. simpl in *. + rewrite andb_true in *. repnd. rewrite Decidable_spec in Hc. rewrite Decidable_spec. + rewrite disjoint_sym in Hc. + rewrite disjoint_sym. + dands;[| eauto using subset_disjoint; fail]. + revert Hc0. + apply Hind. + apply subsetvAppLR; eauto. +Qed. + +Lemma checkBCdisjoint: +(forall (A:NTerm) (lv: list NVar), +checkBC lv A = true +-> disjoint lv (bound_vars A)) +* +(forall (A:BTerm) (lv: list NVar), +checkBC_bt lv A = true +-> disjoint lv (bound_vars_bterm A)). +Proof using. + apply NTerm_BTerm_ind; + [simpl; intros; disjoint_reasoningv2| |];[|]. +- intros ? ? Hind ? Hc. simpl in *. rewrite disjoint_flat_map_r. + rewrite ball_map_true in Hc. eauto. +- intros blv bnt Hind ? Hc. simpl in *. rewrite andb_true in Hc. repnd. + rewrite Decidable_spec in Hc. disjoint_reasoningv. + apply Hind. revert Hc0. apply (fst checkBCSubset). + apply subset_app_l. eauto. +Qed. Lemma checkBCEqset : (forall (appArg:NTerm) lv1 lv2, From d8cfff23543690b1d3cc2faad4a5a5fcb6523e5f Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Thu, 29 Jun 2017 10:27:06 -0400 Subject: [PATCH 07/26] checkBC of change_bvars_alpha. removed 1 unnecessary assumption in a previous lemma (unsafe substitution vars for vars preserves bvars) --- alphaeq.v | 60 +++++++++++++++++++++++++++++++++++++++++++++----- substitution.v | 46 ++++++++++++++++++++++++++------------ 2 files changed, 86 insertions(+), 20 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index b6caff0..3960251 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -295,8 +295,7 @@ SearchAbout @map @combine @prod. Focus 2. introv Hin Hc. rewrite boundvars_ssubst_aux_vars in Hc; auto. - rewrite boundvars_ssubst_aux_vars in Hc; auto; - [|congruence]. + rewrite boundvars_ssubst_aux_vars in Hc; auto. apply in_app_iff in Hc; auto. dorn Hc; [apply Hdis0 in Hin|apply Hdis in Hin];sp; fail. @@ -443,8 +442,7 @@ Proof using. Focus 2. introv Hin Hc. rewrite boundvars_ssubst_aux_vars in Hc; auto. - rewrite boundvars_ssubst_aux_vars in Hc; auto; - [|congruence]. + rewrite boundvars_ssubst_aux_vars in Hc; auto. apply in_app_iff in Hc; auto. dorn Hc; [apply Hdis0 in Hin|apply Hdis in Hin];sp; fail. @@ -542,7 +540,7 @@ Proof using. inverts Hal as Ha1 Ha2 Ha3 Ha4 Ha5. apply (alpha_eq3_change_avoidvars _ (lv4++lv++lva)) in Ha5. apply alpha3_ssubst_aux_allvars_congr2 in Ha5;[| congruence | ]. - Focus 2. rewrite boundvars_ssubst_aux_vars; [|congruence]. + Focus 2. rewrite boundvars_ssubst_aux_vars. rewrite boundvars_ssubst_aux_vars;disjoint_reasoningv. rewrite ssubst_aux_nest_vars_same in Ha5;auto; [| congruence| disjoint_reasoningv| disjoint_reasoningv]. @@ -740,6 +738,56 @@ Proof using. eauto. Qed. + +Lemma change_bvars_alpha_checkbc_aux: forall lv, + (forall nt:NTerm, + let nt' := change_bvars_alpha lv nt in + checkBC ((*free_vars nt++*)lv) nt' = true) + * (forall bt:BTerm, + let bt' := change_bvars_alphabt lv bt in + checkBC_bt ((*free_vars_bterm bt ++ *)lv) bt' = true). +Proof using varclass. + intros. apply NTerm_BTerm_ind; + [intro v; cpx| |]. +- intros ? ? Hind. + simpl. rewrite ball_map_true. + intros x Hin. apply in_map_iff in Hin. exrepnd. subst. + eauto. + +Local Opaque decide. +- intros blv bnt Hind. + simpl. + addFreshVarsSpec2 vn pp. + exrepnd. allsimpl. + rewrite decide_true;[ring_simplify| disjoint_reasoningv2]. +Local Transparent decide. + rewrite (fst (boundvars_substvars_checkbc2 blv vn)). + apply (checkBCStrengthen vn);[| assumption]. + disjoint_reasoningv. +Qed. + + +Lemma betaPreservesBC2 o (lamVar:NVar) (lamBody appArg:NTerm) lv: + let lam := bterm [lamVar] lamBody in + let appT := (oterm o [lam ; bterm [] appArg]) in + subset (free_vars appT) lv + -> checkBC lv appT =true + -> checkBC lv (bcSubst lamBody [(lamVar, appArg)]) = true. +Proof using. + Local Opaque decide. + simpl. rewrite app_nil_r. + setoid_rewrite decide_true at 2;[| disjoint_reasoningv2]. + intros Hs Hc. + ring_simplify in Hc. + repeat rewrite andb_true in Hc. repnd. + unfold bcSubst. + apply betaPreservesBC; auto; simpl; rewrite app_nil_r. + - admit. (*easy. *) + - (* impossible to prove. [change_bvars_alpha] does not have access to [lv] currently. + [lv] may have variables bound above in the subtree, but are not free in [lamBody] or [appArg]. + Nothing prevents [change_bvars_alpha] from picking the same variables again. *) +Abort. + Lemma alpha_eq_cons : forall o1 o2 lbt1 lbt2 b1 b2, alpha_eq_bterm b1 b2 -> alpha_eq (oterm o1 lbt1) (oterm o1 lbt2) @@ -811,7 +859,7 @@ Proof using. addFreshVarsSpec2 vn pp. exrepnd. allsimpl. dands. - + setoid_rewrite boundvars_ssubst_aux_vars;[|congruence]. + + setoid_rewrite boundvars_ssubst_aux_vars. apply NoDupApp; noRepDis. + introv Hin Hinc. rename t into vv. diff --git a/substitution.v b/substitution.v index af1c413..1b29f85 100644 --- a/substitution.v +++ b/substitution.v @@ -5152,12 +5152,11 @@ Qed. Lemma boundvars_ssubst_aux_vars: forall nt lvi lvo, - length lvi = length lvo - -> bound_vars (ssubst_aux nt (var_ren lvi lvo)) + bound_vars (ssubst_aux nt (var_ren lvi lvo)) = bound_vars nt. Proof using. clear hdeq. - nterm_ind1s nt as [v | o lbt Hind] Case; introv Hl; auto. + nterm_ind1s nt as [v | o lbt Hind] Case; intros ? ? . auto. - Case "vterm". simpl. rewrite sub_lmap_find. destruct (lmap_find deq_nvar (var_ren lvi lvo) v) as [s1s| n1n];auto; exrepnd. allsimpl. apply in_var_ren in s1s0. exrepnd. subst. auto. @@ -5173,7 +5172,7 @@ Qed. Lemma boundvars_ssubst_vars: forall nt lvi lvo, - length lvi = length lvo + length lvi = length lvo (*not necessary although it may complicate the proof a bit*) -> disjoint lvo (bound_vars nt) -> bound_vars (ssubst nt (var_ren lvi lvo)) = bound_vars nt. @@ -6651,7 +6650,7 @@ End Test. *) Definition bcSubst (t:NTerm) (sub: Substitution) : NTerm := - let fvSub := flat_map all_vars (range sub) in + let fvSub := (free_vars t) ++ flat_map all_vars (range sub) in let tp := change_bvars_alpha fvSub t in ssubst_aux tp sub. @@ -6773,16 +6772,35 @@ Proof using. Qed. -Lemma betaPreservesBC2 (lamVar:NVar) (appArg:NTerm): - forall (lamBody:NTerm) lv, - checkBC lv appArg = true - -> checkBC lv lamBody = true - -> checkBC lv (bcSubst lamBody [(lamVar, appArg)]) = true. +Lemma boundvars_substvars_checkbc: + (forall (nt:NTerm) lva vsub, + checkBC lva (ssubst_aux nt (ALMapRange vterm vsub)) + = checkBC lva nt)* + (forall (nt:BTerm) lva vsub, + checkBC_bt lva (ssubst_bterm_aux nt (ALMapRange vterm vsub)) + = checkBC_bt lva nt). Proof using. - unfold bcSubst. - intros. simpl. rewrite app_nil_r. - apply betaPreservesBC; auto. -Abort. + clear hdeq. apply NTerm_BTerm_ind. +- intros ? ? ?. simpl. unfold sub_find. rewrite ALMapRangeFindCommute. + dALFind s; refl. +- intros ? ? Hind ? ?. simpl. f_equal. rewrite map_map. apply eq_maps. + intros ? Hin. unfold compose. simpl. eauto. +- intros blv bnt Hind ? ?. simpl. f_equal. + unfold sub_filter. rewrite ALMapRangeFilterCommute. apply Hind. +Qed. + +Lemma boundvars_substvars_checkbc2 lvi lvo : + (forall (nt:NTerm) lva, + checkBC lva (ssubst_aux nt (var_ren lvi lvo)) + = checkBC lva nt)* + (forall (nt:BTerm) lva, + checkBC_bt lva (ssubst_bterm_aux nt (var_ren lvi lvo)) + = checkBC_bt lva nt). +Proof using. + clear hdeq. intros. unfold var_ren. rewrite combine_of_map_snd. + split; intros; apply boundvars_substvars_checkbc. +Qed. + End SubstGeneric2. From 163892082b56abf59a8704d2ae50024f1456a20b Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Thu, 29 Jun 2017 11:05:38 -0400 Subject: [PATCH 08/26] new bcsubst: with new input denoting outside bvars. bcsubst preserves checkBC. --- alphaeq.v | 29 +++++++++++++++-------------- substitution.v | 12 ++++++++---- 2 files changed, 23 insertions(+), 18 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index 3960251..086467e 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -766,27 +766,28 @@ Local Transparent decide. disjoint_reasoningv. Qed. - -Lemma betaPreservesBC2 o (lamVar:NVar) (lamBody appArg:NTerm) lv: +Lemma bcSubstBetaPreservesBC o (lamVar:NVar) (lamBody appArg:NTerm) lv: let lam := bterm [lamVar] lamBody in let appT := (oterm o [lam ; bterm [] appArg]) in - subset (free_vars appT) lv - -> checkBC lv appT =true - -> checkBC lv (bcSubst lamBody [(lamVar, appArg)]) = true. -Proof using. + checkBC lv appT =true + -> checkBC lv (bcSubst lv lamBody [(lamVar, appArg)]) = true. +Proof using varclass. Local Opaque decide. - simpl. rewrite app_nil_r. + simpl. setoid_rewrite decide_true at 2;[| disjoint_reasoningv2]. - intros Hs Hc. + intros Hc. ring_simplify in Hc. repeat rewrite andb_true in Hc. repnd. unfold bcSubst. - apply betaPreservesBC; auto; simpl; rewrite app_nil_r. - - admit. (*easy. *) - - (* impossible to prove. [change_bvars_alpha] does not have access to [lv] currently. - [lv] may have variables bound above in the subtree, but are not free in [lamBody] or [appArg]. - Nothing prevents [change_bvars_alpha] from picking the same variables again. *) -Abort. + simpl. rewrite app_nil_r. + pose proof (fst (change_bvars_alpha_checkbc_aux (lv ++ bound_vars appArg)) lamBody) as Hbc. + pose proof (fst (change_bvars_alpha_spec_aux (lv ++ bound_vars appArg)) lamBody) as Hsp. + simpl in *. revert Hbc Hsp. + generalize (change_bvars_alpha (lv ++ bound_vars appArg) lamBody). + intros tc ? ?. repnd. + apply betaPreservesBC; auto; simpl;[disjoint_reasoningv2|]. + revert Hbc. apply (fst checkBCSubset). apply subset_app_r. reflexivity. +Qed. Lemma alpha_eq_cons : forall o1 o2 lbt1 lbt2 b1 b2, alpha_eq_bterm b1 b2 diff --git a/substitution.v b/substitution.v index 1b29f85..abdfa90 100644 --- a/substitution.v +++ b/substitution.v @@ -6649,10 +6649,6 @@ Section Test. End Test. *) -Definition bcSubst (t:NTerm) (sub: Substitution) : NTerm := - let fvSub := (free_vars t) ++ flat_map all_vars (range sub) in - let tp := change_bvars_alpha fvSub t in - ssubst_aux tp sub. Lemma checkBCSubset : @@ -6801,6 +6797,14 @@ Proof using. split; intros; apply boundvars_substvars_checkbc. Qed. +Definition bcSubst (lva: list NVar) (t:NTerm) (sub: Substitution) : NTerm := + (* in intended apps, callee is supposed to ensure that free vars are supposed to be in [lva]. + [lva] is supposed to contain all enclosing binders of the subtree where t and [sub] are located, + during reduction.*) + let avoid := lva ++ flat_map bound_vars (range sub) in + let tp := change_bvars_alpha avoid t in + ssubst_aux tp sub. + End SubstGeneric2. From b1a882ebc2735db97bec7264846e300d3ea2d54b Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Thu, 29 Jun 2017 13:45:45 -0400 Subject: [PATCH 09/26] needed more freshness on bcSubst --- alphaeq.v | 56 +++++++++++++++++++++++++++++++++++++++++++++----- substitution.v | 2 +- 2 files changed, 52 insertions(+), 6 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index 086467e..29d5365 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -780,13 +780,14 @@ Proof using varclass. repeat rewrite andb_true in Hc. repnd. unfold bcSubst. simpl. rewrite app_nil_r. - pose proof (fst (change_bvars_alpha_checkbc_aux (lv ++ bound_vars appArg)) lamBody) as Hbc. - pose proof (fst (change_bvars_alpha_spec_aux (lv ++ bound_vars appArg)) lamBody) as Hsp. + pose proof (fst (change_bvars_alpha_checkbc_aux (lamVar::lv ++ bound_vars appArg)) lamBody) as Hbc. + pose proof (fst (change_bvars_alpha_spec_aux (lamVar::lv ++ bound_vars appArg)) lamBody) as Hsp. simpl in *. revert Hbc Hsp. - generalize (change_bvars_alpha (lv ++ bound_vars appArg) lamBody). + generalize (change_bvars_alpha (lamVar::lv ++ bound_vars appArg) lamBody). intros tc ? ?. repnd. apply betaPreservesBC; auto; simpl;[disjoint_reasoningv2|]. - revert Hbc. apply (fst checkBCSubset). apply subset_app_r. reflexivity. + revert Hbc. apply (fst checkBCSubset). apply subset_cons1. + apply subset_app_r. reflexivity. Qed. Lemma alpha_eq_cons : forall o1 o2 lbt1 lbt2 b1 b2, @@ -942,6 +943,35 @@ Proof using varclass. eauto. Qed. +Lemma change_bvars_alpha_spec2: forall (nt : NTerm) (lv : list NVar), + let cc := change_bvars_alpha lv nt in + checkBC lv cc = true + /\ disjoint lv (bound_vars cc) + /\ alpha_eq nt cc + /\ (forall vc, varsOfClass (bound_vars nt) vc + -> varsOfClass (bound_vars cc) vc). +Proof using. simpl. + intros. dands; intros; + try apply change_bvars_alpha_spec_varclass; + try apply change_bvars_alpha_checkbc_aux; + try apply change_bvars_alpha_spec_aux. assumption. +Qed. + +Lemma change_bvars_alphabt_spec2: forall (nt : BTerm) (lv : list NVar), + let cc := change_bvars_alphabt lv nt in + checkBC_bt lv cc = true + /\ disjoint lv (bound_vars_bterm cc) + /\ alpha_eq_bterm nt (change_bvars_alphabt lv nt) + /\ (forall vc, varsOfClass (bound_vars_bterm nt) vc + -> varsOfClass (bound_vars_bterm cc) vc). +Proof using. simpl. + intros. dands; intros; + try apply change_bvars_alpha_spec_varclass; + try apply change_bvars_alpha_checkbc_aux; + try apply change_bvars_alpha_spec_aux. assumption. +Qed. + + (* Lemma change_bvars_alpha_spec_varclass: forall lv vc, (forall nt, varsOfClass (bound_vars nt) vc @@ -956,6 +986,13 @@ match goal with remember (change_bvars_alphabt lv nt) as cb; simpl in Hn end. +Ltac add_changebvar_spec4 cb Hn:= +match goal with +| [ |- context[change_bvars_alpha ?lv ?nt] ] => pose proof (change_bvars_alpha_spec2 nt lv) as Hn; + remember (change_bvars_alpha lv nt) as cb; simpl in Hn +| [ |- context[change_bvars_alphabt ?lv ?nt] ] => pose proof (change_bvars_alphabt_spec2 lv nt) as Hn; + remember (change_bvars_alphabt lv nt) as cb; simpl in Hn +end. Theorem alphaeqbt_preserves_wf: forall bt1 bt2, alpha_eq_bterm bt1 bt2 -> (bt_wf bt2 <=> bt_wf bt1). @@ -4287,4 +4324,13 @@ autorewrite with SquiggleEq; apply no_repeats_as_disjoint in H; destruct H as [Hnrd H] end); disjoint_reasoningv; -repeat rewrite in_single_iff in *; subst; try tauto. \ No newline at end of file +repeat rewrite in_single_iff in *; subst; try tauto. + + +Ltac add_changebvar_spec4 cb Hn:= +match goal with +| [ |- context[change_bvars_alpha ?lv ?nt] ] => pose proof (change_bvars_alpha_spec2 nt lv) as Hn; + remember (change_bvars_alpha lv nt) as cb; simpl in Hn +| [ |- context[change_bvars_alphabt ?lv ?nt] ] => pose proof (change_bvars_alphabt_spec2 lv nt) as Hn; + remember (change_bvars_alphabt lv nt) as cb; simpl in Hn +end. diff --git a/substitution.v b/substitution.v index abdfa90..2b205e7 100644 --- a/substitution.v +++ b/substitution.v @@ -6801,7 +6801,7 @@ Definition bcSubst (lva: list NVar) (t:NTerm) (sub: Substitution) : NTerm := (* in intended apps, callee is supposed to ensure that free vars are supposed to be in [lva]. [lva] is supposed to contain all enclosing binders of the subtree where t and [sub] are located, during reduction.*) - let avoid := lva ++ flat_map bound_vars (range sub) in + let avoid := (dom_sub sub) ++ lva ++ flat_map bound_vars (range sub) in let tp := change_bvars_alpha avoid t in ssubst_aux tp sub. From b7e3f7af6068309428d921fbc438e98a5b6eae16 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 07:49:48 -0400 Subject: [PATCH 10/26] WIP. when do functions preserve alpha equality --- alphaeq.v | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/alphaeq.v b/alphaeq.v index 29d5365..f2292e1 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4156,6 +4156,26 @@ Proof. Qed. + +Lemma var_rel_bc_alpha (f:NVar -> NVar): + (forall t, + (forall v:NVar, In v (free_vars t) -> f v =v) + -> checkBC (free_vars t) (tvmap f t) = true + -> alpha_eq t (tvmap f t))* + (forall t, + (forall v:NVar, In v (free_vars_bterm t) -> f v =v) + -> checkBC_bt (free_vars_bterm t) (tvmap_bterm f t) = true + -> alpha_eq_bterm t (tvmap_bterm f t)). +Proof using. + apply NTerm_BTerm_ind; + [ intros v Hin Hc; unfold tvmap; simpl; rewrite Hin; auto; simpl; cpx | |]. +- intros ? ? Hind Hin Hc. unfold tvmap. simpl. unfold id. + constructor;[autorewrite with list; auto|]. admit. (* easy *) +- intros ? ? Hind Hin Hc. unfold tvmap_bterm. simpl. simpl in Hc. + apply andb_true in Hc. repnd. SearchAbout decide. + apply prove_alpha_bterm2. + SearchAbout alpha_eq_bterm. + End AlphaGeneric. Lemma alpha_eq_map_bt_op @@ -4334,3 +4354,26 @@ match goal with | [ |- context[change_bvars_alphabt ?lv ?nt] ] => pose proof (change_bvars_alphabt_spec2 lv nt) as Hn; remember (change_bvars_alphabt lv nt) as cb; simpl in Hn end. + + + +Section AlphaPres. + +Context {NVar VarClass Opid1 Opid2} {deqnvar : Deq NVar} {varcl freshv} + {varclass: @VarType NVar VarClass deqnvar varcl freshv} + {hdeq1 : Deq Opid1} {hdeq2 : Deq Opid2} + {gts1 : GenericTermSig Opid1} + {gts2 : GenericTermSig Opid2}. + +Variable f: (@NTerm NVar Opid1) -> (@NTerm NVar Opid2). + +Hypothesis fVar : forall (v:NVar), alpha_eq (f (vterm v)) (f (vterm v)). + +Lemma preservesAlphaBC lv (t1 t2: @NTerm NVar Opid1) : + checkBC lv t1 = true + -> checkBC lv t2 = true + -> alpha_eq t1 t2 -> alpha_eq (f t1) (f t2). +Proof using. + intros H1c H2c Hal. induction Hal;[ apply fVar |]. +Abort. +End AlphaPres. \ No newline at end of file From 0e312b71e0c012f6a80f3b3b06e99a6913e909ea Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 08:53:48 -0400 Subject: [PATCH 11/26] need to add an invariant for ssubst_aux = tvmap --- alphaeq.v | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/alphaeq.v b/alphaeq.v index f2292e1..17b0147 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4155,9 +4155,31 @@ Proof. assumption. Qed. +Require Import AssociationList. +SearchAbout AssocList. +(* Move to AssocList *) +Definition ALFindEndo {Key:Type} {d:Deq Key} (sub: AssocList Key Key) (k:Key) : Key := + ALFindDef sub k k. -Lemma var_rel_bc_alpha (f:NVar -> NVar): +Lemma var_ren_vmap : + (forall t lv sub, + checkBC lv t = true + -> tvmap (ALFindEndo sub) t = ssubst_aux t (ALMapRange vterm sub))* + (forall t lv sub, + checkBC_bt lv t = true + -> tvmap_bterm (ALFindEndo sub) t = ssubst_bterm_aux t (ALMapRange vterm sub)). +Proof using. + apply NTerm_BTerm_ind. +- simpl. intros v lv sub _. unfold tvmap, ALFindEndo, ALFindDef, sub_find. simpl. + rewrite ALMapRangeFindCommute. destruct (ALFind sub v); auto. +- intros ? ? Hind ? ? Hc. unfold tvmap, id. simpl. f_equal. simpl in *. + apply eq_maps. intros ? Hin. apply Hind with (lv:=lv); auto;[]. + rewrite ball_map_true in Hc. eauto. +- intros blv bnt Hind ? ? Hc. unfold tvmap_bterm. simpl. + rewrite ALFind. + unfold ALMapRange + Lemma var_rel_bc_alpha (f:NVar -> NVar): (forall t, (forall v:NVar, In v (free_vars t) -> f v =v) -> checkBC (free_vars t) (tvmap f t) = true From dbbccaa03d4e8bd233b5880b7654bc54a58378b7 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 10:50:39 -0400 Subject: [PATCH 12/26] characterized tvmap as ssubat_aux for bc terms. --- alphaeq.v | 52 ++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 44 insertions(+), 8 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index 17b0147..6124a5f 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4162,24 +4162,60 @@ SearchAbout AssocList. Definition ALFindEndo {Key:Type} {d:Deq Key} (sub: AssocList Key Key) (k:Key) : Key := ALFindDef sub k k. +(* Move to AssocList *) +Lemma ALFindEndoId {Key:Type} {d:Deq Key} (sub: AssocList Key Key) v : + disjoint [v] (ALDom sub) + -> ALFindEndo sub v = v. +Proof using. + intros. + unfold ALFindEndo, ALFindDef. + rewrite ALFindNoneIf;[refl|]. + noRepDis. +Qed. + +(* Move to AssocList *) +Lemma ALFindMapEndoId {Key:Type} {d:Deq Key} (sub: AssocList Key Key) lv: + disjoint lv (ALDom sub) + -> map (ALFindEndo sub) lv = lv. +Proof using. + intros Hd. + rewrite <- (map_id lv) at 2. + apply eq_maps. + intros ? Hin. + apply ALFindEndoId. + eapply subset_disjoint;[| apply Hd]. + apply singleton_subset. assumption. +Qed. + +(** because the 2 hypotheses, no filtering occurs in ssubst_aux, thus making it equivalent to +tvmap which happily maps ALL VARS, tottally agnostic to the concept of bvars *) Lemma var_ren_vmap : (forall t lv sub, checkBC lv t = true + -> disjoint (ALDom sub) (bound_vars t) -> tvmap (ALFindEndo sub) t = ssubst_aux t (ALMapRange vterm sub))* (forall t lv sub, checkBC_bt lv t = true + -> disjoint (ALDom sub) (bound_vars_bterm t) -> tvmap_bterm (ALFindEndo sub) t = ssubst_bterm_aux t (ALMapRange vterm sub)). Proof using. apply NTerm_BTerm_ind. -- simpl. intros v lv sub _. unfold tvmap, ALFindEndo, ALFindDef, sub_find. simpl. +- simpl. intros v lv sub _ Hd. unfold tvmap, ALFindEndo, ALFindDef, sub_find. simpl. rewrite ALMapRangeFindCommute. destruct (ALFind sub v); auto. -- intros ? ? Hind ? ? Hc. unfold tvmap, id. simpl. f_equal. simpl in *. - apply eq_maps. intros ? Hin. apply Hind with (lv:=lv); auto;[]. - rewrite ball_map_true in Hc. eauto. -- intros blv bnt Hind ? ? Hc. unfold tvmap_bterm. simpl. - rewrite ALFind. - unfold ALMapRange - Lemma var_rel_bc_alpha (f:NVar -> NVar): +- intros ? ? Hind ? ? Hc Hd. unfold tvmap, id. simpl. f_equal. simpl in *. + apply eq_maps. intros ? Hin. + rewrite ball_map_true in Hc. + rewrite disjoint_flat_map_r in Hd. + apply Hind with (lv:=lv); auto. +- intros blv bnt Hind ? ? Hc Hd. unfold tvmap_bterm. simpl in *. unfold dom_lmap. + rewrite ALFindMapEndoId by disjoint_reasoningv2. + rewrite andb_true in Hc. repnd. + f_equal. rewrite sub_filter_disjoint1;[eapply Hind; eauto; disjoint_reasoningv2|];[]. + unfold dom_sub, ALMapRange, ALDom, ALMap. rewrite map_map. unfold compose. simpl. + disjoint_reasoningv2. +Qed. + +Lemma var_rel_bc_alpha (f:NVar -> NVar): (forall t, (forall v:NVar, In v (free_vars t) -> f v =v) -> checkBC (free_vars t) (tvmap f t) = true From 61cab7281568e58b6d6b7ce24a0552dfcfc4b708 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 13:00:26 -0400 Subject: [PATCH 13/26] added NoDup lv to checkBC (barendregt's condition). updated proofs in this library, but not paramcoq-iff. In paramcoq, we don't use simultaneous bvars anyway. --- alphaeq.v | 12 +++++++++--- substitution.v | 33 ++++++++++++++++++--------------- 2 files changed, 27 insertions(+), 18 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index 6124a5f..f00ccf6 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -760,6 +760,7 @@ Local Opaque decide. addFreshVarsSpec2 vn pp. exrepnd. allsimpl. rewrite decide_true;[ring_simplify| disjoint_reasoningv2]. + rewrite decide_true;[ring_simplify| disjoint_reasoningv2]. Local Transparent decide. rewrite (fst (boundvars_substvars_checkbc2 blv vn)). apply (checkBCStrengthen vn);[| assumption]. @@ -774,7 +775,10 @@ Lemma bcSubstBetaPreservesBC o (lamVar:NVar) (lamBody appArg:NTerm) lv: Proof using varclass. Local Opaque decide. simpl. - setoid_rewrite decide_true at 2;[| disjoint_reasoningv2]. + setoid_rewrite decide_true at 4;[| disjoint_reasoningv2; fail]. + simpl in *. + setoid_rewrite decide_true at 3;[| constructor]. + setoid_rewrite decide_true at 1;[| repeat constructor; noRepDis1]. intros Hc. ring_simplify in Hc. repeat rewrite andb_true in Hc. repnd. @@ -4209,8 +4213,9 @@ Proof using. apply Hind with (lv:=lv); auto. - intros blv bnt Hind ? ? Hc Hd. unfold tvmap_bterm. simpl in *. unfold dom_lmap. rewrite ALFindMapEndoId by disjoint_reasoningv2. - rewrite andb_true in Hc. repnd. - f_equal. rewrite sub_filter_disjoint1;[eapply Hind; eauto; disjoint_reasoningv2|];[]. + do 2 rewrite andb_true in Hc. repnd. + f_equal. + rewrite sub_filter_disjoint1;[eapply Hind; eauto; noRepDis1|];[]. unfold dom_sub, ALMapRange, ALDom, ALMap. rewrite map_map. unfold compose. simpl. disjoint_reasoningv2. Qed. @@ -4233,6 +4238,7 @@ Proof using. apply andb_true in Hc. repnd. SearchAbout decide. apply prove_alpha_bterm2. SearchAbout alpha_eq_bterm. +Abort. End AlphaGeneric. diff --git a/substitution.v b/substitution.v index 2b205e7..17c3f69 100644 --- a/substitution.v +++ b/substitution.v @@ -1092,7 +1092,7 @@ with checkBC_bt {NVar: Type} (bt: @BTerm NVar Opid) : bool := match bt with -| bterm blv bnt => (checkBC (blv++lv) bnt) && decide (disjoint blv lv) +| bterm blv bnt => (checkBC (blv++lv) bnt) && decide (NoDup blv) && decide (disjoint blv lv) end. Fixpoint uniq_change_bvars_alpha {NVar VarCl : Type} @@ -6663,11 +6663,13 @@ Proof using. - intros ? ? Hind ? ? Hsub Hc. simpl in *. rewrite ball_map_true in *. eauto. - intros blv ? Hind ? ? Hsub Hc. simpl in *. - rewrite andb_true in *. repnd. rewrite Decidable_spec in Hc. rewrite Decidable_spec. + do 2 rewrite andb_true in *. repnd. + setoid_rewrite Decidable_spec at 2. + rewrite Decidable_spec in Hc. rewrite disjoint_sym in Hc. rewrite disjoint_sym. - dands;[| eauto using subset_disjoint; fail]. - revert Hc0. + dands; auto; [|]; [| eauto using subset_disjoint; fail]. + revert Hc1. apply Hind. apply subsetvAppLR; eauto. Qed. @@ -6685,9 +6687,9 @@ Proof using. [simpl; intros; disjoint_reasoningv2| |];[|]. - intros ? ? Hind ? Hc. simpl in *. rewrite disjoint_flat_map_r. rewrite ball_map_true in Hc. eauto. -- intros blv bnt Hind ? Hc. simpl in *. rewrite andb_true in Hc. repnd. +- intros blv bnt Hind ? Hc. simpl in *. do 2 rewrite andb_true in Hc. repnd. rewrite Decidable_spec in Hc. disjoint_reasoningv. - apply Hind. revert Hc0. apply (fst checkBCSubset). + apply Hind. revert Hc1. apply (fst checkBCSubset). apply subset_app_l. eauto. Qed. @@ -6706,7 +6708,7 @@ Proof using. f_equal; [| eapply proper_decider2;[| apply eq_set_refl | apply Heq]; eauto with typeclass_instances]. - apply Hind. rewrite Heq. reflexivity. + f_equal. apply Hind. rewrite Heq. reflexivity. Qed. Lemma checkBCStrengthen blv : @@ -6722,10 +6724,10 @@ Proof using. - intros ? ? Hind lv Hdis. simpl in *. do 2 rewrite ball_map_true. rewrite disjoint_flat_map_l in Hdis. eauto. - intros bblv bnt Hind lv Hdis. simpl in *. - specialize (Hind (bblv++lv)). do 2 rewrite andb_true. - do 2 rewrite Decidable_spec. + specialize (Hind (bblv++lv)). do 4 rewrite andb_true. + do 3 rewrite Decidable_spec. intros Hc. repnd. - dands;[| disjoint_reasoningv2];[]. + dands; auto;[| disjoint_reasoningv2];[]. rewrite <- Hind; auto;[| disjoint_reasoningv2];[]. apply checkBCEqset. do 2 rewrite app_assoc. @@ -6757,9 +6759,9 @@ Proof using. apply Hind; auto; fail. - intros blv bnt Hind lv Hdis Hca Hcl. simpl in *. - apply andb_true. - apply andb_true in Hcl. repnd. - dands;[| assumption]. + repeat rewrite andb_true. + repeat rewrite andb_true in Hcl. repnd. + dands; auto;[]. cases_if;[rewrite ssubst_aux_nil; assumption|]. apply Hind; auto;[disjoint_reasoningv|]. disjoint_reasoning. @@ -6781,8 +6783,9 @@ Proof using. dALFind s; refl. - intros ? ? Hind ? ?. simpl. f_equal. rewrite map_map. apply eq_maps. intros ? Hin. unfold compose. simpl. eauto. -- intros blv bnt Hind ? ?. simpl. f_equal. - unfold sub_filter. rewrite ALMapRangeFilterCommute. apply Hind. +- intros blv bnt Hind ? ?. simpl. f_equal. f_equal. + unfold sub_filter. rewrite ALMapRangeFilterCommute. + apply Hind. Qed. Lemma boundvars_substvars_checkbc2 lvi lvo : From 67cef41fdcc5f7ad27c460bd38a1930a54e77f48 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 14:20:44 -0400 Subject: [PATCH 14/26] need mapping for both sides --- alphaeq.v | 36 ++++++++++++++++++++++++------------ 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index f00ccf6..40a8515 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4220,24 +4220,36 @@ Proof using. disjoint_reasoningv2. Qed. -Lemma var_rel_bc_alpha (f:NVar -> NVar): - (forall t, - (forall v:NVar, In v (free_vars t) -> f v =v) +Lemma var_rel_bc_alpha : + (forall t sub, + let f:= (ALFindEndo sub) in (* may contain [bvars t]. renaming some of them is the whole point *) + disjoint (ALDom sub) (free_vars t) -> checkBC (free_vars t) (tvmap f t) = true -> alpha_eq t (tvmap f t))* - (forall t, - (forall v:NVar, In v (free_vars_bterm t) -> f v =v) + (forall t sub, + let f:= (ALFindEndo sub) in + disjoint (ALDom sub) (free_vars_bterm t) -> checkBC_bt (free_vars_bterm t) (tvmap_bterm f t) = true -> alpha_eq_bterm t (tvmap_bterm f t)). Proof using. - apply NTerm_BTerm_ind; - [ intros v Hin Hc; unfold tvmap; simpl; rewrite Hin; auto; simpl; cpx | |]. -- intros ? ? Hind Hin Hc. unfold tvmap. simpl. unfold id. + simpl. + apply NTerm_BTerm_ind. +- intros v ? Hin _; unfold tvmap; simpl in *. rewrite ALFindEndoId;[refl|disjoint_reasoningv2]. +- intros ? ? ? Hind Hin Hc. unfold tvmap. simpl. unfold id. constructor;[autorewrite with list; auto|]. admit. (* easy *) -- intros ? ? Hind Hin Hc. unfold tvmap_bterm. simpl. simpl in Hc. - apply andb_true in Hc. repnd. SearchAbout decide. - apply prove_alpha_bterm2. - SearchAbout alpha_eq_bterm. +- intros blv bnt Hind ? Hd Hc. unfold tvmap_bterm. simpl. simpl in Hc. + repeat rewrite andb_true in Hc. repeat rewrite Decidable_spec in Hc. + apply prove_alpha_bterm with (lva:=[]);[| rewrite map_length; refl]. + rewrite app_nil_r. intros lvn H1d _ Hl Hnd. + unfold var_ren. do 2 rewrite combine_of_map_snd. repnd. + simpl in *. + pose proof Hc1 as Hdis. apply checkBCdisjoint in Hdis. + setoid_rewrite <- (fst var_ren_vmap); eauto. + Focus 4. (* subgoal 3 will come from the additional hypothesis *) + setoid_rewrite <- combine_map_fst2;[disjoint_reasoningv2|rw map_length; omega]. + + Focus 4. (* will come from the additional hypothesis *) admit. + Search alpha_eq_bterm. Abort. End AlphaGeneric. From 43b8230c946df2fa2ac1cb55114cea2b7c9c4d24 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 15:06:48 -0400 Subject: [PATCH 15/26] changing only one side doesn't seem to be working --- alphaeq.v | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/alphaeq.v b/alphaeq.v index 40a8515..4f6c4ae 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4239,15 +4239,26 @@ Proof using. constructor;[autorewrite with list; auto|]. admit. (* easy *) - intros blv bnt Hind ? Hd Hc. unfold tvmap_bterm. simpl. simpl in Hc. repeat rewrite andb_true in Hc. repeat rewrite Decidable_spec in Hc. + repnd. symmetry. + apply prove_alpha_bterm2; try rewrite map_length; auto. + Focus 3. + symmetry. + change_to_ssubst_aux8. + unfold var_ren. do 1 rewrite combine_of_map_snd. + setoid_rewrite <- (fst var_ren_vmap); eauto. + symmetry. apply H + + apply prove_alpha_bterm with (lva:=[]);[| rewrite map_length; refl]. rewrite app_nil_r. intros lvn H1d _ Hl Hnd. + SearchAbout ssubst_aux. unfold var_ren. do 2 rewrite combine_of_map_snd. repnd. simpl in *. pose proof Hc1 as Hdis. apply checkBCdisjoint in Hdis. setoid_rewrite <- (fst var_ren_vmap); eauto. Focus 4. (* subgoal 3 will come from the additional hypothesis *) setoid_rewrite <- combine_map_fst2;[disjoint_reasoningv2|rw map_length; omega]. - + SearchAbout NoDup map. Focus 4. (* will come from the additional hypothesis *) admit. Search alpha_eq_bterm. Abort. From 01111b3c729f99af1c076166e88813c4509b3dc1 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 15:51:06 -0400 Subject: [PATCH 16/26] some comments --- alphaeq.v | 24 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index 4f6c4ae..6f5f483 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4240,25 +4240,21 @@ Proof using. - intros blv bnt Hind ? Hd Hc. unfold tvmap_bterm. simpl. simpl in Hc. repeat rewrite andb_true in Hc. repeat rewrite Decidable_spec in Hc. repnd. symmetry. - apply prove_alpha_bterm2; try rewrite map_length; auto. - Focus 3. - symmetry. - change_to_ssubst_aux8. - unfold var_ren. do 1 rewrite combine_of_map_snd. - setoid_rewrite <- (fst var_ren_vmap); eauto. - symmetry. apply H - - apply prove_alpha_bterm with (lva:=[]);[| rewrite map_length; refl]. rewrite app_nil_r. intros lvn H1d _ Hl Hnd. - SearchAbout ssubst_aux. + fold (tvmap (ALFindEndo sub) bnt). + (*tvmap (ALFindEndo sub) bnt as + tvmap (combine blv ((map (ALFindEndo sub) blv))) + (tvmap (ALFilterOut sub blv) bnt) + merge the outer tvmap into the outer one. *) + tmap bnt unfold var_ren. do 2 rewrite combine_of_map_snd. repnd. - simpl in *. + simpl in *. rewrite map_length in Hl. pose proof Hc1 as Hdis. apply checkBCdisjoint in Hdis. setoid_rewrite <- (fst var_ren_vmap); eauto. - Focus 4. (* subgoal 3 will come from the additional hypothesis *) - setoid_rewrite <- combine_map_fst2;[disjoint_reasoningv2|rw map_length; omega]. - SearchAbout NoDup map. + Focus 2. (* subgoal 3 will come from the additional hypothesis *) + setoid_rewrite <- combine_map_fst2;[disjoint_reasoningv2| rewrite map_length; omega]. + fold (tvmap (ALFindEndo sub) bnt). Focus 4. (* will come from the additional hypothesis *) admit. Search alpha_eq_bterm. Abort. From 86a27d56f751fadcd49b34d9d07fe984e4496a90 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 19:59:50 -0400 Subject: [PATCH 17/26] need to added the assunption that the map picks vars diff from inp --- alphaeq.v | 87 +++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 82 insertions(+), 5 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index 6f5f483..134e784 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4166,6 +4166,7 @@ SearchAbout AssocList. Definition ALFindEndo {Key:Type} {d:Deq Key} (sub: AssocList Key Key) (k:Key) : Key := ALFindDef sub k k. + (* Move to AssocList *) Lemma ALFindEndoId {Key:Type} {d:Deq Key} (sub: AssocList Key Key) v : disjoint [v] (ALDom sub) @@ -4177,6 +4178,17 @@ Proof using. noRepDis. Qed. +(* Move to AssocList *) +Lemma ALFindEndoId2 {Key:Type} {d:Deq Key} lv v: + ALFindEndo (map (fun x=> (x,x)) lv) v = v. +Proof using. + unfold ALFindEndo, ALFindDef. + dALFind sd; [| refl]. + symmetry in Heqsd. + apply ALFindSome in Heqsd. apply in_map_iff in Heqsd. + exrepnd. inverts Heqsd0. refl. +Qed. + (* Move to AssocList *) Lemma ALFindMapEndoId {Key:Type} {d:Deq Key} (sub: AssocList Key Key) lv: disjoint lv (ALDom sub) @@ -4220,15 +4232,79 @@ Proof using. disjoint_reasoningv2. Qed. +(* Move :there must be something similar in stdlib or, Extlib, or UsefulTypes.v *) +Definition eqfun {A B:Type} (f g : A -> B) := + forall a, f a = g a. + +Global Instance eqfunEquiv {A B:Type}: Equivalence (@eqfun A B). +Proof using. + constructor; introv; unfold eqfun; try congruence. +Qed. + +(* Move to terms.v *) +Lemma tmap_ext (V1 V2 O1 O2 : Type) (fv gv: V1 -> V2) (fo go : O1 -> O2) + (veq : eqfun fv gv) (oeq : eqfun fo go): + (forall (t : terms.NTerm), tmap fv fo t = tmap gv go t)* + (forall (t : terms.BTerm), tmap_bterm fv fo t = tmap_bterm gv go t). +Proof using. + unfold eqfun in *. + apply NTerm_BTerm_ind; simpl; intros; try congruence; f_equal; try congruence; + apply eq_maps; eauto. +Qed. + +Global Instance tmapext {V1 V2 O1 O2 : Type}: + Proper (eqfun ==> eqfun ==> eq ==> eq) (@tmap V1 V2 O1 O2). +Proof using. + intros ? ? ? ? ? ? ? ? ?. subst. + apply tmap_ext; assumption. +Qed. + + +(* Move to AssocList.v *) +Lemma vmap_app_nest (sub1 sub2: AssocList NVar NVar): + disjoint (ALRange sub1) (ALDom sub2) + -> eqfun (ALFindEndo (sub1++sub2)) ((ALFindEndo sub2) ∘ (ALFindEndo sub1)). +Proof using. + intros Hd. + intros v. unfold compose, ALFindEndo, ALFindDef. + rewrite ALFindApp. dALFind s1v; auto. + rewrite ALFindNoneIf;[refl|]. + apply Hd. symmetry in Heqs1v. + apply ALFindSome in Heqs1v. apply in_map_iff. + eexists; dands ; eauto. +Qed. + +(* Move to AssocList.v *) +Lemma vmap_decompose (lv : list NVar) (sub: AssocList NVar NVar): + let subOuter := map (fun v => (v, (ALFindEndo sub) v)) lv in + let subInner := ALFilter sub lv in + disjoint (ALRange sub) lv + -> eqfun (ALFindEndo sub) ((ALFindEndo subOuter) ∘ (ALFindEndo subInner)). +Proof using. + simpl. intros Hd a. + rewrite <- vmap_app_nest; + [| setoid_rewrite map_map; unfold compose; simpl; rewrite map_id; + eapply subset_disjoint; try apply Hd; apply map_monotone, ALFilterSubset]. + unfold ALFindEndo, ALFindDef. + setoid_rewrite ALFindApp. symmetry. + dALFind sfa; simpl; symmetry in Heqsfa; + [apply ALFindFilterSome in Heqsfa | apply ALFindFilterNone in Heqsfa]; repnd; + try rewrite Heqsfa0;[refl|]. + dALFind sm; symmetry in Heqsm. + - apply ALFindSome in Heqsm. apply in_map_iff in Heqsm. exrepnd. inverts Heqsm0. refl. + - apply ALFindNone in Heqsm. setoid_rewrite map_map in Heqsm. unfold compose in Heqsm. + simpl in Heqsm. rewrite map_id in Heqsm. dorn Heqsfa; cpx;[]. rewrite Heqsfa. refl. +Qed. + Lemma var_rel_bc_alpha : (forall t sub, let f:= (ALFindEndo sub) in (* may contain [bvars t]. renaming some of them is the whole point *) - disjoint (ALDom sub) (free_vars t) + disjoint (ALDom sub) (free_vars t ++ ALRange sub) (** the item after ++ is WLOG. use 2 hops to rename all vars*) -> checkBC (free_vars t) (tvmap f t) = true -> alpha_eq t (tvmap f t))* (forall t sub, let f:= (ALFindEndo sub) in - disjoint (ALDom sub) (free_vars_bterm t) + disjoint (ALDom sub) (free_vars_bterm t ++ ALRange sub) -> checkBC_bt (free_vars_bterm t) (tvmap_bterm f t) = true -> alpha_eq_bterm t (tvmap_bterm f t)). Proof using. @@ -4241,11 +4317,12 @@ Proof using. repeat rewrite andb_true in Hc. repeat rewrite Decidable_spec in Hc. repnd. symmetry. apply prove_alpha_bterm with (lva:=[]);[| rewrite map_length; refl]. - rewrite app_nil_r. intros lvn H1d _ Hl Hnd. - fold (tvmap (ALFindEndo sub) bnt). + rewrite app_nil_r. intros lvn H1d _ Hl Hnd. simpl in *. + erewrite (fun rr p1 p2 => fst (@tmap_ext _ _ _ _ _ rr id id p1 p2)); + [|apply (vmap_decompose blv) | refl ]. (*tvmap (ALFindEndo sub) bnt as tvmap (combine blv ((map (ALFindEndo sub) blv))) - (tvmap (ALFilterOut sub blv) bnt) + (tvmap (ALFilter sub blv) bnt) merge the outer tvmap into the outer one. *) tmap bnt unfold var_ren. do 2 rewrite combine_of_map_snd. repnd. From e1d2ebcfdd3e7cfd1a862f518834c6a46fefd2ca Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 20:43:20 -0400 Subject: [PATCH 18/26] split sub into 2 parts. --- alphaeq.v | 38 ++++++++++++++++++++++++++++++++++---- 1 file changed, 34 insertions(+), 4 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index 134e784..bf8b37b 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4252,6 +4252,17 @@ Proof using. apply eq_maps; eauto. Qed. +Lemma tmap_compose (V1 V2 V3 O1 O2 O3 : Type) (gv: V1 -> V2) (fv : V2 -> V3) + (go : O1 -> O2) (fo : O2 -> O3): + (forall (t : terms.NTerm), tmap (fv ∘ gv) (fo ∘ go) t = tmap fv fo (tmap gv go t))* + (forall (t : terms.BTerm), tmap_bterm (fv ∘ gv) (fo ∘ go) t = tmap_bterm fv fo (tmap_bterm gv go t)). +Proof using. + apply NTerm_BTerm_ind; simpl; intros; + simpl; try congruence; f_equal; + try rewrite map_map; try congruence. + apply eq_maps; eauto. +Qed. + Global Instance tmapext {V1 V2 O1 O2 : Type}: Proper (eqfun ==> eqfun ==> eq ==> eq) (@tmap V1 V2 O1 O2). Proof using. @@ -4299,12 +4310,15 @@ Qed. Lemma var_rel_bc_alpha : (forall t sub, let f:= (ALFindEndo sub) in (* may contain [bvars t]. renaming some of them is the whole point *) - disjoint (ALDom sub) (free_vars t ++ ALRange sub) (** the item after ++ is WLOG. use 2 hops to rename all vars*) + disjoint (ALDom sub) (free_vars t) + -> disjoint (ALRange sub) (bound_vars t) + (** WLOG, because we can use 2 hops. for 1st hop use a one to one papping, which alpha preserves *) -> checkBC (free_vars t) (tvmap f t) = true -> alpha_eq t (tvmap f t))* (forall t sub, let f:= (ALFindEndo sub) in disjoint (ALDom sub) (free_vars_bterm t ++ ALRange sub) + -> disjoint (ALRange sub) (bound_vars_bterm t) (** WLOG, because we can use 2 hops *) -> checkBC_bt (free_vars_bterm t) (tvmap_bterm f t) = true -> alpha_eq_bterm t (tvmap_bterm f t)). Proof using. @@ -4313,13 +4327,29 @@ Proof using. - intros v ? Hin _; unfold tvmap; simpl in *. rewrite ALFindEndoId;[refl|disjoint_reasoningv2]. - intros ? ? ? Hind Hin Hc. unfold tvmap. simpl. unfold id. constructor;[autorewrite with list; auto|]. admit. (* easy *) -- intros blv bnt Hind ? Hd Hc. unfold tvmap_bterm. simpl. simpl in Hc. +- intros blv bnt Hind ? H1d H2d Hc. unfold tvmap_bterm. simpl. simpl in Hc. repeat rewrite andb_true in Hc. repeat rewrite Decidable_spec in Hc. repnd. symmetry. apply prove_alpha_bterm with (lva:=[]);[| rewrite map_length; refl]. - rewrite app_nil_r. intros lvn H1d _ Hl Hnd. simpl in *. + rewrite app_nil_r. intros lvn Had _ Hl Hnd. simpl in *. + unfold var_ren at 1. do 1 rewrite combine_of_map_snd. + rewrite map_length in Hl. + pose proof Hc1 as Hdis. apply checkBCdisjoint in Hdis. + setoid_rewrite <- (fst var_ren_vmap) at 1; eauto; + [|setoid_rewrite <- combine_map_fst2;[disjoint_reasoningv2| rewrite map_length; omega]; fail]. erewrite (fun rr p1 p2 => fst (@tmap_ext _ _ _ _ _ rr id id p1 p2)); - [|apply (vmap_decompose blv) | refl ]. + [|apply (vmap_decompose blv); disjoint_reasoningv2 | refl ]. + change id with ((@id Opid) ∘ (@id Opid)). + rewrite (fst (tmap_compose _ _ _ _ _ _ _ _ _ _)). + unfold tvmap. + rewrite <- (fst (tmap_compose _ _ _ _ _ _ _ _ _ _)). + change ((@id Opid) ∘ (@id Opid)) with (@id Opid). + rewrite <- combine_vars_map. + set (lvi := (map (ALFindEndo sub) blv)). + fold lvi in Hc0. + SearchAbout combine eq map. + setoid_rewrite <- combine_of_map_snd. + setoid_rewrite (fst var_ren_vmap). (*tvmap (ALFindEndo sub) bnt as tvmap (combine blv ((map (ALFindEndo sub) blv))) (tvmap (ALFilter sub blv) bnt) From db4ee3fda78a136c6e9772b82381f7df413709c7 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 21:36:48 -0400 Subject: [PATCH 19/26] need another assumption --- alphaeq.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/alphaeq.v b/alphaeq.v index bf8b37b..cdbd9be 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4307,6 +4307,35 @@ Proof using. simpl in Heqsm. rewrite map_id in Heqsm. dorn Heqsfa; cpx;[]. rewrite Heqsfa. refl. Qed. +(* Move to AssocList.v *) +Lemma vmap_nest_same (vl vi vr : list NVar): + let subOuter := combine vi vr in + let subInner := combine vl vi in + let sub := combine vl vr in + length vi = length vr + -> length vi = length vl + -> NoDup vi + -> eqfun (ALFindEndo sub) ((ALFindEndo subOuter) ∘ (ALFindEndo subInner)). +Proof using. + simpl. intros Hd H1l H2l a. + rewrite (combine_map_snd2 vr vi) at 1 by omega. + rewrite (combine_map_fst2 vi vr) at 3 by omega. + unfold ALFindEndo, ALFindDef. simpl. simpl. unfold compose. simpl. + remember (ALFind (combine vl (map fst (combine vi vr))) a) as ss. + do 1 rewrite combine_of_map_snd. + setoid_rewrite combine_of_map_snd in Heqss. + replace (map (fun x : NVar * (NVar * NVar) => (fst x, snd (snd x))) (combine vl (combine vi vr))) + with (ALMapRange snd (combine vl (combine vi vr))) by refl. + replace (map (fun x : NVar * (NVar * NVar) => (fst x, fst (snd x))) (combine vl (combine vi vr))) + with (ALMapRange fst (combine vl (combine vi vr))) in Heqss by refl. + setoid_rewrite ALFindMap3. + setoid_rewrite ALFindMap3 in Heqss. + subst. + dALFind sa; simpl; symmetry in Heqsa. +- admit. +- admit. +Abort. + Lemma var_rel_bc_alpha : (forall t sub, let f:= (ALFindEndo sub) in (* may contain [bvars t]. renaming some of them is the whole point *) @@ -4347,6 +4376,7 @@ Proof using. rewrite <- combine_vars_map. set (lvi := (map (ALFindEndo sub) blv)). fold lvi in Hc0. + SearchAbout ssubst_aux. SearchAbout combine eq map. setoid_rewrite <- combine_of_map_snd. setoid_rewrite (fst var_ren_vmap). From 7d6aac11ed78ebd80fd44f0ccd947285c2e599e3 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 21:53:33 -0400 Subject: [PATCH 20/26] the additional assumption is messy --- alphaeq.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/alphaeq.v b/alphaeq.v index cdbd9be..b1411df 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4333,7 +4333,14 @@ Proof using. subst. dALFind sa; simpl; symmetry in Heqsa. - admit. -- admit. +- assert (~ LIn a (remove_nvars vl vi)) as Ha by admit. + apply ALFindNone in Heqsa. + setoid_rewrite <- combine_map_fst2 in Heqsa;[| rewrite length_combine_eq; omega]. + rewrite in_remove_nvars in Ha. + dALFind sia; auto. + symmetry in Heqsia. + apply ALFindSome in Heqsia. + apply in_combine_l in Heqsia. tauto. Abort. Lemma var_rel_bc_alpha : From 4179bb8b36ceed8967e6f9ceb6c1ab18dee17732 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 22:33:21 -0400 Subject: [PATCH 21/26] will try to show that the DB results are the same. --- alphaeq.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/alphaeq.v b/alphaeq.v index b1411df..7acec6e 100644 --- a/alphaeq.v +++ b/alphaeq.v @@ -4385,7 +4385,7 @@ Proof using. fold lvi in Hc0. SearchAbout ssubst_aux. SearchAbout combine eq map. - setoid_rewrite <- combine_of_map_snd. +(* setoid_rewrite <- combine_of_map_snd. setoid_rewrite (fst var_ren_vmap). (*tvmap (ALFindEndo sub) bnt as tvmap (combine blv ((map (ALFindEndo sub) blv))) @@ -4400,7 +4400,7 @@ Proof using. setoid_rewrite <- combine_map_fst2;[disjoint_reasoningv2| rewrite map_length; omega]. fold (tvmap (ALFindEndo sub) bnt). Focus 4. (* will come from the additional hypothesis *) admit. - Search alpha_eq_bterm. + Search alpha_eq_bterm. *) Abort. End AlphaGeneric. @@ -4603,4 +4603,4 @@ Lemma preservesAlphaBC lv (t1 t2: @NTerm NVar Opid1) : Proof using. intros H1c H2c Hal. induction Hal;[ apply fVar |]. Abort. -End AlphaPres. \ No newline at end of file +End AlphaPres. From 5ca1a8128a8d8a2be2a60d807bafa4086ef59f9c Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Mon, 3 Jul 2017 23:33:43 -0400 Subject: [PATCH 22/26] almost done with the proof. --- list.v | 29 +++++++++++++++++++++++++++++ termsDB.v | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 80 insertions(+) diff --git a/list.v b/list.v index 2256f10..7d1e04b 100644 --- a/list.v +++ b/list.v @@ -4043,3 +4043,32 @@ Lemma removeConsCancel {A:Type} {deq: Deq A} (r:A)(lv : list A): Proof using. apply (diffAddCancel [r]). Qed. + +(* need more assumptions. [f] could equate everything not in the list to f (head l). + then LHS would say 0 for such elements. RHS would always be not found for such elements. *) +Lemma mapFirstIndex {A:Type} {deq: Deq A}(f:A->A) x l: + NoDup (map f l) + -> firstIndex (f x) (map f l) = firstIndex x l. +Proof using. + intros Hnd. + induction l; [refl|]. + simpl. symmetry. rewrite decide_decideP. + cases_if; subst;[rewrite deq_refl; refl|]. +Abort. + +Lemma mapNodupFirstIndex {A:Type} {deq: Deq A}(f:A->A) x l: + In x l + -> NoDup (map f l) + -> firstIndex (f x) (map f l) = firstIndex x l. +Proof using. + intros Hin Hnd. + induction l; [refl|]. simpl in *. + simpl. symmetry. rewrite decide_decideP. + cases_if; subst;[rewrite deq_refl; refl|]. + dorn Hin;[contradiction|]. + invertsn Hnd. specialize (IHl Hin). + apply (in_map f) in Hin. + rewrite decide_decideP. + cases_if;[ congruence |]. + f_equal. symmetry. eauto. +Qed. \ No newline at end of file diff --git a/termsDB.v b/termsDB.v index 08b7712..a25373b 100644 --- a/termsDB.v +++ b/termsDB.v @@ -1716,6 +1716,57 @@ Proof using getId getIdCorr getNameCorr. rewrite lookupNDef_inserts_neq_seq; auto. lia. Qed. +(* TODO: delete *) +Lemma mapNodupFirstIndex {A:Type} {deq: Deq A}(f:A->A) x l: + In x l + -> NoDup (map f l) + -> firstIndex (f x) (map f l) = firstIndex x l. +Proof using. + intros Hin Hnd. + induction l; [refl|]. simpl in *. + simpl. symmetry. rewrite decide_decideP. + cases_if; subst;[rewrite deq_refl; refl|]. + dorn Hin;[contradiction|]. + invertsn Hnd. specialize (IHl Hin). + apply (in_map f) in Hin. + rewrite decide_decideP. + cases_if;[ congruence |]. + f_equal. symmetry. eauto. +Qed. + + +Lemma var_rel_bc_alpha f + (namePres : forall v, getName (f v) = getName v) + : + (forall (t:@NTerm NVar Opid) (context: list NVar) , + NoDup (map f context) + -> subset (free_vars t) context + -> checkBC (map f context) (tvmap f t) = true + -> toDB getName context t = toDB getName (map f context) (tvmap f t))* + (forall (t:@BTerm NVar Opid) (context: list NVar) , + NoDup (map f context) + -> subset (free_vars_bterm t) context + -> checkBC_bt (map f context) (tvmap_bterm f t) = true + -> toDB_bt getName context t = toDB_bt getName (map f context) (tvmap_bterm f t)). +Proof using. + Local Opaque decide. + apply terms2.NTerm_BTerm_ind. +- intros v ? Hnd Hs Hc. simpl in *. f_equal. f_equal. + symmetry. apply mapNodupFirstIndex; auto;[]. apply singleton_subset. assumption. +- intros ? ? Hind ? Hnd Hs Hc. simpl. f_equal. + repeat rewrite map_map in *. apply eq_maps. simpl in *. + rewrite map_map in Hc. + rewrite ball_map_true in Hc. + rewrite subset_flat_map in Hs. + intros. apply Hind; eauto. + +- intros blv bnt Hind ? Hnd Hs Hc. + simpl. rewrite map_map. unfold compose. f_equal; [apply eq_maps; eauto |]. + rewrite <- map_rev, <- map_app. simpl in *. + repeat rewrite andb_true in Hc. repeat rewrite Decidable_spec in Hc. + repnd. + apply Hind; auto; try rewrite map_app;[apply NoDupApp; auto| |]. +Qed. End DBToNamed. From 9785cd7fa9c4c64b0e88c0e4082aa92aa2601371 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Wed, 12 Jul 2017 16:12:40 -0400 Subject: [PATCH 23/26] old changes, perhaps from July 3 --- termsDB.v | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/termsDB.v b/termsDB.v index a25373b..df08e3e 100644 --- a/termsDB.v +++ b/termsDB.v @@ -1734,7 +1734,29 @@ Proof using. f_equal. symmetry. eauto. Qed. +(* Prove and Move to list.v *) +Lemma noDupRev {A:Type} (la: list A): NoDup la -> NoDup (rev la). +Proof using. +Admitted. + +(* Prove and Move to list.v *) +Lemma eqsetRev {A:Type} (la: list A): eq_set la (rev la). +Proof using. +Admitted. + +(** move to substitution.v *) +Global Instance checkBCProper : + Proper (eq_set ==> eq ==> eq) (@checkBC NVar _ Opid). +Proof using. + intros ? ? ? ? ? ?. subst. + apply checkBCEqset. assumption. +Qed. +(** if we apply (even to binders, unlike subst) ANY varmap f to t, and the result is in BC, + then the result is alpha equal to the input. Sounds too good to be true, but it is. + Note that if the output is in BC, then the input must also be in BC (prove it): + f can only identify different vars, but not distinguish same vars. +*) Lemma var_rel_bc_alpha f (namePres : forall v, getName (f v) = getName v) : @@ -1764,8 +1786,9 @@ Proof using. simpl. rewrite map_map. unfold compose. f_equal; [apply eq_maps; eauto |]. rewrite <- map_rev, <- map_app. simpl in *. repeat rewrite andb_true in Hc. repeat rewrite Decidable_spec in Hc. - repnd. - apply Hind; auto; try rewrite map_app;[apply NoDupApp; auto| |]. + repnd. apply subsetv_remove_nvars in Hs. rewrite eqset_app_comm in Hs. + apply Hind; auto; try rewrite map_app; try rewrite map_rev; + [apply NoDupApp; eauto using noDupRev| |]; try rewrite <- eqsetRev; auto. Qed. End DBToNamed. From f67193babfd183044704d4c6d5d5a15622818ab3 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Wed, 12 Jul 2017 17:08:16 -0400 Subject: [PATCH 24/26] removed the admits, refactoring. --- list.v | 17 ++++++++++++++++- substitution.v | 9 +++++++++ termsDB.v | 35 ----------------------------------- 3 files changed, 25 insertions(+), 36 deletions(-) diff --git a/list.v b/list.v index 7d1e04b..11ed904 100644 --- a/list.v +++ b/list.v @@ -4071,4 +4071,19 @@ Proof using. rewrite decide_decideP. cases_if;[ congruence |]. f_equal. symmetry. eauto. -Qed. \ No newline at end of file +Qed. + + +Lemma eqsetRev {A:Type} (la: list A): eq_set la (rev la). +Proof using. + apply eq_set_iff_eq_set2. unfold eq_set2. + apply in_rev. +Qed. + +Lemma noDupRev {A:Type} (la: list A): NoDup la -> NoDup (rev la). +Proof using. + induction la; auto. + intros Hd. simpl. invertsn Hd. + apply NoDupApp; eauto;[constructor; auto; constructor|]. + rewrite <- eqsetRev. apply disjoint_singleton_r. assumption. +Qed. diff --git a/substitution.v b/substitution.v index 17c3f69..3177c09 100644 --- a/substitution.v +++ b/substitution.v @@ -6711,6 +6711,14 @@ Proof using. f_equal. apply Hind. rewrite Heq. reflexivity. Qed. + +Global Instance checkBCProper : + Proper (eq_set ==> eq ==> eq) (@checkBC NVar _ Opid). +Proof using. + intros ? ? ? ? ? ?. subst. + apply checkBCEqset. assumption. +Qed. + Lemma checkBCStrengthen blv : (forall (appArg:NTerm) lv, disjoint (bound_vars appArg) blv -> checkBC lv appArg = true -> checkBC (blv ++ lv) appArg = true) @@ -7297,3 +7305,4 @@ Proof using. setoid_rewrite (ALFindMap3 f). refl. Qed. + diff --git a/termsDB.v b/termsDB.v index df08e3e..b77d9ef 100644 --- a/termsDB.v +++ b/termsDB.v @@ -1716,41 +1716,6 @@ Proof using getId getIdCorr getNameCorr. rewrite lookupNDef_inserts_neq_seq; auto. lia. Qed. -(* TODO: delete *) -Lemma mapNodupFirstIndex {A:Type} {deq: Deq A}(f:A->A) x l: - In x l - -> NoDup (map f l) - -> firstIndex (f x) (map f l) = firstIndex x l. -Proof using. - intros Hin Hnd. - induction l; [refl|]. simpl in *. - simpl. symmetry. rewrite decide_decideP. - cases_if; subst;[rewrite deq_refl; refl|]. - dorn Hin;[contradiction|]. - invertsn Hnd. specialize (IHl Hin). - apply (in_map f) in Hin. - rewrite decide_decideP. - cases_if;[ congruence |]. - f_equal. symmetry. eauto. -Qed. - -(* Prove and Move to list.v *) -Lemma noDupRev {A:Type} (la: list A): NoDup la -> NoDup (rev la). -Proof using. -Admitted. - -(* Prove and Move to list.v *) -Lemma eqsetRev {A:Type} (la: list A): eq_set la (rev la). -Proof using. -Admitted. - -(** move to substitution.v *) -Global Instance checkBCProper : - Proper (eq_set ==> eq ==> eq) (@checkBC NVar _ Opid). -Proof using. - intros ? ? ? ? ? ?. subst. - apply checkBCEqset. assumption. -Qed. (** if we apply (even to binders, unlike subst) ANY varmap f to t, and the result is in BC, then the result is alpha equal to the input. Sounds too good to be true, but it is. From 96efa97b9b65bec4c10782b875cb4d8f9396971a Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Wed, 12 Jul 2017 17:30:20 -0400 Subject: [PATCH 25/26] move generic lemmas from paramcoq-iff --- UsefulTypes.v | 6 ++++++ list.v | 27 +++++++++++++++++++++++++++ terms2.v | 2 ++ varInterface.v | 11 +++++++++++ 4 files changed, 46 insertions(+) diff --git a/UsefulTypes.v b/UsefulTypes.v index 86c0b5b..b5425bf 100644 --- a/UsefulTypes.v +++ b/UsefulTypes.v @@ -765,3 +765,9 @@ Definition pairMapl {A B A2:Type} (f: A-> A2) (p:A*B) : A2*B := Definition pairMapr {A B B2:Type} (f: B-> B2) (p:A*B) : A*B2 := let (a,b) := p in (a, f b). + + +Ltac destructDecideP := + match goal with + [ |- context [@decideP ?p ?d] ] => destruct (@decideP p d) + end. diff --git a/list.v b/list.v index 11ed904..8ee4f26 100644 --- a/list.v +++ b/list.v @@ -4087,3 +4087,30 @@ Proof using. apply NoDupApp; eauto;[constructor; auto; constructor|]. rewrite <- eqsetRev. apply disjoint_singleton_r. assumption. Qed. + + +Global Instance properEqsetCons {A : Type}: + Proper (eq ==> eq_set ==> eq_set) (@cons A). +Proof using. + intros ? ? ? ? ? ?. subst. + unfold eq_set, subset in *. simpl in *. + firstorder. +Qed. + +Definition singleton {A:Type} (a:A) : list A := [a]. + +Lemma noDupConsIff {A : Type}: + forall a (lb : list A), NoDup (a::lb) <-> NoDup (singleton a) /\ NoDup lb /\ disjoint [a] lb. +Proof using. + intros. rewrite <- noDupApp. refl. +Qed. + +Lemma flat_map_fcons {A B : Type} (f: A->B) (g : A -> list B) (l : list A): + eq_set (flat_map (fun x : A => (f x):: g x) l) (map f l ++ flat_map g l). +Proof using. + rewrite <- flat_map_single. + rewrite <- flat_map_fapp. + refl. +Qed. + +Hint Rewrite @noDupApp @noDupConsIff: SquiggleEq. diff --git a/terms2.v b/terms2.v index 96ce4ae..db02550 100644 --- a/terms2.v +++ b/terms2.v @@ -2145,3 +2145,5 @@ Proof using. destruct l; invertsn Hn. simpl. f_equal. eauto. Qed. + +Hint Rewrite @noDupApp @all_vars_ot @allvars_bterm @varsOfClassConsIff @noDupConsIff: SquiggleEq. diff --git a/varInterface.v b/varInterface.v index 8504fbc..0de0e98 100644 --- a/varInterface.v +++ b/varInterface.v @@ -1528,3 +1528,14 @@ Definition varClassTypeOf (V:Type) {T:Type} {_ : VarClass V T} := T. Hint Rewrite @memvar_nil_r : SquiggleEq. + + +Lemma varsOfClassConsIff {NVar VClass : Type} {H0 : VarClass NVar VClass}: + forall v1 ( lv2 : list NVar) (vc : VClass), + varsOfClass (v1:: lv2) vc <-> varsOfClass (singleton v1) vc /\ varsOfClass lv2 vc. +Proof using. + intros. rewrite <- varsOfClassApp. refl. +Qed. + + + From 10bf25c567d6b14eb51d1c9da3d9dc569bb72d42 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (on Manjaro on brixpro)" Date: Sun, 29 Oct 2017 22:42:18 -0400 Subject: [PATCH 26/26] some lemmas from certicoq --- UsefulTypes.v | 7 +++++++ list.v | 26 ++++++++++++++++++++++++++ termsDB.v | 8 ++++++++ 3 files changed, 41 insertions(+) diff --git a/UsefulTypes.v b/UsefulTypes.v index b5425bf..0248195 100644 --- a/UsefulTypes.v +++ b/UsefulTypes.v @@ -771,3 +771,10 @@ Ltac destructDecideP := match goal with [ |- context [@decideP ?p ?d] ] => destruct (@decideP p d) end. + +Lemma rewritePairMatch {A B C:Type} (p:A*B) +(f : A->B->C): +(let (a,b) := p in f a b) = f (fst p) (snd p). +Proof using. + destruct p; auto. +Qed. diff --git a/list.v b/list.v index 8ee4f26..51292cc 100644 --- a/list.v +++ b/list.v @@ -4114,3 +4114,29 @@ Proof using. Qed. Hint Rewrite @noDupApp @noDupConsIff: SquiggleEq. + + +(* Move to SquiggleEq.list *) +Hint Rewrite app_length repeat_length firstn_length : list. +(* Move to SquiggleEq.list *) + +Lemma listPadId {A:Type} d (l: list A) n : + (n <= length l)%nat -> listPad d l n = l. +Proof using. + clear. + intros Hyp. + unfold listPad. + assert (n-length l =0)%nat as Heq by omega. + rewrite Heq. simpl. + autorewrite with list. refl. +Qed. + +Lemma listPad_length_eq {T} (def:T) (l: list T) (n: nat): +(length l <= n -> length (listPad def l n) = n)%nat. +Proof using. + setoid_rewrite app_length. + intros. + rewrite repeat_length. + omega. +Qed. + diff --git a/termsDB.v b/termsDB.v index b77d9ef..a57a362 100644 --- a/termsDB.v +++ b/termsDB.v @@ -1765,3 +1765,11 @@ Definition getFirstBTermNames {V O }(t:list (@DBTerm V O)) : list V:= end. +Lemma get_bcvars_subst_aux_bt {Name Opid} a n (b : @DBTerm Name Opid): + get_bvars (subst_aux_bt a n b) = get_bvars b. +Proof using. + destruct b; refl. +Qed. + + +