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.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.Tactics.CPSId. Require Import Crypto.Util.Prod. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Sigma.Related. 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 RewriterWf1.Compilers. Import expr.Notations. Import defaults. Import RewriterWf1.Compilers.RewriteRules. Module Import RewriteRules. Import Rewriter.Compilers.RewriteRules. Module Compile. Import Rewriter.Compilers.RewriteRules.Compile. Import RewriterWf1.Compilers.RewriteRules.Compile. Section with_type. 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} (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) (*(raw_pident_bl : forall p q, raw_pident_beq p q = true -> p = q) (raw_pident_lb : forall p q, p = q -> raw_pident_beq p q = true)*). Local Notation type := (type.type base.type). Local Notation pattern := (@pattern.pattern pident). Local Notation expr := (@expr.expr base.type ident). Local Notation UnderLets := (@UnderLets.UnderLets base.type ident). Local Notation ptype := (type.type pattern.base.type). Local Notation value' := (@value' base.type ident). Local Notation value := (@value base.type ident). Local Notation value_with_lets := (@value_with_lets base.type ident). Local Notation Base_value := (@Base_value base.type ident). Local Notation splice_under_lets_with_value := (@splice_under_lets_with_value base.type ident). Local Notation splice_value_with_lets := (@splice_value_with_lets base.type ident). Local Notation reify := (@reify ident). Local Notation reflect := (@reflect ident). Local Notation rawexpr := (@rawexpr ident). Local Notation eval_decision_tree var := (@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 e := (@reveal_rawexpr_cps ident _ e _ id). Section with_var2. Context {var1 var2 : type -> Type}. Context (reify_and_let_binds_base_cps1 : forall (t : base.type), @expr var1 t -> forall T, (@expr var1 t -> @UnderLets var1 T) -> @UnderLets var1 T) (reify_and_let_binds_base_cps2 : forall (t : base.type), @expr var2 t -> forall T, (@expr var2 t -> @UnderLets var2 T) -> @UnderLets var2 T) (wf_reify_and_let_binds_base_cps : forall G (t : base.type) x1 x2 T1 T2 P (Hx : expr.wf G x1 x2) (e1 : expr t -> @UnderLets var1 T1) (e2 : expr t -> @UnderLets var2 T2) (He : forall x1 x2 G' seg, (G' = (seg ++ G)%list) -> expr.wf G' x1 x2 -> UnderLets.wf P G' (e1 x1) (e2 x2)), UnderLets.wf P G (reify_and_let_binds_base_cps1 t x1 T1 e1) (reify_and_let_binds_base_cps2 t x2 T2 e2)). Local Notation wf_value' := (@wf_value' base.type ident var1 var2). Local Notation wf_value := (@wf_value base.type ident var1 var2). Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident var1 var2). Local Notation reify_and_let_binds_cps1 := (@reify_and_let_binds_cps ident var1 reify_and_let_binds_base_cps1). Local Notation reify_and_let_binds_cps2 := (@reify_and_let_binds_cps ident var2 reify_and_let_binds_base_cps2). Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types). Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types). Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 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 eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 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 with_unification_resultT'1 := (@with_unification_resultT' ident var1 pident pident_arg_types). Local Notation with_unification_resultT'2 := (@with_unification_resultT' ident var2 pident pident_arg_types). Local Notation with_unification_resultT1 := (@with_unification_resultT ident var1 pident pident_arg_types). Local Notation with_unification_resultT2 := (@with_unification_resultT ident var2 pident pident_arg_types). Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types). Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types). Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types). Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types). Local Notation wf_rawexpr := (@wf_rawexpr ident var1 var2). (** TODO: Move Me up *) Local Notation unify_pattern'1 := (@unify_pattern' ident var1 pident pident_arg_types pident_unify pident_unify_unknown). Local Notation unify_pattern'2 := (@unify_pattern' ident var2 pident pident_arg_types pident_unify pident_unify_unknown). Local Notation unify_pattern1 := (@unify_pattern ident var1 pident pident_arg_types pident_unify pident_unify_unknown). Local Notation unify_pattern2 := (@unify_pattern ident var2 pident pident_arg_types pident_unify pident_unify_unknown). Local Notation wf_unification_resultT' := (@wf_unification_resultT' ident pident pident_arg_types var1 var2). Local Notation wf_unification_resultT := (@wf_unification_resultT ident pident pident_arg_types var1 var2). Local Notation wf_with_unification_resultT := (@wf_with_unification_resultT ident pident pident_arg_types var1 var2). Local Notation wf_with_unif_rewrite_ruleTP_gen := (@wf_with_unif_rewrite_ruleTP_gen ident pident pident_arg_types var1 var2). Local Notation wf_deep_rewrite_ruleTP_gen := (@wf_deep_rewrite_ruleTP_gen ident var1 var2). Local Notation app_with_unification_resultT_cps1 := (@app_with_unification_resultT_cps pident pident_arg_types (@value var1)). Local Notation app_with_unification_resultT_cps2 := (@app_with_unification_resultT_cps pident pident_arg_types (@value var2)). Local Notation wf_app_with_unification_resultT := (@wf_app_with_unification_resultT ident pident pident_arg_types var1 var2). (* Because [proj1] and [proj2] in the stdlib are opaque *) Local Notation proj1 x := (let (a, b) := x in a). Local Notation proj2 x := (let (a, b) := x in b). Lemma wf_unify_pattern' {G : list { t : _ & (var1 t * var2 t)%type }} {t t'} {p : pattern t} {evm : EvarMap} {re1 re2 e1 e2} (He : @wf_rawexpr G t' re1 e1 re2 e2) : option_eq (wf_unification_resultT' G) (@unify_pattern'1 _ re1 p evm _ (@Some _)) (@unify_pattern'2 _ re2 p evm _ (@Some _)). Proof using Type. revert t' e1 e2 re1 re2 He; induction p; intros; cbn [unify_pattern']. all: repeat first [ progress cbn [Option.bind eq_rect option_eq] in * | assumption | reflexivity | exfalso; assumption | progress subst | progress rewrite_type_transport_correct | progress type_beq_to_eq | progress inversion_option | match goal with | [ H : @wf_rawexpr ?G ?t ?re1 ?e1 ?re2 ?e2 |- context[match ?re1 with _ => _ end] ] => is_var t; is_var re1; is_var e1; is_var re2; is_var e2; is_var G; destruct H end | break_innermost_match_step | progress cps_id'_with_option unify_pattern'_cps_id | match goal with | [ |- context[rew ?pf in _] ] => is_var pf; lazymatch type of pf with | type_of_rawexpr _ = ?t => let t' := fresh "t" in remember t as t' eqn:? in *; destruct pf end | [ H : forall v1 v2, ?PK v1 v2 -> option_eq ?PT (?f1 v1) (?f2 v2) |- option_eq ?PT (?f1 _) (?f2 _) ] => is_var PT; is_var PK; apply H; clear dependent PT | [ H : forall v1 v2, wf_value _ _ _ -> ?PK (?f1 v1) (?f2 v2) |- ?PK (?f1 _) (?f2 _) ] => is_var PK; apply H; clear dependent PK | [ He : wf_rawexpr ?G ?re1 _ ?re2 _ |- wf_value ?G (rew ?pf in value_of_rawexpr ?re1) (value_of_rawexpr ?re2) ] => apply (wf_value_of_wf_rawexpr_gen (pf2:=eq_refl) He) | [ He : wf_rawexpr ?G ?re1 _ ?re2 _ |- wf_unification_resultT' ?G (rew ?pf in value_of_rawexpr ?re1) (rew ?pf2 in value_of_rawexpr ?re2) ] => apply (wf_value_of_wf_rawexpr_gen He) | [ H : wf_rawexpr _ _ _ _ _ |- _ ] => progress (try (unique pose proof (proj1 (eq_type_of_rawexpr_of_wf H))); try (unique pose proof (proj2 (eq_type_of_rawexpr_of_wf H)))) | [ H : ?t1 <> ?t2 |- _ ] => exfalso; apply H; congruence | [ |- context[(rew [?P] ?pf in ?f) ?v] ] => lazymatch P with | fun x : ?A => forall y : @?B x, @?C x y => replace ((rew [P] pf in f) v) with (rew [fun x : A => C x v] pf in f v) by (case pf; reflexivity) end | [ H : (forall t e1 e2 re1 re2, wf_rawexpr _ _ _ _ _ -> option_eq _ (unify_pattern'1 re1 ?p1 ?evm _ (@Some _)) _) |- context[unify_pattern'1 ?re1' ?p1 ?evm _ (@Some _)] ] => specialize (H _ _ _ re1' _ ltac:(eassumption)) | [ H : option_eq ?R ?x ?y |- _ ] => destruct x eqn:?, y eqn:?; cbv [option_eq] in H | [ |- wf_unification_resultT' _ (_, _) (_, _) ] => split; assumption end | progress cbv [Option.bind] in * ]. Qed. Lemma wf_unify_pattern {G : list { t : _ & (var1 t * var2 t)%type }} {t t'} {p : pattern t} {re1 re2 e1 e2} (He : @wf_rawexpr G t' re1 e1 re2 e2) : option_eq (wf_unification_resultT G) (@unify_pattern1 t re1 p _ (@Some _)) (@unify_pattern2 t re2 p _ (@Some _)). Proof using Type. cbv [unify_pattern wf_unification_resultT]. cps_id'_with_option unify_types_cps_id. rewrite <- (wf_unify_types He). cbv [Option.bind]; break_innermost_match_step; [ | reflexivity ]. cps_id'_with_option unify_pattern'_cps_id. pose proof (@wf_unify_pattern' G t t' p ltac:(assumption) re1 re2 e1 e2 He) as H'. match goal with | [ H : option_eq ?R ?x ?y |- _ ] => destruct x eqn:?, y eqn:?; cbv [option_eq] in H end; try solve [ reflexivity | inversion_option | exfalso; assumption ]; cbn [Option.bind option_eq]. cbv [related_unification_resultT related_sigT_by_eq]; exists eq_refl. cbn [eq_rect projT1 projT2]. assumption. Qed. Lemma wf_normalize_deep_rewrite_rule {G} {t} {should_do_again1 with_opt1 under_lets1} {should_do_again2 with_opt2 under_lets2} {r1 r2} (Hwf : @wf_deep_rewrite_ruleTP_gen G t should_do_again1 with_opt1 under_lets1 should_do_again2 with_opt2 under_lets2 r1 r2) : option_eq (UnderLets.wf (fun G' => wf_maybe_do_again_expr G') G) (normalize_deep_rewrite_rule r1) (normalize_deep_rewrite_rule r2). Proof using Type. clear -Hwf. all: destruct_head'_bool. all: cbv [normalize_deep_rewrite_rule wf_deep_rewrite_ruleTP_gen deep_rewrite_ruleTP_gen maybe_option_eq] in *. all: destruct_head'_and. all: repeat first [ assumption | exfalso; assumption | progress cbv [Option.bind option_eq wf_maybe_under_lets_expr] in * | progress inversion_option | match goal with | [ |- ?x = ?x ] => reflexivity | [ |- UnderLets.wf _ _ _ _ ] => constructor end | break_innermost_match_step ]. Qed. Local Ltac fin_handle_list := destruct_head' iff; destruct_head'_and; cbn [length] in *; try solve [ destruct_head'_or; exfalso; repeat match goal with | [ H : ?T, H' : ?T |- _ ] => clear H' | [ H : ?T |- _ ] => lazymatch type of H with | _ = _ :> nat => fail | (_ <= _)%nat => fail | (_ < _)%nat => fail | ~_ = _ :> nat => fail | ~(_ <= _)%nat => fail | ~(_ < _)%nat => fail | _ => clear H end | [ H : context[length ?ls] |- _ ] => generalize dependent (length ls); intros | _ => progress subst | _ => lia end ]. Local Ltac handle_nth_error := repeat match goal with | [ H : nth_error _ _ = None |- _ ] => rewrite nth_error_None in H | [ H : nth_error _ _ = Some _ |- _ ] => unique pose proof (@nth_error_value_length _ _ _ _ H) end; fin_handle_list. Local Ltac handle_swap_list := repeat match goal with | [ H : swap_list _ _ _ = None |- _ ] => rewrite swap_list_None_iff in H | [ H : swap_list _ _ _ = Some _ |- _ ] => unique pose proof (@swap_list_Some_length _ _ _ _ _ H) end; fin_handle_list. Fixpoint wf_eval_decision_tree' {T1 T2} G d (P : option T1 -> option T2 -> Prop) (HPNone : P None None) {struct d} : forall (ctx1 : list (@rawexpr var1)) (ctx2 : list (@rawexpr var2)) (ctxe : list { t : type & @expr var1 t * @expr var2 t }%type) (Hctx1 : length ctx1 = length ctxe) (Hctx2 : length ctx2 = length ctxe) (Hwf : forall t re1 e1 re2 e2, List.In ((re1, re2), existT _ t (e1, e2)) (List.combine (List.combine ctx1 ctx2) ctxe) -> @wf_rawexpr G t re1 e1 re2 e2) cont1 cont2 (Hcont : forall n ls1 ls2, length ls1 = length ctxe -> length ls2 = length ctxe -> (forall t re1 e1 re2 e2, List.In ((re1, re2), existT _ t (e1, e2)) (List.combine (List.combine ls1 ls2) ctxe) -> @wf_rawexpr G t re1 e1 re2 e2) -> (cont1 n ls1 = None <-> cont2 n ls2 = None) /\ P (cont1 n ls1) (cont2 n ls2)), ((@eval_decision_tree var1 T1 ctx1 d cont1) = None <-> (@eval_decision_tree var2 T2 ctx2 d cont2) = None) /\ P (@eval_decision_tree var1 T1 ctx1 d cont1) (@eval_decision_tree var2 T2 ctx2 d cont2). Proof using raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct. clear -HPNone raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct wf_eval_decision_tree'. specialize (fun d => wf_eval_decision_tree' T1 T2 G d P HPNone). destruct d; cbn [eval_decision_tree]; intros; try (clear wf_eval_decision_tree'; tauto). { let d := match goal with d : decision_tree |- _ => d end in specialize (wf_eval_decision_tree' d). cbv [Option.sequence Option.bind Option.sequence_return]; break_innermost_match; specialize_all_ways; handle_swap_list; repeat first [ assumption | match goal with | [ H : ?T, H' : ?T |- _ ] => clear H' end | progress inversion_option | progress destruct_head'_and | progress destruct_head' iff | progress specialize_by_assumption | progress cbn [length] in * | match goal with | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H' | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H' | [ H : length ?x = length ?y, H' : context[length ?x] |- _ ] => rewrite H in H' | [ H : S _ = S _ |- _ ] => inversion H; clear H | [ H : S _ = length ?ls |- _ ] => is_var ls; destruct ls; cbn [length] in H; inversion H; clear H end | congruence | apply conj | progress intros | progress destruct_head'_or ]. } { let d := match goal with d : decision_tree |- _ => d end in pose proof (wf_eval_decision_tree' d) as IHd. let d := match goal with d : option decision_tree |- _ => d end in pose proof (match d as d' return match d' with Some _ => _ | None => True end with | Some d => wf_eval_decision_tree' d | None => I end) as IHapp_case. all: destruct ctx1, ctx2; cbn [length] in *; try (clear wf_eval_decision_tree'; (tauto || congruence)); []. all: lazymatch goal with | [ |- _ /\ ?P match ?d with | TryLeaf _ _ => (?res1 ;; ?ev1)%option | _ => _ end match ?d with | TryLeaf _ _ => (?res2 ;; ?ev2)%option | _ => _ end ] => cut (((res1 = None <-> res2 = None) /\ P res1 res2) /\ ((ev1 = None <-> ev2 = None) /\ P ev1 ev2)); [ clear wf_eval_decision_tree'; intro; destruct_head'_and; destruct_head' iff; destruct d; destruct res1 eqn:?, res2 eqn:?; cbn [Option.sequence]; solve [ intuition (congruence || eauto) ] | ] end. all: split; [ | clear wf_eval_decision_tree'; eapply IHd; eassumption ]. (** We use the trick that [induction] inside [Fixpoint] gives us nested [fix]es that pass the guarded checker, as long as we're careful about how we do things *) let icases := match goal with d : list (_ * decision_tree) |- _ => d end in induction icases as [|icase icases IHicases]; [ | pose proof (wf_eval_decision_tree' (snd icase)) as IHicase ]; clear wf_eval_decision_tree'. (** now we can stop being super-careful about [destruct] ordering because, if we're [Guarded] here (which we are), then we cannot break guardedness from this point on, because we've cleared the bare fixpoint after specializing it to valid arguments *) 2: revert IHicases. all: repeat (rewrite reveal_rawexpr_cps_id; set (reveal_rawexpr _)). all: repeat match goal with H := reveal_rawexpr _ |- _ => subst H end. all:repeat first [ match goal with | [ H : S _ = S _ |- _ ] => inversion H; clear H | [ H : S _ = length ?ls |- _ ] => is_var ls; destruct ls; cbn [length] in H; inversion H; clear H | [ H : forall t re1 e1 re2 e2, _ = _ \/ _ -> _ |- _ ] => pose proof (H _ _ _ _ _ (or_introl eq_refl)); specialize (fun t re1 e1 re2 e2 pf => H t re1 e1 re2 e2 (or_intror pf)) | [ H : wf_rawexpr ?G ?r ?e ?r' ?e' |- context[reveal_rawexpr ?r] ] => apply wf_reveal_rawexpr in H; revert H; generalize (reveal_rawexpr r) (reveal_rawexpr r'); clear r r'; intros r r' H; destruct H | [ H1 : length ?ctx1 = length ?ctxe', H2 : length ?ctx2 = length ?ctxe', H1' : wf_rawexpr _ ?f1 ?f1e ?f2 ?f2e, H2' : wf_rawexpr _ ?x1 ?x1e ?x2 ?x2e |- _ /\ ?P (@eval_decision_tree _ _ (?f1 :: ?x1 :: ?ctx1) _ _) (@eval_decision_tree _ _ (?f2 :: ?x2 :: ?ctx2) _ _) ] => apply IHapp_case with (ctxe:=existT _ _ (f1e, f2e) :: existT _ _ (x1e, x2e) :: ctxe'); clear IHapp_case | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) | [ H : ?x = ?x |- _ ] => clear H | [ |- context [raw_pident_to_typed_invert_bind_args_type ?t ?idc ?p ?f ?pf] ] => generalize (raw_pident_is_simple p) (type_of_raw_pident p f) (raw_pident_to_typed_invert_bind_args_type t idc p f pf); clear p f pf; intros; subst end | tauto | progress subst | progress cbn [length combine List.In fold_right fst snd projT1 projT2 eq_rect Option.sequence Option.sequence_return eq_rect] in * | progress inversion_sigma | progress inversion_prod | progress destruct_head'_sigT | progress destruct_head'_prod | progress destruct_head'_and | progress destruct_head' iff; progress specialize_by (exact eq_refl) | congruence | match goal with | [ |- context[invert_bind_args_unknown] ] => rewrite !invert_bind_args_unknown_correct | [ H : context[invert_bind_args_unknown] |- _ ] => rewrite !invert_bind_args_unknown_correct in H end | rewrite !eval_decision_tree_cont_None | break_innermost_match_step | progress intros | progress destruct_head'_or | solve [ auto ] | match goal with | [ |- wf_rawexpr _ _ _ _ _ ] => constructor | [ H : context[(_ = None <-> _ = None) /\ ?P _ _] |- (_ = None <-> _ = None) /\ ?P _ _ ] => apply H | [ H : fold_right _ None ?ls = None, H' : fold_right _ None ?ls = Some None |- _ ] => exfalso; clear -H H'; is_var ls; destruct ls; cbn [fold_right] in H, H'; break_match_hyps; congruence end | progress break_match | progress cbv [option_bind' Option.bind] | unshelve erewrite raw_pident_to_typed_invert_bind_args; [ shelve | shelve | eassumption | ] | match goal with | [ |- _ /\ ?P (Option.sequence ?x ?y) (Option.sequence ?x' ?y') ] => cut ((x = None <-> x' = None) /\ P x x'); [ destruct x, x'; cbn [Option.sequence]; solve [ intuition congruence ] | ] | [ H1 : length ?ctx1 = length ?ctxe', H2 : length ?ctx2 = length ?ctxe' |- _ /\ ?P (@eval_decision_tree _ _ ?ctx1 _ _) (@eval_decision_tree _ _ ?ctx2 _ _) ] => apply IHicase with (ctxe := ctxe'); auto end ]. } { let d := match goal with d : decision_tree |- _ => d end in specialize (wf_eval_decision_tree' d); rename wf_eval_decision_tree' into IHd. break_innermost_match; handle_swap_list; try tauto; []. lazymatch goal with | [ H : swap_list ?i ?j _ = _ |- _ ] => destruct (swap_list i j ctxe) as [ctxe'|] eqn:? end; handle_swap_list; []. eapply IHd with (ctxe:=ctxe'); clear IHd; try congruence; [ | intros; break_innermost_match; handle_swap_list; apply Hcont; try congruence; [] ]; clear Hcont. all: intros ? ? ? ? ? HIn. 1: eapply Hwf; clear Hwf. 2: lazymatch goal with | [ H : context[List.In _ (combine _ ctxe') -> wf_rawexpr _ _ _ _ _] |- _ ] => apply H; clear H end. all: apply In_nth_error_value in HIn; destruct HIn as [n' HIn]. all: lazymatch goal with | [ H : swap_list ?i ?j _ = _ |- _ ] => apply nth_error_In with (n:=if Nat.eq_dec i n' then j else if Nat.eq_dec j n' then i else n') end. all: repeat first [ reflexivity | match goal with | [ H : context[nth_error (combine _ _) _] |- _ ] => rewrite !nth_error_combine in H | [ |- context[nth_error (combine _ _) _] ] => rewrite !nth_error_combine | [ H : swap_list _ _ ?ls = Some ?ls', H' : context[nth_error ?ls' ?k] |- _ ] => rewrite (nth_error_swap_list H) in H' | [ H : nth_error ?ls ?k = _, H' : context[nth_error ?ls ?k] |- _ ] => rewrite H in H' end | progress subst | progress inversion_option | progress inversion_prod | congruence | progress handle_nth_error | break_innermost_match_step | break_innermost_match_hyps_step ]. } Qed. Lemma wf_eval_decision_tree {T1 T2} G d (P : option T1 -> option T2 -> Prop) (HPNone : P None None) : forall (ctx1 : list (@rawexpr var1)) (ctx2 : list (@rawexpr var2)) (ctxe : list { t : type & @expr var1 t * @expr var2 t }%type) (Hctx1 : length ctx1 = length ctxe) (Hctx2 : length ctx2 = length ctxe) (Hwf : forall t re1 e1 re2 e2, List.In ((re1, re2), existT _ t (e1, e2)) (List.combine (List.combine ctx1 ctx2) ctxe) -> @wf_rawexpr G t re1 e1 re2 e2) cont1 cont2 (Hcont : forall n ls1 ls2, length ls1 = length ctxe -> length ls2 = length ctxe -> (forall t re1 e1 re2 e2, List.In ((re1, re2), existT _ t (e1, e2)) (List.combine (List.combine ls1 ls2) ctxe) -> @wf_rawexpr G t re1 e1 re2 e2) -> (cont1 n ls1 = None <-> cont2 n ls2 = None) /\ P (cont1 n ls1) (cont2 n ls2)), P (@eval_decision_tree var1 T1 ctx1 d cont1) (@eval_decision_tree var2 T2 ctx2 d cont2). Proof using raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct. intros; eapply wf_eval_decision_tree'; eassumption. Qed. Local Ltac do_eq_type_of_rawexpr_of_wf := repeat first [ match goal with | [ |- context[rew [fun t => UnderLets ?var (@?P t)] ?pf in UnderLets.Base ?v] ] => rewrite <- (fun x y p => @Equality.ap_transport _ P (fun t => UnderLets var (P t)) x y p (fun _ => UnderLets.Base)) | [ |- UnderLets.wf _ _ _ _ ] => constructor | [ |- (?x = ?x <-> ?y = ?y) /\ _ ] => split; [ tauto | ] end | apply wf_expr_of_wf_rawexpr' ]. Local Ltac solve_eq_type_of_rawexpr_of_wf := solve [ do_eq_type_of_rawexpr_of_wf ]. Local Ltac gen_do_eq_type_of_rawexpr_of_wf := match goal with | [ |- context[eq_type_of_rawexpr_of_wf ?Hwf] ] => let H' := fresh in pose proof (wf_expr_of_wf_rawexpr Hwf) as H'; rewrite <- (proj1 (eq_expr_of_rawexpr_of_wf Hwf)), <- (proj2 (eq_expr_of_rawexpr_of_wf Hwf)) in H'; destruct Hwf; cbn in H'; cbn [eq_type_of_rawexpr_of_wf eq_rect expr_of_rawexpr type_of_rawexpr] end. (* move me? *) Local Lemma ap_transport_splice {var T} (A B : T -> Type) (x y : T) (p : x = y) (v : @UnderLets var (A x)) (f : A x -> @UnderLets var (B x)) : (rew [fun t => @UnderLets var (B t)] p in UnderLets.splice v f) = UnderLets.splice (rew [fun t => @UnderLets var (A t)] p in v) (fun v => rew [fun t => @UnderLets var (B t)] p in f (rew [A] (eq_sym p) in v)). Proof. case p; reflexivity. Defined. Local Lemma ap_transport_Base {var T} (A : T -> Type) (x y : T) (p : x = y) (v : A x) : (rew [fun t => @UnderLets var (A t)] p in UnderLets.Base v) = UnderLets.Base (rew [A] p in v). Proof. case p; reflexivity. Defined. Local Notation rewrite_rules_goodT := (@rewrite_rules_goodT ident pident pident_arg_types var1 var2). Local Notation wf_rewrite_rule_data := (@wf_rewrite_rule_data ident pident pident_arg_types var1 var2). Local Notation wf_reflect := (@wf_reflect ident var1 var2). Local Notation wf_reify := (@wf_reify ident var1 var2). Local Lemma Some_neq_None_helper {A B x y} : @Some A x = None <-> @Some B y = None. Proof using Type. clear; intuition congruence. Qed. Local Ltac fin_t_common_step := first [ match goal with | [ |- (Some _ = None <-> Some _ = None) /\ _ ] => split; [ exact Some_neq_None_helper | ] | [ |- (?x = ?x <-> ?y = ?y) /\ _ ] => split; [ clear; split; reflexivity | ] | [ |- (Some _ = None <-> None = None) /\ _ ] => exfalso | [ |- (None = None <-> Some _ = None) /\ _ ] => exfalso end ]. Local Ltac handle_lists_of_rewrite_rules := repeat first [ match goal with | [ Hrew : length _ = length _, H : nth_error _ _ = None, H' : nth_error _ _ = Some _ |- _ ] => exfalso; rewrite nth_error_None in H; apply nth_error_value_length in H'; clear -Hrew H H'; try lia | [ H : O = S _ |- _ ] => exfalso; clear -H; congruence | [ H : S _ = O |- _ ] => exfalso; clear -H; congruence end | progress cbv [rewrite_ruleT] in * (* so the nth_error rewrite lines up *) | progress cbn [List.length List.combine List.In Option.bind] in * | match goal with | [ H : S _ = S _ |- _ ] => inversion H; clear H | [ H : length ?ls = O |- _ ] => is_var ls; destruct ls; [ | exfalso; clear -H ] | [ H : length ?ls = S _ |- _ ] => is_var ls; destruct ls; [ exfalso; clear -H | ] | [ H : ?x = ?x |- _ ] => clear H | [ H : forall a b c d e, _ = _ \/ False -> _ |- _ ] => specialize (H _ _ _ _ _ (or_introl eq_refl)) | [ |- context[@nth_error ?A ?ls ?n] ] => destruct (@nth_error A ls n) eqn:? | [ H : forall a b c d, In _ _ -> _, H' : nth_error _ ?n = Some _ |- _ ] => specialize (fun a b c d pf => H a b c d (@nth_error_In _ _ n _ pf)) | [ H : forall a b, In _ _ -> _, H' : nth_error _ ?n = Some _ |- _ ] => specialize (fun a b pf => H a b (@nth_error_In _ _ n _ pf)) | [ H : context[nth_error (combine ?l1 ?l2) ?n] |- _ ] => rewrite (@nth_error_combine _ _ n) in H | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H' | [ H : forall a b c d, Some _ = Some _ -> _ |- _ ] => specialize (H _ _ _ _ eq_refl) | [ H : forall a b, Some _ = Some _ -> _ |- _ ] => specialize (H _ _ eq_refl) end | progress intros | progress destruct_head'_sigT | fin_t_common_step ]. Local Ltac cleanup_after_lists_step := first [ progress subst | progress destruct_head'_sig | progress cbn [eq_rect] in * ]. Local Ltac clear_lists_of_rewrite_rules := match goal with | [ H : length ?ls1 = length ?ls2, H' : nth_error ?ls1 ?n = Some _, H'' : nth_error ?ls2 ?n = Some _ |- _ ] => clear ls1 ls2 n H H' H'' end; repeat cleanup_after_lists_step. Local Ltac try_solve_by_type_of_rawexpr_eqn := match goal with H : _ <> _ |- _ => idtac end; exfalso; repeat match goal with | [ H : ?x <> ?x |- False ] => apply H, eq_refl | [ H : ?x = ?y, H' : ?x <> ?y |- False ] => apply H', H | [ H : ?T |- _ ] => lazymatch T with | _ = _ :> type.type _ => fail | _ <> _ => fail | _ => clear H end | [ H : context[type_of_rawexpr ?r] |- _ ] => generalize dependent (type_of_rawexpr r); clear r; intros | [ H : ?x = ?y |- _ ] => subst x || subst y end; try congruence. Lemma wf_eval_rewrite_rules (do_again1 : forall t : base.type, @expr.expr base.type ident (@value var1) t -> @UnderLets var1 (@expr var1 t)) (do_again2 : forall t : base.type, @expr.expr base.type ident (@value var2) t -> @UnderLets var2 (@expr var2 t)) (wf_do_again : forall G (t : base.type) e1 e2, (exists G', (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) /\ expr.wf G' e1 e2) -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)) (d : @decision_tree raw_pident) (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2) (Hrew : rewrite_rules_goodT rew1 rew2) (re1 : @rawexpr var1) (re2 : @rawexpr var2) {t} G e1 e2 (Hwf : @wf_rawexpr G t re1 e1 re2 e2) : UnderLets.wf (fun G' => expr.wf G') G (rew [fun t => @UnderLets var1 (expr t)] (proj1 (eq_type_of_rawexpr_of_wf Hwf)) in (eval_rewrite_rules1 do_again1 d rew1 re1)) (rew [fun t => @UnderLets var2 (expr t)] (proj2 (eq_type_of_rawexpr_of_wf Hwf)) in (eval_rewrite_rules2 do_again2 d rew2 re2)). Proof using invert_bind_args_unknown_correct pident_unify_unknown_correct raw_pident_to_typed_invert_bind_args. cbv [eval_rewrite_rules Option.sequence_return rewrite_with_rule]. cbv [rewrite_rules_goodT] in Hrew. eapply wf_eval_decision_tree with (ctxe:=[existT _ t (e1, e2)]); cbn [length combine]; try solve [ reflexivity | cbn [combine In]; wf_t; tauto ]. all: split_and. Time all: repeat first [ progress do_eq_type_of_rawexpr_of_wf | handle_lists_of_rewrite_rules ]. clear_lists_of_rewrite_rules. Time all: repeat first [ fin_t_common_step | match goal with | [ H : wf_rawexpr ?G _ _ _ _, H' : forall G', wf_rewrite_rule_data G' _ _ |- _ ] => specialize (H' G) | [ |- context[rew [fun t => @UnderLets ?varp (@?P t)] ?pf in (@UnderLets.splice ?base_type ?ident ?var ?A ?B ?a ?b)] ] => rewrite (@ap_transport_splice varp _ (fun _ => _) P _ _ pf a b : (rew [fun t => @UnderLets varp (P t)] pf in (@UnderLets.splice base_type ident var A B a b)) = _) | [ |- context[rew [fun t => @UnderLets ?varp (@?P t)] ?pf in (@UnderLets.Base ?base_type ?ident ?var ?T ?a)] ] => rewrite ap_transport_Base | [ |- True ] => exact I | [ H : False |- _ ] => exfalso; exact H end | progress subst | progress cbn [Option.bind option_eq projT1 projT2 eq_rect eq_sym eq_trans] in * | progress inversion_option | progress destruct_head'_sigT | progress destruct_head'_sig | progress cbv [wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen option_bind' related_sigT_by_eq] in * | progress intros | match goal with | [ H : wf_rawexpr _ ?r _ _ _ |- context[unify_pattern1 ?r ?pv _ (@Some _)] ] => let H' := fresh in pose proof (wf_unify_pattern (p:=pv) H) as H'; lazymatch type of H' with | option_eq _ ?x ?y => destruct x eqn:?, y eqn:?; cbv [option_eq] in H' end | [ H : wf_deep_rewrite_ruleTP_gen _ ?r1 ?r2 |- context[normalize_deep_rewrite_rule ?r1] ] => let H' := fresh in pose proof (wf_normalize_deep_rewrite_rule H) as H'; lazymatch type of H' with | option_eq _ ?x ?y => destruct x eqn:?, y eqn:?; cbv [option_eq] in H' end | [ H : (forall x y, wf_unification_resultT _ x y -> option_eq _ (app_with_unification_resultT_cps1 ?r1 x _ (@Some _)) (app_with_unification_resultT_cps2 ?r2 y _ (@Some _))), H' : wf_unification_resultT _ ?xv ?yv |- context[app_with_unification_resultT_cps1 ?r1 ?xv _ (@Some _)] ] => specialize (H _ _ H') | [ H : option_eq _ ?x ?y |- _ ] => destruct x eqn:?, y eqn:?; cbv [option_eq] in H | [ |- UnderLets.wf _ _ _ _ ] => constructor | [ |- expr.wf _ (rew _ in expr_of_rawexpr _) (rew _ in expr_of_rawexpr _) ] => apply wf_expr_of_wf_rawexpr' end | progress cps_id'_with_option unify_pattern_cps_id | progress cps_id'_with_option app_with_unification_resultT_cps_id | lazymatch goal with | [ |- context[type.try_make_transport_cps] ] => progress rewrite_type_transport_correct | [ |- context[base.try_make_transport_cps] ] => progress rewrite_type_transport_correct end | progress type_beq_to_eq | break_match_step ltac:(fun v => match v with Sumbool.sumbool_of_bool _ => idtac end) | match goal with | [ H : wf_rawexpr _ _ _ _ _ |- _ ] => let lem1 := constr:(proj1 (eq_type_of_rawexpr_of_wf H)) in let lem2 := constr:(proj2 (eq_type_of_rawexpr_of_wf H)) in progress (lazymatch type of lem1 with | ?x = ?x => idtac | _ => try (unique pose proof lem1) end; lazymatch type of lem2 with | ?x = ?x => idtac | _ => try (unique pose proof lem2) end) end | solve [ try_solve_by_type_of_rawexpr_eqn ] | match goal with | [ |- context[rew ?pf in _] ] => lazymatch pf with | context[eq_type_of_rawexpr_of_wf] => destruct pf end | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice; [ eauto | ]; revgoals | [ H : ?T |- _ ] => has_evar T; solve [ unshelve refine H ] end ]. (* Now we solve the final goal about [maybe_do_again] *) repeat first [ progress destruct_head'_False | progress type.inversion_type | progress eliminate_hprop_eq | break_innermost_match_step | progress cbv [id] in * | match goal with | [ H : wf_maybe_do_again_expr _ ?v _ |- context[?v] ] => clear -H wf_do_again; cbv [wf_maybe_do_again_expr maybe_do_again] in * | [ |- UnderLets.wf _ _ _ _ ] => constructor | [ |- context[type.decode _ _ ?pf ] ] => is_var pf; lazymatch type of pf with | match ?t with type.base _ => _ | _ => _ end => destruct t eqn:? end end | progress destruct_head (@rewrite_ruleTP) | solve [ eauto ] ]. Qed. Section with_do_again. Context (dtree : @decision_tree raw_pident) (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2) (Hrew : rewrite_rules_goodT rew1 rew2) (do_again1 : forall t : base.type, @expr.expr base.type ident (@value var1) t -> @UnderLets var1 (@expr var1 t)) (do_again2 : forall t : base.type, @expr.expr base.type ident (@value var2) t -> @UnderLets var2 (@expr var2 t)) (wf_do_again : forall G G' (t : base.type) e1 e2, (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) -> expr.wf G' e1 e2 -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)). Local Notation assemble_identifier_rewriters' var := (@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 dtree). Local Notation assemble_identifier_rewriters var := (@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 dtree). Lemma wf_assemble_identifier_rewriters' G t re1 e1 re2 e2 K1 K2 (He : @wf_rawexpr G t re1 e1 re2 e2) (HK1 : forall P v, K1 P v = rew [P] (proj1 (eq_type_of_rawexpr_of_wf He)) in v) (HK2 : forall P v, K2 P v = rew [P] (proj2 (eq_type_of_rawexpr_of_wf He)) in v) : wf_value_with_lets G (@assemble_identifier_rewriters' var1 rew1 do_again1 t re1 K1) (@assemble_identifier_rewriters' var2 rew2 do_again2 t re2 K2). Proof. revert dependent G; revert dependent re1; revert dependent re2; induction t as [t|s IHs d IHd]; intros; cbn [assemble_identifier_rewriters']. { rewrite HK1, HK2; apply wf_eval_rewrite_rules; try assumption. intros; destruct_head'_ex; destruct_head'_and; eauto. } { hnf; intros; subst. unshelve eapply IHd; cbn [type_of_rawexpr]; [ shelve | shelve | constructor | cbn; reflexivity | cbn; reflexivity ]. all: rewrite ?HK1, ?HK2. { erewrite (proj1 (eq_expr_of_rawexpr_of_wf He)), (proj2 (eq_expr_of_rawexpr_of_wf He)). eapply wf_rawexpr_Proper_list; [ | eassumption ]; wf_t. } { cbv [rValueOrExpr2]; break_innermost_match; constructor; try apply wf_reify; (eapply wf_value'_Proper_list; [ | eassumption ]); wf_t. } } Qed. Lemma wf_assemble_identifier_rewriters G t (idc : ident t) : wf_value_with_lets G (@assemble_identifier_rewriters var1 rew1 do_again1 t idc) (@assemble_identifier_rewriters var2 rew2 do_again2 t idc). Proof. cbv [assemble_identifier_rewriters]; rewrite !eta_ident_cps_correct. unshelve eapply wf_assemble_identifier_rewriters'; [ shelve | shelve | constructor | | ]; reflexivity. Qed. End with_do_again. End with_var2. End with_type. Section full_with_var2. Context {var1 var2 : type.type base.type -> Type}. Local Notation expr := (@expr.expr base.type ident). Local Notation value := (@Compile.value base.type ident). Local Notation value_with_lets := (@Compile.value_with_lets base.type ident). Local Notation UnderLets := (UnderLets.UnderLets base.type ident). Local Notation reflect := (@Compile.reflect ident). Section with_rewrite_head. Context (rewrite_head1 : forall t (idc : ident t), @value_with_lets var1 t) (rewrite_head2 : forall t (idc : ident t), @value_with_lets var2 t) (wf_rewrite_head : forall G t (idc1 idc2 : ident t), idc1 = idc2 -> wf_value_with_lets G (rewrite_head1 t idc1) (rewrite_head2 t idc2)). Local Notation rewrite_bottomup1 := (@rewrite_bottomup var1 rewrite_head1). Local Notation rewrite_bottomup2 := (@rewrite_bottomup var2 rewrite_head2). Lemma wf_rewrite_bottomup G G' {t} e1 e2 (Hwf : expr.wf G e1 e2) (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value G' v1 v2) : wf_value_with_lets G' (@rewrite_bottomup1 t e1) (@rewrite_bottomup2 t e2). Proof. revert dependent G'; induction Hwf; intros; cbn [rewrite_bottomup]. all: repeat first [ reflexivity | solve [ eauto ] | apply wf_rewrite_head | apply wf_Base_value | apply wf_splice_value_with_lets | apply wf_splice_under_lets_with_value | apply wf_reify_and_let_binds_cps | apply UnderLets.wf_reify_and_let_binds_base_cps | apply wf_reflect | progress subst | progress destruct_head'_ex | progress cbv [wf_value_with_lets wf_value] in * | progress cbn [wf_value' fst snd] in * | progress intros | wf_safe_t_step | eapply wf_value'_Proper_list; [ | solve [ eauto ] ] | match goal with | [ |- UnderLets.wf _ _ _ _ ] => constructor | [ H : _ |- _ ] => apply H; clear H end ]. Qed. End with_rewrite_head. Local Notation nbe var := (@rewrite_bottomup var (fun t idc => reflect (expr.Ident idc))). Lemma wf_nbe G G' {t} e1 e2 (Hwf : expr.wf G e1 e2) (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value G' v1 v2) : wf_value_with_lets G' (@nbe var1 t e1) (@nbe var2 t e2). Proof. eapply wf_rewrite_bottomup; try eassumption. intros; subst; eapply wf_reflect; wf_t. Qed. Section with_rewrite_head2. Context (rewrite_head1 : forall (do_again : forall t : base.type, @expr (@value var1) (type.base t) -> @UnderLets var1 (@expr var1 (type.base t))) t (idc : ident t), @value_with_lets var1 t) (rewrite_head2 : forall (do_again : forall t : base.type, @expr (@value var2) (type.base t) -> @UnderLets var2 (@expr var2 (type.base t))) t (idc : ident t), @value_with_lets var2 t) (wf_rewrite_head : forall do_again1 do_again2 (wf_do_again : forall G' G (t : base.type) e1 e2 (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value G' v1 v2), expr.wf G e1 e2 -> UnderLets.wf (fun G' => expr.wf G') G' (do_again1 t e1) (do_again2 t e2)) G t (idc1 idc2 : ident t), idc1 = idc2 -> wf_value_with_lets G (rewrite_head1 do_again1 t idc1) (rewrite_head2 do_again2 t idc2)). Lemma wf_repeat_rewrite fuel : forall {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value G' v1 v2), wf_value_with_lets G' (@repeat_rewrite var1 rewrite_head1 fuel t e1) (@repeat_rewrite var2 rewrite_head2 fuel t e2). Proof. induction fuel as [|fuel IHfuel]; intros; cbn [repeat_rewrite]; eapply wf_rewrite_bottomup; try eassumption; apply wf_rewrite_head; intros; [ eapply wf_nbe with (t:=type.base _) | eapply IHfuel with (t:=type.base _) ]; eassumption. Qed. Lemma wf_rewrite fuel : forall {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value G' v1 v2), expr.wf G' (@rewrite var1 rewrite_head1 fuel t e1) (@rewrite var2 rewrite_head2 fuel t e2). Proof. intros; eapply wf_reify, wf_repeat_rewrite; eassumption. Qed. End with_rewrite_head2. End full_with_var2. Theorem Wf_Rewrite (rewrite_head : forall var (do_again : forall t : base.type, @expr (@value base.type ident var) (type.base t) -> @UnderLets.UnderLets base.type ident var (@expr var (type.base t))) t (idc : ident t), @value_with_lets base.type ident var t) (wf_rewrite_head : forall var1 var2 do_again1 do_again2 (wf_do_again : forall G G' (t : base.type) e1 e2, (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) -> expr.wf G' e1 e2 -> UnderLets.wf (fun G' => expr.wf G') G (do_again1 t e1) (do_again2 t e2)) t (idc : ident t), wf_value_with_lets nil (rewrite_head var1 do_again1 t idc) (rewrite_head var2 do_again2 t idc)) fuel {t} (e : Expr t) (Hwf : Wf e) : Wf (@Rewrite rewrite_head fuel t e). Proof. intros var1 var2; cbv [Rewrite]; eapply wf_rewrite with (G:=nil); [ | apply Hwf | wf_t ]. intros; subst; eapply wf_value'_Proper_list; [ | eapply wf_rewrite_head ]; wf_t. Qed. End Compile. End RewriteRules. End Compilers.