diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterInterpProofs1.v | 1349 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterProofs.v | 29 |
3 files changed, 1373 insertions, 6 deletions
diff --git a/_CoqProject b/_CoqProject index 9fdef01d8..4dec8ffeb 100644 --- a/_CoqProject +++ b/_CoqProject @@ -262,6 +262,7 @@ src/Experiments/NewPipeline/LanguageWf.v src/Experiments/NewPipeline/MiscCompilerPasses.v src/Experiments/NewPipeline/MiscCompilerPassesProofs.v src/Experiments/NewPipeline/Rewriter.v +src/Experiments/NewPipeline/RewriterInterpProofs1.v src/Experiments/NewPipeline/RewriterProofs.v src/Experiments/NewPipeline/RewriterRulesGood.v src/Experiments/NewPipeline/RewriterRulesInterpGood.v diff --git a/src/Experiments/NewPipeline/RewriterInterpProofs1.v b/src/Experiments/NewPipeline/RewriterInterpProofs1.v new file mode 100644 index 000000000..450c9ba09 --- /dev/null +++ b/src/Experiments/NewPipeline/RewriterInterpProofs1.v @@ -0,0 +1,1349 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Coq.Lists.SetoidList. +Require Import Coq.Lists.List. +Require Import Coq.Classes.Morphisms. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.FSets.FMapPositive. +Require Import Coq.Logic.FunctionalExtensionality. +Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Experiments.NewPipeline.LanguageInversion. +Require Import Crypto.Experiments.NewPipeline.LanguageWf. +Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. +Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Experiments.NewPipeline.Rewriter. +Require Import Crypto.Experiments.NewPipeline.RewriterWf1. +Require Import Crypto.Util.MSetPositive.Facts. +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.Tactics.CPSId. +Require Import Crypto.Util.Tactics.SetEvars. +Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.Tactics.TransparentAssert. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Sigma.Related. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.SetoidList. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.CPSNotations. +Require Import Crypto.Util.HProp. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Notations. +Import ListNotations. Local Open Scope bool_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 RewriterWf1.Compilers. + Import expr.Notations. + Import defaults. + Import Rewriter.Compilers.RewriteRules. + Import RewriterWf1.Compilers.RewriteRules. + + Module Import RewriteRules. + Module Compile. + Import Rewriter.Compilers.RewriteRules.Compile. + Import RewriterWf1.Compilers.RewriteRules.Compile. + + Section with_var. + Local Notation type_of_list + := (fold_right (fun a b => prod a b) unit). + Local Notation type_of_list_cps + := (fold_right (fun a K => a -> K)). + Context {ident var : type.type base.type -> Type} + (eta_ident_cps : forall {T : type.type base.type -> Type} {t} (idc : ident t) + (f : forall t', ident t' -> T t'), + T t) + {pident : type.type pattern.base.type -> Type} + (pident_arg_types : forall t, pident t -> list Type) + (pident_unify pident_unify_unknown : forall t t' (idc : pident t) (idc' : ident t'), option (type_of_list (pident_arg_types t idc))) + {raw_pident : Type} + (strip_types : forall t, pident t -> raw_pident) + (raw_pident_beq : raw_pident -> raw_pident -> bool) + + (full_types : raw_pident -> Type) + (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc)) + (type_of_raw_pident : forall (pidc : raw_pident), full_types pidc -> type.type base.type) + (raw_pident_to_typed : forall (pidc : raw_pident) (args : full_types pidc), ident (type_of_raw_pident pidc args)) + (raw_pident_is_simple : raw_pident -> bool) + (pident_unify_unknown_correct + : forall t t' idc idc', pident_unify_unknown t t' idc idc' = pident_unify t t' idc idc') + (invert_bind_args_unknown_correct + : forall t idc pidc, invert_bind_args_unknown t idc pidc = invert_bind_args t idc pidc) + (eta_ident_cps_correct : forall T t idc f, @eta_ident_cps T t idc f = f _ idc) + (raw_pident_to_typed_invert_bind_args_type + : forall t idc p f, invert_bind_args t idc p = Some f -> t = type_of_raw_pident p f) + (raw_pident_to_typed_invert_bind_args + : forall t idc p f (pf : invert_bind_args t idc p = Some f), + raw_pident_to_typed p f = rew [ident] raw_pident_to_typed_invert_bind_args_type t idc p f pf in idc). + + Local Notation type := (type.type base.type). + Local Notation expr := (@expr.expr base.type ident var). + Local Notation pattern := (@pattern.pattern pident). + Local Notation UnderLets := (@UnderLets.UnderLets base.type ident var). + Local Notation ptype := (type.type pattern.base.type). + Local Notation value' := (@value' base.type ident var). + Local Notation value := (@value base.type ident var). + Local Notation value_with_lets := (@value_with_lets base.type ident var). + Local Notation Base_value := (@Base_value base.type ident var). + Local Notation splice_under_lets_with_value := (@splice_under_lets_with_value base.type ident var). + Local Notation splice_value_with_lets := (@splice_value_with_lets base.type ident var). + Local Notation rawexpr := (@rawexpr ident var). + Local Notation eval_decision_tree := (@eval_decision_tree ident var raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation reveal_rawexpr_cps_gen := (@reveal_rawexpr_cps_gen ident var). + Local Notation reveal_rawexpr_cps := (@reveal_rawexpr_cps ident var). + Local Notation eval_rewrite_rules := (@eval_rewrite_rules ident var pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types). + Local Notation rewrite_with_rule := (@rewrite_with_rule ident var pident pident_arg_types pident_unify pident_unify_unknown). + Let type_base (t : base.type) : type := type.base t. + Coercion type_base : base.type >-> type. + + Context (reify_and_let_binds_base_cps : forall (t : base.type), expr t -> forall T, (expr t -> UnderLets T) -> UnderLets T). + + Local Notation "e <---- e' ; f" := (splice_value_with_lets e' (fun e => f%under_lets)) : under_lets_scope. + Local Notation "e <----- e' ; f" := (splice_under_lets_with_value e' (fun e => f%under_lets)) : under_lets_scope. + Local Notation "e1 === e2" := (existT expr _ e1 = existT expr _ e2) : type_scope. + + Local Existing Instance SetoidList.eqlistA_equiv. + + Local Ltac rew_swap_list_step := + match goal with + | [ H : swap_list ?a ?b ?ls1 = Some ?ls2, H' : context[swap_list ?a ?b ?ls2] |- _ ] + => rewrite (swap_swap_list H) in H' + | [ H : swap_list ?a ?b ?ls1 = Some ?ls2 |- context[swap_list ?a ?b ?ls2] ] + => rewrite (swap_swap_list H) + | [ H : swap_list ?a ?b ?ls1 = Some ?ls2 |- context[swap_list ?a ?b ?ls1] ] + => rewrite H + | [ H : swap_list ?a ?b ?ls1 = Some ?ls2, + H' : swap_list ?a ?b ?ls3 = Some ?ls4, + Hl : eqlistA ?R ?ls2 ?ls3 + |- _ ] + => unique pose proof (swap_swap_list_eqlistA H H' Hl) + end. + + Local Ltac rew_eval_decision_tree_step := + match goal with + | [ H : (forall ctx' cont', eval_decision_tree ctx' ?d cont' = None \/ _) + |- context[eval_decision_tree ?ctx ?d ?cont] ] + => let H' := fresh in + destruct (H ctx cont) as [H' | [? [? [H' ?] ] ] ]; rewrite H' + end. + + Local Hint Constructors eqlistA. + Local Hint Unfold rawexpr_equiv. + Local Hint Unfold rawexpr_equiv_expr. + + Lemma eval_decision_tree_correct_Switch_cons + {T} ctx icase icases app_case d cont + (res := @eval_decision_tree T ctx (Switch (icase :: icases) app_case d) cont) + : (exists b, + res = match ctx with + | r :: ctx + => eval_decision_tree ctx (snd icase) (fun k ctx' => cont k (reveal_rawexpr_cps_gen (Some b) r _ id :: ctx')) + | _ => None + end) + \/ res = eval_decision_tree ctx (Switch icases app_case d) cont + \/ res = match app_case with + | Some app_case => eval_decision_tree ctx app_case cont + | None => None + end + \/ res = eval_decision_tree ctx d cont. + Proof using raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct. + destruct icase as [p icase]; subst res; cbn [fst snd]. + destruct ctx as [|r ctx]; [ now cbn; auto | ]. + destruct r. + all: cbn [eval_decision_tree fold_right]. + all: destruct app_case as [app_case|]. + Set Ltac Profiling. + Reset Ltac Profile. + all: repeat first [ match goal with + | [ |- context[?x = ?x \/ _] ] => solve [ auto ] + | [ |- context[_ \/ ?x = ?x] ] => solve [ auto ] + | [ H : ?x = ?y |- context[?y = ?x \/ _] ] => solve [ auto ] + | [ H : ?y = ?x |- context[?x = ?y \/ _] ] => solve [ auto ] + | [ H : _ = ?v |- (exists b, ?v = _) \/ _ ] + => left; eexists; (idtac + symmetry); eassumption + | [ H : ?v = _ |- (exists b, ?v = _) \/ _ ] + => left; eexists; (idtac + symmetry); eassumption + | [ H : context[invert_bind_args_unknown ?a ?b ?c] |- _ ] => rewrite invert_bind_args_unknown_correct in H + | [ |- context[invert_bind_args_unknown ?a ?b ?c] ] => rewrite invert_bind_args_unknown_correct + | [ H : context[eval_decision_tree _ _ (fun _ _ => None)] |- _ ] + => rewrite eval_decision_tree_cont_None in H + | [ |- context[eval_decision_tree _ _ (fun _ _ => None)] ] + => rewrite eval_decision_tree_cont_None + | [ |- (exists b, ?f _ = ?f _) \/ _ ] + => left; eexists; reflexivity + end + | progress subst + | progress inversion_sigma + | progress inversion_option + | progress cbv [reveal_rawexpr_cps reveal_rawexpr_cps_gen value] in * + | progress cbn [value'] in * + | progress expr.invert_match + | break_match_hyps_step ltac:(fun v => is_var v; let t := type of v in unify t type) + | break_match_step ltac:(fun v => is_var v; let t := type of v in unify t type) + | match goal with + | [ |- context[match ?d with Failure => _ | _ => _ end] ] => is_var d; destruct d + end + | progress cbn [eq_rect Option.sequence Option.sequence_return] in * + | progress cbv [id option_bind' Option.bind Option.sequence Option.sequence_return] in * + | match goal with + | [ H : invert_bind_args _ _ _ = Some _ |- _ ] + => pose proof (@raw_pident_to_typed_invert_bind_args _ _ _ _ H); + generalize dependent (@raw_pident_to_typed_invert_bind_args_type _ _ _ _ H); clear H; intros + | [ |- context[rew [?P] ?pf in ?v] ] + => lazymatch type of pf with + | ?t1 = ?t2 + => generalize dependent v; generalize dependent pf; + (generalize dependent t1 || generalize dependent t2); + intros; subst + end + | [ H : ?t = rew [?P] ?pf in ?v |- _ ] + => generalize dependent t; intros; subst + | [ H : context[rew [?P] ?pf in ?v] |- _ ] + => lazymatch type of pf with + | ?t1 = ?t2 + => generalize dependent v; generalize dependent pf; + (generalize dependent t1 || generalize dependent t2); + intros; subst + end + | [ |- context[match @fold_right ?A ?B ?f ?v ?ls with Some _ => _ | _ => _ end] ] + => destruct (@fold_right A B f v ls) eqn:? + end + | break_innermost_match_step ]. + Qed. + + Fixpoint eval_decision_tree_correct {T} d ctx cont + (res := @eval_decision_tree T ctx d cont) + {struct d} + : res = None + \/ exists n ctx', + res = cont n ctx' + /\ SetoidList.eqlistA rawexpr_equiv ctx ctx'. + Proof using raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct. + specialize (eval_decision_tree_correct T). + subst res; cbv zeta in *; destruct d. + all: [ > specialize (eval_decision_tree_correct ltac:(assumption)) + | clear eval_decision_tree_correct + | + | specialize (eval_decision_tree_correct ltac:(assumption)) ]. + { cbn [eval_decision_tree]; cbv [Option.sequence]; break_innermost_match; eauto. + all: right; repeat esplit; (idtac + symmetry); (eassumption + reflexivity). } + { cbn; eauto. } + { let d := match goal with d : decision_tree |- _ => d end in + pose proof (eval_decision_tree_correct d) as eval_decision_tree_correct_default. + let app_case := match goal with app_case : option decision_tree |- _ => app_case end in + pose proof (match app_case return match app_case with Some _ => _ | _ => _ end with + | Some app_case => eval_decision_tree_correct app_case + | None => I + end) as eval_decision_tree_correct_app_case. + let icases := match goal with icases : list (_ * decision_tree) |- _ => icases end in + induction icases as [|icase icases IHicases]; + [ clear eval_decision_tree_correct | specialize (eval_decision_tree_correct (snd icase)) ]. + (* now that we have set up guardedness correctly, we can + stop worrying so much about what order we destruct + things in *) + 2: destruct (@eval_decision_tree_correct_Switch_cons _ ctx icase icases app_case d cont) + as [ [? H] | [H| [H|H] ] ]; + rewrite H; try assumption. + all: destruct app_case as [app_case|]; try (left; reflexivity). + all: destruct ctx as [|ctx0 ctx]; [ try (left; reflexivity) | ]. + all: try destruct ctx0. + all: cbn [eval_decision_tree fold_right]; cbv [reveal_rawexpr_cps reveal_rawexpr_cps_gen Option.sequence Option.sequence_return]. + all: repeat first [ rew_eval_decision_tree_step + | progress cbv [value id] in * + | progress cbn [value'] in * + | assumption + | reflexivity + | progress subst + | progress inversion_option + | expr.invert_match_step + | match goal with + | [ |- ?x = ?x \/ _ ] => left; reflexivity + | [ |- Some _ = None \/ _ ] => right + | [ |- None = Some _ \/ _ ] => right + | [ |- ?v = None \/ _ ] + => lazymatch v with + | match ?d with Failure => None | TryLeaf _ _ => None | _ => _ end + => let H := fresh in + assert (H : v = None) by (destruct d; auto); rewrite H + | match ?d with Failure => ?x | TryLeaf _ _ => ?y | _ => _ end + => let H := fresh in + assert (H : v = x \/ v = y) by (destruct d; auto); + destruct H as [H|H]; rewrite H + end + | [ |- context[match ?x with nil => None | cons _ _ => _ end] ] + => is_var x; destruct x + | [ |- match match ?x with nil => None | cons _ _ => _ end with None => None | Some _ => _ end = None \/ _ ] + => is_var x; destruct x; [ left; reflexivity | ] + | [ |- _ \/ exists n ctx', ?f ?a ?b = ?f n ctx' /\ _ ] + => right; exists a, b; split; [ reflexivity | ] + | [ |- exists n ctx', ?f ?a ?b = ?f n ctx' /\ _ ] + => right; exists a, b; split; [ reflexivity | ] + | [ H : ?f ?a ?b = Some ?v |- exists n ctx', Some ?v = ?f n ctx' /\ _ ] + => exists a, b; split; [ symmetry; assumption | ] + end + | break_match_hyps_step ltac:(fun v => is_var v; let t := type of v in unify t type) + | match goal with + | [ H : rawexpr_equiv ?a ?b |- eqlistA _ _ _ ] => unique assert (rawexpr_equiv b a) by (symmetry; exact H) + | [ H : eqlistA _ (_ :: _) _ |- eqlistA _ _ _ ] => inversion H; clear H; subst + | [ H : eqlistA _ nil _ |- eqlistA _ _ _ ] => inversion H; clear H; subst + | [ |- eqlistA _ (cons _ _) (cons _ _) ] => constructor + | [ |- eqlistA _ nil nil ] => constructor + | [ |- rawexpr_equiv _ _ ] => solve [ auto ] + | [ |- rawexpr_equiv (rValue ?v) ?r ] => change (rawexpr_equiv (rExpr v) r) + end + | break_innermost_match_step + | break_innermost_match_hyps_step ]. } + { cbn [eval_decision_tree]; + repeat first [ rew_eval_decision_tree_step + | rew_swap_list_step + | solve [ eauto ] + | break_innermost_match_step ]. } + Qed. + + Lemma eval_rewrite_rules_correct + (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t)) + (maybe_do_again + := fun (should_do_again : bool) (t : base.type) + => if should_do_again return ((@expr.expr base.type ident (if should_do_again then value else var) t) -> UnderLets (expr t)) + then do_again t + else UnderLets.Base) + (d : decision_tree) + (rew_rules : rewrite_rulesT) + (e : rawexpr) + (res := @eval_rewrite_rules do_again d rew_rules e) + : res = UnderLets.Base (expr_of_rawexpr e) + \/ exists n pf e', + nth_error rew_rules n = Some pf + /\ Some res + = rewrite_with_rule do_again (expr_of_rawexpr e) e' pf + /\ rawexpr_equiv e e'. + Proof using raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct. + subst res; cbv [eval_rewrite_rules]. + refine (let H := eval_decision_tree_correct d [e] _ in _). + destruct H as [H| [? [? [H ?] ] ] ]; rewrite H; cbn [Option.sequence Option.sequence_return]; + [ left; reflexivity | ]; clear H. + inversion_head' eqlistA. + unfold Option.bind at 1. + break_innermost_match_step; [ | left; reflexivity ]. + cbn [Option.bind Option.sequence Option.sequence_return]. + match goal with + | [ |- (Option.sequence_return ?x ?y) = _ \/ _ ] + => destruct x eqn:? + end; [ | left; reflexivity ]; cbn [Option.sequence_return]. + right; repeat esplit; try eassumption; auto. + Qed. + End with_var. + + Section with_interp. + Local Notation type_of_list + := (fold_right (fun a b => prod a b) unit). + Local Notation type_of_list_cps + := (fold_right (fun a K => a -> K)). + Context {ident : type.type base.type -> Type} + {ident_interp : forall t, ident t -> type.interp base.interp t} + (eta_ident_cps : forall {T : type.type base.type -> Type} {t} (idc : ident t) + (f : forall t', ident t' -> T t'), + T t) + {pident : type.type pattern.base.type -> Type} + (pident_arg_types : forall t, pident t -> list Type) + (pident_unify pident_unify_unknown : forall t t' (idc : pident t) (idc' : ident t'), option (type_of_list (pident_arg_types t idc))) + {raw_pident : Type} + (strip_types : forall t, pident t -> raw_pident) + (raw_pident_beq : raw_pident -> raw_pident -> bool) + + (full_types : raw_pident -> Type) + (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc)) + (type_of_raw_pident : forall (pidc : raw_pident), full_types pidc -> type.type base.type) + (raw_pident_to_typed : forall (pidc : raw_pident) (args : full_types pidc), ident (type_of_raw_pident pidc args)) + (raw_pident_is_simple : raw_pident -> bool) + (pident_unify_unknown_correct + : forall t t' idc idc', pident_unify_unknown t t' idc idc' = pident_unify t t' idc idc') + (invert_bind_args_unknown_correct + : forall t idc pidc, invert_bind_args_unknown t idc pidc = invert_bind_args t idc pidc) + (eta_ident_cps_correct : forall T t idc f, @eta_ident_cps T t idc f = f _ idc) + (raw_pident_to_typed_invert_bind_args_type + : forall t idc p f, invert_bind_args t idc p = Some f -> t = type_of_raw_pident p f) + (raw_pident_to_typed_invert_bind_args + : forall t idc p f (pf : invert_bind_args t idc p = Some f), + raw_pident_to_typed p f = rew [ident] raw_pident_to_typed_invert_bind_args_type t idc p f pf in idc) + (pident_to_typed + : forall t idc (evm : EvarMap), + type_of_list (pident_arg_types t idc) -> ident (pattern.type.subst_default t evm)) + (ident_interp_Proper : forall t, Proper (eq ==> type.eqv) (@ident_interp t)) + (pident_unify_to_typed + : forall t t' idc idc' v, + pident_unify t t' idc idc' = Some v + -> forall evm pf, + rew [ident] pf in @pident_to_typed t idc evm v = idc'). + + Local Notation var := (type.interp base.interp) (only parsing). + Local Notation type := (type.type base.type). + Local Notation expr := (@expr.expr base.type ident var). + Local Notation pattern := (@pattern.pattern pident). + Local Notation UnderLets := (@UnderLets.UnderLets base.type ident var). + Local Notation ptype := (type.type pattern.base.type). + Local Notation value' := (@value' base.type ident var). + Local Notation value := (@value base.type ident var). + Local Notation value_with_lets := (@value_with_lets base.type ident var). + Local Notation Base_value := (@Base_value base.type ident var). + Local Notation splice_under_lets_with_value := (@splice_under_lets_with_value base.type ident var). + Local Notation splice_value_with_lets := (@splice_value_with_lets base.type ident var). + Local Notation rawexpr := (@rawexpr ident var). + Local Notation eval_decision_tree := (@eval_decision_tree ident var raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation eval_rewrite_rules := (@eval_rewrite_rules ident var pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types). + Local Notation rewrite_with_rule := (@rewrite_with_rule ident var pident pident_arg_types pident_unify pident_unify_unknown). + Local Notation reify := (@reify ident var). + Local Notation reflect := (@reflect ident var). + (*Local Notation rawexpr_equiv_expr := (@rawexpr_equiv_expr ident var).*) + Local Notation rewrite_rule_data_interp_goodT := (@rewrite_rule_data_interp_goodT ident pident pident_arg_types pident_to_typed ident_interp). + Local Notation rewrite_rules_interp_goodT := (@rewrite_rules_interp_goodT ident pident pident_arg_types pident_to_typed ident_interp). + Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pident pident_arg_types). + Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pident pident_arg_types). + Local Notation unify_pattern := (@unify_pattern ident var pident pident_arg_types pident_unify pident_unify_unknown). + Local Notation unify_pattern' := (@unify_pattern' ident var pident pident_arg_types pident_unify pident_unify_unknown). + Local Notation under_with_unification_resultT_relation_hetero := (@under_with_unification_resultT_relation_hetero ident var pident pident_arg_types). + Local Notation under_with_unification_resultT'_relation_hetero := (@under_with_unification_resultT'_relation_hetero ident var pident pident_arg_types). + Local Notation assemble_identifier_rewriters := (@assemble_identifier_rewriters ident var eta_ident_cps pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation assemble_identifier_rewriters' := (@assemble_identifier_rewriters' ident var pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation pattern_default_interp' := (@pattern_default_interp' ident pident pident_arg_types pident_to_typed (@ident_interp)). + Local Notation pattern_default_interp := (@pattern_default_interp ident pident pident_arg_types pident_to_typed (@ident_interp)). + Local Notation pattern_collect_vars := (@pattern.collect_vars pident). + Local Notation app_with_unification_resultT_cps := (@app_with_unification_resultT_cps pident pident_arg_types). + Local Notation app_transport_with_unification_resultT'_cps := (@app_transport_with_unification_resultT'_cps pident pident_arg_types). + Local Notation with_unification_resultT' := (@with_unification_resultT' pident pident_arg_types). + Local Notation value'_interp := (@value'_interp ident ident_interp). + Local Notation eval_decision_tree_correct := (@eval_decision_tree_correct ident var raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple invert_bind_args_unknown_correct raw_pident_to_typed_invert_bind_args_type raw_pident_to_typed_invert_bind_args). + Local Notation expr_interp_related := (@expr.interp_related _ ident _ ident_interp). + Local Notation UnderLets_interp_related := (@UnderLets.interp_related _ ident _ ident_interp _ _ expr_interp_related). + Local Notation rawexpr_interp_related := (@rawexpr_interp_related ident ident_interp). + Local Notation value_interp_related := (@value_interp_related ident ident_interp). + Local Notation unification_resultT'_interp_related := (@unification_resultT'_interp_related ident pident pident_arg_types ident_interp). + Local Notation unification_resultT_interp_related := (@unification_resultT_interp_related ident pident pident_arg_types ident_interp). + Let type_base (t : base.type) : type := type.base t. + Coercion type_base : base.type >-> type. + + Context (reify_and_let_binds_base_cps : forall (t : base.type), expr t -> forall T, (expr t -> UnderLets T) -> UnderLets T) + (interp_reify_and_let_binds_base + : forall t e v, + expr_interp_related e v + -> UnderLets_interp_related (@reify_and_let_binds_base_cps t e _ UnderLets.Base) v). + + Local Notation reify_and_let_binds_cps := (@reify_and_let_binds_cps ident var reify_and_let_binds_base_cps). + Local Notation "e <---- e' ; f" := (splice_value_with_lets e' (fun e => f%under_lets)) : under_lets_scope. + Local Notation "e <----- e' ; f" := (splice_under_lets_with_value e' (fun e => f%under_lets)) : under_lets_scope. + + Local Lemma pident_unify_to_typed' + : forall t t' idc idc' v, + pident_unify t t' idc idc' = Some v + -> forall evm pf, + @pident_to_typed t idc evm v = rew [ident] pf in idc'. + Proof using pident_unify_to_typed. + intros t t' idc idc' v H evm pf. + pose proof (@pident_unify_to_typed t t' idc idc' v H evm (eq_sym pf)). + subst; reflexivity. + Qed. + + Lemma interp_Base_value {t v1 v2} + : value_interp_related v1 v2 + -> value_interp_related (@Base_value t v1) v2. + Proof using Type. + cbv [Base_value]; destruct t; exact id. + Qed. + + Lemma interp_splice_under_lets_with_value_of_ex {T T' t R e f v} + : (exists fv (xv : T'), + UnderLets.interp_related ident_interp R e xv + /\ (forall x1 x2, + R x1 x2 + -> value_interp_related (f x1) (fv x2)) + /\ fv xv = v) + -> value_interp_related (@splice_under_lets_with_value T t e f) v. + Proof using Type. + induction t as [|s IHs d IHd]. + all: repeat first [ progress cbn [value_interp_related splice_under_lets_with_value] in * + | progress intros + | progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | eassumption + | solve [ eauto ] + | now (eapply UnderLets.splice_interp_related_of_ex; eauto) + | match goal with + | [ H : _ |- _ ] => eapply H; clear H + | [ |- exists fv xv, _ /\ _ /\ _ ] + => do 2 eexists; repeat apply conj; [ eassumption | | ] + end ]. + Qed. + + Lemma interp_splice_value_with_lets_of_ex {t t' e f v} + : (exists fv xv, + value_interp_related e xv + /\ (forall x1 x2, + value_interp_related x1 x2 + -> value_interp_related (f x1) (fv x2)) + /\ fv xv = v) + -> value_interp_related (@splice_value_with_lets t t' e f) v. + Proof using Type. + cbv [splice_value_with_lets]; break_innermost_match. + { apply interp_splice_under_lets_with_value_of_ex. } + { intros; destruct_head'_ex; destruct_head'_and; subst; eauto. } + Qed. + + Lemma interp_reify_and_let_binds {with_lets t v1 v} + : value_interp_related v1 v + -> UnderLets_interp_related (@reify_and_let_binds_cps with_lets t v1 _ UnderLets.Base) v. + Proof using interp_reify_and_let_binds_base. + cbv [reify_and_let_binds_cps]; break_innermost_match; + repeat first [ progress intros + | progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | solve [ eauto ] + | apply reify_interp_related + | eapply @UnderLets.splice_interp_related_of_ex with (RA:=expr_interp_related); + eexists (fun x => x), _; repeat apply conj; + [ eassumption | | reflexivity ] ]. + Qed. + + (*Local Infix "===" := expr_interp_related : type_scope. + Local Infix "====" := value_interp_related : type_scope. + Local Infix "=====" := rawexpr_interp_related : type_scope.*) + + Fixpoint types_match_with (evm : EvarMap) {t} (e : rawexpr) (p : pattern t) {struct p} : Prop + := match p, e with + | pattern.Wildcard t, e + => pattern.type.subst t evm = Some (type_of_rawexpr e) + | pattern.Ident t idc, rIdent known t' _ _ _ + => pattern.type.subst t evm = Some t' + | pattern.App s d f x, rApp f' x' _ _ + => @types_match_with evm _ f' f + /\ @types_match_with evm _ x' x + | pattern.Ident _ _, _ + | pattern.App _ _ _ _, _ + => False + end. + + Lemma preunify_types_to_match_with {t re p evm} + : match @preunify_types ident var pident t re p with + | Some None => True + | Some (Some (pt, t')) => pattern.type.subst pt evm = Some t' + | None => False + end + -> types_match_with evm re p. + Proof using Type. + revert re; induction p; intro; cbn [preunify_types types_match_with]; + break_innermost_match; try exact id. + all: repeat first [ progress Bool.split_andb + | progress type_beq_to_eq + | progress inversion_option + | progress Reflect.beq_to_eq + (@type.type_beq pattern.base.type pattern.base.type.type_beq) + (@type.internal_type_dec_bl pattern.base.type pattern.base.type.type_beq pattern.base.type.internal_type_dec_bl) + (@type.internal_type_dec_lb pattern.base.type pattern.base.type.type_beq pattern.base.type.internal_type_dec_lb) + | progress subst + | reflexivity + | progress cbn [Option.bind pattern.type.subst_default pattern.type.subst] + | rewrite pattern.type.eq_subst_default_relax + | rewrite pattern.type.subst_relax + | match goal with + | [ H : (forall re, match preunify_types re ?p with _ => _ end -> _) + |- context[preunify_types ?re' ?p] ] + => specialize (H re') + end + | break_innermost_match_hyps_step + | progress intros + | solve [ auto ] + | exfalso; assumption + | progress type.inversion_type + | progress cbv [Option.bind] in * ]. + Qed. + + Lemma unify_types_match_with {t re p evm} + : @unify_types ident var pident t re p _ id = Some evm + -> types_match_with evm re p. + Proof using Type. + intro H; apply preunify_types_to_match_with; revert H. + cbv [unify_types id]. + break_innermost_match; intros; inversion_option; try exact I. + RewriteRules.pattern.type.add_var_types_cps_id. + cbv [option_type_type_beq] in *; break_innermost_match_hyps; type_beq_to_eq; inversion_option. + let H := match goal with H : option_beq _ _ _ = true |- _ => H end in + apply internal_option_dec_bl in H; + [ | intros; type_beq_to_eq; assumption ]. + subst. + assumption. + Qed. + + Local Notation mk_new_evm0 evm ls + := (fold_right + (fun i k evm' + => k match PositiveMap.find i evm with + | Some v => PositiveMap.add i v evm' + | None => evm' + end) (fun evm' => evm') + (List.rev ls)) (only parsing). + + Local Notation mk_new_evm' evm ps + := (mk_new_evm0 + evm + (PositiveSet.elements ps)) (only parsing). + + Local Notation mk_new_evm evm ps + := (mk_new_evm' evm ps (PositiveMap.empty _)) (only parsing). + + Lemma types_match_with_Proper_evm {t p evm evm' re} + (Hevm : forall k, PositiveSet.mem k (pattern_collect_vars p) = true -> PositiveMap.find k evm = PositiveMap.find k evm') + : @types_match_with evm t re p <-> @types_match_with evm' t re p. + Proof using Type. + revert re; induction p, re; cbn [types_match_with pattern_collect_vars] in *. + all: repeat first [ progress cbn [type_of_rawexpr] in * + | match goal with + | [ H : context[PositiveSet.mem _ (PositiveSet.union _ _)] |- _ ] + => setoid_rewrite PositiveSetFacts.union_b in H + | [ H : context[orb _ _ = true] |- _ ] + => setoid_rewrite Bool.orb_true_iff in H + end + | reflexivity + | progress split_contravariant_or + | progress specialize_by_assumption + | erewrite pattern.type.subst_eq_if_mem by eassumption + | match goal with + | [ H : _ |- _ ] => rewrite H by assumption + | [ |- (?x = Some ?y) <-> (?x' = Some ?y) ] + => cut (x = x'); [ let H := fresh in intro H; rewrite H; reflexivity | ] + end + | apply pattern.type.subst_eq_if_mem ]. + Qed. + + Lemma mem_pattern_collect_vars_types_match_with {evm t re p x} + (H : @types_match_with evm t re p) + (Hmem : PositiveSet.mem x (pattern_collect_vars p) = true) + : PositiveMap.find x evm <> None. + Proof using Type. + revert re H; induction p; intros. + all: repeat first [ progress cbn [pattern_collect_vars types_match_with] in * + | eapply pattern.type.mem_collect_vars_subst_Some_find; eassumption + | progress destruct_head'_and + | progress specialize_by_assumption + | assumption + | exfalso; assumption + | rewrite PositiveSetFacts.union_b, Bool.orb_true_iff in * + | progress destruct_head'_or + | break_innermost_match_hyps_step + | match goal with + | [ H : forall re, types_match_with ?evm re ?p -> _, H' : types_match_with ?evm _ ?p |- _ ] => specialize (H _ H') + end ]. + Qed. + + Lemma mem_collect_vars_pattern_to_type {t p k} + : PositiveSet.mem k (pattern.type.collect_vars t) = true + -> PositiveSet.mem k (@pattern_collect_vars t p) = true. + Proof using Type. + induction p. + all: repeat first [ progress intros + | assumption + | progress cbn [pattern_collect_vars pattern.type.collect_vars] in * + | progress split_contravariant_or + | progress specialize_by_assumption + | rewrite PositiveSetFacts.union_b, Bool.orb_true_iff in * + | solve [ auto ] ]. + Qed. + + Lemma eq_subst_types_pattern_collect_vars t0 pt t evm evm0 + (evm' := mk_new_evm' evm (@pattern_collect_vars t0 pt) evm0) + (Hty : pattern.type.subst t0 evm = Some t) + : pattern.type.subst t0 evm' = Some t. + Proof using Type. + rewrite <- Hty; symmetry; apply pattern.type.subst_eq_Some_if_mem; subst evm'; intros; try congruence; []. + rewrite pattern.base.fold_right_evar_map_find_In. + erewrite mem_collect_vars_pattern_to_type by eassumption. + break_innermost_match; congruence. + Qed. + + Lemma eq_subst_types_pattern_collect_vars_empty_iff t0 pt evm (evm0:=PositiveMap.empty _) + (evm' := mk_new_evm' evm (@pattern_collect_vars t0 pt) evm0) + : pattern.type.subst t0 evm = pattern.type.subst t0 evm'. + Proof using Type. + apply pattern.type.subst_eq_if_mem; subst evm' evm0; intro. + intro H; rewrite pattern.base.fold_right_evar_map_find_In, PositiveMap.gempty, mem_collect_vars_pattern_to_type by assumption. + break_innermost_match; reflexivity. + Qed. + + Lemma types_match_with_new_evm_iff {t re p evm} + (evm' := mk_new_evm evm (pattern_collect_vars p)) + : @types_match_with evm' t re p <-> @types_match_with evm t re p. + Proof using Type. + clear -type_base; subst evm'; apply types_match_with_Proper_evm. + intro k; rewrite pattern.base.fold_right_evar_map_find_In. + intro H; rewrite H. + rewrite PositiveMap.gempty. + break_innermost_match; reflexivity. + Qed. + + Lemma eq_type_of_rawexpr_of_types_match_with {t re p evm} + (Ht : @types_match_with evm t re p) + (Ht' : rawexpr_types_ok re (type_of_rawexpr re)) + (evm' := mk_new_evm evm (pattern_collect_vars p)) + : pattern.type.subst t evm' = Some (type_of_rawexpr re). + Proof using Type. + clear -Ht Ht' type_base. + subst evm'. + apply eq_subst_types_pattern_collect_vars. + revert re Ht Ht'; induction p. + all: repeat first [ progress intros + | progress cbn [type_of_rawexpr types_match_with pattern.type.subst rawexpr_types_ok] in * + | progress cbv [Option.bind] in * + | progress inversion_option + | progress specialize_by_assumption + | progress specialize_by eauto using rawexpr_types_ok_for_type_of_rawexpr + | progress subst + | assumption + | reflexivity + | exfalso; assumption + | progress destruct_head'_and + | break_innermost_match_hyps_step + | match goal with + | [ H : forall re, types_match_with ?evm re ?p -> _, H' : types_match_with ?evm _ ?p |- _ ] + => specialize (H _ H') + | [ H : rawexpr_types_ok _ _ |- _ ] => apply eq_type_of_rawexpr_of_rawexpr_types_ok in H + | [ H : context[type_of_rawexpr ?re] |- _ ] + => generalize dependent (type_of_rawexpr re) + | [ H : type.arrow _ _ = type.arrow _ _ |- _ ] + => inversion_clear H + end ]. + Qed. + + Lemma eq_type_of_rawexpr_of_types_match_with' {t re p evm} + (Ht : @types_match_with evm t re p) + (Ht' : rawexpr_types_ok re (type_of_rawexpr re)) + (evm' := mk_new_evm evm (pattern_collect_vars p)) + : type_of_rawexpr re = pattern.type.subst_default t evm'. + Proof using Type. + symmetry; eapply pattern.type.subst_Some_subst_default, eq_type_of_rawexpr_of_types_match_with; eassumption. + Qed. + + Lemma app_transport_with_unification_resultT'_pattern_default_interp'_cps_id + {K t p evm1 evm2 args k T k'} + : @app_transport_with_unification_resultT'_cps + _ t p evm1 evm2 _ + (@pattern_default_interp' K t p _ k) args + T k' + = (v0 <- (@app_transport_with_unification_resultT'_cps + _ t p evm1 evm2 _ + (@pattern_default_interp' _ t p _ id) args + _ (@Some _)); + k' (k v0))%option. + Proof using Type. + revert K evm1 evm2 args k T k'; induction p. + all: repeat first [ progress intros + | progress cbn [pattern_default_interp' unification_resultT' app_transport_with_unification_resultT'_cps eq_rect] in * + | reflexivity + | progress inversion_option + | progress subst + | progress cbv [id Option.bind option_map] in * + | progress fold (@with_unification_resultT') + | rewrite app_lam_type_of_list + | break_innermost_match_step + | break_innermost_match_hyps_step + | progress rewrite_type_transport_correct + | progress type_beq_to_eq + | progress cps_id'_with_option app_transport_with_unification_resultT'_cps_id + | match goal with + | [ H : forall K evm1 evm2 args k T k', _ = _, H' : context[app_transport_with_unification_resultT'_cps (pattern_default_interp' _ ?evm1v ?kv) ?argsv ?Tv ?k'v] |- _ ] + => lazymatch kv with + | @id _ => fail + | (fun x => x) => fail + | _ => idtac + end; + rewrite (H _ _ _ _ kv Tv k'v) in H' + | [ H : forall K evm1 evm2 args k T k', _ = _ |- context[app_transport_with_unification_resultT'_cps (pattern_default_interp' _ ?evm1v ?kv) ?argsv ?Tv ?k'v] ] + => lazymatch kv with + | @id _ => fail + | (fun x => x) => fail + | _ => idtac + end; + rewrite (H _ _ _ _ kv Tv k'v) + end ]. + Qed. + + Local Ltac solve_side_condition_equations := + repeat + repeat + first [ progress intros + | assumption + | progress subst + | progress cbv [Option.bind] in * + | progress inversion_option + | match goal with + | [ |- ?x = ?x ] => reflexivity + | [ H : ?x = ?x |- _ ] => clear H + | [ H : expr_interp_related _ _ |- type_of_rawexpr _ = _ ] => clear H + | [ H : rawexpr_interp_related _ _ |- type_of_rawexpr _ = _ ] => clear H + | [ H : types_match_with _ _ _ |- type_of_rawexpr _ = _ ] => apply eq_type_of_rawexpr_of_types_match_with in H; [ | eapply rawexpr_types_ok_for_type_of_rawexpr; eassumption ] + | [ H : rawexpr_types_ok _ _ |- type_of_rawexpr _ = _ ] => apply eq_type_of_rawexpr_of_rawexpr_types_ok in H + | [ H : context[pattern.type.subst ?t (fold_right (fun i k evm' => k match PositiveMap.find i ?evm with _ => _ end) _ _ (PositiveMap.empty _))] |- _ ] + => rewrite <- eq_subst_types_pattern_collect_vars_empty_iff in H + | [ H : type.arrow _ _ = type.arrow _ _ |- _ = _ :> type ] + => inversion H; clear H + | [ |- type.arrow _ _ = type.arrow _ _ ] => apply f_equal2 + | [ |- _ = _ :> type ] + => match goal with + | [ |- context[type_of_rawexpr ?re] ] + => is_var re; generalize dependent (type_of_rawexpr re) + | [ H : context[type_of_rawexpr ?re] |- _ ] + => is_var re; generalize dependent (type_of_rawexpr re) + end + end + | progress cbn [pattern.type.subst] in * + | progress break_match_hyps + | match goal with + | [ |- pattern.type.subst_default ?t _ = pattern.type.subst_default ?t _ ] => reflexivity + | [ |- ?t = pattern.type.subst_default _ _ ] + => is_var t; symmetry; apply pattern.type.subst_Some_subst_default + end ]. + + Lemma interp_unify_pattern' {t re p evm res v} + (Hre : rawexpr_interp_related re v) + (H : @unify_pattern' t re p evm _ (@Some _) = Some res) + (Ht : @types_match_with evm t re p) + (Ht' : rawexpr_types_ok re (type_of_rawexpr re)) + (evm' := mk_new_evm evm (pattern_collect_vars p)) + (*Hty : type_of_rawexpr re = pattern.type.subst_default t evm' + := eq_type_of_rawexpr_of_types_match_with' Ht Ht'*) + (Hty : type_of_rawexpr re = pattern.type.subst_default t evm' + := eq_type_of_rawexpr_of_types_match_with' Ht Ht') + : exists resv : _, + unification_resultT'_interp_related res resv + /\ app_transport_with_unification_resultT'_cps + (pattern_default_interp' p evm' id) resv _ (@Some _) + = Some (rew Hty in v). + Proof using pident_unify_unknown_correct pident_unify_to_typed. + clear -pident_unify_unknown_correct pident_unify_to_typed Hre H Ht Ht' Hty. + clearbody Hty. + (*assert (Ht : @types_match_with evm t re p) by (eapply types_match_with_of_unify_pattern'; eassumption).*) + assert (Hevm' : @types_match_with evm' t re p) by now apply types_match_with_new_evm_iff. + clearbody evm'; cbv [unification_resultT'_interp_related]. + revert re res v evm' H Hre Hty Ht' Ht Hevm'; induction p; cbn [unify_pattern' related_unification_resultT' unification_resultT' rawexpr_interp_related app_transport_with_unification_resultT'_cps pattern_default_interp'] in *. + all: repeat + ((unshelve + (repeat first [ progress intros + | rewrite pident_unify_unknown_correct in * + | progress cbv [Option.bind option_bind'] in * + | progress cbn [fst snd rawexpr_interp_related eq_rect rawexpr_types_ok] in * + | progress inversion_option + | progress destruct_head'_ex + | progress destruct_head'_and + | progress inversion_sigma + | progress subst + | progress eliminate_hprop_eq + | progress specialize_by_assumption + | progress specialize_by eauto using rawexpr_types_ok_for_type_of_rawexpr + | exfalso; assumption + | assumption + | match goal with + | [ |- ?x = ?x ] => reflexivity + | [ |- { x : _ | _ = x } ] => eexists; reflexivity + | [ |- exists x, _ = x /\ _ ] => eexists; split; [ reflexivity | ] + | [ |- exists x, _ /\ Some x = Some _ ] => eexists; split; [ | reflexivity ] + end + | progress cps_id'_with_option unify_pattern'_cps_id + | progress cps_id'_with_option app_transport_with_unification_resultT'_cps_id + | progress rewrite_type_transport_correct + | progress type_beq_to_eq + | rewrite app_lam_type_of_list + | break_innermost_match_hyps_step + | break_innermost_match_step + | match goal with + | [ |- exists x : _ * _, (_ /\ _) /\ _ ] => eexists (_, _); split; [ split; eassumption | ] + | [ |- exists res, value_interp_related (value_of_rawexpr _) res ] + => eexists; eapply value_of_rawexpr_interp_related; eassumption + | [ |- value_interp_related (value_of_rawexpr _) _ ] + => eapply value_of_rawexpr_interp_related; eassumption + | [ |- Some _ = Some _ ] => apply f_equal + | [ H : context[eq_type_of_rawexpr_of_types_match_with' ?H1 ?H2] |- _ ] + => generalize dependent (eq_type_of_rawexpr_of_types_match_with' H1 H2) + | [ H : context[rew ?pf in _] |- _ ] + => tryif is_var pf then destruct pf else generalize dependent pf + | [ |- context[rew ?pf in _] ] + => tryif is_var pf then destruct pf else generalize dependent pf + | [ |- context[rew _ in rew _ in _] ] + => rewrite <- eq_trans_rew_distr + | [ |- (rew ?pf1 in ?f) (rew ?pf2 in ?x) = ?f ?x ] + => clear; cbv [eq_rect] + end + | progress cbn [type_of_rawexpr expr.interp types_match_with pattern.type.subst pattern.type.subst_default] in * + | erewrite pident_unify_to_typed' with (pf:=eq_refl) by eassumption + | break_match_step ltac:(fun _ => idtac) + | progress fold (@with_unification_resultT') in * + | match goal with + | [ H : context[app_transport_with_unification_resultT'_cps (pattern_default_interp' _ ?evm1v ?kv) ?argsv ?Tv ?k'v] |- _ ] + => lazymatch kv with + | @id _ => fail + | (fun x => x) => fail + | _ => idtac + end; + rewrite (@app_transport_with_unification_resultT'_pattern_default_interp'_cps_id _ _ _ _ _ argsv kv Tv k'v) in H + | [ |- context[app_transport_with_unification_resultT'_cps (pattern_default_interp' _ ?evm1v ?kv) ?argsv ?Tv ?k'v] ] + => lazymatch kv with + | @id _ => fail + | (fun x => x) => fail + | _ => idtac + end; + setoid_rewrite (@app_transport_with_unification_resultT'_pattern_default_interp'_cps_id _ _ _ _ _ argsv kv Tv k'v) + | [ H : app_transport_with_unification_resultT'_cps ?f ?x _ (@Some _) = ?a, + H' : app_transport_with_unification_resultT'_cps ?f' ?x _ (@Some _) = ?a' + |- _ ] + => unify f f'; + assert (a = a') by (etransitivity; (idtac + symmetry); eassumption); + clear H' + | [ H : context[ex _] |- _ ] + => unshelve edestruct H; clear H; + lazymatch goal with + | [ |- rawexpr_types_ok _ _ ] => eapply rawexpr_types_ok_for_type_of_rawexpr; eassumption + | [ |- unify_pattern' _ _ _ _ _ = Some _ ] => eassumption + | [ |- types_match_with ?evm _ _ ] => tryif is_evar evm then idtac else assumption + | [ |- rawexpr_interp_related _ _ ] => eassumption + | _ => idtac + end; shelve_unifiable; + [ shelve.. | ] + | [ |- type_of_rawexpr _ = _ ] => solve [ solve_side_condition_equations ] + | [ |- types_match_with _ _ _ ] => solve [ solve_side_condition_equations ] + end ])); + shelve_unifiable). + 1-2:match goal with + | [ H : ?x == ?y |- ?x = ?y ] + => apply (type.eqv_iff_eq_of_funext (fun _ _ => functional_extensionality)), H + end. + Qed. + + Lemma interp_unify_pattern {t re p v res} + (Hre : rawexpr_interp_related re v) + (Ht' : rawexpr_types_ok re (type_of_rawexpr re)) + (H : @unify_pattern t re p _ (@Some _) = Some res) + (evm' := mk_new_evm (projT1 res) (pattern_collect_vars p)) + : exists resv, + unification_resultT_interp_related res resv + /\ exists Hty, (app_with_unification_resultT_cps (@pattern_default_interp t p) resv _ (@Some _) = Some (existT (fun evm => type.interp base.interp (pattern.type.subst_default t evm)) evm' (rew Hty in v))). + Proof using pident_unify_unknown_correct pident_unify_to_typed. + subst evm'; cbv [unify_pattern unification_resultT_interp_related unification_resultT related_unification_resultT app_with_unification_resultT_cps pattern_default_interp] in *. + repeat + (unshelve + (repeat first [ progress cbv [Option.bind related_sigT_by_eq] in * + | progress cbn [projT1 projT2 eq_rect] in * + | progress destruct_head'_ex + | progress destruct_head'_and + | progress inversion_option + | progress subst + | exfalso; assumption + | eassumption + | match goal with + | [ H : unify_types _ _ _ _ = Some _ |- _ ] => apply unify_types_match_with in H + | [ H : unify_pattern' _ _ _ _ _ = Some _, H'' : rawexpr_types_ok _ _ |- _ ] + => let T := type of H in + unique pose proof (H : id T) (* save an extra copy *); + epose proof (interp_unify_pattern' _ H _ H'') + | [ H : pattern.type.app_forall_vars (pattern.type.lam_forall_vars _) _ = Some _ |- _ ] => pose proof (pattern.type.app_forall_vars_lam_forall_vars H); clear H + | [ H : pattern.type.app_forall_vars (pattern.type.lam_forall_vars _) _ = None |- None = Some _ ] + => exfalso; revert H; + lazymatch goal with + | [ |- ?x = None -> False ] + => change (x <> None) + end; + rewrite app_lam_forall_vars_not_None_iff + end + | progress cps_id'_with_option unify_types_cps_id + | progress cps_id'_with_option unify_pattern'_cps_id + | progress cps_id'_with_option app_transport_with_unification_resultT'_cps_id + | break_innermost_match_hyps_step + | break_innermost_match_step + | match goal with + | [ |- exists x : sigT _, _ ] => eexists (existT _ _ _) + | [ |- { pf : _ = _ | _ } ] => exists eq_refl + | [ |- { pf : _ = _ & _ } ] => exists eq_refl + | [ |- _ /\ _ ] => split + | [ |- Some _ = Some _ ] => apply f_equal + | [ |- existT _ _ _ = existT _ _ _ ] => apply Sigma.path_sigT_uncurried + | [ H : forall x : rawexpr_types_ok ?a ?b, _, H' : rawexpr_types_ok ?a ?b |- _ ] => specialize (H H') + end + | break_match_step ltac:(fun _ => idtac) + | reflexivity + | progress intros + | eapply mem_pattern_collect_vars_types_match_with; eassumption + | exists (eq_type_of_rawexpr_of_types_match_with' ltac:(eassumption) ltac:(eassumption)) + | match goal with + | [ |- rew ?pf in _ = rew ?pf' in _ ] + => cut (pf = pf'); generalize pf pf'; [ intros; subst; reflexivity | clear; cbv beta zeta; intros ]; + lazymatch goal with + | [ |- ?a = ?b :> (?x = ?y) ] + => generalize dependent x; generalize dependent y; intros; subst; eliminate_hprop_eq; reflexivity + end + end ])). + (* For 8.7 compatibility *) + Grab Existential Variables. + all: assumption. + Qed. + + Lemma interp_maybe_do_again + (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t)) + (Hdo_again : forall t e v, + expr.interp_related_gen ident_interp (fun t => value_interp_related) e v + -> UnderLets_interp_related (do_again t e) v) + {should_do_again : bool} {t e v} + (He : (if should_do_again return @expr.expr _ _ (if should_do_again then _ else _) _ -> _ + then expr.interp_related_gen ident_interp (fun t => value_interp_related) + else expr_interp_related) e v) + : UnderLets_interp_related (@maybe_do_again _ _ do_again should_do_again t e) v. + Proof using Type. + cbv [maybe_do_again]; break_innermost_match; [ apply Hdo_again | cbn [UnderLets.interp_related] ]; + assumption. + Qed. + + Lemma interp_rewrite_with_rule + (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t)) + (Hdo_again : forall t e v, + expr.interp_related_gen ident_interp (fun t => value_interp_related) e v + -> UnderLets_interp_related (do_again t e) v) + (rewr : rewrite_ruleT) + (Hrewr : rewrite_rule_data_interp_goodT (projT2 rewr)) + t e re v1 v2 + (Ht : t = type_of_rawexpr re) + (Ht' : rawexpr_types_ok re (type_of_rawexpr re)) + (He : expr_interp_related e v2) + : @rewrite_with_rule do_again t e re rewr = Some v1 + -> rawexpr_interp_related re (rew Ht in v2) + -> UnderLets_interp_related v1 v2. + Proof using pident_unify_to_typed pident_unify_unknown_correct. + destruct rewr as [p r]. + cbv [rewrite_with_rule]. + repeat first [ match goal with + | [ |- Option.bind ?x _ = Some _ -> _ ] + => destruct x eqn:?; cbn [Option.bind]; [ | intros; solve [ inversion_option ] ] + end + | progress cps_id'_with_option unify_pattern_cps_id + | progress cps_id'_with_option app_with_unification_resultT_cps_id ]. + repeat first [ break_match_step ltac:(fun v => match v with Sumbool.sumbool_of_bool _ => idtac end) + | progress rewrite_type_transport_correct + | progress type_beq_to_eq + | progress cbv [option_bind'] in * + | progress cbn [Option.bind projT1 projT2 UnderLets.interp eq_rect UnderLets_interp_related] in * + | progress destruct_head'_sigT + | progress destruct_head'_sig + | progress inversion_option + | progress subst + | solve [ intros; inversion_option ] + | rewrite UnderLets_interp_related_splice_iff + | match goal with + | [ H : Option.bind ?x _ = Some _ |- _ ] + => destruct x eqn:?; cbn [Option.bind] in H; [ | solve [ inversion_option ] ] + | [ |- expr.interp _ (UnderLets.interp _ (maybe_do_again _ _ _ _)) == _ ] + => apply interp_maybe_do_again_gen; [ assumption | ] + | [ |- context[rew ?pf in _] ] => is_var pf; destruct pf + end ]. + repeat first [ progress destruct_head'_ex + | progress destruct_head'_sig + | progress destruct_head'_and + | exfalso; assumption + | progress inversion_option + | progress subst + | progress cbv [related_sigT_by_eq] in * + | progress cbn [projT1 projT2 eq_rect] in * + | match goal with + | [ H : unify_pattern _ _ _ _ = Some _ |- _ ] => eapply interp_unify_pattern in H; [ | eassumption | eassumption ] + | [ H : unification_resultT_interp_related _ _, Hrewr : rewrite_rule_data_interp_goodT _ |- _ ] + => specialize (Hrewr _ _ H) + | [ H : option_eq _ ?x ?y, H' : ?x' = Some _ |- _ ] + => change x with x' in H; rewrite H' in H; + destruct y eqn:?; cbn [option_eq] in H + | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H' + | [ H : app_with_unification_resultT_cps _ _ _ (@Some _) = Some (existT _ ?evm _) |- _ ] + => is_var evm; + let H' := fresh in + pose proof (projT1_app_with_unification_resultT _ H) as H'; + cbn [projT1] in H'; subst evm + end + | progress cbv [deep_rewrite_ruleTP_gen_good_relation] in * + | unshelve (eapply UnderLets.splice_interp_related_of_ex; eexists (fun x => rew _ in x), _; repeat apply conj; + [ eassumption | intros | ]); + [ etransitivity; eassumption | .. ] + | match goal with + | [ H : ?R ?xv ?v + |- UnderLets_interp_related (fv <-- maybe_do_again _ _ _ ((rew _ in fun x => x) ?xv); _) _ ] + => unshelve (eapply UnderLets.splice_interp_related_of_ex; + eexists (fun x => rew _ in x), (rew _ in v); repeat apply conj; + [ eapply interp_maybe_do_again; try eassumption | | ]) + end ]. + all: repeat first [ assumption + | progress intros + | reflexivity + | progress eliminate_hprop_eq + | progress cbn [UnderLets.interp_related eq_rect] in * + | match goal with + | [ |- context[rew _ in rew _ in _] ] + => rewrite <- eq_trans_rew_distr + | [ |- context[rew ?pf in _] ] + => tryif is_var pf then destruct pf else generalize pf + end ]. + Qed. + + Lemma interp_eval_rewrite_rules + (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t)) + (d : decision_tree) + (rew_rules : rewrite_rulesT) + (re : rawexpr) v + (Hre : rawexpr_types_ok re (type_of_rawexpr re)) + (res := @eval_rewrite_rules do_again d rew_rules re) + (Hdo_again : forall t e v, + expr.interp_related_gen ident_interp (fun t => value_interp_related) e v + -> UnderLets_interp_related (do_again t e) v) + (Hr : rawexpr_interp_related re v) + (Hrew_rules : rewrite_rules_interp_goodT rew_rules) + : UnderLets_interp_related res v. + Proof using raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct pident_unify_unknown_correct pident_unify_to_typed. + subst res; cbv [eval_rewrite_rules]. + refine (let H := eval_decision_tree_correct d [re] _ in _). + destruct H as [H| [? [? [H ?] ] ] ]; rewrite H; cbn [Option.sequence Option.sequence_return UnderLets_interp_related]; + [ now apply expr_of_rawexpr_interp_related | ]; clear H. + inversion_head' eqlistA. + unfold Option.bind at 1. + break_innermost_match_step; [ | cbn [Option.sequence_return UnderLets_interp_related]; now apply expr_of_rawexpr_interp_related ]. + cbn [Option.bind Option.sequence Option.sequence_return UnderLets_interp_related]. + match goal with + | [ |- ?R (Option.sequence_return ?x ?y) _ ] + => destruct x eqn:Hinterp + end; cbn [Option.sequence_return UnderLets.interp]; [ | now apply expr_of_rawexpr_interp_related ]. + unshelve (eapply interp_rewrite_with_rule; [ | | | | eassumption | ]; try eassumption). + { apply eq_type_of_rawexpr_equiv; assumption. } + { eapply Hrew_rules, nth_error_In; rewrite <- sigT_eta; eassumption. } + { erewrite <- rawexpr_types_ok_iff_of_rawexpr_equiv, <- eq_type_of_rawexpr_equiv by eassumption; assumption. } + { apply expr_of_rawexpr_interp_related; assumption. } + { apply rawexpr_interp_related_Proper_rawexpr_equiv; assumption. } + Qed. + + Lemma interp_assemble_identifier_rewriters' + (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t)) + (dt : decision_tree) + (rew_rules : rewrite_rulesT) + t re K + (res := @assemble_identifier_rewriters' dt rew_rules do_again t re K) + (Hre : rawexpr_types_ok re (type_of_rawexpr re)) + (Ht : type_of_rawexpr re = t) + v + (HK : K = (fun P v => rew [P] Ht in v))(* + /\ rew pf in value_of_rawexpr re = ev })*) + (Hdo_again : forall t e v, + expr.interp_related_gen ident_interp (fun t => value_interp_related) e v + -> UnderLets_interp_related (do_again t e) v) + (Hrew_rules : rewrite_rules_interp_goodT rew_rules) + (Hr : rawexpr_interp_related re v) + : value_interp_related res (rew Ht in v). + Proof using raw_pident_to_typed_invert_bind_args_type raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct pident_unify_unknown_correct pident_unify_to_typed. + subst K res. + revert dependent re; induction t as [t|s IHs d IHd]; cbn [assemble_identifier_rewriters' value'_interp]; + intros; fold (@type.interp). + { cbn [value_interp_related]. + destruct Ht; cbn [eq_rect]. + apply interp_eval_rewrite_rules; [ | exact Hdo_again | | ]; assumption. } + { cbn [value_interp_related]. + intros x1 x2 Hx. + lazymatch goal with + | [ |- context[assemble_identifier_rewriters' _ _ _ _ ?re ?K] ] => apply (IHd re eq_refl); clear IHd + end. + { cbv [rValueOrExpr2]; destruct s; cbn. + all: repeat apply conj; try reflexivity. + all: repeat match goal with + | [ H : _ = _ |- _ ] => revert H + | [ H : rawexpr_types_ok _ _ |- _ ] => revert H + end. + all: clear. + all: generalize dependent (type_of_rawexpr re); intros; subst; assumption. } + cbn [rawexpr_interp_related type.interp type_of_rawexpr]. + do 2 eexists. + exists (eq_sym Ht). + unshelve eexists. + { clear; cbv [rValueOrExpr2 type_of_rawexpr]; destruct s; reflexivity. } + repeat apply conj. + all: repeat first [ instantiate (1:=ltac:(eassumption)) + | match goal with + | [ |- expr_interp_related (rew [?P] ?H in ?v) ?ev ] + => is_evar ev; + refine (_ : expr_interp_related (rew [P] H in v) (rew [type.interp base.interp] H in _)) + end + | assumption + | progress cbv [eq_sym eq_rect] + | break_innermost_match_step + | reflexivity + | apply expr_of_rawexpr_interp_related + | apply reify_interp_related ]. } + Qed. + + Lemma interp_assemble_identifier_rewriters + (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t)) + (d : decision_tree) + (rew_rules : rewrite_rulesT) + t idc v + (res := @assemble_identifier_rewriters d rew_rules do_again t idc) + (Hdo_again : forall t e v, + expr.interp_related_gen ident_interp (fun t => value_interp_related) e v + -> UnderLets_interp_related (do_again t e) v) + (Hrew_rules : rewrite_rules_interp_goodT rew_rules) + (Hv : ident_interp t idc == v) + : value_interp_related res v. + Proof using eta_ident_cps_correct raw_pident_to_typed_invert_bind_args_type raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct pident_unify_unknown_correct pident_unify_to_typed. + subst res; cbv [assemble_identifier_rewriters]. + rewrite eta_ident_cps_correct. + match goal with + | [ |- ?R (assemble_identifier_rewriters' ?d ?rew_rules ?do_again ?t ?re' ?K) _ ] + => apply interp_assemble_identifier_rewriters' with (re:=re') (Ht:=eq_refl) + end. + all: cbn [rawexpr_interp_related expr.interp rawexpr_types_ok type_of_rawexpr]. + all: try solve [ reflexivity + | assumption + | auto ]. + Qed. + End with_interp. + + Section with_cast. + Context (cast_outside_of_range : ZRange.zrange -> Z -> Z). + Local Notation var := (type.interp base.interp). + Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). + Local Notation value_interp_related := (@value_interp_related ident (@ident_interp)). + Local Notation expr_interp_related := (@expr.interp_related _ ident _ (@ident_interp)). + + Section with_rewrite_head. + Context (rewrite_head : forall t (idc : ident t), value_with_lets t) + (interp_rewrite_head : forall t idc v, ident_interp idc == v -> value_interp_related (rewrite_head t idc) v). + + Lemma interp_rewrite_bottomup {t e v} + (He : expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v) + : value_interp_related (@rewrite_bottomup var rewrite_head t e) v. + Proof using interp_rewrite_head. + induction e; cbn [rewrite_bottomup value_interp_related expr.interp_related_gen] in *; auto. + all: repeat first [ apply interp_Base_value + | eassumption + | progress cbv beta + | progress intros + | progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | match goal with + | [ IH : forall v, expr.interp_related_gen _ _ ?e v -> _, H' : expr.interp_related_gen _ _ ?e _ |- _ ] + => specialize (IH _ H') + end + | apply reflect_interp_related + | eapply interp_splice_value_with_lets_of_ex; + do 2 eexists; repeat apply conj; [ eassumption | | reflexivity ] + | eapply @interp_splice_under_lets_with_value_of_ex with (R:=expr_interp_related); + do 2 eexists; repeat apply conj + | apply interp_reify_and_let_binds + | apply UnderLets.reify_and_let_binds_base_interp_related + | match goal with + | [ H : _ |- _ ] => eapply H; clear H + | [ |- ?f ?x = ?f ?y ] => is_evar x; reflexivity + | [ |- ?x = ?x ] => reflexivity + end ]. + Qed. + End with_rewrite_head. + + Local Notation nbe := (@rewrite_bottomup var (fun t idc => reflect (expr.Ident idc))). + + Lemma interp_nbe {t e v} + (He : expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v) + : value_interp_related (@nbe t e) v. + Proof using Type. + eapply interp_rewrite_bottomup; try eassumption. + intros; apply reflect_interp_related; cbv [expr.interp_related]; cbn [expr.interp_related_gen]; assumption. + Qed. + + Lemma interp_repeat_rewrite + {rewrite_head fuel t e v} + (retT := value_interp_related (@repeat_rewrite _ rewrite_head fuel t e) v) + (Hrewrite_head + : forall do_again + (Hdo_again : forall t e v, + expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v + -> UnderLets.interp_related (@ident_interp) (expr.interp_related (@ident_interp)) (do_again t e) v) + t idc v, + ident_interp idc == v + -> value_interp_related (@rewrite_head do_again t idc) v) + (He : expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v) + : retT. + Proof using Type. + subst retT. + revert rewrite_head t e v Hrewrite_head He. + induction fuel as [|fuel IH]; cbn [repeat_rewrite]; intros; + apply interp_rewrite_bottomup; auto; intros; + apply Hrewrite_head; auto; intros. + { refine (@interp_nbe (type.base _) _ _ _); assumption. } + { refine (IH _ (type.base _) _ _ _ _); auto. } + Qed. + + Lemma interp_related_rewrite + {rewrite_head fuel t e v} + (retT := expr.interp_related (@ident_interp) (@rewrite _ rewrite_head fuel t e) v) + (Hrewrite_head + : forall do_again + (Hdo_again : forall t e v, + expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v + -> UnderLets.interp_related (@ident_interp) (expr.interp_related (@ident_interp)) (do_again t e) v) + t idc v, + ident_interp idc == v + -> value_interp_related (@rewrite_head do_again t idc) v) + (He : expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v) + : retT. + Proof using Type. + subst retT; cbv [rewrite]. + apply reify_interp_related, interp_repeat_rewrite; auto. + Qed. + + Lemma interp_rewrite + {rewrite_head fuel G t e1 e2} + (retT := expr.interp (@ident_interp) (@rewrite _ rewrite_head fuel t e1) == expr.interp (@ident_interp) e2) + (Hrewrite_head + : forall do_again + (Hdo_again : forall t e v, + expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v + -> UnderLets.interp_related (@ident_interp) (expr.interp_related (@ident_interp)) (do_again t e) v) + t idc v, + ident_interp idc == v + -> value_interp_related (@rewrite_head do_again t idc) v) + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> value_interp_related v1 v2) + (Hwf : expr.wf G e1 e2) + : retT. + Proof using Type. + apply expr.eqv_of_interp_related, interp_related_rewrite; try assumption; []. + eapply expr.interp_related_gen_of_wf; eassumption. + Qed. + + Lemma InterpRewrite + {rewrite_head fuel t e} + (retT := expr.Interp (@ident_interp) (@Rewrite rewrite_head fuel t e) == expr.Interp (@ident_interp) e) + (Hrewrite_head + : forall do_again + (Hdo_again : forall t e v, + expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v + -> UnderLets.interp_related (@ident_interp) (expr.interp_related (@ident_interp)) (do_again t e) v) + t idc v, + ident_interp idc == v + -> value_interp_related (@rewrite_head _ do_again t idc) v) + (Hwf : expr.Wf e) + : retT. + Proof using Type. + subst retT; cbv [Rewrite expr.Interp]. + eapply interp_rewrite; eauto; cbn [List.In]; tauto. + Qed. + End with_cast. + End Compile. + End RewriteRules. +End Compilers. diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v index 3857c8520..888e8f8fb 100644 --- a/src/Experiments/NewPipeline/RewriterProofs.v +++ b/src/Experiments/NewPipeline/RewriterProofs.v @@ -12,7 +12,9 @@ Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesPr Require Import Crypto.Experiments.NewPipeline.Rewriter. Require Import Crypto.Experiments.NewPipeline.RewriterWf1. Require Import Crypto.Experiments.NewPipeline.RewriterWf2. +Require Import Crypto.Experiments.NewPipeline.RewriterInterpProofs1. Require Import Crypto.Experiments.NewPipeline.RewriterRulesGood. +Require Import Crypto.Experiments.NewPipeline.RewriterRulesInterpGood. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SpecializeAllWays. @@ -38,13 +40,17 @@ Module Compilers. Import Rewriter.Compilers. Import RewriterWf1.Compilers. Import RewriterWf2.Compilers. + Import RewriterInterpProofs1.Compilers. Import RewriterRulesGood.Compilers. + Import RewriterRulesInterpGood.Compilers. Import expr.Notations. Import defaults. Import Rewriter.Compilers.RewriteRules. Import RewriterWf1.Compilers.RewriteRules. Import RewriterWf2.Compilers.RewriteRules. + Import RewriterInterpProofs1.Compilers.RewriteRules. Import RewriterRulesGood.Compilers.RewriteRules. + Import RewriterRulesInterpGood.Compilers.RewriteRules. Module Import RewriteRules. @@ -65,7 +71,13 @@ Module Compilers. with nocore; try reflexivity. Local Ltac start_Interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := - start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0. + start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0; + eapply Compile.InterpRewrite; [ | assumption ]; + intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed); + eauto using + pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed, + @ident.gen_interp_Proper, eq_refl + with nocore. Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e). Proof. @@ -106,20 +118,23 @@ Module Compilers. == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. start_Interp_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0). - Admitted. + apply nbe_rewrite_rules_interp_good. + Qed. Lemma Interp_gen_RewriteArith {cast_outside_of_range} (max_const_val : Z) {t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArith max_const_val t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. start_Interp_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0). - Admitted. + apply arith_rewrite_rules_interp_good. + Qed. Lemma Interp_gen_RewriteArithWithCasts {cast_outside_of_range} {t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArithWithCasts t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. start_Interp_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0). - Admitted. + apply arith_with_casts_rewrite_rules_interp_good. + Qed. Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (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)) @@ -129,7 +144,8 @@ Module Compilers. == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. start_Interp_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0). - Admitted. + eapply fancy_rewrite_rules_interp_good; eassumption. + Qed. Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z) (value_range flag_range : ZRange.zrange) @@ -140,7 +156,8 @@ Module Compilers. == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. start_Interp_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0). - Admitted. + eapply fancy_with_casts_rewrite_rules_interp_good; eassumption. + Qed. Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e. Proof. apply Interp_gen_RewriteNBE; assumption. Qed. |