From d5ef124b940f6ad6c0e126f1077c905a37db0f36 Mon Sep 17 00:00:00 2001 From: Yannick Forster Date: Wed, 25 Oct 2023 12:05:51 +0200 Subject: [PATCH] linearize case --- erasure-plugin/theories/ETransform.v | 9 +- erasure/theories/EImplementBox.v | 179 ++++++++++++++++++++------- template-coq/theories/EtaExpand.v | 6 +- 3 files changed, 143 insertions(+), 51 deletions(-) diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v index fe2ab20b3..96ac13bbf 100644 --- a/erasure-plugin/theories/ETransform.v +++ b/erasure-plugin/theories/ETransform.v @@ -567,7 +567,7 @@ Qed. From MetaCoq.Erasure Require Import EImplementBox. Program Definition implement_box_transformation {efl : EEnvFlags} - {has_app : has_tApp} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} : + {has_app : has_tApp} {has_letin : has_tLetIn} {has_cofix : has_tCoFix = false} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} : Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram block_wcbv_flags) (eval_eprogram block_wcbv_flags) := {| name := "transforming to constuctors as blocks"; transform p _ := EImplementBox.implement_box_program p ; @@ -577,7 +577,7 @@ Program Definition implement_box_transformation {efl : EEnvFlags} Next Obligation. intros. cbn in *. destruct p. split. - - eapply implement_box_env_wf_glob; eauto. + - eapply implement_box_env_wf_glob; eauto. - now eapply transform_wellformed'. Qed. Next Obligation. @@ -588,11 +588,12 @@ Next Obligation. Qed. #[global] -Instance implement_box_extends (efl : EEnvFlags) {has_app : has_tApp} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} : - TransformExt.t (implement_box_transformation (has_app := has_app) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks)) extends_eprogram extends_eprogram. +Instance implement_box_extends (efl : EEnvFlags) {has_app : has_tApp} {has_letin : has_tLetIn} {has_cofix : has_tCoFix = false} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} : + TransformExt.t (implement_box_transformation (has_app := has_app) (has_letin := has_letin) (has_cofix := has_cofix) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks)) extends_eprogram extends_eprogram. Proof. red. intros p p' pr pr' [ext eq]. rewrite /transform /= /implement_box_program /=. split => /=. eapply (implement_box_env_extends has_app ext). apply pr. apply pr'. now rewrite -eq. Qed. + diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v index b322d74d8..47e8fc094 100644 --- a/erasure/theories/EImplementBox.v +++ b/erasure/theories/EImplementBox.v @@ -40,8 +40,9 @@ Section implement_box. | tApp u v := tApp (implement_box u) (implement_box v) | tLetIn na b b' => EAst.tLetIn na (implement_box b) (implement_box b') | tCase ind c brs => - let brs' := map_InP brs (fun x H => (x.1, implement_box x.2)) in - EAst.tCase (ind.1, 0) (implement_box c) brs' + let brs' := map_InP brs (fun x H => (x.1, lift 1 #|x.1| (implement_box x.2))) in + EAst.tLetIn (nNamed "discr") (implement_box c) + (EAst.tCase (ind.1, 0) (tRel 0) brs') | tProj p c => EAst.tProj {| proj_ind := p.(proj_ind); proj_npars := 0; proj_arg := p.(proj_arg) |} (implement_box c) | tFix mfix idx => let mfix' := map_InP mfix (fun d H => {| dname := dname d; dbody := implement_box d.(dbody); rarg := d.(rarg) |}) in @@ -93,44 +94,120 @@ Section implement_box. unfold test_def in *; simpl closed in *; try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy. + rtoProp. split. eauto. + solve_all. + replace (#|x.1| + S k) with (#|x.1| + k + 1) by lia. + eapply closedn_lift. eauto. Qed. Hint Rewrite @forallb_InP_spec : isEtaExp. Transparent isEtaExp_unfold_clause_1. + Lemma implement_box_lift a k b : + implement_box (lift a k b) = lift a k (implement_box b). + Proof. + revert k. + funelim (implement_box b); intros k; cbn; simp implement_box; try easy. + - destruct (Nat.leb_spec k i); reflexivity. + - f_equal. rewrite !map_map_compose. solve_all. + eapply In_All. eauto. + - cbn. f_equal. rewrite !map_map. solve_all. + eapply In_All. intros. eapply H; eauto. + - cbn. do 2 f_equal. 1: eauto. + rewrite !map_map. solve_all. + eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. + replace (#|x.1| + S k) with (S (#|x.1| + k)) by lia. + erewrite H; eauto. + rewrite permute_lift. lia. + f_equal. lia. + - cbn. f_equal. rewrite !map_map. solve_all. + eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. + f_equal. now rewrite map_length. + - cbn. f_equal. rewrite !map_map. solve_all. + eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. + f_equal. now rewrite map_length. + Qed. + + (* Lemma implement_box_subst a k b : *) + (* implement_box (subst a k b) = subst (map implement_box a) k (implement_box b). *) + (* Proof using Type. *) + (* revert k. *) + (* funelim (implement_box b); intros k; cbn; simp implement_box; try easy. *) + (* all: try now (cbn; f_equal; eauto). *) + (* - destruct (Nat.leb_spec k i). *) + (* + erewrite nth_error_map. *) + (* destruct nth_error; cbn. *) + (* * now rewrite implement_box_lift. *) + (* * len. *) + (* + reflexivity. *) + (* - f_equal. rewrite !map_map_compose. solve_all. *) + (* eapply In_All. eauto. *) + (* - cbn. f_equal. rewrite !map_map. solve_all. *) + (* eapply In_All. intros. eapply H; eauto. *) + (* - cbn. do 2 f_equal. 1: eauto. *) + (* rewrite !map_map. solve_all. *) + (* eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. *) + (* replace (#|x.1| + S k) with (S (#|x.1| + k)) by lia. *) + (* rewrite commut_lift_subst. *) + (* f_equal. *) + (* eapply H; eauto. *) + (* - cbn. f_equal. rewrite !map_map. solve_all. *) + (* eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. *) + (* f_equal. now rewrite map_length. *) + (* - cbn. f_equal. rewrite !map_map. solve_all. *) + (* eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. *) + (* f_equal. now rewrite map_length. *) + (* Qed. *) + Lemma implement_box_csubst a k b : + closed a -> implement_box (ECSubst.csubst a k b) = ECSubst.csubst (implement_box a) k (implement_box b). Proof using Type. - revert a k. - funelim (implement_box b); intros a k; cbn; simp implement_box; try easy. + intros Ha. + revert k. + funelim (implement_box b); intros k; cbn; simp implement_box; try easy. + all: try now (cbn; f_equal; eauto). - destruct Nat.compare => //. - f_equal. rewrite !map_map_compose. solve_all. eapply In_All. eauto. - cbn. f_equal. rewrite !map_map. solve_all. - eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto. - - cbn. rewrite H0. f_equal. rewrite !map_map. solve_all. - eapply In_All. cbn. intros ? ?. f_equal. rewrite H; eauto. + eapply In_All. intros. eapply H; eauto. + - cbn. do 2 f_equal. 1: eauto. + rewrite !map_map. solve_all. + eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. + setoid_rewrite -> closed_subst at 2. + replace (#|x.1| + S k) with ((#|x.1| + k) + 1) by lia. + rewrite <- commut_lift_subst_rec. 2: lia. + rewrite <- closed_subst. + 2, 3: eapply closed_implement_box; eauto. + f_equal. + eapply H; eauto. - cbn. f_equal. rewrite !map_map. solve_all. - eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto. + eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. f_equal. now rewrite map_length. - cbn. f_equal. rewrite !map_map. solve_all. - eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto. + eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. f_equal. now rewrite map_length. Qed. Lemma implement_box_substl s t : + All (fun x => closed x) s -> implement_box (substl s t) = substl (map implement_box s) (implement_box t). Proof using Type. - induction s in t |- *; simpl; auto. - rewrite IHs //. f_equal. + induction s in t |- *; simpl; auto; intros Hall. + inversion Hall. + rewrite IHs //. now rewrite implement_box_csubst. Qed. Lemma implement_box_iota_red pars args br : + All (fun x => closed x) args -> implement_box (EGlobalEnv.iota_red pars args br) = EGlobalEnv.iota_red pars (map implement_box args) (on_snd implement_box br). Proof using Type. + intros Hall. unfold EGlobalEnv.iota_red. rewrite implement_box_substl //. + solve_all. now eapply All_skipn. now rewrite map_rev map_skipn. Qed. @@ -153,9 +230,11 @@ Section implement_box. Qed. Lemma implement_box_cunfold_fix mfix idx n f : + All (λ x : term, closed x) (fix_subst mfix) -> cunfold_fix mfix idx = Some (n, f) -> cunfold_fix (map (map_def implement_box) mfix) idx = Some (n, implement_box f). Proof using Type. + intros Hcl. unfold cunfold_fix. rewrite nth_error_map. destruct nth_error eqn:heq. @@ -165,13 +244,15 @@ Section implement_box. Qed. Lemma implement_box_cunfold_cofix mfix idx n f : + All (λ x : term, closed x) (cofix_subst mfix) -> cunfold_cofix mfix idx = Some (n, f) -> cunfold_cofix (map (map_def implement_box) mfix) idx = Some (n, implement_box f). Proof using Type. + intros Hcl. unfold cunfold_cofix. rewrite nth_error_map. destruct nth_error eqn:heq. - intros [= <- <-] => /=. f_equal. + intros [= <- <-] => /=. f_equal. rewrite implement_box_substl //. 2:congruence. f_equal. f_equal. apply implement_box_cofix_subst. Qed. @@ -364,12 +445,12 @@ Definition switch_off_box (efl : EEnvFlags) := {| has_axioms := efl.(has_axioms) ; has_cstr_params := efl.(has_cstr_params) ; term_switches := disable_box_term_flags efl.(term_switches) ; cstr_as_blocks := efl.(cstr_as_blocks) |}. Lemma transform_wellformed' {efl : EEnvFlags} {Σ : list (kername × global_decl)} n t : - has_tApp -> + has_tApp -> has_tLetIn -> wf_glob Σ -> @wellformed efl Σ n t -> @wellformed (switch_off_box efl) (implement_box_env Σ) n (implement_box t). Proof. - intros hasa. + intros hasa hasl. revert n. funelim (implement_box t); simp_eta; cbn -[implement_box lookup_inductive lookup_constructor lookup_constructor_pars_args GlobalContextMap.lookup_constructor_pars_args isEtaExp]; intros m Hwf Hw; rtoProp; try split; eauto. @@ -383,6 +464,8 @@ Proof. + solve_all. + destruct block_args; cbn in *; eauto. - rewrite lookup_inductive_implement_box. intuition auto. solve_all. + replace (#|x.1| + S m) with ((#|x.1| + m) + 1) by lia. + eapply wellformed_lift. eauto. - rewrite lookup_constructor_implement_box. intuition auto. - unfold wf_fix in *. rtoProp. solve_all. solve_all. now eapply isLambda_implement_box. - unfold wf_fix in *. rtoProp. solve_all. @@ -393,7 +476,7 @@ Proof. Qed. Lemma transform_wellformed_decl' {efl : EEnvFlags} {Σ : global_declarations} d : - has_tApp -> + has_tApp -> has_tLetIn -> wf_glob Σ -> @wf_global_decl efl Σ d -> @wf_global_decl (switch_off_box efl) (implement_box_env Σ) (implement_box_decl d). @@ -412,10 +495,10 @@ Proof. Qed. Lemma implement_box_env_wf_glob {efl : EEnvFlags} {Σ : global_declarations} : - has_tApp -> + has_tApp -> has_tLetIn -> wf_glob (efl := efl) Σ -> wf_glob (efl := switch_off_box efl) (implement_box_env Σ). Proof. - intros hasapp wfg. + intros hasapp haslet wfg. assert (extends_prefix Σ Σ). now exists []. revert H wfg. generalize Σ at 2 3. induction Σ; cbn; constructor; auto. @@ -472,13 +555,14 @@ Lemma implement_box_eval {efl : EEnvFlags} (fl := block_wcbv_flags) : with_constructor_as_block = true -> has_cstr_params = false -> has_tApp -> + has_tCoFix = false -> forall (Σ : global_declarations), @wf_glob efl Σ -> forall t t', @wellformed efl Σ 0 t -> EWcbvEval.eval Σ t t' -> @EWcbvEval.eval block_wcbv_flags (implement_box_env Σ) (implement_box t) (implement_box t'). Proof. - intros cstrbl prms hasapp Σ wfΣ. + intros cstrbl prms hasapp hascofix Σ wfΣ. eapply (EWcbvEvalCstrsAsBlocksInd.eval_preserve_mkApps_ind fl cstrbl (efl := efl) Σ _ (wellformed Σ) (Qpres := Qpreserves_wellformed efl _ wfΣ)) => //. @@ -508,40 +592,49 @@ Proof. pose proof (Hcon := H1). rewrite /constructor_isprop_pars_decl in H1. destruct lookup_constructor as [[[]] | ] eqn:eqc; cbn in H1; invs H1. + eapply eval_zeta => //. + 1: eauto. rewrite H8. + cbn [csubst Nat.compare]. eapply eval_iota_block => //. - + cbn [fst]. eapply e0. + + eapply value_final. eapply eval_to_value; eauto. + unfold constructor_isprop_pars_decl. rewrite lookup_constructor_implement_box. cbn [fst]. - rewrite eqc //= H7 //. - + now rewrite map_InP_spec nth_error_map H2; eauto. + rewrite eqc //= H7 //. rewrite H8. + reflexivity. + + rewrite !map_InP_spec. + rewrite map_map. + rewrite nth_error_map H2; eauto. + reflexivity. + + rewrite map_InP_spec. len. + rewrite map_InP_spec. len. - + rewrite H8. rewrite map_InP_spec. len. - + rewrite map_InP_spec. rewrite -implement_box_iota_red. now rewrite H8. + + rewrite map_InP_spec. + cbn [csubst]. + cbn [fst snd]. + rewrite closed_subst. + { eapply wellformed_closed in i2. + cbn in i2 |- *. solve_all. + now eapply closed_implement_box. + } + rewrite Nat.add_0_r. + rewrite simpl_subst_k. reflexivity. + rewrite -implement_box_iota_red. + 2: eauto. + eapply wellformed_closed in i2. + cbn in i2. + solve_all. - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end. simp implement_box in *. eapply eval_fix' => //; eauto. rewrite map_InP_spec. - now eapply implement_box_cunfold_fix. + eapply implement_box_cunfold_fix. + eapply forallb_All. eapply closed_fix_subst. + eapply wellformed_closed in i4. + now cbn in i4. eauto. - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end. - simp implement_box in *. - eapply eval_cofix_case. - 2: now eapply implement_box_cunfold_cofix. - { rewrite implement_box_mkApps in e0. - simp implement_box in e0. rewrite map_InP_spec in e0. - cbn -[implement_box] in e0. - exact e0. - } - rewrite implement_box_mkApps in e. - simp implement_box in e. + rewrite wellformed_mkApps in i2. eauto. + cbn in i2. rtoProp. congruence. - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end. - simp implement_box in *. - eapply eval_cofix_proj. - 2: now eapply implement_box_cunfold_cofix. { rewrite implement_box_mkApps in e0. - simp implement_box in e0. rewrite map_InP_spec in e0. - cbn -[implement_box] in e0. - exact e0. - } - rewrite implement_box_mkApps in e. - simp implement_box in e. + rewrite wellformed_mkApps in i2. eauto. + cbn in i2. rtoProp. congruence. - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end. simp implement_box in *. econstructor. diff --git a/template-coq/theories/EtaExpand.v b/template-coq/theories/EtaExpand.v index 754f5548c..00d8b41cc 100644 --- a/template-coq/theories/EtaExpand.v +++ b/template-coq/theories/EtaExpand.v @@ -102,8 +102,7 @@ Section Eta. in match nth_error def' i with | Some d => eta_fixpoint def' i d (map (eta_expand Γ) args) - | None => tVar ("Error: lookup of a fixpoint failed for " - ++ string_of_term t) + | None => tVar ("Error: lookup of a fixpoint failed") end | tRel n => match nth_error Γ n with @@ -126,8 +125,7 @@ Section Eta. {| dname := dname d ; dtype := dtype d ; dbody := eta_expand (ctx ++ Γ) d.(dbody) ; rarg := rarg d |}) def) in match nth_error def' i with | Some d => eta_fixpoint def' i d [] - | None => tVar ("Error: lookup of a fixpoint failed for " - ++ string_of_term t) + | None => tVar ("Error: lookup of a fixpoint failed ") end | tCoFix def i => tCoFix (map (map_def id (eta_expand (repeat None (#|def|) ++ Γ))) def) i (* NOTE: we know that constructors and constants are not applied at this point,