diff options
Diffstat (limited to 'src/RewriterRulesGood.v')
-rw-r--r-- | src/RewriterRulesGood.v | 227 |
1 files changed, 24 insertions, 203 deletions
diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v index c05bcc23e..2d3ed96e2 100644 --- a/src/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -1,221 +1,42 @@ Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. -Require Import Coq.Lists.List. -Require Import Coq.Classes.Morphisms. -Require Import Coq.MSets.MSetPositive. -Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Language. -Require Import Crypto.LanguageInversion. -Require Import Crypto.LanguageWf. -Require Import Crypto.UnderLetsProofs. -Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Rewriter. +Require Import Crypto.RewriterFull. Require Import Crypto.RewriterWf1. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SpecializeAllWays. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.RewriteHyp. -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. -Require Import Crypto.Util.Decidable. -Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. -Import EqNotations. Module Compilers. - Import Language.Compilers. - Import LanguageInversion.Compilers. - Import LanguageWf.Compilers. - Import UnderLetsProofs.Compilers. - Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. - Import Rewriter.Compilers. + Import RewriterFull.Compilers. Import RewriterWf1.Compilers. - Import expr.Notations. - Import RewriterWf1.Compilers.RewriteRules. - Import defaults. Module Import RewriteRules. - Import Rewriter.Compilers.RewriteRules. + Import RewriterFull.Compilers.RewriteRules. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. - Section good. - Context {var1 var2 : type -> Type}. + Lemma RewriterRulesNBEWf : Wf_GoalT RewriterNBE. + Proof. prove_good (). Qed. - Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) var1 var2). + Lemma RewriterRulesArithWf max_const : Wf_GoalT (RewriterArith max_const). + Proof. prove_good (). Qed. - Lemma wf_list_rect {T A} - G N1 N2 C1 C2 ls1 ls2 - (HN : Compile.wf_value G N1 N2) - (HC : forall G' x1 x2 xs1 xs2 rec1 rec2, - (exists seg, G' = (seg ++ G)%list) - -> Compile.wf_value G x1 x2 - -> List.Forall2 (Compile.wf_value G) xs1 xs2 - -> Compile.wf_value G' rec1 rec2 - -> Compile.wf_value G' (C1 x1 xs1 rec1) (C2 x2 xs2 rec2)) - (Hls : List.Forall2 (Compile.wf_value G) ls1 ls2) - : Compile.wf_value - G - (list_rect (fun _ : list (@Compile.value base.type ident var1 (type.base T)) - => @Compile.value base.type ident var1 A) - N1 C1 ls1) - (list_rect (fun _ : list (@Compile.value base.type ident var2 (type.base T)) - => @Compile.value base.type ident var2 A) - N2 C2 ls2). - Proof. induction Hls; cbn [list_rect]; try eapply HC; eauto using (ex_intro _ nil). Qed. + Lemma RewriterRulesArithWithCastsWf : Wf_GoalT RewriterArithWithCasts. + Proof. prove_good (). Qed. - Lemma wf_nat_rect {A} - G O1 O2 S1 S2 n - (HO : Compile.wf_value_with_lets G O1 O2) - (HS : forall G' n rec1 rec2, - (exists seg, G' = (seg ++ G)%list) - -> Compile.wf_value_with_lets G' rec1 rec2 - -> Compile.wf_value_with_lets G' (S1 n rec1) (S2 n rec2)) - : Compile.wf_value_with_lets - G - (nat_rect (fun _ => @Compile.value_with_lets base.type ident var1 A) O1 S1 n) - (nat_rect (fun _ => @Compile.value_with_lets base.type ident var2 A) O2 S2 n). - Proof. induction n; cbn [nat_rect]; try eapply HS; eauto using (ex_intro _ nil). Qed. + Lemma RewriterRulesStripLiteralCastsWf : Wf_GoalT RewriterStripLiteralCasts. + Proof. prove_good (). Qed. - Global Strategy -100 [rewrite_rules Compile.rewrite_rules_goodT_curried_cps]. - - Local Ltac start_good := - match goal with - | [ |- rewrite_rules_goodT ?rew1 ?rew2 ] - => let H := fresh in - pose proof (@Compile.rewrite_rules_goodT_by_curried _ _ _ _ _ rew1 rew2 eq_refl) as H; - let data := lazymatch rew1 with rewrite_rules ?data _ => data end in - let h := head data in - cbv [h rewrite_rules] in H; - let h' := lazymatch type of H with - | context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => head rew1 - end in - let pident_arg_types - := lazymatch type of H with - | context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => pident_arg_types - end in - cbv [h' pident_arg_types Compile.rewrite_rules_goodT_curried_cps] in H; - (* make [Qed] not take forever by explicitly recording a cast node *) - let H' := fresh in - pose proof H as H'; clear H; - apply H'; clear H'; intros - end. - - Local Ltac fin_wf := - repeat first [ progress intros - | match goal with - | [ |- expr.wf _ (_ @ _) (_ @ _) ] => constructor - | [ |- expr.wf _ (#_) (#_) ] => constructor - | [ |- expr.wf _ ($_) ($_) ] => constructor - | [ |- expr.wf _ (expr.Abs _) (expr.Abs _) ] => constructor; intros - | [ H : @List.In ?T _ ?ls |- _ ] => is_evar ls; unify ls (@nil T); cbn [List.In] in H - | [ |- List.In ?v ?ls ] => is_evar ls; instantiate (1:=cons v _) - end - | progress subst - | progress destruct_head'_or - | progress destruct_head'_False - | progress inversion_sigma - | progress inversion_prod - | assumption - | esplit; revgoals; solve [ fin_wf ] - | econstructor; solve [ fin_wf ] - | progress cbn [List.In fst snd eq_rect] in * ]. - - Local Ltac handle_reified_rewrite_rules := - repeat - first [ match goal with - | [ |- option_eq _ ?x ?y ] - => lazymatch x with Some _ => idtac | None => idtac end; - lazymatch y with Some _ => idtac | None => idtac end; - progress cbn [option_eq] - | [ |- UnderLets.wf _ _ (Reify.expr_value_to_rewrite_rule_replacement ?rii1 ?sda _) (Reify.expr_value_to_rewrite_rule_replacement ?rii2 ?sda _) ] - => apply (fun H => @Reify.wf_expr_value_to_rewrite_rule_replacement _ _ _ rii1 rii2 H sda); intros - | [ |- option_eq _ (Compile.reflect_ident_iota _) (Compile.reflect_ident_iota _) ] - => apply Reify.wf_reflect_ident_iota - | [ |- ?x = ?x ] => reflexivity - end - | break_innermost_match_step - | progress cbv [Compile.wf_maybe_do_again_expr] in * - | progress fin_wf ]. - - Local Ltac handle_extra_nbe := - repeat first [ match goal with - | [ |- expr.wf _ (reify_list _) (reify_list _) ] => rewrite expr.wf_reify_list - | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper] - | [ |- List.Forall2 _ (List.map _ _) (List.map _ _) ] => rewrite Forall2_map_map_iff - | [ |- List.Forall _ (seq _ _) ] => rewrite Forall_seq - end - | progress intros - | progress fin_wf ]. - - Local Notation nbe_rewrite_rules := (rewrite_rules nbe_rewriter_data _). - Lemma nbe_rewrite_rules_good - : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules. - Proof using Type. - Time start_good. - Time all: abstract (handle_reified_rewrite_rules; handle_extra_nbe). - Qed. - - Local Ltac handle_extra_arith_rules := - repeat first [ progress cbv [option_eq SubstVarLike.is_var_fst_snd_pair_opp_cast] in * - | break_innermost_match_step - | match goal with - | [ Hwf : Compile.wf_value _ ?x _, H : context[SubstVarLike.is_recursively_var_or_ident _ ?x] |- _ ] => erewrite SubstVarLike.wfT_is_recursively_var_or_ident in H by exact Hwf - end - | congruence - | progress fin_wf ]. - - Local Notation arith_rewrite_rules max_const := (rewrite_rules (arith_rewriter_data max_const) _). - Lemma arith_rewrite_rules_good max_const - : rewrite_rules_goodT (arith_rewrite_rules max_const) (arith_rewrite_rules max_const). - Proof using Type. - Time start_good. - Time all: handle_reified_rewrite_rules; handle_extra_arith_rules. - Time Qed. - - Local Notation arith_with_casts_rewrite_rules := (rewrite_rules arith_with_casts_rewriter_data _). - Lemma arith_with_casts_rewrite_rules_good - : rewrite_rules_goodT arith_with_casts_rewrite_rules arith_with_casts_rewrite_rules. - Proof using Type. - Time start_good. - Time all: handle_reified_rewrite_rules. - Time Qed. - - Local Notation strip_literal_casts_rewrite_rules := (rewrite_rules strip_literal_casts_rewriter_data _). - Lemma strip_literal_casts_rewrite_rules_good - : rewrite_rules_goodT strip_literal_casts_rewrite_rules strip_literal_casts_rewrite_rules. - Proof using Type. - Time start_good. - Time all: handle_reified_rewrite_rules. - Time Qed. - - Local Notation fancy_rewrite_rules invert_low invert_high := (rewrite_rules (fancy_rewriter_data invert_low invert_high) _). - Lemma fancy_rewrite_rules_good - (invert_low invert_high : Z -> Z -> option Z) - (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) - (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) - : rewrite_rules_goodT (fancy_rewrite_rules invert_low invert_high) (fancy_rewrite_rules invert_low invert_high). - Proof using Type. - Time start_good. - Time all: handle_reified_rewrite_rules. - Time Qed. - - Local Notation fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range := (rewrite_rules (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range) _). - Lemma fancy_with_casts_rewrite_rules_good + Lemma RewriterRulesToFancyWf (invert_low invert_high : Z -> Z -> option Z) - (value_range flag_range : ZRange.zrange) (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) - : rewrite_rules_goodT (fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range) (fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range). - Proof using Type. - Time start_good. - Time all: handle_reified_rewrite_rules. - Time Qed. - End good. + : Wf_GoalT (RewriterToFancy invert_low invert_high). + Proof. prove_good (). Qed. + + Lemma RewriterRulesToFancyWithCastsWf + (invert_low invert_high : Z -> Z -> option Z) + (value_range flag_range : ZRange.zrange) + (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) + : Wf_GoalT (RewriterToFancyWithCasts invert_low invert_high value_range flag_range). + Proof. prove_good (). Qed. End RewriteRules. End Compilers. |