diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretationProofs.v | 5 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Language.v | 13 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 35 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 69 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/UnderLetsProofs.v | 310 |
6 files changed, 237 insertions, 197 deletions
diff --git a/.gitignore b/.gitignore index 51f1d10ce..a832118d6 100644 --- a/.gitignore +++ b/.gitignore @@ -45,6 +45,8 @@ nra.cache /time-of-build-pretty.log /time-of-build.log +/*.out + # compilation outputs /*.o etc/tscfreq diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v index 2d871b103..0e7d55c7a 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v @@ -1281,8 +1281,8 @@ Module Compilers. assert (arg1_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg1) by (hnf; etransitivity; [ eassumption | symmetry; eassumption ]). assert (arg2_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg2) - by (hnf; etransitivity; [ symmetry; eassumption | eassumption ]). - rewrite <- (@GeneralizeVar.Interp_GeneralizeVar _ E) by auto. + by (hnf; etransitivity; [ symmetry; eassumption | eassumption ]). + rewrite <- (@GeneralizeVar.Interp_GeneralizeVar _ _ E) by auto. apply Interp_EtaExpandWithListInfoFromBound; auto with wf. Qed. @@ -1324,7 +1324,6 @@ Module Compilers. | rewrite <- Extract_FromFlat_ToFlat by auto with typeclass_instances; apply Interp_PartialEvaluateWithBounds_bounded; auto | rewrite Extract_FromFlat_ToFlat by auto with wf typeclass_instances | progress intros - | progress cbv [ident.interp] | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ] | solve [ eauto with wf typeclass_instances ] | erewrite !Interp_PartialEvaluateWithBounds diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index bd668c50e..07b416f54 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -1021,13 +1021,11 @@ Module Compilers. Definition cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z. Proof. exact v. Qed. - - (** Interpret identifiers where [Z_cast] is an opaque identity - function when the value is not inside the range *) - Definition interp {t} (idc : ident t) : type.interp base.interp t - := @gen_interp cast_outside_of_range t idc. - Global Arguments interp _ !_ / . End with_base. + + (** Interpret identifiers where [Z_cast] is an opaque identity + function when the value is not inside the range *) + Notation interp := (@gen_interp cast_outside_of_range). Notation LiteralUnit := (@Literal base.type.unit). Notation LiteralZ := (@Literal base.type.Z). Notation LiteralBool := (@Literal base.type.bool). @@ -1297,14 +1295,13 @@ Module Compilers. Notation "x || y" := (#Z_lor @ x @ y)%expr : expr_scope. Notation "x 'mod' y" := (#Z_modulo @ x @ y)%expr : expr_scope. Notation "- x" := (#Z_opp @ x)%expr : expr_scope. - Global Arguments interp _ !_. Global Arguments gen_interp _ _ !_. End Notations. End ident. Export ident.Notations. Notation ident := ident.ident. - Global Strategy -1000 [expr.Interp expr.interp ident.interp type.interp base.interp base.base_interp ident.gen_interp]. + Global Strategy -1000 [expr.Interp expr.interp type.interp base.interp base.base_interp ident.gen_interp]. Ltac reify var term := expr.reify base.type ident ltac:(base.reify) ident.reify var term. Ltac Reify term := diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 4caa34297..1a90024e4 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -728,18 +728,21 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ End with_1. End interp_gen. - Section for_interp. + Section with_cast. + Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}. + Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). + Local Notation interp := (@expr.interp _ _ _ (@ident_interp)). + Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)). Local Open Scope etype_scope. - Import defaults. Lemma wf_interp_Proper G {t} e1 e2 (Hwf : @wf _ _ _ _ G t e1 e2) (HG : forall t v1 v2, In (existT _ t (v1, v2)) G -> v1 == v2) : interp e1 == interp e2. - Proof. apply @wf_interp_Proper_gen1 with (G:=G); eauto using ident.interp_Proper. Qed. + Proof. apply @wf_interp_Proper_gen1 with (G:=G); eauto using ident.gen_interp_Proper. Qed. - Lemma Wf_Interp_Proper {t} (e : Expr t) : Wf e -> Proper type.eqv (Interp e). + Lemma Wf_Interp_Proper {t} (e : expr.Expr t) : Wf e -> Proper type.eqv (Interp e). Proof. repeat intro; apply wf_interp_Proper with (G:=nil); cbn [List.In]; intuition eauto. Qed. - End for_interp. + End with_cast. Section invert. Section with_var2. @@ -1420,21 +1423,17 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ Proof. apply @Interp_gen2_GeneralizeVar; eassumption. Qed. End gen1. - Lemma interp_from_flat_to_flat' - {t} (e1 : expr t) (e2 : expr t) G ctx - (H_ctx_G : forall t v1 v2, List.In (existT _ t (v1, v2)) G - -> (exists v2', PositiveMap.find v1 ctx = Some (existT _ t v2') /\ v2' == v2)) - (Hwf : expr.wf G e1 e2) - cur_idx - (Hidx : forall p, PositiveMap.mem p ctx = true -> BinPos.Pos.lt p cur_idx) - : interp (from_flat (to_flat' e1 cur_idx) _ ctx) == interp e2. - Proof. apply @interp_gen1_from_flat_to_flat' with (G:=G); eauto using ident.interp_Proper. Qed. + Section with_cast. + Context {cast_outside_of_range : zrange -> Z -> Z}. + + Local Notation Interp := (expr.Interp (@ident.gen_interp cast_outside_of_range)). - Lemma Interp_FromFlat_ToFlat {t} (e : Expr t) (Hwf : expr.Wf e) : Interp (FromFlat (ToFlat e)) == Interp e. - Proof. apply @Interp_gen1_FromFlat_ToFlat; eauto using ident.interp_Proper. Qed. + Lemma Interp_FromFlat_ToFlat {t} (e : Expr t) (Hwf : expr.Wf e) : Interp (FromFlat (ToFlat e)) == Interp e. + Proof. apply @Interp_gen1_FromFlat_ToFlat; eauto using ident.gen_interp_Proper. Qed. - Lemma Interp_GeneralizeVar {t} (e : Expr t) (Hwf : expr.Wf e) : Interp (GeneralizeVar (e _)) == Interp e. - Proof. apply Interp_FromFlat_ToFlat, Hwf. Qed. + Lemma Interp_GeneralizeVar {t} (e : Expr t) (Hwf : expr.Wf e) : Interp (GeneralizeVar (e _)) == Interp e. + Proof. apply Interp_FromFlat_ToFlat, Hwf. Qed. + End with_cast. End GeneralizeVar. Ltac prove_Wf _ := diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 59ce4a33e..ac6cd218d 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -675,6 +675,30 @@ Module Pipeline. Record to_fancy_args := { invert_low : Z (*log2wordmax*) -> Z -> option Z ; invert_high : Z (*log2wordmax*) -> Z -> option Z }. + Definition RewriteAndEliminateDeadAndInline {t} + (DoRewrite : Expr t -> Expr t) + (with_dead_code_elimination : bool) + (with_subst01 : bool) + (E : Expr t) + : Expr t + := let E := DoRewrite E in + (* Note that DCE evaluates the expr with two different [var] + arguments, and so results in a pipeline that is 2x slower + unless we pass through a uniformly concrete [var] type + first *) + dlet_nd e := ToFlat E in + let E := FromFlat e in + let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in + dlet_nd e := ToFlat E in + let E := FromFlat e in + let E := if with_subst01 then Subst01.Subst01 E else E in + let E := UnderLets.LetBindReturn E in + let E := DoRewrite E in (* after inlining, see if any new rewrite redexes are available *) + dlet_nd e := ToFlat E in + let E := FromFlat e in + let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in + E. + Definition BoundsPipeline (with_dead_code_elimination : bool := true) (with_subst01 : bool) @@ -688,22 +712,7 @@ Module Pipeline. := (*let E := expr.Uncurry E in*) let E := PartialEvaluateWithListInfoFromBounds E arg_bounds in let E := PartialEvaluate E in - let E := RewriteRules.RewriteArith 0 E in - (* Note that DCE evaluates the expr with two different [var] - arguments, and so results in a pipeline that is 2x slower - unless we pass through a uniformly concrete [var] type - first *) - dlet_nd e := ToFlat E in - let E := FromFlat e in - let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in - dlet_nd e := ToFlat E in - let E := FromFlat e in - let E := if with_subst01 then Subst01.Subst01 E else E in - let E := UnderLets.LetBindReturn E in - let E := RewriteRules.RewriteArith 0 E in (* after inlining, see if any new rewrite redexes are available *) - dlet_nd e := ToFlat E in - let E := FromFlat e in - let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in + let E := RewriteAndEliminateDeadAndInline (RewriteRules.RewriteArith 0) with_dead_code_elimination with_subst01 E in let E := RewriteRules.RewriteArith (2^8) E in (* reassociate small consts *) let E := match translate_to_fancy with | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancy invert_low invert_high E @@ -788,7 +797,8 @@ Module Pipeline. | solve [ auto with interp wf ] | solve [ typeclasses eauto ] | break_innermost_match_step - | solve [ auto 100 with wf ] ]. + | solve [ auto 100 with wf ] + | progress intros ]. Class bounds_goodT {t} bounds := bounds_good : @@ -800,6 +810,30 @@ Module Pipeline. Hint Extern 1 (type_goodT _) => vm_compute; reflexivity : typeclass_instances. + Lemma Wf_RewriteAndEliminateDeadAndInline {t} DoRewrite with_dead_code_elimination with_subst01 + (Wf_DoRewrite : forall E, Wf E -> Wf (DoRewrite E)) + E + (Hwf : Wf E) + : Wf (@RewriteAndEliminateDeadAndInline t DoRewrite with_dead_code_elimination with_subst01 E). + Proof. cbv [RewriteAndEliminateDeadAndInline Let_In]; wf_interp_t. Qed. + + Global Hint Resolve @Wf_RewriteAndEliminateDeadAndInline : wf. + + Lemma Interp_RewriteAndEliminateDeadAndInline {cast_outside_of_range} {t} DoRewrite with_dead_code_elimination with_subst01 + (Interp_DoRewrite : forall E, Wf E -> expr.Interp (@ident.gen_interp cast_outside_of_range) (DoRewrite E) == expr.Interp (@ident.gen_interp cast_outside_of_range) E) + (Wf_DoRewrite : forall E, Wf E -> Wf (DoRewrite E)) + E + (Hwf : Wf E) + : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteAndEliminateDeadAndInline t DoRewrite with_dead_code_elimination with_subst01 E) + == expr.Interp (@ident.gen_interp cast_outside_of_range) E. + Proof. + cbv [RewriteAndEliminateDeadAndInline Let_In]; + repeat (wf_interp_t || rewrite !Interp_DoRewrite). + Qed. + + Global Hint Rewrite @Interp_RewriteAndEliminateDeadAndInline : interp. + + Local Opaque RewriteAndEliminateDeadAndInline. Lemma BoundsPipeline_correct (with_dead_code_elimination : bool := true) (with_subst01 : bool) @@ -862,6 +896,7 @@ Module Pipeline. all: wf_interp_t. } { wf_interp_t. } } Qed. + Local Transparent RewriteAndEliminateDeadAndInline. Definition BoundsPipeline_correct_transT {t} diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v index 8882f7a47..dcc5cf28b 100644 --- a/src/Experiments/NewPipeline/UnderLetsProofs.v +++ b/src/Experiments/NewPipeline/UnderLetsProofs.v @@ -144,9 +144,16 @@ Module Compilers. : expr.Wf e -> expr.Wf (SubstVarLike.SubstVarFstSndPairOpp e). Proof. apply Wf_SubstVarOrIdent. Qed. - Lemma Interp_SubstVarFstSndPairOpp {t} (e : expr.Expr t) (Hwf : expr.Wf e) - : defaults.Interp (SubstVarLike.SubstVarFstSndPairOpp e) == defaults.Interp e. - Proof. apply Interp_SubstVarOrIdent, Hwf. Qed. + Section with_cast. + Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}. + Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). + Local Notation interp := (@expr.interp _ _ _ (@ident_interp)). + Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)). + + Lemma Interp_SubstVarFstSndPairOpp {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : Interp (SubstVarLike.SubstVarFstSndPairOpp e) == Interp e. + Proof. apply Interp_SubstVarOrIdent, Hwf. Qed. + End with_cast. End SubstVarLike. Hint Resolve SubstVarLike.Wf_SubstVar SubstVarLike.Wf_SubstVarFstSndPairOpp SubstVarLike.Wf_SubstVarLike SubstVarLike.Wf_SubstVarOrIdent : wf. @@ -477,6 +484,7 @@ Module Compilers. Context (cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z). Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). Local Notation interp := (@expr.interp _ _ _ (@ident_interp)). + Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)). Lemma interp_reify_and_let_binds_base_cps {t e T k} @@ -512,161 +520,161 @@ Module Compilers. eapply interp_reify_and_let_binds_base_cps; cbn [UnderLets.interp]. trivial. Qed. - End with_cast. - Lemma Wf_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : expr.Wf (LetBindReturn e). - Proof. intros ??; apply wf_let_bind_return, Hwf. Qed. + Local Ltac interp_to_expr_reify_and_let_binds_base_cps_t Hk := + repeat first [ progress subst + | progress destruct_head' False + | progress destruct_head'_and + | progress destruct_head' iff + | progress specialize_by_assumption + | progress expr.inversion_wf_constr + | progress expr.inversion_expr + | progress expr.invert_subst + | progress destruct_head'_sig + | progress destruct_head'_ex + | progress destruct_head'_and + | progress type.inversion_type + | progress base.type.inversion_type + | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind to_expr expr.interp ident.interp ident.gen_interp type.eqv length list_rect combine In] in * + | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in * + | rewrite base.try_make_transport_cps_correct in * + | progress type_beq_to_eq + | discriminate + | congruence + | apply Hk + | exists nil; reflexivity + | eexists (cons _ nil); reflexivity + | rewrite app_assoc; eexists; reflexivity + | rewrite expr.reify_list_cons + | rewrite expr.reify_list_nil + | progress interp_safe_t + | match goal with + | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H + | [ H : forall t v1 v2, In _ _ -> _ == _, H' : In _ _ |- _ ] => apply H in H' + end + | progress inversion_option + | progress break_innermost_match_hyps + | progress expr.inversion_wf_one_constr + | progress expr.invert_match_step + | match goal with + | [ |- ?R (expr.interp _ ?e1) (expr.interp _ ?e2) ] + => solve [ eapply (@expr.wf_interp_Proper _ _ _ e1 e2); eauto ] + | [ H : context[reflect_list (reify_list _)] |- _ ] => rewrite expr.reflect_reify_list in H + | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ] + => pose proof (fun x y pf => H x y (or_introl pf)); + pose proof (fun x y pf => H x y (or_intror pf)); + clear H + end + | progress interp_unsafe_t_step + | match goal with + | [ H : expr.wf _ (reify_list _) ?e |- _ ] + => is_var e; destruct (reflect_list e) eqn:?; expr.invert_subst; + [ rewrite expr.wf_reify_list in H | apply expr.wf_reflect_list in H ] + | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H + | [ H : context[expr.interp _ _ = _] |- expr.interp _ (to_expr _) = ?k2 _ ] + => erewrite H; clear H; + [ match goal with + | [ |- ?k (expr.interp ?ii ?e) = ?k' ?v ] + => has_evar e; + let p := fresh in + set (p := expr.interp ii e); + match v with + | context G[expr.interp ii ?e'] + => unify e e'; let v' := context G[p] in change (k p = k' v') + end; + clearbody p; reflexivity + end + | .. ] + end ]. - Local Ltac interp_to_expr_reify_and_let_binds_base_cps_t Hk := - repeat first [ progress subst - | progress destruct_head' False - | progress destruct_head'_and - | progress destruct_head' iff - | progress specialize_by_assumption - | progress expr.inversion_wf_constr - | progress expr.inversion_expr - | progress expr.invert_subst - | progress destruct_head'_sig - | progress destruct_head'_ex - | progress destruct_head'_and - | progress type.inversion_type - | progress base.type.inversion_type - | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind to_expr expr.interp ident.interp ident.gen_interp type.eqv length list_rect combine In] in * - | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in * - | rewrite base.try_make_transport_cps_correct in * - | progress type_beq_to_eq - | discriminate - | congruence - | apply Hk - | exists nil; reflexivity - | eexists (cons _ nil); reflexivity - | rewrite app_assoc; eexists; reflexivity - | rewrite expr.reify_list_cons - | rewrite expr.reify_list_nil - | progress interp_safe_t - | match goal with - | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H - | [ H : forall t v1 v2, In _ _ -> _ == _, H' : In _ _ |- _ ] => apply H in H' - end - | progress inversion_option - | progress break_innermost_match_hyps - | progress expr.inversion_wf_one_constr - | progress expr.invert_match_step - | match goal with - | [ |- ?R (expr.interp _ ?e1) (expr.interp _ ?e2) ] - => solve [ eapply (@expr.wf_interp_Proper _ _ e1 e2); eauto ] - | [ H : context[reflect_list (reify_list _)] |- _ ] => rewrite expr.reflect_reify_list in H - | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ] - => pose proof (fun x y pf => H x y (or_introl pf)); - pose proof (fun x y pf => H x y (or_intror pf)); - clear H - end - | progress interp_unsafe_t_step - | match goal with - | [ H : expr.wf _ (reify_list _) ?e |- _ ] - => is_var e; destruct (reflect_list e) eqn:?; expr.invert_subst; - [ rewrite expr.wf_reify_list in H | apply expr.wf_reflect_list in H ] - | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H - | [ H : context[expr.interp _ _ = _] |- expr.interp _ (to_expr _) = ?k2 _ ] - => erewrite H; clear H; - [ match goal with - | [ |- ?k (expr.interp ?ii ?e) = ?k' ?v ] - => has_evar e; - let p := fresh in - set (p := expr.interp ii e); - match v with - | context G[expr.interp ii ?e'] - => unify e e'; let v' := context G[p] in change (k p = k' v') - end; - clearbody p; reflexivity - end - | .. ] - end ]. - - Lemma interp_to_expr_reify_and_let_binds_base_cps {t : base.type} {t' : base.type} (e1 : expr (type.base t)) (e2 : expr (type.base t)) - G - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) - (Hwf : expr.wf G e1 e2) - (k1 : expr (type.base t) -> UnderLets _ (expr (type.base t'))) - (k2 : base.interp t -> base.interp t') - (Hk : forall e1 v, defaults.interp e1 == v -> defaults.interp (to_expr (k1 e1)) == k2 v) - : defaults.interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (defaults.interp e2). - Proof. - revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros; + Lemma interp_to_expr_reify_and_let_binds_base_cps {t : base.type} {t' : base.type} (e1 : expr (type.base t)) (e2 : expr (type.base t)) + G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) + (Hwf : expr.wf G e1 e2) + (k1 : expr (type.base t) -> UnderLets _ (expr (type.base t'))) + (k2 : base.interp t -> base.interp t') + (Hk : forall e1 v, interp e1 == v -> interp (to_expr (k1 e1)) == k2 v) + : interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (interp e2). + Proof. + revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros; try (cbv [SubstVarLike.is_var_fst_snd_pair_opp] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption); break_innermost_match; interp_to_expr_reify_and_let_binds_base_cps_t Hk. - all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. - all: revert dependent k1; revert dependent k2. - all: lazymatch goal with - | [ H : length ?l1 = length ?l2 |- _ ] - => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros - end; - interp_to_expr_reify_and_let_binds_base_cps_t Hk. - Qed. + all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. + all: revert dependent k1; revert dependent k2. + all: lazymatch goal with + | [ H : length ?l1 = length ?l2 |- _ ] + => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros + end; + interp_to_expr_reify_and_let_binds_base_cps_t Hk. + Qed. - Lemma interp_let_bind_return {t} (e1 e2 : expr t) - G - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) - (Hwf : expr.wf G e1 e2) - : defaults.interp (let_bind_return e1) == defaults.interp e2. - Proof. - revert dependent G; induction t; intros; cbn [let_bind_return type.eqv expr.interp] in *; cbv [invert_Abs respectful] in *; - repeat first [ progress wf_safe_t - | progress expr.invert_subst - | progress expr.invert_match - | progress expr.inversion_wf - | progress break_innermost_match_hyps - | progress destruct_head' False - | solve [ wf_t ] - | match goal with - | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] - => eapply (H e0 (e @ $v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ] - | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] - => cbn [expr.interp]; eapply H; [ | solve [ wf_t ] ]; solve [ wf_t ] - end ]; - []. - { pose (P := fun t => { e1e2 : expr t * expr t | expr.wf G (fst e1e2) (snd e1e2) }). - pose ((exist _ (e1, e2) Hwf) : P _) as pkg. - change e1 with (fst (proj1_sig pkg)). - change e2 with (snd (proj1_sig pkg)). - clearbody pkg; clear Hwf e1 e2. - type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ]. - cbn [fst snd proj1_sig proj2_sig] in *. - repeat match goal with - | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ] - => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity) - | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] - => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity) - | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] - => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity) - end. - assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity). - revert pf. - rewrite H'; clear H'. - induction Hwf; break_innermost_match; break_innermost_match_hyps; - repeat first [ progress intros - | progress type.inversion_type - | progress base.type.inversion_type - | progress wf_safe_t - | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal to_expr] in * + Lemma interp_let_bind_return {t} (e1 e2 : expr t) + G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) + (Hwf : expr.wf G e1 e2) + : interp (let_bind_return e1) == interp e2. + Proof. + revert dependent G; induction t; intros; cbn [let_bind_return type.eqv expr.interp] in *; cbv [invert_Abs respectful] in *; + repeat first [ progress wf_safe_t + | progress expr.invert_subst + | progress expr.invert_match + | progress expr.inversion_wf + | progress break_innermost_match_hyps + | progress destruct_head' False + | solve [ wf_t ] | match goal with - | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) - | [ H : forall x (pf : ?a = ?a), _ |- _ ] => specialize (fun x => H x eq_refl) - | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl) - | [ H : forall x y z (pf : ?a = ?a), _ |- _ ] => specialize (fun x y z => H x y z eq_refl) - | [ |- context[(expr_let x := _ in _)%expr] ] => progress cbn [expr.interp]; cbv [LetIn.Let_In] - | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ] - => eapply H; eauto with nocore - end - | solve [ eauto ] - | solve [ eapply expr.wf_interp_Proper; eauto ] ]. - all: eapply interp_to_expr_reify_and_let_binds_base_cps with (k1:=Base) (k2:=(fun x => x)); eauto; wf_safe_t. } - Qed. + | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] + => eapply (H e0 (e @ $v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ] + | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] + => cbn [expr.interp]; eapply H; [ | solve [ wf_t ] ]; solve [ wf_t ] + end ]; + []. + { pose (P := fun t => { e1e2 : expr t * expr t | expr.wf G (fst e1e2) (snd e1e2) }). + pose ((exist _ (e1, e2) Hwf) : P _) as pkg. + change e1 with (fst (proj1_sig pkg)). + change e2 with (snd (proj1_sig pkg)). + clearbody pkg; clear Hwf e1 e2. + type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ]. + cbn [fst snd proj1_sig proj2_sig] in *. + repeat match goal with + | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ] + => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity) + end. + assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity). + revert pf. + rewrite H'; clear H'. + induction Hwf; break_innermost_match; break_innermost_match_hyps; + repeat first [ progress intros + | progress type.inversion_type + | progress base.type.inversion_type + | progress wf_safe_t + | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal to_expr] in * + | match goal with + | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) + | [ H : forall x (pf : ?a = ?a), _ |- _ ] => specialize (fun x => H x eq_refl) + | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl) + | [ H : forall x y z (pf : ?a = ?a), _ |- _ ] => specialize (fun x y z => H x y z eq_refl) + | [ |- context[(expr_let x := _ in _)%expr] ] => progress cbn [expr.interp]; cbv [LetIn.Let_In] + | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ] + => eapply H; eauto with nocore + end + | solve [ eauto ] + | solve [ eapply expr.wf_interp_Proper; eauto ] ]. + all: eapply interp_to_expr_reify_and_let_binds_base_cps with (k1:=Base) (k2:=(fun x => x)); eauto; wf_safe_t. } + Qed. - Lemma Interp_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : defaults.Interp (LetBindReturn e) == defaults.Interp e. - Proof. - apply interp_let_bind_return with (G:=nil); cbn [List.In]; eauto; tauto. - Qed. + Lemma Interp_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : Interp (LetBindReturn e) == Interp e. + Proof. + apply interp_let_bind_return with (G:=nil); cbn [List.In]; eauto; tauto. + Qed. + End with_cast. + + Lemma Wf_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : expr.Wf (LetBindReturn e). + Proof. intros ??; apply wf_let_bind_return, Hwf. Qed. End reify. End UnderLets. |