From 93c066f9c9c2c8fefb2204599b2d564738e9aecc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Mar 2019 21:02:38 -0500 Subject: Standardize list wf things Rather than using Forall2 in some places and a combination of length, combine, and In in others, we now primarily use Forall2. There is probably some dead tactic code as a result of this that I just haven't bothered to clean up. --- src/LanguageWf.v | 32 +++++--------------------------- 1 file changed, 5 insertions(+), 27 deletions(-) (limited to 'src/LanguageWf.v') diff --git a/src/LanguageWf.v b/src/LanguageWf.v index 4485bc841..6c5ce6ea5 100644 --- a/src/LanguageWf.v +++ b/src/LanguageWf.v @@ -933,12 +933,12 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ Local Notation expr1 := (@expr.expr base.type ident.ident var1). Local Notation expr2 := (@expr.expr base.type ident.ident var2). - Lemma wf_reify_list_Forall2 G {t} e1 e2 + Lemma wf_reify_list G {t} e1 e2 : @wf _ _ var1 var2 G _ (reify_list (t:=t) e1) (reify_list (t:=t) e2) <-> List.Forall2 (wf G) e1 e2. Proof. revert e2; induction e1 as [|e1 e1s IHe1s], e2 as [|e2 e2s]; - rewrite ?expr.reify_list_cons, ?expr.reify_list_nil; cbn [length combine]; + rewrite ?expr.reify_list_cons, ?expr.reify_list_nil; repeat first [ progress apply conj | progress intros | progress destruct_head'_and @@ -961,12 +961,6 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ | solve [ eauto ] ]. Qed. - Lemma wf_reify_list G {t} e1 e2 - : @wf _ _ var1 var2 G _ (reify_list (t:=t) e1) (reify_list (t:=t) e2) - <-> (List.length e1 = List.length e2 - /\ forall e1' e2', List.In (e1', e2') (List.combine e1 e2) -> wf G e1' e2'). - Proof. now rewrite wf_reify_list_Forall2, Forall2_forall_In_combine_iff. Qed. - Lemma wf_reflect_list G {t} e1 e2 : @wf _ _ var1 var2 G (type.base (base.type.list t)) e1 e2 -> (invert_expr.reflect_list e1 = None <-> invert_expr.reflect_list e2 = None). @@ -1060,13 +1054,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ Lemma wf_reify {t} v G : expr.wf G (@GallinaReify.base.reify var1 t v) (@GallinaReify.base.reify var2 t v). Proof. induction t; cbn; cbv [option_map]; break_innermost_match; repeat constructor; auto; []. - rewrite wf_reify_list, !map_length, combine_map_map, combine_same, map_map; split; auto; intros *; []. - cbn [fst snd]; rewrite in_map_iff; intros. - repeat first [ progress destruct_head'_and - | progress destruct_head'_ex - | progress inversion_prod - | progress subst - | solve [ eauto ] ]. + rewrite wf_reify_list, Forall2_map_map_iff, Forall2_Forall, Forall_forall; cbv [Proper]; auto. Qed. Lemma wf_smart_Literal {t v G} @@ -1074,20 +1062,10 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ Proof using Type. induction t; cbn; eta_expand; repeat constructor; auto. all: rewrite wf_reify_list + rewrite wf_reify_option. - all: repeat first [ rewrite map_length - | progress cbv [option_map option_eq] - | apply conj + all: repeat first [ progress cbv [option_map option_eq Proper] | reflexivity - | progress intros - | progress destruct_head'_ex - | progress destruct_head'_and - | progress inversion_prod - | progress subst + | rewrite Forall2_map_map_iff, Forall2_Forall, Forall_forall | break_innermost_match_step - | progress rewrite combine_map_map in * - | progress rewrite combine_same in * - | progress rewrite map_map in * - | progress rewrite in_map_iff in * | solve [ auto ] ]. Qed. -- cgit v1.2.3