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/AbstractInterpretationWf.v | 32 ++++++++++++++++++++++++++---- src/LanguageWf.v | 32 +++++------------------------- src/RewriterRulesGood.v | 24 +++++++++++++++++++++++ src/UnderLetsProofs.v | 44 +++++++++++++++++++++++++++++++++++++++--- 4 files changed, 98 insertions(+), 34 deletions(-) (limited to 'src') diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v index 85eef1cae..25c8ba574 100644 --- a/src/AbstractInterpretationWf.v +++ b/src/AbstractInterpretationWf.v @@ -10,6 +10,7 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Option. Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.Forall. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. @@ -314,13 +315,34 @@ Module Compilers. {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)} {is_annotated_for_Proper : forall t t', Proper (eq ==> abstract_domain'_R _ ==> eq) (@is_annotated_for t t')} (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2)) - (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2) + (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> List.Forall2 (@abstract_domain'_R t) l1 l2) (extract_option_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_eq (option_eq (abstract_domain'_R _)) (extract_option_state t v1) (extract_option_state t v2)). Local Instance abstract_interp_ident_Proper_arrow s d : Proper (eq ==> abstract_domain'_R s ==> abstract_domain'_R d) (abstract_interp_ident (type.arrow s d)) := abstract_interp_ident_Proper (type.arrow s d). + Local Ltac handle_Forall2_step := + first [ match goal with + | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper] + | [ |- List.Forall2 _ (List.map _ _) (List.map _ _) ] => rewrite Forall2_map_map_iff + | [ |- List.Forall2 _ (List.combine _ _) (List.combine _ _) ] + => eapply Forall2_combine; [ intros | eassumption | eassumption ] + | [ |- List.Forall2 _ (List.combine ?x _) (List.combine ?x _) ] + => eapply Forall2_combine; + [ intros + | instantiate (1:=fun a b => a = b /\ List.In a x); + rewrite Forall2_Forall, Forall_forall; cbv [Proper]; auto + | eassumption ] + | [ H : expr.wf _ ?d1 ?d2, H' : List.Forall2 (expr.wf _) ?xs ?ys + |- expr.wf ?G (nth_default ?d1 ?xs ?n) (nth_default ?d2 ?ys ?n) ] + => cut (List.Forall2 (expr.wf G) xs ys /\ expr.wf G d1 d2); + [ rewrite Forall2_forall_iff''; + let H := fresh in intros [? H]; apply H + | ] + end ]. + + Section with_var2. Context {var1 var2 : type -> Type}. @@ -472,7 +494,9 @@ Module Compilers. |- ?R ?a1 ?a2 ] => apply H | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n') + | [ H : length ?x = length ?y |- context[length ?x] ] => rewrite H end + | handle_Forall2_step | break_innermost_match_step | break_innermost_match_hyps_step | progress expr.invert_match @@ -580,6 +604,7 @@ Module Compilers. | progress expr.invert_subst | progress expr.inversion_wf_constr | progress expr.inversion_expr + | handle_Forall2_step | wf_safe_t_step | progress destruct_head' (@partial.wf_value) | solve [ eapply wf_annotate; wf_t; try apply DefaultValue.expr.base.wf_default @@ -734,11 +759,10 @@ Module Compilers. intros; subst; cbv [option_map extract_list_state]; break_innermost_match; reflexivity. Qed. Lemma extract_list_state_rel - : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2. + : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> List.Forall2 (@abstract_domain'_R t) l1 l2. Proof. intros; cbv [extract_list_state] in *; subst; inversion_option; subst. - rewrite combine_same, List.in_map_iff in *. - destruct_head'_ex; destruct_head'_and; inversion_prod; subst; reflexivity. + now rewrite Forall2_Forall, Forall_forall; cbv [Proper]. Qed. Lemma extract_option_state_rel 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. diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v index 7cbe4e560..c9c41a392 100644 --- a/src/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -20,6 +20,7 @@ Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Prod. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.ListUtil.ForallIn. +Require Import Crypto.Util.ListUtil.Forall. Require Import Crypto.Util.Option. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.HProp. @@ -282,6 +283,29 @@ Module Compilers. exfalso; clear -H H'; congruence | [ H : Compile.wf_value _ (reify_list _) (reify_list _) |- _ ] => hnf in H; rewrite expr.wf_reify_list in H + | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper] + | [ |- List.Forall2 _ (List.map _ _) (List.map _ _) ] => rewrite Forall2_map_map_iff + | [ |- List.Forall2 _ (List.repeat _ _) (List.repeat _ _) ] + => rewrite Forall2_repeat_iff + | [ |- List.Forall2 _ (List.rev _) (List.rev _) ] + => rewrite Forall2_rev_iff + | [ |- List.Forall _ (seq _ _) ] => rewrite Forall_seq + | [ |- List.Forall2 _ (firstn _ _) (firstn _ _) ] + => now apply Forall2_firstn + | [ |- List.Forall2 _ (skipn _ _) (skipn _ _) ] + => now apply Forall2_skipn + | [ |- List.Forall2 _ (List.combine _ _) (List.combine _ _) ] + => eapply Forall2_combine; [ intros | eassumption | eassumption ] + | [ |- List.Forall2 _ (update_nth _ _ _) (update_nth _ _ _) ] + => apply Forall2_update_nth; intros + | [ H : List.Forall2 _ ?x ?y |- context[@List.length ?T ?y] ] + => rewrite <- (@eq_length_Forall2 _ T _ x y H) + | [ H : Forall2 (expr.wf ?G) ?xs ?ys |- Forall2 (fun a b => UnderLets.wf (fun G' => expr.wf G') ?G _ _) ?xs ?ys ] + => eapply Forall2_Proper_impl; [ .. | exact H ]; try reflexivity; repeat intro + | [ H : Forall2 ?P ?xs ?ys, Hx : nth_error ?xs ?n = _, Hy : nth_error ?ys ?n = _ |- _ ] + => let H' := fresh in + pose proof H as H'; + rewrite Forall2_forall_iff_nth_error in H'; specialize (H' n); rewrite Hx, Hy in H'; clear n Hx Hy | [ H : length ?l = length ?l' |- context[length ?l] ] => rewrite H | [ H : context[combine (firstn ?n _) (firstn ?n _)] |- _ ] => rewrite <- firstn_combine in H | [ H : context[combine (skipn ?n _) (skipn ?n _)] |- _ ] => rewrite <- skipn_combine in H diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index 5b7caa0d6..0705ec94d 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -8,10 +8,12 @@ Require Import Crypto.UnderLets. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Option. +Require Import Crypto.Util.ListUtil.Forall. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.SpecializeAllWays. Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.SplitInContext. Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Import EqNotations. @@ -285,7 +287,7 @@ Module Compilers. { eapply He; eauto; rewrite ?app_assoc; eauto. } } Qed. - Lemma wf_splice_list_no_order {A1 B1 A2 B2} + Lemma wf_splice_list_no_order_nth_error {A1 B1 A2 B2} {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} G @@ -319,6 +321,32 @@ Module Compilers. end ]. Qed. + Lemma wf_splice_list_no_order {A1 B1 A2 B2} + {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} + {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} + G + (x1 : list (@UnderLets var1 A1)) (x2 : list (@UnderLets var2 A2)) + (P_Proper_list : forall G1 G2 a1 a2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + -> P G1 a1 a2 -> P G2 a1 a2) + (Hx : List.Forall2 (wf P G) x1 x2) + (e1 : list A1 -> @UnderLets var1 B1) (e2 : list A2 -> @UnderLets var2 B2) + (He : forall G' a1 a2, (exists seg, G' = seg ++ G) + -> length a1 = length x1 + -> length a2 = length x2 + -> List.Forall2 (P G') a1 a2 + -> @wf _ _ Q G' (e1 a1) (e2 a2)) + : @wf _ _ Q G (splice_list x1 e1) (splice_list x2 e2). + Proof. + setoid_rewrite Forall2_forall_In_combine_iff in He. + apply @wf_splice_list_no_order_nth_error with (P:=P); try assumption; + eauto using eq_length_Forall2. + { intro n; rewrite Forall2_forall_iff_nth_error in Hx; specialize (Hx n). + intros; cbv [option_eq] in *; break_innermost_match_hyps; inversion_option; subst; assumption. } + { rewrite Forall2_forall_In_combine_iff in Hx; destruct Hx. + intros; eapply He; try apply conj; eauto; congruence. } + Qed. + Lemma wf_list_rect {A B Pnil Pcons ls A' B' Pnil' Pcons' ls'} {RA : A -> A' -> Prop} {RB G} (Hnil : wf RB G Pnil Pnil') (Hcons : forall x x', @@ -707,6 +735,10 @@ Module Compilers. | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ] => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H + | [ H : List.Forall2 _ ?xs ?ys |- _ ] + => match xs with nil => idtac | _::_ => idtac end; + match ys with nil => idtac | _::_ => idtac end; + inversion H; clear H end | progress subst | progress destruct_head' False @@ -739,6 +771,8 @@ Module Compilers. | match goal with |- wf _ _ _ _ => constructor end | match goal with | [ H : context[wf _ _ _ _] |- wf _ _ _ _ ] => apply H; eauto with nocore + | [ H : Forall2 (expr.wf _) ?xs ?ys |- Forall2 (expr.wf _) ?xs ?ys ] + => eapply Forall2_Proper_impl; [ .. | exact H ]; repeat intro; try reflexivity end | progress wf_unsafe_t_step | match goal with @@ -765,7 +799,7 @@ Module Compilers. all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. all: revert dependent k1; revert dependent k2. all: lazymatch goal with - | [ H : length ?l1 = length ?l2 |- _ ] + | [ |- context[List.Forall2 _ ?l1 ?l2] ] => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros end; wf_reify_and_let_binds_base_cps_t Hk. @@ -899,6 +933,10 @@ Module Compilers. => pose proof (fun x y pf => H x y (or_introl pf)); pose proof (fun x y pf => H x y (or_intror pf)); clear H + | [ H : List.Forall2 _ ?xs ?ys |- _ ] + => match xs with nil => idtac | _::_ => idtac end; + match ys with nil => idtac | _::_ => idtac end; + inversion H; clear H end | progress interp_unsafe_t_step | match goal with @@ -938,7 +976,7 @@ Module Compilers. all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. all: revert dependent k1; revert dependent k2. all: lazymatch goal with - | [ H : length ?l1 = length ?l2 |- _ ] + | [ |- context[List.Forall2 _ ?l1 ?l2 ] ] => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros end; interp_to_expr_reify_and_let_binds_base_cps_t Hk. -- cgit v1.2.3