diff options
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 6b081e6e5..72d62e8fa 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -18,6 +18,7 @@ Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.RewriteHyp. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.RewriteHyp. Require Import Crypto.Util.FMapPositive.Equality. Require Import Crypto.Util.MSetPositive.Equality. Require Import Crypto.Util.Prod. @@ -57,6 +58,17 @@ Module Compilers. repeat match goal with H : _ |- _ => etransitivity; rewrite H; clear H; [ | reflexivity ] end. reflexivity. Qed. + + Lemma unify_extracted_cps_id {pt et T k} + : @pattern.base.unify_extracted_cps pt et T k = k (@pattern.base.unify_extracted_cps pt et _ id). + Proof using Type. + revert et T k; induction pt, et; cbn [pattern.base.unify_extracted_cps]; cbv [id] in *; intros; + repeat first [ reflexivity + | progress inversion_option + | progress subst + | break_innermost_match_step + | rewrite_hyp !* ]. + Qed. End base. Module type. @@ -70,6 +82,18 @@ Module Compilers. reflexivity. Qed. + Lemma unify_extracted_cps_id {pt et T k} + : @pattern.type.unify_extracted_cps pt et T k = k (@pattern.type.unify_extracted_cps pt et _ id). + Proof using Type. + revert et T k; induction pt, et; cbn [pattern.type.unify_extracted_cps]; cbv [id] in *; intros; + repeat first [ reflexivity + | progress inversion_option + | progress subst + | apply base.unify_extracted_cps_id + | break_innermost_match_step + | rewrite_hyp !* ]. + Qed. + Lemma app_forall_vars_under_forall_vars_relation {p k1 k2 F v1 v2 evm} : @pattern.type.under_forall_vars_relation p k1 k2 F v1 v2 |