From 5e9ae4f4f92fda8c3af2017c1e52f017ca37eb23 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 27 Nov 2023 18:11:53 +0100 Subject: [PATCH 1/7] Adapted extraction correctness, only remaining wf_glob proofs --- erasure/theories/Typed/CertifyingEta.v | 6 +- erasure/theories/Typed/Erasure.v | 169 +++++++++++++--- erasure/theories/Typed/ErasureCorrectness.v | 117 ++++++++---- erasure/theories/Typed/Extraction.v | 34 ++-- .../theories/Typed/ExtractionCorrectness.v | 180 ++++++++++++++---- erasure/theories/Typed/TypeAnnotations.v | 45 +++-- 6 files changed, 408 insertions(+), 143 deletions(-) diff --git a/erasure/theories/Typed/CertifyingEta.v b/erasure/theories/Typed/CertifyingEta.v index 38803b4b5..2b99f0690 100644 --- a/erasure/theories/Typed/CertifyingEta.v +++ b/erasure/theories/Typed/CertifyingEta.v @@ -167,6 +167,8 @@ Definition restrict_env (Σ : global_declarations) (kns : list kername) : global | None => false end) Σ. +Import PCUICWfEnv PCUICWfEnvImpl. + Definition eta_global_env (overridden_masks : kername -> option bitmask) (trim_consts trim_inds : bool) @@ -176,7 +178,9 @@ Definition eta_global_env let Σp := PCUICProgram.trans_env_env (TemplateToPCUIC.trans_global_env Σ) in let Σe := erase_global_decls_deps_recursive - (PEnv.declarations Σp) (PEnv.universes Σp) (PEnv.retroknowledge Σp) (assume_env_wellformed _) + (X_type := optimized_abstract_env_impl (guard := fake_guard_impl_instance)) + (X := build_wf_env_from_env Σp (assume_env_wellformed _)) + (PEnv.declarations Σp) (PEnv.universes Σp) (PEnv.retroknowledge Σp) (todo "eq") seeds erasure_ignore in let (const_masks, ind_masks) := analyze_env overridden_masks Σe in let const_masks := (if trim_consts then trim_const_masks else id) const_masks in diff --git a/erasure/theories/Typed/Erasure.v b/erasure/theories/Typed/Erasure.v index 8092b1566..967f1f175 100644 --- a/erasure/theories/Typed/Erasure.v +++ b/erasure/theories/Typed/Erasure.v @@ -210,7 +210,7 @@ Context (rΣ : global_env_ext) Definition erase_rel : Relation_Definitions.relation (∑ Γ t, welltyped rΣ Γ t) := fun '(Γs; ts; wfs) '(Γl; tl; wfl) => - ∥∑m, red rΣ Γl tl m × term_sub_ctx (Γs, ts) (Γl, m)∥. + ∥∑m, red rΣ Γl tl m × term_sub_ctx (Γs, ts) (Γl, m)∥. Lemma cored_prod_l (Σ : global_env_ext) Γ na A A' B : cored Σ Γ A A' -> @@ -1413,26 +1413,23 @@ Instance fake_guard_impl_instance : abstract_guard_impl := Axiom fake_normalization : PCUICSN.Normalization. Global Existing Instance fake_normalization. (* Definition norm := forall Σ : global_env_ext, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ. *) -Program Definition erase_global_decl - (Σext : global_env_ext) - (wfΣext : ∥ wf_ext Σext ∥) - (kn : kername) - (decl : PCUICEnvironment.global_decl) - (wt : ∥on_global_decl cumulSpec0 (lift_typing typing) Σext kn decl∥) - : global_decl := +Program Definition erase_global_decl {X_type : abstract_env_impl} {X : X_type.π2.π1} + (Σext : global_env_ext) + (hr : Σext ∼_ext X) + (kn : kername) + (decl : PCUICEnvironment.global_decl) + (wt : ∥on_global_decl cumulSpec0 (lift_typing typing) Σext kn decl∥) + : global_decl := match decl with | PCUICEnvironment.ConstantDecl cst => - match @erase_constant_decl canonical_abstract_env_impl _ _ _ Σext _ cst _ with + match @erase_constant_decl X_type X _ _ Σext hr cst _ with | inl cst => ConstantDecl cst | inr ta => TypeAliasDecl ta end - | PCUICEnvironment.InductiveDecl mib => InductiveDecl (@erase_ind canonical_abstract_env_impl _ _ _ Σext _ kn mib _) + | PCUICEnvironment.InductiveDecl mib => InductiveDecl (@erase_ind X_type X _ _ Σext hr kn mib _) end. -Next Obligation. unshelve econstructor; eauto. Defined. - Next Obligation. now eapply fake_normalization. Defined. -Next Obligation. now unshelve econstructor;eauto. Defined. -Next Obligation. eapply (fake_normalization _ X _ _ H). Defined. +Next Obligation. eapply fake_normalization; auto. Defined. Fixpoint box_type_deps (t : box_type) : KernameSet.t := match t with @@ -1468,34 +1465,75 @@ Definition decl_deps (decl : global_decl) : KernameSet.t := | _ => KernameSet.empty end. +Import PCUICWfEnv. + +Lemma abstract_eq_wf (X_type : abstract_env_impl) (X : X_type.π1) Σ : + (forall Σ', Σ' ∼ X -> Σ' = Σ) -> Σ ∼ X × ∥ wf Σ ∥. +Proof. + intros heq. + pose proof (abstract_env_exists X) as [[Σ' hΣ']]. + pose proof (abstract_env_wf _ hΣ'). + rewrite <- (heq _ hΣ'). split; auto. +Qed. + +Lemma wf_pop_decl Σ kn decl decls : + wf Σ -> + Σ.(declarations) = (kn, decl) :: decls -> + wf_ext ({| universes := Σ.(universes); retroknowledge := Σ.(retroknowledge); + declarations := decls |}, universes_decl_of_decl decl). +Proof. + intros [] h. rewrite h in o0. + depelim o0. + split. cbn. + split; cbn; eauto. cbn. + now depelim o1. +Qed. + +Lemma sq_wf_pop_decl Σ kn decl decls : + ∥ wf Σ ∥ -> + Σ.(declarations) = (kn, decl) :: decls -> + ∥ wf_ext ({| universes := Σ.(universes); retroknowledge := Σ.(retroknowledge); + declarations := decls |}, universes_decl_of_decl decl) ∥. +Proof. + intros [[]] h; sq. rewrite h in o0. + depelim o0. + split. cbn. + split; cbn; eauto. cbn. + now depelim o1. +Qed. + (** Erase the global declarations by the specified names and their non-erased dependencies recursively. Ignore dependencies for which [ignore_deps] returnes [true] *) Program Fixpoint erase_global_decls_deps_recursive - (Σ : PCUICEnvironment.global_declarations) - (universes : ContextSet.t) - (retroknowledge : Retroknowledge.t) - (wfΣ : ∥wf (mk_global_env universes Σ retroknowledge)∥) - (include : KernameSet.t) - (ignore_deps : kername -> bool) : global_env := - match Σ with + {X_type : abstract_env_impl} {X : X_type.π1} + (decls : PCUICEnvironment.global_declarations) + (univs : ContextSet.t) + (retro : Retroknowledge.t) + (prop : forall Σ', abstract_env_rel X Σ' -> Σ' = {| declarations := decls; universes := univs; retroknowledge := retro |}) + (include : KernameSet.t) + (ignore_deps : kername -> bool) : global_env := + match decls with | [] => [] | (kn, decl) :: Σ => let Σext := (Σ, universes_decl_of_decl decl) in + let X' := abstract_pop_decls X in + let Xext := abstract_make_wf_env_ext (X_type := X_type) X' (universes_decl_of_decl decl) _ in + let env := (mk_global_env univs Σ retro, universes_decl_of_decl decl) in if KernameSet.mem kn include then (** We still erase ignored inductives and constants for two reasons: - For inductives, we want to allow pattern matches on them and we need information about them to print names. - For constants, we use their type to do deboxing. *) - let decl := erase_global_decl ((mk_global_env universes Σ retroknowledge), PCUICLookup.universes_decl_of_decl decl) _ kn decl _ in + let decl := @erase_global_decl X_type Xext env _ kn decl _ in let with_deps := negb (ignore_deps kn) in let new_deps := if with_deps then decl_deps decl else KernameSet.empty in - let Σer := erase_global_decls_deps_recursive - Σ universes retroknowledge _ + let Σer := erase_global_decls_deps_recursive (X:=X') + Σ univs retro _ (KernameSet.union new_deps include) ignore_deps in (kn, with_deps, decl) :: Σer else - erase_global_decls_deps_recursive Σ universes retroknowledge _ include ignore_deps + erase_global_decls_deps_recursive (X:=X') Σ univs retro _ include ignore_deps end. Ltac invert_wf := match goal with @@ -1504,18 +1542,89 @@ Ltac invert_wf := | [H : on_global_decls_data _ _ _ _ _ _ _ |- _] => inversion H; subst; clear H; cbn in * end. Next Obligation. - repeat invert_wf;split;auto;split;auto. + eapply abstract_eq_wf in prop as [hΣ [wf]]. + eapply abstract_pop_decls_correct in H; tea. + 2:{ cbn. intros Σ0' hΣ0'. pose proof (abstract_env_irr _ hΣ hΣ0'). subst Σ0'. + exists (kn, decl). reflexivity. } + destruct Σ0. cbn in *. + destruct H as [? []]. subst. + eapply wf_pop_decl in wf; cbn; eauto. Qed. Next Obligation. - repeat invert_wf. - destruct decl;cbn in *;auto. + pose proof (abstract_env_exists X) as [[Σr hΣr]]. + pose proof (abstract_env_wf _ hΣr) as [wf]. + set (X' := abstract_make_wf_env_ext _ _ _). + set (prf := fun (Σ0 : PCUICEnvironment.global_env) (_ : _) => _) in X'. + clearbody prf. + specialize (prop _ hΣr). subst. + pose proof (abstract_env_ext_exists (abstract_make_wf_env_ext (abstract_pop_decls X) + (universes_decl_of_decl decl) prf)). + pose proof (abstract_env_exists (abstract_pop_decls X)) as [[Σpop hΣpop]]. + eapply (abstract_pop_decls_correct X Σ) in hΣr; tea. + 2:{ intros. pose proof (abstract_env_irr _ H0 hΣr). subst. now eexists. } + destruct hΣr as [? []]. subst. + destruct H as [[Σext hΣext]]. + epose proof (abstract_make_wf_env_ext_correct (abstract_pop_decls X) (universes_decl_of_decl decl) prf _ _ hΣpop hΣext). + subst Σext. destruct Σpop. cbn in *. now subst. Qed. Next Obligation. - repeat invert_wf;split;auto;split;auto. + eapply abstract_eq_wf in prop as [equiv [wf]]. + sq. + depelim wf; cbn in *. depelim o0. now depelim o1. Qed. Next Obligation. - repeat invert_wf;split;auto;split;auto. + eapply abstract_eq_wf in prop as [equiv [wf]]. + eapply abstract_pop_decls_correct in H; tea. + 2:{ cbn. intros Σ0' hΣ0'. pose proof (abstract_env_irr _ equiv hΣ0'). subst Σ0'. + exists (kn, decl0). reflexivity. } + destruct Σ', H as [? []]. subst. cbn. + noconf H0. cbn in H1. subst retro. reflexivity. Qed. +Next Obligation. + pose proof (abstract_env_exists X) as [[Σr hΣr]]. + pose proof (abstract_env_wf _ hΣr) as [wf]. + sq. specialize (prop _ hΣr). subst Σr. + eapply abstract_pop_decls_correct in H; tea. + 2:{ cbn. intros Σ0' hΣ0'. pose proof (abstract_env_irr _ hΣr hΣ0'). subst Σ0'. + exists (kn, decl). reflexivity. } + destruct Σ', H as [? []]. subst. cbn. + noconf H0. cbn in H1. subst retro. reflexivity. +Qed. + +Program Fixpoint erase_global_decls_recursive + {X_type : abstract_env_impl} {X : X_type.π1} + (decls : PCUICEnvironment.global_declarations) + (univs : ContextSet.t) + (retro : Retroknowledge.t) + (prop : forall Σ', abstract_env_rel X Σ' -> Σ' = {| declarations := decls; universes := univs; retroknowledge := retro |}) + : global_env := + match decls with + | [] => [] + | (kn, decl) :: Σ => + let Σext := (Σ, universes_decl_of_decl decl) in + let X' := abstract_pop_decls X in + let Xext := abstract_make_wf_env_ext (X_type := X_type) X' (universes_decl_of_decl decl) _ in + let env := (mk_global_env univs Σ retro, universes_decl_of_decl decl) in + (** We still erase ignored inductives and constants for two reasons: + - For inductives, we want to allow pattern matches on them and we need + information about them to print names. + - For constants, we use their type to do deboxing. *) + let decl := @erase_global_decl X_type Xext env _ kn decl _ in + let Σer := erase_global_decls_recursive (X:=X') Σ univs retro _ in + (kn, true, decl) :: Σer + end. +Next Obligation. + eapply erase_global_decls_deps_recursive_obligation_1; trea. +Defined. +Next Obligation. + eapply (erase_global_decls_deps_recursive_obligation_2 X_type X); trea. +Defined. +Next Obligation. + eapply erase_global_decls_deps_recursive_obligation_3; trea. +Qed. +Next Obligation. + eapply erase_global_decls_deps_recursive_obligation_4; trea. +Defined. End EraseEnv. diff --git a/erasure/theories/Typed/ErasureCorrectness.v b/erasure/theories/Typed/ErasureCorrectness.v index 45d392b0e..70155c107 100644 --- a/erasure/theories/Typed/ErasureCorrectness.v +++ b/erasure/theories/Typed/ErasureCorrectness.v @@ -96,24 +96,35 @@ Qed. End ECorrect. Opaque erase_type flag_of_type ErasureFunction.wf_reduction. +Import ssreflect. + +Section EEnvCorrect. + +Import PCUICWfEnv PCUICWfEnvImpl. + +Existing Instance config.extraction_checker_flags. +Existing Instance PCUICSN.extraction_normalizing. +Context {X_type : PCUICWfEnv.abstract_env_impl} {X : X_type.π1}. +Context {normalising_in: + forall Σ : global_env_ext, wf_ext Σ -> PCUICWfEnv.abstract_env_rel X Σ -> PCUICSN.NormalizationIn Σ}. Lemma erase_global_decls_deps_recursive_correct decls univs retro wfΣ include ignore_deps : let Σ := mk_global_env univs decls retro in (forall k, ignore_deps k = false) -> (forall k, KernameSet.In k include -> P.lookup_env Σ k <> None) -> - includes_deps Σ (trans_env (erase_global_decls_deps_recursive decls univs retro wfΣ include ignore_deps)) include. + includes_deps Σ (trans_env (erase_global_decls_deps_recursive (X_type := X_type) (X := X) decls univs retro wfΣ include ignore_deps)) include. Proof. cbn. cut (is_true (KernameSet.subset include include)); [|now apply KernameSet.subset_spec]. generalize include at 1 3 5 as include'. intros include' sub no_ignores all_in. - induction decls as [|(kn, decl) Σ0 IH] in univs, decls, retro, wfΣ, all_in, include, include', sub |- *. + induction decls as [|(kn, decl) Σ0 IH] in X_type, X, univs, decls, retro, wfΣ, all_in, include, include', sub |- *. { intros kn isin. cbn. now apply all_in in isin. } simpl in *. match goal with - | |- context[erase_global_decl _ ?wfΣarg _ _ ?wfdeclarg] => - set (wfΣext := wfΣarg) in *; clearbody wfΣext; + | |- context[erase_global_decl _ ?wfΣarg _ ?wfdeclarg] => + set (wfΣext := wfΣarg) in *; set (wfdecl := wfdeclarg) in *; clearbody wfdecl end. match goal with @@ -121,13 +132,17 @@ Proof. set (wfΣprev := wfΣarg) in *; clearbody wfΣprev end. - destruct wfΣ as [wfΣ]. rewrite no_ignores;cbn. destruct KernameSet.mem eqn:mem; cycle 1. - intros kn' isin. - change {| P.universes := univs; P.declarations := (kn, decl) :: Σ0; P.retroknowledge := retro |} with - (add_global_decl {| P.universes := univs; P.declarations := Σ0; P.retroknowledge := retro|} (kn, decl)). + change {| P.universes := univs; P.declarations := (kn, wfdecl) :: Σ0; P.retroknowledge := retro |} with + (add_global_decl {| P.universes := univs; P.declarations := Σ0; P.retroknowledge := retro|} (kn, wfdecl)). + pose proof (abstract_env_ext_wf _ wfΣext) as []. + pose proof (abstract_env_exists X) as [[Σfull hfull]]. + pose proof (abstract_env_wf _ hfull) as [wffull]. apply global_erases_with_deps_weaken; auto. + { pose proof (wfΣ _ hfull). now subst Σfull. } + set (prf := (fun (Σ : global_env) => _)). eapply IH; eauto. intros k kisin. specialize (all_in _ kisin). @@ -140,10 +155,14 @@ Proof. - cbn in *. intros k isin. destruct (Kername.eq_dec k kn) as [->|]; cycle 1. - { change {| P.universes := univs; P.declarations := (kn, decl) :: Σ0; P.retroknowledge := retro |} with - (add_global_decl {| P.universes := univs; P.declarations := Σ0; P.retroknowledge := retro |} (kn, decl)). + { change {| P.universes := univs; P.declarations := (kn, wfdecl) :: Σ0; P.retroknowledge := retro |} with + (add_global_decl {| P.universes := univs; P.declarations := Σ0; P.retroknowledge := retro |} (kn, wfdecl)). + pose proof (abstract_env_ext_wf _ wfΣext) as []. + pose proof (abstract_env_exists X) as [[Σfull hfull]]. + pose proof (abstract_env_wf _ hfull) as [wffull]. apply global_erases_with_deps_cons; auto. - eapply (IH _ _ wfΣprev _ (KernameSet.singleton k)). + { pose proof (wfΣ _ hfull). now subst Σfull. } + eapply (IH _ _ _ _ wfΣprev _ (KernameSet.singleton k)). - apply KernameSet.subset_spec. intros ? ?. eapply KernameSet.singleton_spec in H; subst a. @@ -161,7 +180,7 @@ Proof. - now apply KernameSet.singleton_spec. } cbn. - destruct decl; [left|right]. + destruct wfdecl; [left|right]. all: unfold declared_constant, declared_minductive, P.declared_constant, P.declared_minductive; cbn. unfold Erasure.erase_constant_decl. @@ -169,9 +188,8 @@ Proof. all: try rewrite eq_kername_refl. + eexists; split; [left;reflexivity|]. unfold erase_constant_decl. - destruct flag_of_type; cbn in *. - destruct conv_ar; cbn in *. - destruct wfΣprev as [wfΣprev]. + destruct flag_of_type. + destruct conv_ar. * destruct c eqn:Hc; cbn in *. destruct cst_body0 eqn:Hcb; cbn in *; cycle 1. { eexists; split;cbn; unfold EGlobalEnv.declared_constant;cbn. @@ -185,24 +203,32 @@ Proof. noconf H. constructor. } - destruct wfdecl as [wfdecl]. + pose proof (abstract_env_ext_wf _ wfΣext) as []. + pose proof (abstract_env_exists X) as [[Σfull hfull]]. + pose proof (abstract_env_wf _ hfull) as [wffull]. + (* pose proof (abstract_env_exists (abstract_pop_decls X)) as [[Σpop hpop]]. + pose proof (abstract_env_wf _ hpop) as [wfpop]. + eapply abstract_pop_decls_correct in hpop; tea. *) + + destruct c0 as [ctx univ [r]]. destruct r. - apply @type_reduction with (B := mkNormalArity ctx univ) in wfdecl; eauto. + eapply @type_reduction with (B := mkNormalArity ctx univ) in clrel_rel; eauto. cbn in *. constructor. eapply (Is_type_extends (({| P.universes := univs; P.declarations := Σ0; P.retroknowledge := retro |}, _))). - constructor. - 2: now eauto. - 2:{ eapply extends_decls_extends_subrel, strictly_extends_decls_extends_decls. + constructor. eapply X0. clear wfΣext. specialize (wfΣ _ hfull). now subst Σfull. + { eapply extends_decls_extends_subrel, strictly_extends_decls_extends_decls. unfold strictly_extends_decls; trea. eexists. cbn; auto. eexists [_]. cbn. reflexivity. reflexivity. } eauto. eexists. split; [eassumption|]. left. apply isArity_mkNormalArity. + clear wfΣext. specialize (wfΣ _ hfull). subst Σfull. + depelim wffull; cbn in *. depelim o0. now depelim o1. * eexists; split;cbn; unfold EGlobalEnv.declared_constant;cbn. - now rewrite eq_kername_refl. + now rewrite eq_kername_refl. unfold trans_cst; cbn. destruct c; cbn in *. destruct cst_body0; cbn in *; cycle 1. @@ -212,28 +238,51 @@ Proof. | |- context[erase _ _ _ _ ?p] => set (twt := p) in *; clearbody twt end. - destruct wfdecl as [wfdecl]. + set (wfext := abstract_make_wf_env_ext _ _ _). + (* destruct wfdecl as [wfdecl]. *) split. - -- apply @type_reduction with (B := cst_type0) in wfdecl as wfdecl1; eauto. - 2: repeat invert_wf;split;auto;split;auto. - eapply (erases_extends (_, _)). - 2: now eauto. - 1: repeat invert_wf;split;auto;split;auto. - 1: repeat invert_wf;split;auto. - 2: { eexists. reflexivity. eexists [_]; reflexivity. reflexivity. } - 1: constructor;auto. + -- set (decl' := ConstantDecl _) in *. + pose proof (abstract_env_ext_wf _ wfΣext) as []. + pose proof (abstract_env_exists X) as [[Σfull hfull]]. + pose proof (abstract_env_wf _ hfull) as [wffull]. + pose proof (wfΣ _ hfull). + pose proof (abstract_env_exists (abstract_pop_decls X)) as [[Σpop hpop]]. + pose proof (abstract_env_wf _ hpop) as [wfpop]. + eapply abstract_pop_decls_correct in hpop; tea. + 2:{ intros. pose proof (abstract_env_irr _ hfull H0). subst Σfull Σ. cbn. now eexists. } + subst Σfull. destruct hpop as [? []]. cbn in *. subst. + destruct Σpop as [univspop Σpop retropop]; cbn in *. + (* pose proof (abstract_make_wf_env_ext_correct _ wfext). + destruct wfdecl as [wfdecl onud]. + eapply @type_reduction with (B := cst_type0) in wfdecl as wfdecl1; eauto. + 2:{ depelim wfΣ. depelim o0. depelim o2. now cbn in on_global_decl_d. } *) + + eapply (erases_extends (_, _)); eauto. + 1:{ depelim wffull. depelim o0. depelim o1. now cbn in on_global_decl_d. } + 1:{ eexists. reflexivity. eexists [_]; reflexivity. reflexivity. } now apply erases_erase. -- intros. noconf H. - destruct wfΣext. assert (unfold_add_gd : forall univs decls (decl : kername × global_decl), add_global_decl (mk_global_env univs decls retro) decl = {| P.universes := univs; P.declarations := decl :: decls; P.retroknowledge := retro |}) by reflexivity. - rewrite <- unfold_add_gd. + rewrite -{1}unfold_add_gd. repeat invert_wf. + pose proof (abstract_env_ext_wf _ wfΣext) as []. + pose proof (abstract_env_exists X) as [[Σfull hfull]]. + pose proof (abstract_env_wf _ hfull) as [wffull]. + pose proof (wfΣ _ hfull). + pose proof (abstract_env_exists (abstract_pop_decls X)) as [[Σpop hpop]]. + pose proof (abstract_env_wf _ hpop) as [wfpop]. + eapply abstract_pop_decls_correct in hpop; tea. + 2:{ intros. pose proof (abstract_env_irr _ hfull H0). subst Σfull Σ. cbn. now eexists. } + subst Σfull. destruct hpop as [? []]. cbn in *. subst. + destruct Σpop as [univspop Σpop retropop]; cbn in *. apply erases_deps_cons;eauto;cbn in *. - constructor;eauto. + { now depelim wfpop. } + { now depelim wffull. } + depelim wffull. cbn in *. depelim o0. depelim o1. cbn in on_global_decl_d. eapply (@erase_global_erases_deps (_, _)); eauto. - { now apply erases_erase. } + now apply erases_erase. eapply IH. ++ apply KernameSet.subset_spec. intros ? isin'. @@ -249,3 +298,5 @@ Proof. cbn in *. apply erase_ind_correct. Qed. + +End EEnvCorrect. \ No newline at end of file diff --git a/erasure/theories/Typed/Extraction.v b/erasure/theories/Typed/Extraction.v index 9ff35f659..92a62bd91 100644 --- a/erasure/theories/Typed/Extraction.v +++ b/erasure/theories/Typed/Extraction.v @@ -43,34 +43,34 @@ Record extract_pcuic_params := Lemma fresh_global_erase_global_decl_rec : - forall (Σ0 : global_declarations) (universes0 : ContextSet.t) (retroknowledge0 : Retroknowledge.t) - (wfΣ : ∥ wf ({| PEnv.universes := universes0; PEnv.declarations := Σ0; PEnv.retroknowledge := retroknowledge0 |}) ∥) + forall X_type X (Σ0 : global_declarations) (universes0 : ContextSet.t) (retroknowledge0 : Retroknowledge.t) + wfΣ (seeds : KernameSet.t) (ignore : kername -> bool) kn, EnvMap.EnvMap.fresh_global kn Σ0 -> - ExAst.fresh_global kn (erase_global_decls_deps_recursive Σ0 universes0 retroknowledge0 wfΣ seeds ignore). + ExAst.fresh_global kn (@erase_global_decls_deps_recursive X_type X Σ0 universes0 retroknowledge0 wfΣ seeds ignore). Proof. - intros Σ0 universes0 retroknowledge0 wfΣ seeds ignore kn fresh. - revert wfΣ seeds. - induction Σ0;intros wfΣ seeds. + intros X_type X Σ0 universes0 retroknowledge0 wfΣ seeds ignore kn fresh. + revert X_type X wfΣ seeds. + induction Σ0;intros X_type X wfΣ seeds. - constructor. - cbn. destruct a;cbn. inversion fresh;cbn in *;subst;clear fresh. destruct (KernameSet.mem _ _) eqn:Hmem;cbn. * constructor;auto. - now apply IHΣ0. + now eapply IHΣ0. * now apply IHΣ0. Qed. Lemma fresh_globals_erase_global_decl_rec : - forall (Σ0 : global_declarations) (universes0 : ContextSet.t) (retroknowledge0 : Retroknowledge.t) - (wfΣ : ∥ wf ({| PEnv.universes := universes0; PEnv.declarations := Σ0; PEnv.retroknowledge := retroknowledge0 |}) ∥) + forall X_type X (Σ0 : global_declarations) (universes0 : ContextSet.t) (retroknowledge0 : Retroknowledge.t) + wfΣ (seeds : KernameSet.t) (ignore : kername -> bool), EnvMap.EnvMap.fresh_globals Σ0 -> - ExAst.fresh_globals (erase_global_decls_deps_recursive Σ0 universes0 retroknowledge0 wfΣ seeds ignore). + ExAst.fresh_globals (@erase_global_decls_deps_recursive X_type X Σ0 universes0 retroknowledge0 wfΣ seeds ignore). Proof. - intros Σ0 universes0 retroknowledge0 wfΣ seeds ignore fresh. - revert wfΣ seeds. - induction Σ0;intros wfΣ seeds;cbn in *. + intros X_type X Σ0 universes0 retroknowledge0 wfΣ seeds ignore fresh. + revert X_type X wfΣ seeds. + induction Σ0;intros X_type X wfΣ seeds;cbn in *. - constructor. - destruct a;cbn. inversion fresh;subst. @@ -87,12 +87,18 @@ Program Definition extract_pcuic_env (wfΣ : ∥wf Σ ∥) (seeds : KernameSet.t) (ignore : kername -> bool) : result ExAst.global_env _ := - let Σ := timed "Erasure" (fun _ => erase_global_decls_deps_recursive (declarations Σ) (universes Σ) (retroknowledge Σ) wfΣ seeds ignore) in + let Σ := timed "Erasure" + (fun _ => erase_global_decls_deps_recursive (X_type := PCUICWfEnvImpl.optimized_abstract_env_impl (guard := fake_guard_impl_instance)) + (X := PCUICWfEnvImpl.build_wf_env_from_env Σ wfΣ) + (declarations Σ) (universes Σ) (retroknowledge Σ) _ seeds ignore) in if optimize_prop_discr params then let Σ := timed "Removal of prop discrimination" (fun _ => OptimizePropDiscr.remove_match_on_box_env Σ _) in compose_transforms (extract_transforms params) Σ else Ok Σ. +Next Obligation. + destruct Σ; eauto. +Qed. Next Obligation. apply fresh_globals_erase_global_decl_rec. sq. diff --git a/erasure/theories/Typed/ExtractionCorrectness.v b/erasure/theories/Typed/ExtractionCorrectness.v index 6eb8525f8..3a531aba3 100644 --- a/erasure/theories/Typed/ExtractionCorrectness.v +++ b/erasure/theories/Typed/ExtractionCorrectness.v @@ -1,9 +1,10 @@ -From Coq Require Import List. +From Coq Require Import List ssreflect ssrbool. From MetaCoq.Erasure.Typed Require Import ErasureCorrectness. From MetaCoq.Erasure.Typed Require Import ExAst. From MetaCoq.Erasure.Typed Require Import Extraction. From MetaCoq.Erasure.Typed Require Import Optimize. From MetaCoq.Erasure.Typed Require Import OptimizeCorrectness. +From MetaCoq.Erasure.Typed Require Import OptimizePropDiscr. From MetaCoq.Erasure.Typed Require Import ResultMonad. From MetaCoq.Erasure.Typed Require Import WcbvEvalAux. From Equations Require Import Equations. @@ -76,21 +77,85 @@ Proof. Qed. Module PEnv := PCUICAst.PCUICEnvironment. +Import PCUICWfEnv ErasureFunction ErasureFunctionProperties. -(*Lemma wf_erase_global_decl : - forall (H : EWellformed.EEnvFlags) (k : kername) (g : PCUICAst.PCUICEnvironment.global_decl) +Lemma extends_trans Σ Σ' Σ'' : + EGlobalEnv.extends Σ Σ' -> + EGlobalEnv.extends Σ' Σ'' -> + EGlobalEnv.extends Σ Σ''. +Proof. + intros e e' kn h h'. + eapply e in h'. now eapply e' in h'. +Qed. + +(* Lemma trans_global_decl_erase {X_type X} : + trans_global_decl (@Erasure.erase_global_decl X_type X Σ prf kn decl ond) = *) + +Lemma filter_deps_ext deps deps' l : + KernameSet.Equal deps deps' -> + filter_deps deps l = filter_deps deps' l. +Proof. + induction l as [|[kn d] decls] in deps, deps' |- *; cbn; auto. + destruct (KernameSet.mem kn deps) eqn:e. + eapply KernameSet.mem_spec in e. + intros kne. eapply kne in e. eapply KernameSet.mem_spec in e. rewrite e. + rewrite (IHdecls _ _ kne); eauto. destruct d. f_equal. eapply IHdecls. now rewrite kne. + f_equal. + intros hne. + destruct (KernameSet.mem kn deps') eqn:e'. + rewrite <- hne in e'. congruence. + now eapply IHdecls. +Qed. + +Lemma trans_env_erase_global_decls {X_type X} decls univs retro prf deps deps' ignored : + (forall k, ignored k = false) -> + KernameSet.Subset deps deps' -> + EGlobalEnv.extends (trans_env (@Erasure.erase_global_decls_deps_recursive X_type X decls univs retro prf deps ignored)) + (filter_deps deps' (trans_env (@Erasure.erase_global_decls_recursive X_type X decls univs retro prf))). +Proof. + induction decls in X_type, X, deps, deps', ignored, prf |- *. + - now cbn. + - cbn. intros hign hsub. + destruct a. destruct g. + destruct (KernameSet.mem k deps) eqn:e; cbn [map filter_deps]. + assert (KernameSet.mem k deps') as ->. + { eapply KernameSet.mem_spec in e. + now apply KernameSet.mem_spec. } + set (er := Erasure.erase_global_decl _ _ _ _ _). + set (er' := Erasure.erase_global_decl _ _ _ _ _). + set (prf' := fun (Σ : PCUICAst.PCUICEnvironment.global_env) => _). + assert (trans_global_decl er = trans_global_decl er'). admit. + rewrite <- H. + destruct (trans_global_decl er) eqn:eqr. + rewrite hign. + eapply extends_cons. + unfold trans_env in IHdecls. + eapply (IHdecls _ _ prf'); eauto. cbn [negb]. + intros kn. + rewrite !KernameSet.union_spec. +Admitted. + +Lemma wf_erase_global_decl : + forall (H := EWellformed.all_env_flags) + X_type X + (k : kername) (g : PCUICAst.PCUICEnvironment.global_decl) (decls : list (kername * PCUICAst.PCUICEnvironment.global_decl)) - (univs : Universes.ContextSet.t) retros w wt (Σex : global_env), + (univs : Universes.ContextSet.t) retros prf w wt (Σex : global_env) prf' seeds ignored, + let eg := (@Erasure.erase_global_decl X_type + (abstract_make_wf_env_ext X (PCUICAst.PCUICLookup.universes_decl_of_decl g) prf) + ({| PEnv.universes := univs; PEnv.declarations := decls; PEnv.retroknowledge := retros |}, + PCUICAst.PCUICLookup.universes_decl_of_decl g) + w k g wt) in + (forall kn, ignored kn = false) -> + Σex = @Erasure.erase_global_decls_deps_recursive X_type X decls univs retros prf' + (KernameSet.union (Erasure.decl_deps eg) seeds) ignored -> EWellformed.wf_glob (trans_env Σex) -> EWellformed.wf_global_decl (trans_env Σex) - (trans_global_decl - (Erasure.erase_global_decl - ({| PEnv.universes := univs; PEnv.declarations := decls; PEnv.retroknowledge := retros |}, - PCUICAst.PCUICLookup.universes_decl_of_decl g) - w k g wt)) = true. + (trans_global_decl eg) = true. Proof. - intros H k g decls univs w wt Σex wf_global. + intros H X_type X k g decls univs retros prf w wt Σex prf' seeds ignored eg hign eqex wf_global. + revert eqex. subst eg. unfold Erasure.erase_global_decl. destruct g. - destruct (Erasure.erase_constant_decl) eqn:Hdecl. @@ -98,11 +163,33 @@ Proof. destruct (Erasure.flag_of_type), conv_ar;try congruence. inversion Hdecl;subst;clear Hdecl. unfold trans_global_decl,trans_cst. - cbn. + cbn [EWellformed.wf_global_decl]. unfold MCOption.option_default. - (* global_erased_with_deps *) - (* erase_constant_body_correct'' *) -Qed *) + destruct EAst.cst_body eqn:heq. + set (deps := KernameSet.union _ _). + unshelve eapply (erase_constant_body_correct'' (X_type := X_type) (decls := decls) seeds) in heq as [[t0 [T [[] ?]]]]. + shelve. intros. eapply Erasure.fake_normalization; tea. + { intros. now rewrite (prf' _ H0). } + 2:exact w. + intros ->. + eapply EWellformed.extends_wellformed; tea. + set (prf'' := fun _ => _). clearbody prf''. cbn in prf''. + rewrite erase_global_deps_erase_global. + clear. + induction decls. red; auto. + cbn -[Erasure.erase_global_decls_deps_recursive]. + destruct a as [kn []]. + set (prf0 := (fun (pf : _) => _)). + set (prf1 := (fun (pf : _) => _)). + set (prf2 := (fun (pf : _) => _)). + clearbody prf2. + cbn -[erase_global Erasure.erase_global_decls_deps_recursive]. + destruct (KernameSet.mem _ _) eqn:e. + set (prf3 := (fun (pf : _) => _)). + clearbody prf3. + + +Admitted. Ltac invert_wf := @@ -112,17 +199,16 @@ Ltac invert_wf := | [H : P.on_global_decls_data _ _ _ _ _ _ _ |- _] => inversion H; subst; clear H; cbn in * end. -(* -Lemma wf_erase_global_decls_recursive `{EWellformed.EEnvFlags} : - forall decls univs retros w seeds (ignored : kername -> bool), - let Σex := - Erasure.erase_global_decls_deps_recursive decls univs retros w seeds ignored in +Lemma wf_erase_global_decls_recursive (H := EWellformed.all_env_flags) : + forall X_type X decls univs retros w seeds (ignored : kername -> bool), + (forall k, ignored k = false) -> + let Σex := @Erasure.erase_global_decls_deps_recursive X_type X decls univs retros w seeds ignored in EWellformed.wf_glob (trans_env Σex). Proof. - intros decls univs retros w seeds ignored ?. + intros X_type X decls univs retros w seeds ignored hign ?. subst Σex. revert seeds. - induction decls;intros seeds;auto;try constructor. + induction decls in X_type, X, w |- *;intros seeds;auto;try constructor. simpl. destruct a;simpl. destruct (KernameSet.mem _ _);cbn. @@ -132,21 +218,22 @@ Proof. apply IHdecls. * cbn. remember (KernameSet.union _ _) as kns. - clear Heqkns. + rewrite hign in Heqkns. cbn in Heqkns. remember (Erasure.erase_global_decls_deps_recursive decls univs _ _ _ _) as Σex. assert (EWellformed.wf_glob (trans_env Σex)) by now subst Σex. - now apply wf_erase_global_decl. + rewrite -/(trans_env _). + eapply wf_erase_global_decl; eauto. rewrite HeqΣex. f_equal. exact Heqkns. * sq. apply OptimizePropDiscr.trans_env_fresh_global. apply fresh_globals_erase_global_decl_rec. change decls with (PEnv.declarations {| PEnv.universes := univs; PEnv.declarations := decls; PEnv.retroknowledge := retros |}). - apply PCUICWfEnvImpl.wf_fresh_globals. - repeat invert_wf;split;auto;split;auto. + eapply Erasure.abstract_eq_wf in w as [? []]. + apply PCUICWfEnvImpl.wf_fresh_globals; eauto. + eapply Erasure.wf_pop_decl in X0; trea. eapply X0. apply fresh_global_erase_global_decl_rec. - change decls with (PEnv.declarations - {| PEnv.universes := univs; PEnv.declarations := decls; PEnv.retroknowledge := retros |}). - now repeat invert_wf. + eapply Erasure.abstract_eq_wf in w as [? []]. + eapply PCUICWfEnvImpl.wf_fresh_globals in X0. now depelim X0. - apply IHdecls. Qed. @@ -157,19 +244,25 @@ Lemma optimize_correct `{EWellformed.EEnvFlags} Σ fgΣ t v : @Prelim.Ee.eval default_wcbv_flags (trans_env Σ) t v -> @Prelim.Ee.eval (EWcbvEval.disable_prop_cases opt_wcbv_flags) - (trans_env (OptimizePropDiscr.optimize_env Σ fgΣ)) - (EOptimizePropDiscr.optimize (EEnvMap.GlobalContextMap.make (trans_env Σ) (OptimizePropDiscr.trans_env_fresh_globals _ fgΣ)) t) - (EOptimizePropDiscr.optimize (EEnvMap.GlobalContextMap.make (trans_env Σ) (OptimizePropDiscr.trans_env_fresh_globals _ fgΣ)) v). + (trans_env (map (on_snd (remove_match_on_box_decl (EEnvMap.GlobalContextMap.make (trans_env Σ) (OptimizePropDiscr.trans_env_fresh_globals _ fgΣ)))) Σ)) + (EOptimizePropDiscr.remove_match_on_box (EEnvMap.GlobalContextMap.make (trans_env Σ) (OptimizePropDiscr.trans_env_fresh_globals _ fgΣ)) t) + (EOptimizePropDiscr.remove_match_on_box (EEnvMap.GlobalContextMap.make (trans_env Σ) (OptimizePropDiscr.trans_env_fresh_globals _ fgΣ)) v). Proof. intros cl_t cl_env wfg ev. - rewrite OptimizePropDiscr.trans_env_optimize_env. remember (EEnvMap.GlobalContextMap.make _ _) as Σ0. - unshelve eapply (EOptimizePropDiscr.optimize_correct (fl := default_wcbv_flags) (Σ := Σ0));subst;cbn;eauto. + assert (trans_env (map (on_snd (remove_match_on_box_decl Σ0)) Σ) = + EOptimizePropDiscr.remove_match_on_box_env Σ0) as ->. + { cbn. rewrite /trans_env HeqΣ0 map_map_compose. cbn. rewrite /trans_env. + rewrite map_map_compose /on_snd. cbn. eapply map_ext. + intros [[] []]; cbn. destruct c as [[] []] => //. reflexivity. + do 2 f_equal. rewrite /EOptimizePropDiscr.remove_match_on_box_constant_decl /=. + now destruct o; cbn. } + unshelve eapply (EOptimizePropDiscr.remove_match_on_box_correct (fl := default_wcbv_flags) (Σ := Σ0));subst;cbn;eauto. Qed. Theorem extract_correct - `{EWellformed.EEnvFlags} + (H := EWellformed.all_env_flags) (wfl := opt_wcbv_flags) (Σ : P.global_env_ext) (wfΣ : ∥wf_ext Σ∥) kn ui ind c ui' ignored exΣ : @@ -188,24 +281,27 @@ Proof. destruct dearg_transform eqn:dt; cbn -[dearg_transform] in *; [|congruence]. injection ex as ->. destruct wfΣ. - eapply erases_correct with (Σ' := trans_env (Erasure.erase_global_decls_deps_recursive (PCUICAst.PCUICEnvironment.declarations Σ) - (PCUICAst.PCUICEnvironment.universes Σ) _ (wf_squash (sq w)) + eapply erases_correct with + (Σ' := trans_env (Erasure.erase_global_decls_deps_recursive (PCUICAst.PCUICEnvironment.declarations Σ) + (PCUICAst.PCUICEnvironment.universes Σ) _ _ (KernameSet.singleton kn) ignored)) in ev as (erv&erase_to&[erev]);eauto. + depelim erase_to;[|easy]. constructor. eapply dearg_transform_correct; eauto. clear dt. - eapply (@OptimizePropDiscr.optimize_correct _ default_wcbv_flags _ _ (tConst kn) (tConstruct ind c []));eauto. + eapply (@optimize_correct _ _ _ (tConst kn) (tConstruct ind c []));eauto. * remember (Erasure.erase_global_decls_deps_recursive _ _ _ _ _ _) as eΣ. - assert (EWellformed.wf_glob (trans_env eΣ)) by now subst eΣ;eapply wf_erase_global_decls_recursive. + assert (EWellformed.wf_glob (trans_env eΣ)). + { subst eΣ. now eapply wf_erase_global_decls_recursive. } now apply EWellformed.wellformed_closed_env. - * eapply wf_erase_global_decls_recursive. + * eapply wf_erase_global_decls_recursive; auto. + + now eexists. + eapply inversion_Const in wt as (?&?&?&?&?); auto. clear dt. eapply global_erased_with_deps_erases_deps_tConst; eauto. destruct Σ as [Σ0 univ_decls]. destruct Σ0 as [univs Σ1]. - apply wf_ext_wf in w as w1. + apply wf_ext_wf in w as w1. cbn. eapply erase_global_decls_deps_recursive_correct;eauto. * unfold PCUICAst.declared_constant in *. cbn. @@ -213,10 +309,10 @@ Proof. intros eq. set (env := {| PEnv.declarations := Σ1 |}) in *. eapply (lookup_global_In_wf _ env) in d; eauto. * now apply KernameSet.singleton_spec. + Unshelve. eapply fresh_globals_erase_global_decl_rec. + now eapply PCUICWfEnvImpl.wf_fresh_globals. Qed. -*) - (* Print Assumptions extract_correct. *) (** There are some assumptions of which almost all are in MetaCoq. diff --git a/erasure/theories/Typed/TypeAnnotations.v b/erasure/theories/Typed/TypeAnnotations.v index a59888cda..f82f22bd7 100644 --- a/erasure/theories/Typed/TypeAnnotations.v +++ b/erasure/theories/Typed/TypeAnnotations.v @@ -368,13 +368,12 @@ Proof. econstructor; eauto. Qed. -#[program] Definition erase_constant_decl_impl := - @erase_constant_decl canonical_abstract_env_impl (ltac:(now unshelve econstructor;eauto)) - PCUICSN.extraction_normalizing _. +#[program] Definition erase_constant_decl_impl X_type X := + @erase_constant_decl X_type X PCUICSN.extraction_normalizing _. Next Obligation. apply Erasure.fake_normalization; eauto. Defined. -Definition annotate_types_erase_constant_decl cst wt : - match erase_constant_decl_impl Σ eq_refl cst wt with +Definition annotate_types_erase_constant_decl X_type X cst wt eq : + match erase_constant_decl_impl X_type X Σ eq cst wt with | inl cst => constant_body_annots box_type cst | _ => unit end. @@ -392,48 +391,48 @@ Proof. cbn in *. destruct wt. econstructor; eauto. - reflexivity. + exact eq. Defined. - (* Context (nin : forall Σ : global_env_ext, wf_ext Σ -> Σ ∼_ext X -> PCUICSN.NormalizationIn Σ). *) -Definition annotate_types_erase_global_decl kn decl wt : - global_decl_annots box_type (erase_global_decl Σ wfextΣ kn decl wt). +Definition annotate_types_erase_global_decl X_type X eq kn decl wt : + global_decl_annots box_type (@erase_global_decl X_type X Σ eq kn decl wt). Proof. unfold erase_global_decl. destruct decl; [|exact tt]. cbn. - pose proof (annotate_types_erase_constant_decl c wt). - unfold erase_constant_decl_impl in *. - unfold Erasure.erase_global_decl_obligation_2; cbn. - unfold erase_constant_decl_impl_obligation_1 in X. + pose proof (annotate_types_erase_constant_decl X_type X c wt). + unfold erase_constant_decl_impl in *. cbn in X0. + specialize (X0 eq). cbn. destruct erase_constant_decl; [|exact tt]. - cbn. exact X. + cbn. exact X0. Defined. End fix_env. -Definition annotate_types_erase_global_decls_deps_recursive Σ universes retros wfΣ include ignore_deps : - env_annots box_type (erase_global_decls_deps_recursive Σ universes retros wfΣ include ignore_deps). +Definition annotate_types_erase_global_decls_deps_recursive X_type X Σ universes retros wfΣ include ignore_deps : + env_annots box_type (@erase_global_decls_deps_recursive X_type X Σ universes retros wfΣ include ignore_deps). Proof. revert include. - induction Σ; intros include; [exact tt|]. + induction Σ in X, X_type, wfΣ |- *; intros include; [exact tt|]. cbn in *. destruct a. destruct KernameSet.mem. - cbn. match goal with - | |- context[erase_global_decl ?a ?b ?c ?d ?e] => - pose proof (annotate_types_erase_global_decl a b c d e) + | |- context[ @erase_global_decl ?X_type ?X ?a ?b ?c ?d ?e] => + unshelve epose proof (annotate_types_erase_global_decl a _ X_type X b c d e) end. + { eapply abstract_eq_wf in wfΣ as [equiv [wf]]. + eapply (sq_wf_pop_decl _ _ _ _ (sq wf)); cbn; trea. } match goal with | |- context[erase_global_decls_deps_recursive _ _ _ ?prf ?incl _] => - specialize (IHΣ prf incl ) + specialize (IHΣ _ _ prf incl ) end. - exact (X, IHΣ). + exact (X0, IHΣ). - match goal with | |- context[erase_global_decls_deps_recursive _ _ _ ?prf ?incl _] => - specialize (IHΣ prf incl) + specialize (IHΣ _ _ prf incl) end. exact IHΣ. Defined. @@ -557,7 +556,7 @@ Proof. exact (ta.1, f _ All_nil _ ta.2.2). - exact (annot_dearg_single _ ta argsa). - exact (annot_dearg_single _ ta argsa). - - destruct indn. + - destruct indn. refine (annot_mkApps _ argsa). cbn in *. refine (ta.1, _). From e60bf4d3b885a4007cb618891a6149d1b28c3e69 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 28 Nov 2023 14:29:38 +0100 Subject: [PATCH 2/7] WIP on wellformedness proof --- erasure/theories/Typed/ErasureCorrectness.v | 22 ++- .../theories/Typed/ExtractionCorrectness.v | 129 ++++++++++++------ 2 files changed, 109 insertions(+), 42 deletions(-) diff --git a/erasure/theories/Typed/ErasureCorrectness.v b/erasure/theories/Typed/ErasureCorrectness.v index 70155c107..70f1812bb 100644 --- a/erasure/theories/Typed/ErasureCorrectness.v +++ b/erasure/theories/Typed/ErasureCorrectness.v @@ -54,7 +54,7 @@ Qed. Section ECorrect. Existing Instance config.extraction_checker_flags. - Existing Instance PCUICSN.extraction_normalizing. + Context {no: @PCUICSN.normalizing_flags config.extraction_checker_flags}. Context {X_type : PCUICWfEnv.abstract_env_impl} {X : projT1 (projT2 X_type)}. Context {normalising_in: forall Σ : global_env_ext, wf_ext Σ -> PCUICWfEnv.abstract_env_ext_rel X Σ -> PCUICSN.NormalizationIn Σ}. @@ -78,6 +78,26 @@ Proof. apply IHl. Qed. +Lemma erase_ind_body_wellformed Σ wfΣ kn mib oib wf : + EWellformed.wf_inductive (trans_oib (@erase_ind_body X_type X _ _ Σ wfΣ kn mib oib wf)). +Proof. + generalize (erase_ind_body_correct _ wfΣ _ _ _ wf). + set (oib' := trans_oib _). clearbody oib'. + induction 1. + unfold EWellformed.wf_inductive. + destruct H0. + unfold EWellformed.wf_projections. + destruct wf as [[i []]]. + destruct oib, oib'; cbn in *. + destruct ind_projs1; eauto. + depelim H0. destruct ind_ctors1; eauto. + now depelim H. + destruct ind_ctors1; eauto. cbn. depelim H. depelim H0. + depelim onProjections; cbn in *. depelim onConstructors. depelim onConstructors. depelim o; cbn in *. + destruct H. rewrite <- H. eapply Forall2_length in H2. rewrite <- H2, on_projs_all. rewrite <- cstr_args_length. + apply eqb_refl. depelim H. now depelim H0. +Qed. + Lemma erase_ind_correct Σ wfΣ kn mib wf : erases_mutual_inductive_body mib (trans_mib (@erase_ind X_type X _ _ Σ wfΣ kn mib wf)). Proof. diff --git a/erasure/theories/Typed/ExtractionCorrectness.v b/erasure/theories/Typed/ExtractionCorrectness.v index 3a531aba3..a0e796b00 100644 --- a/erasure/theories/Typed/ExtractionCorrectness.v +++ b/erasure/theories/Typed/ExtractionCorrectness.v @@ -107,34 +107,89 @@ Proof. now eapply IHdecls. Qed. -Lemma trans_env_erase_global_decls {X_type X} decls univs retro prf deps deps' ignored : +Lemma extends_cons_right Σ Σ' kn d : + EGlobalEnv.fresh_global kn Σ -> + EGlobalEnv.extends Σ Σ' -> + EGlobalEnv.extends Σ ((kn, d) :: Σ'). +Proof. + intros hf he kn' d' hl. + cbn. + destruct (eqb_spec kn' kn). subst. + now eapply EGlobalEnv.lookup_env_Some_fresh in hl. + now eapply he in hl. +Qed. +Import EnvMap. + +Lemma trans_env_erase_global_decls {X_type X} decls nin eq univs retro prf deps deps' ignored : (forall k, ignored k = false) -> KernameSet.Subset deps deps' -> - EGlobalEnv.extends (trans_env (@Erasure.erase_global_decls_deps_recursive X_type X decls univs retro prf deps ignored)) - (filter_deps deps' (trans_env (@Erasure.erase_global_decls_recursive X_type X decls univs retro prf))). + EnvMap.fresh_globals decls -> + EGlobalEnv.extends + (filter_deps deps (@erase_global X_type X decls nin eq)) + (trans_env (@Erasure.erase_global_decls_deps_recursive X_type X decls univs retro prf deps' ignored)). Proof. - induction decls in X_type, X, deps, deps', ignored, prf |- *. + induction decls in X_type, X, deps, deps', ignored, eq, nin, prf |- *. - now cbn. - - cbn. intros hign hsub. - destruct a. destruct g. - destruct (KernameSet.mem k deps) eqn:e; cbn [map filter_deps]. - assert (KernameSet.mem k deps') as ->. - { eapply KernameSet.mem_spec in e. - now apply KernameSet.mem_spec. } - set (er := Erasure.erase_global_decl _ _ _ _ _). - set (er' := Erasure.erase_global_decl _ _ _ _ _). - set (prf' := fun (Σ : PCUICAst.PCUICEnvironment.global_env) => _). - assert (trans_global_decl er = trans_global_decl er'). admit. - rewrite <- H. - destruct (trans_global_decl er) eqn:eqr. - rewrite hign. - eapply extends_cons. - unfold trans_env in IHdecls. - eapply (IHdecls _ _ prf'); eauto. cbn [negb]. - intros kn. - rewrite !KernameSet.union_spec. + - cbn. intros hign hsub hf. depelim hf. + destruct d; cbn [map filter_deps]; + try set (er := Erasure.erase_global_decl _ _ _ _ _); + try set (er' := erase_constant_decl _ _ _ _); + try set (prf' := fun (Σ : PCUICAst.PCUICEnvironment.global_env) => _); + try set (prf'' := fun (Σ : PCUICAst.PCUICEnvironment.global_env) => _). + + destruct (KernameSet.mem kn deps) eqn:e. + * assert (KernameSet.mem kn deps') as ->. + { eapply KernameSet.mem_spec in e. + now apply KernameSet.mem_spec. } + assert (trans_global_decl er = E.ConstantDecl er'.1) as H0. admit. + rewrite <- H0. + eapply extends_cons. + unfold trans_env in IHdecls. + eapply (IHdecls _ _ _ _ prf''); eauto. cbn [negb]. + rewrite hign /=. + intros kn'. + rewrite !KernameSet.union_spec. + intuition eauto. + change (constant_decls_deps er'.1) with (global_decl_deps (E.ConstantDecl er'.1)) in H2. rewrite -H0 in H2. + clear -H2. destruct er as [[ty []] | |[]]; cbn in *; rewrite ?KernameSet.union_spec in H2 *; + intuition auto; knset. + * destruct (KernameSet.mem kn deps') eqn:e'. + rewrite hign. cbn [map]. + eapply extends_cons_right. admit. + eapply IHdecls; eauto. cbn -[er]. intros kn'. rewrite !KernameSet.union_spec. intuition eauto. + eapply IHdecls; eauto. + + destruct (KernameSet.mem kn deps) eqn:e. + * assert (KernameSet.mem kn deps') as ->. + { eapply KernameSet.mem_spec in e. + now apply KernameSet.mem_spec. } + cbn [map]. cbn in er. + assert (trans_global_decl er = E.InductiveDecl (erase_mutual_inductive_body m)) as H0. admit. + rewrite -H0. + eapply extends_cons. + eapply IHdecls; eauto. + intros kn'; knset. + * destruct (KernameSet.mem kn deps') eqn:e'. + rewrite hign. cbn [map]. + eapply extends_cons_right. admit. + eapply IHdecls; eauto. cbn -[er]. intros kn'. rewrite !KernameSet.union_spec. intuition eauto. + eapply IHdecls; eauto. Admitted. +Lemma wf_trans_inductives (m : PCUICAst.PCUICEnvironment.mutual_inductive_body) {X_type X no nin} Σ hΣ kn prf : + forallb EWellformed.wf_inductive (map trans_oib (@Erasure.erase_ind X_type X no nin Σ hΣ kn m prf).(ind_bodies)). +Proof. + destruct m. + cbn. + set (prf' := Erasure.erase_ind_obligation_1 _ _ _ _). clearbody prf'. + rewrite forallb_map. + set (fn := fun oib _ => _). + assert (forall x y, EWellformed.wf_inductive (trans_oib (fn x y))). + { intros [] hin. unfold fn. + apply (@erase_ind_body_wellformed no X_type X nin Σ hΣ kn _ _ (prf' _ hin)). } + clear -H. clearbody fn. clear -H. + induction ind_bodies; cbn => //. + rewrite IHind_bodies; eauto. rewrite andb_true_r; eauto. +Qed. + Lemma wf_erase_global_decl : forall (H := EWellformed.all_env_flags) X_type X @@ -165,32 +220,24 @@ Proof. unfold trans_global_decl,trans_cst. cbn [EWellformed.wf_global_decl]. unfold MCOption.option_default. - destruct EAst.cst_body eqn:heq. + destruct EAst.cst_body eqn:heq => //. set (deps := KernameSet.union _ _). unshelve eapply (erase_constant_body_correct'' (X_type := X_type) (decls := decls) seeds) in heq as [[t0 [T [[] ?]]]]. - shelve. intros. eapply Erasure.fake_normalization; tea. + shelve. 4:exact w. intros. eapply Erasure.fake_normalization; tea. { intros. now rewrite (prf' _ H0). } - 2:exact w. intros ->. eapply EWellformed.extends_wellformed; tea. set (prf'' := fun _ => _). clearbody prf''. cbn in prf''. rewrite erase_global_deps_erase_global. - clear. - induction decls. red; auto. - cbn -[Erasure.erase_global_decls_deps_recursive]. - destruct a as [kn []]. - set (prf0 := (fun (pf : _) => _)). - set (prf1 := (fun (pf : _) => _)). - set (prf2 := (fun (pf : _) => _)). - clearbody prf2. - cbn -[erase_global Erasure.erase_global_decls_deps_recursive]. - destruct (KernameSet.mem _ _) eqn:e. - set (prf3 := (fun (pf : _) => _)). - clearbody prf3. - - -Admitted. - + eapply trans_env_erase_global_decls; tea. subst deps. cbn [Erasure.decl_deps cst_body cst_type]. + intros kn'. rewrite !KernameSet.union_spec. intuition eauto. + pose proof (abstract_env_ext_wf _ w) as []. + eapply (PCUICWfEnvImpl.wf_fresh_globals _ X0). + * intros ->. cbn. + destruct o => //=. + - intros he => /=. + eapply wf_trans_inductives. +Qed. Ltac invert_wf := match goal with From 40d2284fc809addac642a2b381de4c9680686e04 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 28 Nov 2023 15:53:40 +0100 Subject: [PATCH 3/7] Finished proof of correctness for typed erasure --- erasure/theories/Typed/ErasureCorrectness.v | 22 ---- .../theories/Typed/ExtractionCorrectness.v | 112 ++++++++++++++++-- utils/theories/MCList.v | 28 +++++ 3 files changed, 133 insertions(+), 29 deletions(-) diff --git a/erasure/theories/Typed/ErasureCorrectness.v b/erasure/theories/Typed/ErasureCorrectness.v index 70f1812bb..df3370493 100644 --- a/erasure/theories/Typed/ErasureCorrectness.v +++ b/erasure/theories/Typed/ErasureCorrectness.v @@ -29,28 +29,6 @@ Local Ltac invert_wf := | [H : on_global_decls _ _ _ _ (_ :: _) |- _] => inversion H;subst;clear H;cbn in * end. - -Lemma map_map_In {X Y Z} xs (f : forall (x : X), In x xs -> Y) (g : Y -> Z) : - map g (map_In xs f) = map_In xs (fun x isin => g (f x isin)). -Proof. - induction xs in xs, f |- *; [easy|]. - cbn. - f_equal. - apply IHxs. -Qed. - -Lemma map_In_ext {X Y : Type} {xs : list X} {f : forall x, In x xs -> Y} g : - (forall x isin, f x isin = g x isin) -> - map_In xs f = map_In xs g. -Proof. - induction xs in xs, f, g |- *; intros all_eq; [easy|]. - cbn. - f_equal. - - apply all_eq. - - apply IHxs. - intros; apply all_eq. -Qed. - Section ECorrect. Existing Instance config.extraction_checker_flags. diff --git a/erasure/theories/Typed/ExtractionCorrectness.v b/erasure/theories/Typed/ExtractionCorrectness.v index a0e796b00..4295b2f65 100644 --- a/erasure/theories/Typed/ExtractionCorrectness.v +++ b/erasure/theories/Typed/ExtractionCorrectness.v @@ -120,6 +120,45 @@ Proof. Qed. Import EnvMap. +Opaque Erasure.flag_of_type. + +Lemma erase_erasable {X_type X nin Γ t wt} : + (forall Σ, abstract_env_ext_rel X Σ -> ∥ isErasable Σ Γ t ∥) -> + @erase X_type X nin Γ t wt = EAst.tBox. +Proof. + intros his. + rewrite erase_equation_1. + destruct inspect_bool. now cbn. + elimtype False. + move/negP: i => hi. apply hi. + now apply/is_erasableP. +Qed. + +Lemma one_inductive_body_eq x y : + x.(E.ind_name) = y.(E.ind_name) -> + x.(E.ind_propositional) = y.(E.ind_propositional) -> + x.(E.ind_kelim) = y.(E.ind_kelim) -> + x.(E.ind_ctors) = y.(E.ind_ctors) -> + x.(E.ind_projs) = y.(E.ind_projs) -> + x = y. +Proof. + destruct x, y; cbn in *; intros; f_equal; eauto. +Qed. + +Lemma fresh_global_filter_deps {X_type X} {decls nin prf} {kn deps}: + EnvMap.fresh_global kn decls -> + EGlobalEnv.fresh_global kn (filter_deps deps (@erase_global X_type X decls nin prf)). +Proof. + induction 1 in X_type, X, nin, prf, deps |- *; cbn. + - constructor. + - destruct x as [kn' []]; cbn in H |- *; + destruct (KernameSet.mem kn' deps). + + constructor. now cbn. eapply IHForall. + + eapply IHForall. + + constructor. now cbn. eapply IHForall. + + eapply IHForall. +Qed. + Lemma trans_env_erase_global_decls {X_type X} decls nin eq univs retro prf deps deps' ignored : (forall k, ignored k = false) -> KernameSet.Subset deps deps' -> @@ -140,7 +179,46 @@ Proof. * assert (KernameSet.mem kn deps') as ->. { eapply KernameSet.mem_spec in e. now apply KernameSet.mem_spec. } - assert (trans_global_decl er = E.ConstantDecl er'.1) as H0. admit. + assert (trans_global_decl er = E.ConstantDecl er'.1) as H0. + { subst er er'. clear. + destruct c as [ty [] rel]. + 2:{ cbn. + unfold Erasure.erase_constant_decl, Erasure.erase_constant_decl_clause_1. + destruct (Erasure.flag_of_type), conv_ar; try congruence; reflexivity. } + unfold erase_constant_decl, erase_constant_body. + cbn -[erase Erasure.erase_constant_decl abstract_make_wf_env_ext]. + unfold Erasure.erase_constant_decl, Erasure.erase_constant_decl_clause_1. + destruct (Erasure.flag_of_type), conv_ar; try congruence. + { cbn in c. + epose proof (Erasure.conv_arity_Is_conv_to_Arity c). + set (Σ := {| PEnv.universes := _ |}) in *. + set (Σ' := {| PEnv.universes := _ ; PEnv.declarations := decls |}) in *. + rewrite erase_erasable. + intros ? HΣ. + destruct H as [ar [[] isar]]. + set (obl := fun (Σ : PCUICAst.PCUICEnvironment.global_env) _ => _) in HΣ. + eapply Erasure.abstract_eq_wf in prf as [HΣ' [wf]]. + pose proof (abstract_env_exists (abstract_pop_decls X)) as [[Σpop hΣpop]]. + eapply abstract_make_wf_env_ext_correct in HΣ; tea. subst Σ0. + eapply abstract_pop_decls_correct in hΣpop; tea. + 2:{ intros. pose proof (abstract_env_irr _ HΣ' H). subst Σ0. cbn. now eexists. } + destruct hΣpop as [? []]. destruct Σpop; cbn in *. subst. + depelim wf. depelim o0. depelim o1. cbn in on_global_decl_d. + sq. exists ar. split; [|now left]. + unshelve eapply PCUICSR.type_reduction. 4:apply X0. constructor; eauto. exact on_global_decl_d. + reflexivity. } + { cbn [trans_global_decl]. unfold trans_cst, cst_body. + unfold erase_constant_body; cbn -[erase]. do 3 f_equal. + eapply erase_irrel_global_env. + clear; intros ?? h1 h2. + pose proof (abstract_env_exists (abstract_pop_decls X)) as [[[] hΣpop]]. + split; intros. + do 2 (erewrite <- abstract_env_lookup_correct'; tea). + eapply abstract_make_wf_env_ext_correct in H; tea. + eapply abstract_make_wf_env_ext_correct in h2; tea. congruence. + do 2 (erewrite abstract_primitive_constant_correct; tea). + eapply abstract_make_wf_env_ext_correct in H; tea. + eapply abstract_make_wf_env_ext_correct in h2; tea. congruence. } } rewrite <- H0. eapply extends_cons. unfold trans_env in IHdecls. @@ -154,7 +232,8 @@ Proof. intuition auto; knset. * destruct (KernameSet.mem kn deps') eqn:e'. rewrite hign. cbn [map]. - eapply extends_cons_right. admit. + eapply extends_cons_right. + now eapply fresh_global_filter_deps. eapply IHdecls; eauto. cbn -[er]. intros kn'. rewrite !KernameSet.union_spec. intuition eauto. eapply IHdecls; eauto. + destruct (KernameSet.mem kn deps) eqn:e. @@ -162,17 +241,35 @@ Proof. { eapply KernameSet.mem_spec in e. now apply KernameSet.mem_spec. } cbn [map]. cbn in er. - assert (trans_global_decl er = E.InductiveDecl (erase_mutual_inductive_body m)) as H0. admit. + assert (trans_global_decl er = E.InductiveDecl (erase_mutual_inductive_body m)) as H0. + { clear. subst er. + unfold trans_global_decl. f_equal. + unfold trans_mib, erase_mutual_inductive_body. + f_equal. + unfold Erasure.erase_ind. cbn. + rewrite map_map_In. + pose proof (Erasure.abstract_eq_wf _ _ _ prf) as [h [wf]]. + eapply map_mapIn_eq. intros x hin. + destruct x. unfold erase_one_inductive_body. cbn -[Erasure.erase_ind_body]. + eapply one_inductive_body_eq. + 1-3:reflexivity. + { cbn [E.ind_ctors trans_oib]. rewrite /trans_ctors. + unfold Erasure.erase_ind_body. + cbn [ExAst.ind_ctors]. rewrite map_map_In. + eapply map_mapIn_eq. + intros [] hin'. + destruct decompose_arr; reflexivity. } + { cbn. rewrite map_In_spec map_map_compose //. } } rewrite -H0. eapply extends_cons. eapply IHdecls; eauto. intros kn'; knset. * destruct (KernameSet.mem kn deps') eqn:e'. rewrite hign. cbn [map]. - eapply extends_cons_right. admit. + eapply extends_cons_right. now eapply fresh_global_filter_deps. eapply IHdecls; eauto. cbn -[er]. intros kn'. rewrite !KernameSet.union_spec. intuition eauto. eapply IHdecls; eauto. -Admitted. +Qed. Lemma wf_trans_inductives (m : PCUICAst.PCUICEnvironment.mutual_inductive_body) {X_type X no nin} Σ hΣ kn prf : forallb EWellformed.wf_inductive (map trans_oib (@Erasure.erase_ind X_type X no nin Σ hΣ kn m prf).(ind_bodies)). @@ -215,7 +312,7 @@ Proof. destruct g. - destruct (Erasure.erase_constant_decl) eqn:Hdecl. * unfold Erasure.erase_constant_decl,Erasure.erase_constant_decl_clause_1 in *. - destruct (Erasure.flag_of_type), conv_ar;try congruence. + destruct (Erasure.flag_of_type), conv_ar; try congruence. inversion Hdecl;subst;clear Hdecl. unfold trans_global_decl,trans_cst. cbn [EWellformed.wf_global_decl]. @@ -225,7 +322,7 @@ Proof. unshelve eapply (erase_constant_body_correct'' (X_type := X_type) (decls := decls) seeds) in heq as [[t0 [T [[] ?]]]]. shelve. 4:exact w. intros. eapply Erasure.fake_normalization; tea. { intros. now rewrite (prf' _ H0). } - intros ->. + intros ->. cbn. eapply EWellformed.extends_wellformed; tea. set (prf'' := fun _ => _). clearbody prf''. cbn in prf''. rewrite erase_global_deps_erase_global. @@ -238,6 +335,7 @@ Proof. - intros he => /=. eapply wf_trans_inductives. Qed. +Transparent Erasure.flag_of_type. Ltac invert_wf := match goal with diff --git a/utils/theories/MCList.v b/utils/theories/MCList.v index 73f659d9f..27e54ef68 100644 --- a/utils/theories/MCList.v +++ b/utils/theories/MCList.v @@ -1213,6 +1213,34 @@ Proof. funelim (map_In l g) => //; simpl; rewrite (H f0); trivial. Qed. +Lemma map_map_In {X Y Z} xs (f : forall (x : X), In x xs -> Y) (g : Y -> Z) : + map g (map_In xs f) = map_In xs (fun x isin => g (f x isin)). +Proof. + induction xs in xs, f |- *; [easy|]. + cbn. + f_equal. + apply IHxs. +Qed. + +Lemma map_In_ext {X Y : Type} {xs : list X} {f : forall x, In x xs -> Y} g : + (forall x isin, f x isin = g x isin) -> + map_In xs f = map_In xs g. +Proof. + induction xs in xs, f, g |- *; intros all_eq; [easy|]. + cbn. + f_equal. + - apply all_eq. + - apply IHxs. + intros; apply all_eq. +Qed. + +Lemma map_mapIn_eq {A B} (l : list A) f (g : A -> B) : + (forall x hin, f x hin = g x) -> + map_In l f = map g l. +Proof. + intros hin. rewrite <- map_In_spec. now apply map_In_ext. +Qed. + Lemma rev_repeat {A : Type} (n : nat) (a : A) : List.rev (repeat a n) = repeat a n. Proof. From f7918c380cc4d866d026379ca69675483c9d8d71 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 5 Dec 2023 12:03:51 +0100 Subject: [PATCH 4/7] Generalized theorems for typed optimization --- erasure-plugin/theories/ETransform.v | 18 +-- .../theories/Typed/ExtractionCorrectness.v | 105 ++++++++++++++++++ erasure/theories/Typed/OptimizeCorrectness.v | 42 +++++++ 3 files changed, 157 insertions(+), 8 deletions(-) diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v index 26208dd22..219b33a54 100644 --- a/erasure-plugin/theories/ETransform.v +++ b/erasure-plugin/theories/ETransform.v @@ -204,7 +204,9 @@ Program Definition erase_transform {guard : abstract_guard_impl} : Transform.t _ /\ NormalizationIn_erase_pcuic_program_1 p.1 /\ NormalizationIn_erase_pcuic_program_2 p.1 ; transform p hp := let nhs := proj2 (proj2 hp) in - @erase_program guard p (proj1 nhs) (proj2 nhs) (proj1 hp) ; + @erase_ + + program guard p (proj1 nhs) (proj2 nhs) (proj1 hp) ; post p := [/\ wf_eprogram_env all_env_flags p & EEtaExpandedFix.expanded_eprogram_env p]; obseq p hp p' v v' := let Σ := p.1 in Σ ;;; [] |- v ⇝ℇ v' |}. @@ -380,14 +382,14 @@ Qed. Instance rebuild_wf_env_extends {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp : TransformExt.t (rebuild_wf_env_transform with_exp) (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1). Proof. - red. intros p p' pr pr' ext. red. now rewrite /transform /=. + red. intros p p' pr pr' ext. red. now rewrite /transform /=. Qed. #[global] Instance rebuild_wf_env_extends' {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp : TransformExt.t (rebuild_wf_env_transform with_exp) extends_eprogram extends_eprogram_env. Proof. - red. intros p p' pr pr' [? ?]. now rewrite /transform /=. + red. intros p p' pr pr' [? ?]. now rewrite /transform /=. Qed. Program Definition remove_params_optimization {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false} @@ -431,7 +433,7 @@ Instance remove_params_extends' {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.wi TransformExt.t (remove_params_optimization (wcon:=wcon)) extends_eprogram_env extends_eprogram. Proof. red. intros p p' pr pr' [ext eq]. rewrite /transform /= /strip_program. rewrite eq. - red. cbn -[strip_env strip]. split. eapply strip_extends_env => //. apply pr. apply pr'. + red. cbn -[strip_env strip]. split. eapply strip_extends_env => //. apply pr. apply pr'. cbn -[strip_env strip]. eapply strip_extends => //. apply pr'. rewrite -eq. apply pr. Qed. @@ -470,7 +472,7 @@ Instance remove_params_fast_extends {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEva (efl := all_env_flags): TransformExt.t (remove_params_fast_optimization (wcon:=wcon)) (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1). Proof. - red. intros p p' pr pr' ext. rewrite /transform /=. + red. intros p p' pr pr' ext. rewrite /transform /=. rewrite -!ERemoveParams.Fast.strip_env_fast. eapply strip_extends_env => //. apply pr. apply pr'. Qed. @@ -523,7 +525,7 @@ Qed. Instance remove_match_on_box_extends' {fl : WcbvFlags} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} : TransformExt.t (remove_match_on_box_trans (wcon:=wcon) (hastrel := hastrel) (hastbox := hastbox)) extends_eprogram_env extends_eprogram. Proof. - red. intros p p' pr pr' [ext eq]. rewrite /transform /= /remove_match_on_box_program. split. + red. intros p p' pr pr' [ext eq]. rewrite /transform /= /remove_match_on_box_program. split. eapply remove_match_on_box_extends_env => //. apply pr. apply pr'. rewrite -eq. eapply wellformed_remove_match_on_box_extends; eauto. apply pr. apply pr'. @@ -567,7 +569,7 @@ Instance inline_projections_optimization_extends' {fl : WcbvFlags} {wcon : EWcbv {hastrel : has_tRel} {hastbox : has_tBox} : TransformExt.t (inline_projections_optimization (wcon:=wcon) (hastrel := hastrel) (hastbox := hastbox)) extends_eprogram_env extends_eprogram. Proof. - red. intros p p' pr pr' [ext eq]. rewrite /transform /= /optimize_program /=. split. + red. intros p p' pr pr' [ext eq]. rewrite /transform /= /optimize_program /=. split. eapply optimize_extends_env => //. apply pr. apply pr'. rewrite -eq. eapply wellformed_optimize_extends; eauto. apply pr. apply pr'. @@ -616,7 +618,7 @@ Instance constructors_as_blocks_extends' (efl : EEnvFlags) TransformExt.t (constructors_as_blocks_transformation (has_app := has_app) (has_rel := has_rel) (hasbox := hasbox) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks)) extends_eprogram_env extends_eprogram. Proof. - red. intros p p' pr pr' [ext eq]. rewrite /transform /=. split. + red. intros p p' pr pr' [ext eq]. rewrite /transform /=. split. eapply transform_blocks_env_extends => //. apply pr. apply pr'. unfold transform_blocks_program => /=. rewrite -eq. diff --git a/erasure/theories/Typed/ExtractionCorrectness.v b/erasure/theories/Typed/ExtractionCorrectness.v index 4295b2f65..21eb95b05 100644 --- a/erasure/theories/Typed/ExtractionCorrectness.v +++ b/erasure/theories/Typed/ExtractionCorrectness.v @@ -458,6 +458,111 @@ Proof. now eapply PCUICWfEnvImpl.wf_fresh_globals. Qed. +From Coq Require Import String. +Local Open Scope string_scope. + +Import MCMonadNotation. + +Definition compute_masks overridden_masks do_trim_const_masks do_trim_ctor_masks Σ : result dearg_set bytestring.string := + let (const_masks, ind_masks) := Utils.timed "Dearg analysis" (fun _ => analyze_env overridden_masks Σ) in + let const_masks := (if do_trim_const_masks then trim_const_masks else id) const_masks in + let ind_masks := (if do_trim_ctor_masks then trim_ind_masks else id) ind_masks in + throwIf (negb (is_expanded_env ind_masks const_masks Σ)) + "Erased environment is not expanded enough for dearging to be provably correct"%bs ;; + throwIf (negb (valid_masks_env ind_masks const_masks Σ)) + "Analysis produced masks that ask to remove live arguments"%bs ;; + Ok (Build_dearg_set const_masks ind_masks). + +Definition dearg_env masks Σ := + debox_env_types (dearg_env masks.(ind_masks) masks.(const_masks) Σ). + +Import PCUICWfEnvImpl. + +Program Definition dearg_term {Σ} (wfΣ : ∥wf_ext Σ∥) (masks : dearg_set) (t : PCUICAst.term) (w : welltyped Σ [] t) : term := + let wfext := @abstract_make_wf_env_ext _ (optimized_abstract_env_impl (guard := Erasure.fake_guard_impl_instance)) (PCUICWfEnvImpl.build_wf_env_from_env Σ (map_squash fst wfΣ)) Σ.2 _ in + dearg masks.(ind_masks) masks.(const_masks) (erase _ wfext (normalization_in := _) [] t _). + Next Obligation. + refine (let 'sq wfΣ := wfΣ in let nin := Erasure.fake_normalization Σ wfΣ in _). + eapply nin. destruct Σ. apply H. + Qed. + + Next Obligation. + destruct Σ. apply w. + Qed. + +Theorem extract_correct_gen + (H := EWellformed.all_env_flags) + (wfl := opt_wcbv_flags) + (Σ : P.global_env_ext) (wfΣ : ∥wf_ext Σ∥) + t v ignored exΣ masks : + axiom_free Σ -> + forall wt : welltyped Σ [] t, + forall wv : welltyped Σ [] v, + Σ p⊢ t ⇓ v -> + (isErasable Σ [] t -> False) -> + (forall k, ignored k = false) -> + let t' := dearg_term wfΣ masks t wt in + extract_pcuic_env + (pcuic_args extract_within_coq) + Σ (wf_squash wfΣ) (EAstUtils.term_global_deps t') ignored = Ok exΣ -> + compute_masks (fun _ => None) true true exΣ = Ok masks -> + ∥trans_env exΣ e⊢ t' ⇓ dearg_term wfΣ masks v wv ∥. +Proof. + intros ax [T wt] wv ev not_erasable no_ignores ex. + cbn -[dearg_transform] in *. + destruct dearg_transform eqn:dt; cbn -[dearg_transform] in *; [|congruence]. + intros [=->]. + destruct wfΣ. + unfold dearg_term. + set (e := abstract_make_wf_env_ext _ _ _). + pose proof (abstract_env_ext_exists e) as [[Σe he]]. + unfold dearg_term in ex. + match goal with + [H := context [ @erase ?X_type ?X ?nin ?Γ t ?wt ] |- _ ] => + pose proof (@erases_erase X_type X nin Γ t wt _ he) + end. + cbn in he. subst Σe. destruct Σ as [Σ univs]; cbn [fst snd] in *. + eapply erases_correct with + (Σ' := trans_env (Erasure.erase_global_decls_deps_recursive (PCUICAst.PCUICEnvironment.declarations Σ) + (PCUICAst.PCUICEnvironment.universes Σ) _ _ + _ ignored)) in ev as (erv&erase_to&[erev]);eauto. + 2:{ now eexists. } + intros Σex. + * move: dt. unfold dearg_transform. eapply dearg_correct. + 2:{ unshelve eapply (erases_erase (X_type := (optimized_abstract_env_impl (guard := Erasure.fake_guard_impl_instance)))). exact e. 3:now destruct Σ. + * intros. pose proof (abstract_env_ext_irr _ he H0). subst Σ0. now apply Erasure.fake_normalization. + * intros Σ0 he'; pose proof (abstract_env_ext_irr _ he he'); subst Σ0. cbn in he, he'. subst Σe. now destruct Σ. } + 3:{ intros hm. + + eapply dearg_correct. + + depelim erase_to;[|easy]. + constructor. + eapply dearg_transform_correct; eauto. + clear dt. + eapply (@optimize_correct _ _ _ (tConst kn) (tConstruct ind c []));eauto. + * remember (Erasure.erase_global_decls_deps_recursive _ _ _ _ _ _) as eΣ. + assert (EWellformed.wf_glob (trans_env eΣ)). + { subst eΣ. now eapply wf_erase_global_decls_recursive. } + now apply EWellformed.wellformed_closed_env. + * eapply wf_erase_global_decls_recursive; auto. + + now eexists. + + eapply inversion_Const in wt as (?&?&?&?&?); auto. + clear dt. + eapply global_erased_with_deps_erases_deps_tConst; eauto. + destruct Σ as [Σ0 univ_decls]. + destruct Σ0 as [univs Σ1]. + apply wf_ext_wf in w as w1. cbn. + eapply erase_global_decls_deps_recursive_correct;eauto. + * unfold PCUICAst.declared_constant in *. + cbn. + intros ? ->%KernameSet.singleton_spec;cbn in *. + intros eq. set (env := {| PEnv.declarations := Σ1 |}) in *. + eapply (lookup_global_In_wf _ env) in d; eauto. + * now apply KernameSet.singleton_spec. + Unshelve. eapply fresh_globals_erase_global_decl_rec. + now eapply PCUICWfEnvImpl.wf_fresh_globals. +Qed. + (* Print Assumptions extract_correct. *) (** There are some assumptions of which almost all are in MetaCoq. diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v index 5259d56f7..5f7d180ca 100644 --- a/erasure/theories/Typed/OptimizeCorrectness.v +++ b/erasure/theories/Typed/OptimizeCorrectness.v @@ -4418,6 +4418,48 @@ Proof. + depelim ev. Qed. +Import MCMonadNotation ResultMonad. +From Coq Require Import String. +Definition compute_masks overridden_masks (do_trim_const_masks do_trim_ctor_masks : bool) Σ : result dearg_set bytestring.string := + let (const_masks, ind_masks) := Utils.timed "Dearg analysis" (fun _ => analyze_env overridden_masks Σ) in + let const_masks := (if do_trim_const_masks then trim_const_masks else id) const_masks in + let ind_masks := (if do_trim_ctor_masks then trim_ind_masks else id) ind_masks in + throwIf (negb (is_expanded_env ind_masks const_masks Σ)) + "Erased environment is not expanded enough for dearging to be provably correct"%bs ;; + throwIf (negb (valid_masks_env ind_masks const_masks Σ)) + "Analysis produced masks that ask to remove live arguments"%bs ;; + Ok (Build_dearg_set const_masks ind_masks). + +Definition dearg_env masks Σ := + debox_env_types (dearg_env masks.(ind_masks) masks.(const_masks) Σ). + +Import PCUICWfEnvImpl PCUICWfEnv PCUICTyping. + +Definition dearg_term masks t := + dearg masks.(ind_masks) masks.(const_masks) t. + +Lemma dearg_transform_gen_correct {wfl : WcbvFlags} overridden_masks do_trim_const_masks do_trim_ctor_masks : + forall (Σ Σopt : global_env) t v masks, + with_constructor_as_block = false -> + env_closed (trans_env Σ) -> + compute_masks overridden_masks do_trim_const_masks do_trim_ctor_masks Σ = ResultMonad.Ok masks -> + closed t -> + valid_cases masks.(ind_masks) t -> + is_expanded masks.(ind_masks) masks.(const_masks) t -> + trans_env Σ e⊢ t ⇓ v -> trans_env (dearg_env masks Σ) e⊢ dearg_term masks t ⇓ dearg_term masks v. +Proof. + intros Σ Σopt t v masks block cl opt clt vc expc ev. + unfold compute_masks in opt. cbn in opt. + destruct analyze_env; cbn in *. + destruct is_expanded_env eqn:exp; cbn in *; [|congruence]. + destruct valid_masks_env eqn:valid; cbn in *; [|congruence]. + injection opt as <-. + set (im := (if do_trim_ctor_masks then trim_ind_masks else id) ind_masks) in *; clearbody im. + set (cm := (if do_trim_const_masks then trim_const_masks else id) const_masks) in *; clearbody cm. + apply eval_debox_env_types;eauto. + apply dearg_correct; eauto. +Qed. + Lemma dearg_transform_correct {wfl : WcbvFlags} overridden_masks do_trim_const_masks do_trim_ctor_masks : ExtractTransformCorrect (dearg_transform overridden_masks do_trim_const_masks do_trim_ctor_masks true true true). Proof. From c2620bb8002a988de5c3d281e9067f0079be9380 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 7 Dec 2023 14:11:47 +0100 Subject: [PATCH 5/7] Typed erasure variant --- erasure-plugin/_PluginProject.in | 29 +- erasure-plugin/src/g_metacoq_erasure.mlg | 15 +- .../src/metacoq_erasure_plugin.mlpack | 17 +- erasure-plugin/theories/ETransform.v | 310 +++++++++++++++++- erasure-plugin/theories/Erasure.v | 136 +++++++- erasure-plugin/theories/ErasureCorrectness.v | 18 +- erasure/theories/Typed/CertifyingEta.v | 14 +- .../theories/Typed/ExtractionCorrectness.v | 158 +++++---- test-suite/erasure_live_test.v | 8 +- 9 files changed, 602 insertions(+), 103 deletions(-) diff --git a/erasure-plugin/_PluginProject.in b/erasure-plugin/_PluginProject.in index 217e83bb3..089e2bba1 100644 --- a/erasure-plugin/_PluginProject.in +++ b/erasure-plugin/_PluginProject.in @@ -11,6 +11,11 @@ src/wGraph.ml src/wGraph.mli src/etaExpand.mli src/etaExpand.ml +src/utils.mli +src/utils.ml + +src/resultMonad.mli +src/resultMonad.ml # From PCUIC src/pCUICPrimitive.mli @@ -79,6 +84,24 @@ src/eSpineView.ml src/eRemoveParams.mli src/eRemoveParams.ml +# Typed erasure +src/exAst.mli +src/exAst.ml +src/optimize.mli +src/optimize.ml +src/vectorDef.mli +src/vectorDef.ml +src/vector.mli +src/vector.ml +src/fin.mli +src/fin.ml +src/extractionCorrectness.mli +src/extractionCorrectness.ml +src/optimizeCorrectness.mli +src/optimizeCorrectness.ml +src/erasure.mli +src/erasure.ml + src/erasureFunction.mli src/erasureFunction.ml src/erasureFunctionProperties.mli @@ -87,6 +110,8 @@ src/ePretty.mli src/ePretty.ml src/eOptimizePropDiscr.mli src/eOptimizePropDiscr.ml +src/optimizePropDiscr.mli +src/optimizePropDiscr.ml src/eProgram.mli src/eProgram.ml src/eInlineProjections.mli @@ -95,8 +120,8 @@ src/eConstructorsAsBlocks.mli src/eConstructorsAsBlocks.ml src/eTransform.mli src/eTransform.ml -src/erasure.mli -src/erasure.ml +src/erasure0.mli +src/erasure0.ml src/g_metacoq_erasure.mlg src/metacoq_erasure_plugin.mlpack diff --git a/erasure-plugin/src/g_metacoq_erasure.mlg b/erasure-plugin/src/g_metacoq_erasure.mlg index 99b1c9dd1..6f10e648b 100644 --- a/erasure-plugin/src/g_metacoq_erasure.mlg +++ b/erasure-plugin/src/g_metacoq_erasure.mlg @@ -25,12 +25,15 @@ let pr_char_list l = (* We allow utf8 encoding *) str (Caml_bytestring.caml_string_of_bytestring l) -let check ~bypass ~fast env evm c = +let check ~bypass ~fast ?(with_types=false) env evm c = debug (fun () -> str"Quoting"); let term = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass env evm) (EConstr.to_constr evm c) in let erase = time (str"Erasure") - (if fast then Erasure.erase_fast_and_print_template_program - else Erasure.erase_and_print_template_program) + (if fast then Erasure0.erase_fast_and_print_template_program + else + if with_types then + Erasure0.typed_erase_and_print_template_program + else Erasure0.erase_and_print_template_program) term in Feedback.msg_info (pr_char_list erase) @@ -43,6 +46,12 @@ VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY let (c, _) = Constrintern.interp_constr env evm c in check ~bypass:true ~fast:false env evm c } +| [ "MetaCoq" "Typed" "Erase" constr(c) ] -> { + let env = Global.env () in + let evm = Evd.from_env env in + let (c, _) = Constrintern.interp_constr env evm c in + check ~bypass:true ~fast:false ~with_types:true env evm c + } | [ "MetaCoq" "Erase" constr(c) ] -> { let env = Global.env () in let evm = Evd.from_env env in diff --git a/erasure-plugin/src/metacoq_erasure_plugin.mlpack b/erasure-plugin/src/metacoq_erasure_plugin.mlpack index 8bd95c56b..a366f9564 100644 --- a/erasure-plugin/src/metacoq_erasure_plugin.mlpack +++ b/erasure-plugin/src/metacoq_erasure_plugin.mlpack @@ -2,12 +2,17 @@ MSetWeakList EqdepFacts Ssrbool -Utils +Fin +Vector +VectorDef +Utils +ResultMonad WGraph UGraph0 EtaExpand + WcbvEval Classes0 Logic1 @@ -60,7 +65,15 @@ EOptimizePropDiscr EInlineProjections EConstructorsAsBlocks EProgram -ETransform +OptimizePropDiscr + +ExAst +Optimize +OptimizeCorrectness Erasure +ExtractionCorrectness + +ETransform +Erasure0 G_metacoq_erasure diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v index 219b33a54..fd18daaa9 100644 --- a/erasure-plugin/theories/ETransform.v +++ b/erasure-plugin/theories/ETransform.v @@ -204,9 +204,7 @@ Program Definition erase_transform {guard : abstract_guard_impl} : Transform.t _ /\ NormalizationIn_erase_pcuic_program_1 p.1 /\ NormalizationIn_erase_pcuic_program_2 p.1 ; transform p hp := let nhs := proj2 (proj2 hp) in - @erase_ - - program guard p (proj1 nhs) (proj2 nhs) (proj1 hp) ; + @erase_program guard p (proj1 nhs) (proj2 nhs) (proj1 hp) ; post p := [/\ wf_eprogram_env all_env_flags p & EEtaExpandedFix.expanded_eprogram_env p]; obseq p hp p' v v' := let Σ := p.1 in Σ ;;; [] |- v ⇝ℇ v' |}. @@ -260,6 +258,285 @@ Next Obligation. cbn; intros. sq. now subst. Qed. +(** Typed erasure variant, using erasure but also keeping type information useful for later optimizations, + e.g., de-arging. *) + +Definition typed_erasure_pre (p : pcuic_program) := + ∥ wt_pcuic_program (cf := config.extraction_checker_flags) p ∥ + /\ PCUICEtaExpand.expanded_pcuic_program p + /\ NormalizationIn_erase_pcuic_program_1 p.1 + /\ NormalizationIn_erase_pcuic_program_2 p.1. + +From MetaCoq.Erasure.Typed Require Import Erasure ExAst Optimize ExtractionCorrectness OptimizeCorrectness. +From MetaCoq.Erasure Require Import EWellformed. +From MetaCoq.PCUIC Require Import PCUICTyping. +From MetaCoq.SafeChecker Require Import PCUICWfEnvImpl. +Set Equations Transparent. +Equations? erase_program_typed guard (p : pcuic_program) (pre : typed_erasure_pre p) : ExAst.global_env * EAst.term := + erase_program_typed guard p pre := + let wfΣ : ∥ wf_ext p.1 ∥ := _ in + let X := PCUICWfEnvImpl.build_wf_env_from_env p.1 (map_squash fst wfΣ) in + let t' := erase_term wfΣ p.2 _ in + (erase_global_decls_deps_recursive + (X_type := PCUICWfEnvImpl.optimized_abstract_env_impl (guard := guard)) + (X := X) (PEnv.declarations p.1) (PEnv.universes p.1) (PEnv.retroknowledge p.1) + (fun Σ' eq => _) + (EAstUtils.term_global_deps t') (fun _ => false), t'). +Proof. + - destruct pre0. destruct H. destruct X. now sq. + - destruct pre0 as [[[wf []]] _]. now eexists. + - cbn in eq. rewrite eq. clear; destruct p.1; cbn in *. + set(x := eval_eprogram_env). + destruct g; cbn in *. + now destruct trans_env_env; cbn. +Qed. + +Definition trans_ex_prog (p : ExAst.global_env * EAst.term) : EAst.global_context * EAst.term := + (ExAst.trans_env p.1, p.2). + +Definition eval_typed_eprogram fl := + (fun p v => ∥ @EWcbvEval.eval fl (ExAst.trans_env p.1) p.2 v ∥). + +Program Definition typed_erase_transform (guard := fake_guard_impl_instance) : + Transform.t _ _ PCUICAst.term EAst.term PCUICAst.term EAst.term + eval_pcuic_program (eval_typed_eprogram EWcbvEval.default_wcbv_flags) := + {| name := "typed erasure"; + pre p := + ∥ wt_pcuic_program (cf := config.extraction_checker_flags) p ∥ + /\ PCUICEtaExpand.expanded_pcuic_program p + /\ NormalizationIn_erase_pcuic_program_1 p.1 + /\ NormalizationIn_erase_pcuic_program_2 p.1 ; + transform p hp := erase_program_typed guard p hp ; + post p := [/\ wf_eprogram all_env_flags (trans_ex_prog p) & + EEtaExpandedFix.expanded_eprogram (trans_ex_prog p)]; + obseq p hp p' v v' := let Σ := p.1 in Σ ;;; [] |- v ⇝ℇ v' |}. + +Next Obligation. + cbn -[erase_program]. + intros p (wtp&etap&?&?). + destruct erase_program_typed eqn:e. + split. + - unfold erase_program_typed, erase_pcuic_program in e. + set (egf := erase_global_decls_deps_recursive _ _ _ _ _ _) in e. + unfold erase_term in e. + set (ef := erase _ _ _ _ _) in e. + cbn -[egf ef] in e. injection e. intros <- <-. clear e. + unfold trans_ex_prog in *. + split. + now eapply wf_erase_global_decls_recursive. + cbn [fst snd]. + eapply extends_wellformed. + now eapply wf_erase_global_decls_recursive. + 2:unshelve eapply (erase_wellformed_weaken (PEnv.declarations p.1) _ _ _ (Γ:=[])); tea. + 4:exact KernameSet.empty. + 2:{ intros. now eapply Erasure.fake_normalization. } + 2:{ abstract (cbn; destruct p; destruct g; cbn; congruence). } + rewrite erase_global_deps_erase_global. + eapply trans_env_erase_global_decls; eauto. + intros kn hin. rewrite KernameSet.union_spec in hin. destruct hin; [knset|]. + unfold erase_term. + match goal with + | [ H : context [@erase ?X_type ?X ?nin ?G ?t ?wt ] |- context [ @erase ?X_type' ?X' ?nin' ?G' ?t' ?wt' ] ] => + rewrite -(@erase_irrel_global_env X_type X nin X_type' X' nin' G t wt wt'); eauto + end. + red. cbn. intros; subst; intuition eauto. + destruct wtp. eapply wf_fresh_globals, w. + - todo "expanded". +Qed. + +Next Obligation. + intros guard. + set (cf := extraction_checker_flags). + cbn. red. + move=> p v [[wf [T [HT1 HT2]]]]. unfold eval_pcuic_program, eval_typed_eprogram. + unfold erase_program_typed. + set (er := erase_global_decls_deps_recursive _ _ _ _ _ _). + set (et := erase_term _ _ _). + unshelve edestruct (erase_pcuic_program_normalization_helper); cbn in *; try now destruct wf; eauto. + destruct p as [Σ t]. + intros [ev]. + cbn in ev. clear H0. + unfold erase_term, make_env in et. + set (e := abstract_make_wf_env_ext _ _ _) in *. + cbn [fst snd] in et. + pose proof (abstract_env_ext_exists e) as [[Σe he]]. + match goal with + [H := context [ @erase ?X_type ?X ?nin ?Γ t ?wt ] |- _ ] => + pose proof (@erases_erase X_type X nin Γ t wt _ he) + end. + cbn in he. subst Σe. destruct Σ as [Σ univs]; cbn [fst snd] in *. + assert (wv : welltyped (Σ, univs) [] v). + { destruct wf. destruct s. eexists. eapply PCUICClassification.subject_reduction_eval; tea. } + eapply ErasureCorrectness.erases_correct with (Σ := (trans_env_env Σ, univs)) (Σ' := trans_env er) in ev as (erv&erase_to&[erev]);eauto. + - apply wf. + - destruct wf. destruct s; now eexists. + - destruct wf as [wf []]. eapply erase_global_erases_deps; tea. + subst er. + set (obl := fun Σ' => _). + set (obl' := fun Σ' => _). + destruct Σ. destruct trans_env_env. cbn -[build_wf_env_from_env e] in *. + eapply (ErasureCorrectness.erase_global_decls_deps_recursive_correct _ _ _ _); eauto. + intros k hin. + eapply term_global_deps_spec in hin; tea. red in hin. destruct hin as [[decl eq]]. + cbn in eq. cbn. now rewrite eq. cbn. eapply wf. +Qed. + +(** De-arging requires first the removal of match-on-box which allows getting rid of all + dependencies on propositional inductive types. *) +Import EOptimizePropDiscr OptimizePropDiscr EWcbvEval. + +Definition remove_match_on_box_typed_env m (Σ : global_env) := + map (on_snd (remove_match_on_box_decl m)) Σ. + +Definition map_of_typed_global_env (p : global_env) (fr : fresh_globals p) := + GlobalContextMap.make (trans_env p) (OptimizePropDiscr.remove_match_on_box_env_obligation_1 p fr). + +Definition pre_remove_match_on_box_typed efl (p : global_env * term) : Prop := + wf_eprogram efl (trans_ex_prog p) /\ EEtaExpandedFix.expanded_eprogram (trans_ex_prog p). + +Lemma pre_remove_match_on_box_typed_fresh efl p : pre_remove_match_on_box_typed efl p -> fresh_globals p.1. +Proof. + intros []. destruct H. eapply wf_glob_fresh in H. +Admitted. + +Lemma map_trans_env Σ m : map (on_snd (EOptimizePropDiscr.remove_match_on_box_decl m)) (trans_env Σ) = trans_env (map (on_snd (OptimizePropDiscr.remove_match_on_box_decl m)) Σ). +Proof. + induction Σ; cbn => //=. + destruct a as [[kn b] d]; cbn. f_equal. + unfold on_snd. cbn. f_equal. destruct d => //. destruct o => //. + now apply IHΣ. +Qed. + +Definition remove_match_on_box_program_typed efl (p : global_env * term) (pre : pre_remove_match_on_box_typed efl p) : global_env * term := + let m := map_of_typed_global_env p.1 (pre_remove_match_on_box_typed_fresh efl p pre) in + (remove_match_on_box_typed_env m p.1, EOptimizePropDiscr.remove_match_on_box m p.2). +Import EOptimizePropDiscr. + +Program Definition remove_match_on_box_typed_transform {fl : WcbvFlags} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} : + Transform.t _ _ EAst.term EAst.term _ _ (eval_typed_eprogram fl) (eval_typed_eprogram (disable_prop_cases fl)) := + {| name := "optimize_prop_discr"; + transform p pr := remove_match_on_box_program_typed efl p pr ; + pre p := pre_remove_match_on_box_typed efl p; + post p := pre_remove_match_on_box_typed efl p; + obseq p hp p' v v' := v' = EOptimizePropDiscr.remove_match_on_box (map_of_typed_global_env p.1 (pre_remove_match_on_box_typed_fresh efl p hp)) v |}. + +Next Obligation. + move=> fl wcon efl hastrel hastbox [Σ t] [wfp etap]. + cbn in *. split. + - cbn in *. unfold trans_ex_prog in *. cbn [fst snd] in *. + unfold remove_match_on_box_program_typed; cbn [fst snd]. + cbn. + rewrite trans_env_remove_match_on_box_env. + split. + + eapply remove_match_on_box_env_wf => //. + cbn. eapply wfp. + + cbn -[remove_match_on_box_env]. + rewrite /map_of_typed_global_env. + set (obl := trans_env_fresh_globals _ _). + set (obl' := OptimizePropDiscr.remove_match_on_box_env_obligation_1 _ _). + assert (obl = obl') by apply proof_irrelevance. clearbody obl obl'; subst obl'. + eapply remove_match_on_box_wellformed_irrel. cbn. eapply wfp. + eapply remove_match_on_box_wellformed => //=. apply wfp. apply wfp. + - todo "excpanded". (* eapply remove_match_on_box_program_expanded.*) +Qed. +Next Obligation. + red. move=> fl wcon efl hastrel hastbox [Σ t] /= v [wfe wft] [ev]. + cbn -[trans_env] in ev. + unfold eval_typed_eprogram, remove_match_on_box_program_typed. cbn -[trans_env]. + set (obl := pre_remove_match_on_box_typed_fresh _ _ _). + eapply (EOptimizePropDiscr.remove_match_on_box_correct (Σ := map_of_typed_global_env _ obl) t v) in ev; cbn -[trans_env]; eauto. + eexists; split => //. rewrite -map_trans_env. now sq. + apply wfe. + eapply wellformed_closed_env, wfe. + eapply wellformed_closed, wfe. + Unshelve. eauto. +Qed. + +Definition check_dearging_precond Σ t := + if closed_env (trans_env Σ) then + match ExtractionCorrectness.compute_masks (fun _ : kername => None) true true Σ with + | ResultMonad.Ok masks => + if valid_cases (ind_masks masks) t && is_expanded (ind_masks masks) (const_masks masks) t then Some masks else None + | _ => None + end + else None. + +Definition check_dearging_trans p := + ((check_dearging_precond p.1 p.2, p.1), p.2). + +Definition eval_typed_eprogram_masks fl := + (fun (p : (option dearg_set * global_env) * term) v => ∥ @EWcbvEval.eval fl (ExAst.trans_env p.1.2) p.2 v ∥). + +Definition post_dearging_checks efl (p : (option dearg_set × global_env) × term) := + (p.1.1 = check_dearging_precond p.1.2 p.2) /\ + wf_eprogram efl (trans_env p.1.2, p.2) /\ EEtaExpandedFix.expanded_eprogram (trans_env p.1.2, p.2). + +Program Definition dearging_checks_transform {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} : + Transform.t _ _ EAst.term EAst.term _ _ (eval_typed_eprogram opt_wcbv_flags) (eval_typed_eprogram_masks opt_wcbv_flags) := + {| name := "dearging"; + transform p _ := check_dearging_trans p ; + pre p := pre_remove_match_on_box_typed efl p; + post := post_dearging_checks efl; + obseq p hp p' v v' := v' = v |}. +Next Obligation. + cbn. intros. split => //. +Qed. +Next Obligation. + cbn. intros. red. cbn. intros. exists v; split => //. +Qed. + +Definition dearg (p : (option dearg_set × global_env) * term) : global_context * term := + match p.1.1 with + | Some masks => (trans_env (dearg_env masks p.1.2), dearg_term masks p.2) + | None => (trans_env p.1.2, p.2) + end. + +Program Definition dearging_transform {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} : + Transform.t _ _ EAst.term EAst.term _ _ (eval_typed_eprogram_masks opt_wcbv_flags) (eval_eprogram opt_wcbv_flags) := + {| name := "dearging"; + transform p _ := dearg p ; + pre p := post_dearging_checks efl p; + post p := wf_eprogram efl p /\ EEtaExpandedFix.expanded_eprogram p ; + obseq p hp p' v v' := v' = (dearg (p.1, v)).2 |}. + +Next Obligation. +Proof. + cbn. intros. + unfold dearg. + destruct p. rewrite H. + destruct check_dearging_precond eqn:eqp; cbn => //. + split. + - split; cbn. clear H. unfold dearg_env. + all:todo "wf". + - todo "expanded". +Qed. + +Next Obligation. + cbn. intros. red. + intros p v [he [wfe exp]]. unfold eval_typed_eprogram_masks. + intros [ev]. + unfold dearg. rewrite he. + destruct (check_dearging_precond) as [masks|] eqn:cpre. + * eapply (extract_correct_gen' _ _ _ masks) in ev as ev'. destruct ev' as [ev']. + eexists. split. red. sq. cbn. exact ev'. auto. + - destruct wfe. now eapply wellformed_closed_env. + - destruct wfe. now eapply wellformed_closed. + - move: cpre. unfold check_dearging_precond. destruct closed_env => //. + destruct ExtractionCorrectness.compute_masks => //. + destruct (_ && _) => //. congruence. + - move: cpre. rewrite /check_dearging_precond. + destruct closed_env => //. + destruct ExtractionCorrectness.compute_masks => //. + destruct valid_cases eqn:vc => //. cbn. + destruct is_expanded => //. now intros [= ->]. + - move: cpre. rewrite /check_dearging_precond. + destruct closed_env => //. + destruct ExtractionCorrectness.compute_masks => //. + destruct valid_cases eqn:vc => //. cbn. + destruct is_expanded eqn:ise => //. now intros [= ->]. + * exists v. cbn. split => //. +Qed. + Definition extends_eprogram (p p' : eprogram) := extends p.1 p'.1 /\ p.2 = p'.2. @@ -364,30 +641,39 @@ Qed. Definition rebuild_wf_env {efl} (p : eprogram) (hwf : wf_eprogram efl p): eprogram_env := (GlobalContextMap.make p.1 (wf_glob_fresh p.1 (proj1 hwf)), p.2). -Program Definition rebuild_wf_env_transform {fl : EWcbvEval.WcbvFlags} {efl} (with_exp : bool) : +Definition preserves_expansion with_fix p := + if with_fix then EEtaExpandedFix.expanded_eprogram p + else EEtaExpanded.expanded_eprogram_cstrs p. + +Definition preserves_expansion_env with_fix p := + if with_fix then EEtaExpandedFix.expanded_eprogram_env p + else EEtaExpanded.expanded_eprogram_env_cstrs p. + +Program Definition rebuild_wf_env_transform {fl : EWcbvEval.WcbvFlags} {efl} (with_exp with_fix : bool) : Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram fl) (eval_eprogram_env fl) := {| name := "rebuilding environment lookup table"; - pre p := wf_eprogram efl p /\ (with_exp ==> EEtaExpanded.expanded_eprogram_cstrs p); + pre p := wf_eprogram efl p /\ (with_exp -> preserves_expansion with_fix p); transform p pre := rebuild_wf_env p (proj1 pre); - post p := wf_eprogram_env efl p /\ (with_exp ==> EEtaExpanded.expanded_eprogram_env_cstrs p); + post p := wf_eprogram_env efl p /\ (with_exp -> preserves_expansion_env with_fix p); obseq p hp p' v v' := v = v' |}. Next Obligation. - cbn. intros fl efl [] input [wf exp]; cbn; split => //. + cbn. unfold preserves_expansion, preserves_expansion_env. + intros fl efl [] [] input [wf exp]; cbn; split => //. Qed. Next Obligation. - cbn. intros fl efl [] input v [] ev p'; exists v; split => //. + cbn. intros fl efl [] [] input v [] ev p'; exists v; split => //. Qed. #[global] -Instance rebuild_wf_env_extends {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp : - TransformExt.t (rebuild_wf_env_transform with_exp) (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1). +Instance rebuild_wf_env_extends {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp with_fix : + TransformExt.t (rebuild_wf_env_transform with_exp with_fix) (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1). Proof. red. intros p p' pr pr' ext. red. now rewrite /transform /=. Qed. #[global] -Instance rebuild_wf_env_extends' {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp : - TransformExt.t (rebuild_wf_env_transform with_exp) extends_eprogram extends_eprogram_env. +Instance rebuild_wf_env_extends' {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp with_fix : + TransformExt.t (rebuild_wf_env_transform with_exp with_fix) extends_eprogram extends_eprogram_env. Proof. red. intros p p' pr pr' [? ?]. now rewrite /transform /=. Qed. diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v index 3da0fa38e..91b749cec 100644 --- a/erasure-plugin/theories/Erasure.v +++ b/erasure-plugin/theories/Erasure.v @@ -21,7 +21,7 @@ Local Open Scope string_scope2. shrinking of the global environment dependencies + the optimization that removes all pattern-matches on propositions. *) -Import Transform. +Import Common.Transform.Transform. #[local] Existing Instance extraction_checker_flags. #[local] Existing Instance PCUICSN.extraction_normalizing. @@ -45,10 +45,10 @@ Axiom assume_preservation_template_program_env_expansion : Program Definition eta_expand K : Transform.t _ _ Ast.term Ast.term _ _ eval_template_program_env eval_template_program := {| name := "eta expand cstrs and fixpoints"; - pre := fun p => ∥ wt_template_program_env p ∥ /\ K (eta_expand_global_env p.1) ; - transform p _ := EtaExpand.eta_expand_program p ; - post := fun p => ∥ wt_template_program p ∥ /\ EtaExpand.expanded_program p /\ K p.1; - obseq p hp p' v v' := v' = EtaExpand.eta_expand p.1 [] v |}. + pre := fun p => ∥ wt_template_program_env p ∥ /\ K (eta_expand_global_env p.1) ; + transform p _ := EtaExpand.eta_expand_program p ; + post := fun p => ∥ wt_template_program p ∥ /\ EtaExpand.expanded_program p /\ K p.1; + obseq p hp p' v v' := v' = EtaExpand.eta_expand p.1 [] v |}. Next Obligation. let p := match goal with H : program _ _ |- _ => H end in destruct p. split; [|split]; auto; now apply assume_welltyped_template_program_expansion. @@ -65,19 +65,19 @@ Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl} (ef (* Simulation of the guarded fixpoint rules with a single unguarded one: the only "stuck" fixpoints remaining are unapplied. This translation is a noop on terms and environments. *) - guarded_to_unguarded_fix (fl := default_wcbv_flags) (wcon := eq_refl) eq_refl ▷ + guarded_to_unguarded_fix (fl := {| with_prop_case := true; with_guarded_fix := true; with_constructor_as_block := false |}) (wcon := eq_refl) eq_refl ▷ (* Remove all constructor parameters *) remove_params_optimization (wcon := eq_refl) ▷ (* Rebuild the efficient lookup table *) - rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true ▷ + rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true false ▷ (* Remove all cases / projections on propositional content *) remove_match_on_box_trans (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ (* Rebuild the efficient lookup table *) - rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true ▷ + rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true false ▷ (* Inline projections to cases *) inline_projections_optimization (fl := EWcbvEval.target_wcbv_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ (* Rebuild the efficient lookup table *) - rebuild_wf_env_transform (efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) true ▷ + rebuild_wf_env_transform (efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) true false ▷ (* First-order constructor representation *) constructors_as_blocks_transformation (efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) @@ -131,14 +131,14 @@ Proof. Qed. Lemma verified_lambdabox_pipeline_extends {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : - TransformExt.t verified_lambdabox_pipeline (fun p p' => extends (EEnvMap.GlobalContextMap.global_decls p.1) + TransformExt.t (verified_lambdabox_pipeline) (fun p p' => extends (EEnvMap.GlobalContextMap.global_decls p.1) (EEnvMap.GlobalContextMap.global_decls p'.1)) (fun p p' => extends p.1 p'.1). Proof. unfold verified_lambdabox_pipeline. tc. Qed. Lemma verified_lambdabox_pipeline_extends' {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : - TransformExt.t verified_lambdabox_pipeline extends_eprogram_env extends_eprogram. + TransformExt.t (verified_lambdabox_pipeline) extends_eprogram_env extends_eprogram. Proof. unfold verified_lambdabox_pipeline. tc. Qed. @@ -163,8 +163,8 @@ Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EW eta_expand (K _ T3) ▷ (* Casts are removed, application is binary, case annotations are inferred from the global environment *) template_to_pcuic_transform (K _ T2). + Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : -Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ Ast.term EAst.term _ _ TemplateProgram.eval_template_program @@ -172,6 +172,81 @@ Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellf pre_erasure_pipeline ▷ verified_erasure_pipeline. + +Program Definition verified_lambdabox_typed_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : + Transform.t _ _ EAst.term EAst.term _ _ + (EProgram.eval_eprogram_env {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |}) + (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := + (* Simulation of the guarded fixpoint rules with a single unguarded one: + the only "stuck" fixpoints remaining are unapplied. + This translation is a noop on terms and environments. *) + guarded_to_unguarded_fix (fl := {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |}) (wcon := eq_refl) eq_refl ▷ + (* Remove all constructor parameters *) + remove_params_optimization (wcon := eq_refl) ▷ + (* Rebuild the efficient lookup table *) + rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true false ▷ + (* Inline projections to cases *) + inline_projections_optimization (fl := EWcbvEval.target_wcbv_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ + (* Rebuild the efficient lookup table *) + rebuild_wf_env_transform (efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) true false ▷ + (* First-order constructor representation *) + constructors_as_blocks_transformation + (efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) + (has_app := eq_refl) (has_pars := eq_refl) (has_rel := eq_refl) (hasbox := eq_refl) (has_cstrblocks := eq_refl). + + (* At the end of erasure we get a well-formed program (well-scoped globally and localy), without + parameters in inductive declarations. The constructor applications are also transformed to a first-order + "block" application, of the right length, and the evaluation relation does not need to consider guarded + fixpoints or case analyses on propositional content. All fixpoint bodies start with a lambda as well. + Finally, projections are inlined to cases, so no `tProj` remains. *) + + Import EGlobalEnv EWellformed. + + Next Obligation. + destruct H. split => //. sq. + now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs. + Qed. + +Local Obligation Tactic := intros; eauto. + +Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : + Transform.t _ _ + PCUICAst.term EAst.term _ _ + PCUICTransform.eval_pcuic_program + (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := + (* a bunch of nonsense for normalization preconditions *) + let K ty (T : ty -> _) p + := let p := T p in + (PCUICTyping.wf_ext p -> PCUICSN.NormalizationIn p) /\ + (PCUICTyping.wf_ext p -> PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn p) in + let T1 (p:global_env_ext_map) := p in + (* Branches of cases are expanded to bind only variables, constructor types are expanded accordingly *) + pcuic_expand_lets_transform (K _ T1) ▷ + (* Erasure of proofs terms in Prop and types *) + typed_erase_transform ▷ + (* Remove match on box early for dearging *) + remove_match_on_box_typed_transform (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ + (* Check if the preconditions for dearging are valid, otherwise dearging will be the identity *) + dearging_checks_transform (hastrel := eq_refl) (hastbox := eq_refl) ▷ + dearging_transform (hastrel := eq_refl) (hastbox := eq_refl) ▷ + rebuild_wf_env_transform true true ▷ + verified_lambdabox_typed_pipeline. + + Next Obligation. + cbn in H. split; cbn; intuition eauto. + Qed. + Next Obligation. + cbn in H |- *; intuition eauto. + Qed. + +Program Definition typed_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : + Transform.t _ _ + Ast.term EAst.term _ _ + TemplateProgram.eval_template_program + (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := + pre_erasure_pipeline ▷ + verified_typed_erasure_pipeline. + (* At the end of erasure we get a well-formed program (well-scoped globally and localy), without parameters in inductive declarations. The constructor applications are also transformed to a first-order "block" application, of the right length, and the evaluation relation does not need to consider guarded @@ -199,16 +274,34 @@ Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := E erase_transform ▷ guarded_to_unguarded_fix (wcon := eq_refl) eq_refl ▷ remove_params_fast_optimization (wcon := eq_refl) ▷ - rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true ▷ + rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true false ▷ remove_match_on_box_trans (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ - rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true ▷ + rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true false ▷ inline_projections_optimization (fl := EWcbvEval.target_wcbv_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ let efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags) in - rebuild_wf_env_transform (efl := efl) true ▷ + rebuild_wf_env_transform (efl := efl) true false ▷ constructors_as_blocks_transformation (efl := efl) (has_app := eq_refl) (has_pars := eq_refl) (has_rel := eq_refl) (hasbox := eq_refl) (has_cstrblocks := eq_refl). Next Obligation. destruct H; split => //. now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs. Qed. +Next Obligation. + cbn in H. split; cbn; intuition eauto. +Qed. +Next Obligation. + cbn in H. split; cbn; intuition eauto. +Qed. +Next Obligation. + cbn in H. split; cbn; intuition eauto. +Qed. +Next Obligation. + cbn in H. split; cbn; intuition eauto. +Qed. +Next Obligation. + cbn in H. split; cbn; intuition eauto. +Qed. +Next Obligation. + cbn in H. split; cbn; intuition eauto. +Qed. Definition run_erase_program_fast {guard : abstract_guard_impl} := run erasure_pipeline_fast. @@ -262,3 +355,16 @@ Next Obligation. pose proof @PCUICSN.normalization. split; typeclasses eauto. Qed. + +Program Definition typed_erase_and_print_template_program (p : Ast.Env.program) + : string := + let p' := run typed_erasure_pipeline p _ in + time "Pretty printing" EPretty.print_program p'. +Next Obligation. + split. + now eapply assume_that_we_only_erase_on_welltyped_programs. + cbv [PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn]. + pose proof @PCUICSN.normalization. + split; typeclasses eauto. +Qed. + diff --git a/erasure-plugin/theories/ErasureCorrectness.v b/erasure-plugin/theories/ErasureCorrectness.v index b32f2b6a9..9d2f538a6 100644 --- a/erasure-plugin/theories/ErasureCorrectness.v +++ b/erasure-plugin/theories/ErasureCorrectness.v @@ -16,7 +16,7 @@ Import PCUICTransform (template_to_pcuic_transform, pcuic_expand_lets_transform) shrinking of the global environment dependencies + the optimization that removes all pattern-matches on propositions. *) -Import Transform. +Import Common.Transform.Transform. #[local] Obligation Tactic := program_simpl. @@ -671,7 +671,7 @@ Section PCUICenv. rewrite /EGlobalEnv.lookup_constructor /EGlobalEnv.lookup_inductive /EGlobalEnv.lookup_minductive. destruct EGlobalEnv.lookup_env eqn:e => //=. destruct g => //. - eapply he in declm; tea. subst m. + eapply he in declm; tea. subst m. cbn. rewrite nth_error_map decli /=. rewrite nth_error_map declc /=. intuition congruence. Qed. @@ -684,7 +684,7 @@ Proof. rewrite /EGlobalEnv.lookup_constructor_pars_args /EGlobalEnv.lookup_inductive_pars. rewrite /EGlobalEnv.lookup_constructor /EGlobalEnv.lookup_inductive. destruct EGlobalEnv.lookup_minductive => //=. - destruct nth_error => //. destruct nth_error => //. congruence. + destruct nth_error => //=. destruct nth_error => //=. congruence. Qed. Lemma compile_evalue_erase (Σ : PCUICAst.PCUICEnvironment.global_env_ext) (Σ' : EEnvMap.GlobalContextMap.t) v : @@ -752,9 +752,9 @@ Qed. Definition fo_evalue (p : program E.global_context EAst.term) : Prop := firstorder_evalue p.1 p.2. Definition fo_evalue_map (p : program EEnvMap.GlobalContextMap.t EAst.term) : Prop := firstorder_evalue p.1 p.2. -#[global] Instance rebuild_wf_env_transform_pres_fo {fl : WcbvFlags} {efl : EEnvFlags} we : +#[global] Instance rebuild_wf_env_transform_pres_fo {fl : WcbvFlags} {efl : EEnvFlags} we wf : ETransformPresFO.t - (rebuild_wf_env_transform we) fo_evalue fo_evalue_map (fun p pr fo => rebuild_wf_env p pr.p1). + (rebuild_wf_env_transform we wf) fo_evalue fo_evalue_map (fun p pr fo => rebuild_wf_env p pr.p1). Proof. split => //. Qed. Definition is_eta_app (p : program E.global_context EAst.term) : Prop := EEtaExpanded.isEtaExp p.1 p.2. @@ -763,9 +763,9 @@ Definition is_eta_app_map (p : program EEnvMap.GlobalContextMap.t EAst.term) : P Definition is_eta_fix_app (p : program E.global_context EAst.term) : Prop := EEtaExpandedFix.isEtaExp p.1 [] p.2. Definition is_eta_fix_app_map (p : program EEnvMap.GlobalContextMap.t EAst.term) : Prop := EEtaExpandedFix.isEtaExp p.1 [] p.2. -#[global] Instance rebuild_wf_env_transform_pres_app {fl : WcbvFlags} {efl : EEnvFlags} we : +#[global] Instance rebuild_wf_env_transform_pres_app {fl : WcbvFlags} {efl : EEnvFlags} we : ETransformPresApp.t - (rebuild_wf_env_transform we) is_eta_app is_eta_app_map. + (rebuild_wf_env_transform we false) is_eta_app is_eta_app_map. Proof. split => //. - intros. unfold transform, rebuild_wf_env_transform. f_equal. apply proof_irrelevance. @@ -774,10 +774,10 @@ Proof. split => //. - intros. unshelve eexists. { destruct pr as [[? ?] ?]; split; [split|]; cbn in * => //. now move/andP: H0 => [] /andP[]. - destruct we => //=. move/andP: H1 => [] ? ?. apply /andP. split => //. } + destruct we => //=. intros. specialize (H1 H2). move/andP: H1 => [] ? ?. apply /andP. split => //. } unshelve eexists. { destruct pr as [[? ?] ?]; split; [split|]; cbn in * => //. now move/andP: H0 => [] /andP[]. - destruct we => //=. move/andP: H1 => [] ?. cbn. move/EEtaExpanded.isEtaExp_tApp_arg => etau. + destruct we => //=. intros h; specialize (H1 h). move/andP: H1 => [] ?. cbn. move/EEtaExpanded.isEtaExp_tApp_arg => etau. apply /andP. split => //. } cbn. reflexivity. Qed. diff --git a/erasure/theories/Typed/CertifyingEta.v b/erasure/theories/Typed/CertifyingEta.v index 2b99f0690..3f3fb0a82 100644 --- a/erasure/theories/Typed/CertifyingEta.v +++ b/erasure/theories/Typed/CertifyingEta.v @@ -169,6 +169,18 @@ Definition restrict_env (Σ : global_declarations) (kns : list kername) : global Import PCUICWfEnv PCUICWfEnvImpl. +Lemma eq_eta_global_env (cf := config.extraction_checker_flags) Σ' Σ : + abstract_env_rel (abstract_env_impl := (@optimized_abstract_env_impl config.extraction_checker_flags fake_guard_impl_instance).π1) (build_wf_env_from_env (cf := config.extraction_checker_flags) Σ' (assume_env_wellformed Σ')) Σ -> + Σ = + {| + PEnv.universes := PEnv.universes Σ'; + PEnv.declarations := PEnv.declarations Σ'; + PEnv.retroknowledge := PEnv.retroknowledge Σ' + |}. +Proof. + cbn. intros ->. now destruct Σ'. +Qed. + Definition eta_global_env (overridden_masks : kername -> option bitmask) (trim_consts trim_inds : bool) @@ -180,7 +192,7 @@ Definition eta_global_env erase_global_decls_deps_recursive (X_type := optimized_abstract_env_impl (guard := fake_guard_impl_instance)) (X := build_wf_env_from_env Σp (assume_env_wellformed _)) - (PEnv.declarations Σp) (PEnv.universes Σp) (PEnv.retroknowledge Σp) (todo "eq") + (PEnv.declarations Σp) (PEnv.universes Σp) (PEnv.retroknowledge Σp) (eq_eta_global_env _) seeds erasure_ignore in let (const_masks, ind_masks) := analyze_env overridden_masks Σe in let const_masks := (if trim_consts then trim_const_masks else id) const_masks in diff --git a/erasure/theories/Typed/ExtractionCorrectness.v b/erasure/theories/Typed/ExtractionCorrectness.v index 21eb95b05..99c279643 100644 --- a/erasure/theories/Typed/ExtractionCorrectness.v +++ b/erasure/theories/Typed/ExtractionCorrectness.v @@ -473,14 +473,22 @@ Definition compute_masks overridden_masks do_trim_const_masks do_trim_ctor_masks "Analysis produced masks that ask to remove live arguments"%bs ;; Ok (Build_dearg_set const_masks ind_masks). -Definition dearg_env masks Σ := - debox_env_types (dearg_env masks.(ind_masks) masks.(const_masks) Σ). +Import PCUICWfEnvImpl PCUICAst.PCUICEnvironment. -Import PCUICWfEnvImpl. +Program Definition make_env {Σ} (wfΣ : ∥wf_ext Σ∥) := + @abstract_make_wf_env_ext _ (optimized_abstract_env_impl (guard := Erasure.fake_guard_impl_instance)) (PCUICWfEnvImpl.build_wf_env_from_env Σ (map_squash fst wfΣ)) Σ.2 _. -Program Definition dearg_term {Σ} (wfΣ : ∥wf_ext Σ∥) (masks : dearg_set) (t : PCUICAst.term) (w : welltyped Σ [] t) : term := - let wfext := @abstract_make_wf_env_ext _ (optimized_abstract_env_impl (guard := Erasure.fake_guard_impl_instance)) (PCUICWfEnvImpl.build_wf_env_from_env Σ (map_squash fst wfΣ)) Σ.2 _ in - dearg masks.(ind_masks) masks.(const_masks) (erase _ wfext (normalization_in := _) [] t _). +Program Definition erase_env {Σ} wfΣ seeds ignore := + Erasure.erase_global_decls_deps_recursive (X_type := PCUICWfEnvImpl.optimized_abstract_env_impl (guard := Erasure.fake_guard_impl_instance)) + (X := PCUICWfEnvImpl.build_wf_env_from_env Σ wfΣ) + (declarations Σ) (universes Σ) (retroknowledge Σ) _ seeds ignore. + Next Obligation. + destruct Σ => //. + Qed. + +Program Definition erase_term {Σ} (wfΣ : ∥wf_ext Σ∥) (t : PCUICAst.term) (w : welltyped Σ [] t) : term := + let wfext := make_env wfΣ in + (erase _ wfext (normalization_in := _) [] t _). Next Obligation. refine (let 'sq wfΣ := wfΣ in let nin := Erasure.fake_normalization Σ wfΣ in _). eapply nin. destruct Σ. apply H. @@ -490,77 +498,111 @@ Program Definition dearg_term {Σ} (wfΣ : ∥wf_ext Σ∥) (masks : dearg_set) destruct Σ. apply w. Qed. +Lemma remove_match_on_box_env_lemma {Σ} (wfΣ : ∥ wf Σ ∥) seeds ignore : + fresh_globals (erase_env wfΣ seeds ignore). +Proof. + destruct wfΣ. + unfold erase_env. + now eapply fresh_globals_erase_global_decl_rec, wf_fresh_globals. +Qed. + +Lemma remove_match_on_box_trans_env {Σ} (wfΣ : ∥ wf Σ ∥) seeds ignore : + EnvMap.fresh_globals (trans_env (erase_env wfΣ seeds ignore)). +Proof. + destruct wfΣ. + unfold erase_env. + eapply OptimizePropDiscr.remove_match_on_box_env_obligation_1. + now eapply fresh_globals_erase_global_decl_rec, wf_fresh_globals. +Qed. + +Import EWellformed. Theorem extract_correct_gen (H := EWellformed.all_env_flags) - (wfl := opt_wcbv_flags) + (wfl := default_wcbv_flags) (Σ : P.global_env_ext) (wfΣ : ∥wf_ext Σ∥) - t v ignored exΣ masks : + t v ignored masks : axiom_free Σ -> forall wt : welltyped Σ [] t, - forall wv : welltyped Σ [] v, Σ p⊢ t ⇓ v -> (isErasable Σ [] t -> False) -> (forall k, ignored k = false) -> - let t' := dearg_term wfΣ masks t wt in - extract_pcuic_env - (pcuic_args extract_within_coq) - Σ (wf_squash wfΣ) (EAstUtils.term_global_deps t') ignored = Ok exΣ -> - compute_masks (fun _ => None) true true exΣ = Ok masks -> - ∥trans_env exΣ e⊢ t' ⇓ dearg_term wfΣ masks v wv ∥. + let t' := erase_term wfΣ t wt in + let deps := (EAstUtils.term_global_deps t') in + let erΣ := erase_env (map_squash fst wfΣ) deps ignored in + let gerΣ := EEnvMap.GlobalContextMap.make (trans_env erΣ) + (trans_env_fresh_globals erΣ (remove_match_on_box_env_lemma (map_squash fst wfΣ) deps ignored)) in + let erΣ := remove_match_on_box_env erΣ (remove_match_on_box_env_lemma _ deps ignored) in + compute_masks (fun _ => None) true true erΣ = Ok masks -> + let t'' := EOptimizePropDiscr.remove_match_on_box gerΣ t' in + valid_cases (ind_masks masks) t'' -> + is_expanded (ind_masks masks) (const_masks masks) t'' -> + exists v', Σ;;; [] |- v ⇝ℇ v' /\ + ∥ EWcbvEval.eval (wfl := opt_wcbv_flags) (trans_env (dearg_env masks erΣ)) (dearg_term masks t'') (dearg_term masks (EOptimizePropDiscr.remove_match_on_box gerΣ v')) ∥. Proof. - intros ax [T wt] wv ev not_erasable no_ignores ex. + intros ax [T wt] ev not_erasable no_ignores t' deps er ger er' hmas t'' vcs isexp. cbn -[dearg_transform] in *. - destruct dearg_transform eqn:dt; cbn -[dearg_transform] in *; [|congruence]. - intros [=->]. destruct wfΣ. - unfold dearg_term. - set (e := abstract_make_wf_env_ext _ _ _). + unfold erase_term, make_env in t'. + set (e := abstract_make_wf_env_ext _ _ _) in *. pose proof (abstract_env_ext_exists e) as [[Σe he]]. - unfold dearg_term in ex. match goal with [H := context [ @erase ?X_type ?X ?nin ?Γ t ?wt ] |- _ ] => pose proof (@erases_erase X_type X nin Γ t wt _ he) end. cbn in he. subst Σe. destruct Σ as [Σ univs]; cbn [fst snd] in *. - eapply erases_correct with - (Σ' := trans_env (Erasure.erase_global_decls_deps_recursive (PCUICAst.PCUICEnvironment.declarations Σ) - (PCUICAst.PCUICEnvironment.universes Σ) _ _ - _ ignored)) in ev as (erv&erase_to&[erev]);eauto. + assert (wv : welltyped (Σ, univs) [] v). + { eexists. eapply PCUICClassification.subject_reduction_eval; tea. } + eapply erases_correct with (Σ' := trans_env er) in ev as (erv&erase_to&[erev]);eauto. 2:{ now eexists. } - intros Σex. - * move: dt. unfold dearg_transform. eapply dearg_correct. - 2:{ unshelve eapply (erases_erase (X_type := (optimized_abstract_env_impl (guard := Erasure.fake_guard_impl_instance)))). exact e. 3:now destruct Σ. - * intros. pose proof (abstract_env_ext_irr _ he H0). subst Σ0. now apply Erasure.fake_normalization. - * intros Σ0 he'; pose proof (abstract_env_ext_irr _ he he'); subst Σ0. cbn in he, he'. subst Σe. now destruct Σ. } - 3:{ intros hm. - - eapply dearg_correct. - + depelim erase_to;[|easy]. - constructor. - eapply dearg_transform_correct; eauto. - clear dt. - eapply (@optimize_correct _ _ _ (tConst kn) (tConstruct ind c []));eauto. - * remember (Erasure.erase_global_decls_deps_recursive _ _ _ _ _ _) as eΣ. - assert (EWellformed.wf_glob (trans_env eΣ)). - { subst eΣ. now eapply wf_erase_global_decls_recursive. } + * exists erv. split => //. + sq. + eapply dearg_transform_gen_correct; eauto. + + assert (EWellformed.wf_glob (trans_env er')). + { subst er'. rewrite trans_env_remove_match_on_box_env. + eapply EOptimizePropDiscr.remove_match_on_box_env_wf => //. + now eapply wf_erase_global_decls_recursive. } now apply EWellformed.wellformed_closed_env. - * eapply wf_erase_global_decls_recursive; auto. - + now eexists. - + eapply inversion_Const in wt as (?&?&?&?&?); auto. - clear dt. - eapply global_erased_with_deps_erases_deps_tConst; eauto. - destruct Σ as [Σ0 univ_decls]. - destruct Σ0 as [univs Σ1]. - apply wf_ext_wf in w as w1. cbn. - eapply erase_global_decls_deps_recursive_correct;eauto. - * unfold PCUICAst.declared_constant in *. - cbn. - intros ? ->%KernameSet.singleton_spec;cbn in *. - intros eq. set (env := {| PEnv.declarations := Σ1 |}) in *. - eapply (lookup_global_In_wf _ env) in d; eauto. - * now apply KernameSet.singleton_spec. - Unshelve. eapply fresh_globals_erase_global_decl_rec. - now eapply PCUICWfEnvImpl.wf_fresh_globals. + + subst t''. + eapply EOptimizePropDiscr.closed_remove_match_on_box. + eapply EWellformed.wellformed_closed. + unshelve eapply (erase_wellformed_weaken (declarations Σ) _ _ _ (Γ:=[])). + 2:{ cbn; congruence. } 2:exact deps. intros. + now eapply Erasure.fake_normalization. + + subst t'' t'. + rewrite trans_env_remove_match_on_box_env. + unshelve eapply (EOptimizePropDiscr.remove_match_on_box_correct (fl := default_wcbv_flags)) => //=. + { reflexivity. } + { cbn. now eapply wf_erase_global_decls_recursive. } + { simpl. eapply EWellformed.wellformed_closed_env. + now eapply wf_erase_global_decls_recursive. } + eapply wellformed_closed. + unshelve eapply (erase_wellformed_weaken (declarations Σ) _ _ _ (Γ := [])). + 2:{ cbn; congruence. } 2:exact deps. intros. eapply Erasure.fake_normalization; eauto. + * eapply erase_global_erases_deps; tea. + subst er. unfold erase_env. + set (obl := fun Σ' => _). + destruct Σ; cbn [declarations retroknowledge universes] in *. + eapply (erase_global_decls_deps_recursive_correct _ _ _ obl); eauto. + intros k hin. + eapply term_global_deps_spec in hin; tea. red in hin. destruct hin as [[decl eq]]. + cbn in eq. cbn. now rewrite eq. cbn. eapply w. +Qed. + +Theorem extract_correct_gen' + (H := EWellformed.all_env_flags) + (wfl := opt_wcbv_flags) + (Σ : ExAst.global_env) t v masks : + EGlobalEnv.closed_env (trans_env Σ) -> + ELiftSubst.closedn 0 t -> + trans_env Σ e⊢ t ⇓ v -> + compute_masks (fun _ => None) true true Σ = Ok masks -> + valid_cases (ind_masks masks) t -> + is_expanded (ind_masks masks) (const_masks masks) t -> + ∥ EWcbvEval.eval (trans_env (dearg_env masks Σ)) (dearg_term masks t) (dearg_term masks v) ∥. +Proof. + intros cle clt ev hmas vcs isexp. + sq. + eapply dearg_transform_gen_correct; eauto. Qed. (* Print Assumptions extract_correct. *) diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v index b3f89a2fb..fd4d37a63 100644 --- a/test-suite/erasure_live_test.v +++ b/test-suite/erasure_live_test.v @@ -20,6 +20,9 @@ Unset MetaCoq Debug. Definition test (p : Ast.Env.program) : string := erase_and_print_template_program p. +Definition testty (p : Ast.Env.program) : string := + typed_erase_and_print_template_program p. + Definition test_fast (p : Ast.Env.program) : string := erase_fast_and_print_template_program p. @@ -33,6 +36,8 @@ Definition exprooftest := Eval lazy in test exproof. MetaCoq Quote Recursively Definition exintro := (@exist _ _ 0 (@eq_refl _ 0) : {x : nat | x = 0}). Definition exintrotest := Eval lazy in test exintro. +Definition ex_type_introtest := Eval lazy in testty exintro. + Definition idnat := ((fun (X : Set) (x : X) => x) nat). MetaCoq Quote Recursively Definition idnatc := idnat. @@ -136,7 +141,7 @@ MetaCoq Quote Recursively Definition p_arden_size := arden_size. Definition P_arden_size := Eval lazy in test p_arden_size. (** SASL tautology function: variable arity **) -Require Import Bool. +From Coq Require Import Bool. Fixpoint tautArg (n:nat) : Type := match n with | 0 => bool @@ -345,6 +350,7 @@ Time Definition P_provedCopyx := Eval lazy in (test_fast cbv_provedCopyx). From MetaCoq.ErasurePlugin Require Import Loader. MetaCoq Erase provedCopyx. +MetaCoq Typed Erase provedCopyx. (* 0.2s purely in the bytecode VM *) (*Time Definition P_provedCopyxvm' := Eval vm_compute in (test p_provedCopyx). *) (* Goal From ea4ab2dd43e2bd2f985dcd200e04a76b0ba541d4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 12 Dec 2023 17:47:46 +0100 Subject: [PATCH 6/7] Prove that dearging preserves eta-expanded constructors and fixpoints (tricky!) --- erasure-plugin/theories/ETransform.v | 155 ++-- erasure-plugin/theories/Erasure.v | 3 +- erasure/theories/EEtaExpandedFix.v | 9 +- erasure/theories/EOptimizePropDiscr.v | 101 +++ erasure/theories/ErasureFunctionProperties.v | 2 +- erasure/theories/Typed/ErasureCorrectness.v | 31 +- erasure/theories/Typed/ExAst.v | 4 +- .../theories/Typed/ExtractionCorrectness.v | 121 +++ erasure/theories/Typed/Optimize.v | 22 +- erasure/theories/Typed/OptimizeCorrectness.v | 747 +++++++++++++++++- erasure/theories/Typed/OptimizePropDiscr.v | 4 +- 11 files changed, 1085 insertions(+), 114 deletions(-) diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v index fd18daaa9..a9247e437 100644 --- a/erasure-plugin/theories/ETransform.v +++ b/erasure-plugin/theories/ETransform.v @@ -341,7 +341,11 @@ Next Obligation. end. red. cbn. intros; subst; intuition eauto. destruct wtp. eapply wf_fresh_globals, w. - - todo "expanded". + - move: e. rewrite /erase_program_typed. + intros [= <- <-]. unfold trans_ex_prog; cbn -[trans_env]. + red. split; cbn -[trans_env]. + eapply expanded_erase_global_decls_recursive; eauto. eapply etap. + eapply expanded_erase => //; eauto. eapply etap. Qed. Next Obligation. @@ -394,10 +398,23 @@ Definition map_of_typed_global_env (p : global_env) (fr : fresh_globals p) := Definition pre_remove_match_on_box_typed efl (p : global_env * term) : Prop := wf_eprogram efl (trans_ex_prog p) /\ EEtaExpandedFix.expanded_eprogram (trans_ex_prog p). +Lemma fresh_global_trans kn g : EnvMap.EnvMap.fresh_global kn (trans_env g) -> fresh_global kn g. +Proof. + induction g as [ | [[kn' b] d] tl]; cbn; auto; constructor; eauto. + - now depelim H. + - depelim H. eapply Forall_map_inv in H0. ELiftSubst.solve_all. +Qed. + Lemma pre_remove_match_on_box_typed_fresh efl p : pre_remove_match_on_box_typed efl p -> fresh_globals p.1. Proof. intros []. destruct H. eapply wf_glob_fresh in H. -Admitted. + revert H. clear. + destruct p; cbn. clear. + intros h; depind h. + - destruct g; noconf H. constructor. + - destruct g0; noconf H0. destruct p as [[kn' b] d']. noconf H0. + constructor; eauto. now eapply fresh_global_trans. +Qed. Lemma map_trans_env Σ m : map (on_snd (EOptimizePropDiscr.remove_match_on_box_decl m)) (trans_env Σ) = trans_env (map (on_snd (OptimizePropDiscr.remove_match_on_box_decl m)) Σ). Proof. @@ -437,8 +454,13 @@ Next Obligation. assert (obl = obl') by apply proof_irrelevance. clearbody obl obl'; subst obl'. eapply remove_match_on_box_wellformed_irrel. cbn. eapply wfp. eapply remove_match_on_box_wellformed => //=. apply wfp. apply wfp. - - todo "excpanded". (* eapply remove_match_on_box_program_expanded.*) + - rewrite /trans_ex_prog /= /remove_match_on_box_typed_env. cbn. + rewrite -map_trans_env. unfold trans_ex_prog in *. cbn -[trans_env] in *. + set (e' := map_of_typed_global_env _ _). + eapply (remove_match_on_box_program_expanded_fix (e', t) wfp). + unfold e'. unfold map_of_typed_global_env. red. cbn. eapply etap. Qed. + Next Obligation. red. move=> fl wcon efl hastrel hastbox [Σ t] /= v [wfe wft] [ev]. cbn -[trans_env] in ev. @@ -461,6 +483,25 @@ Definition check_dearging_precond Σ t := end else None. +Lemma check_dearging_precond_spec env t d : + check_dearging_precond env t = Some d -> + closed_env (trans_env env) /\ + valid_masks_env (ind_masks d) (const_masks d) env /\ + is_expanded_env (ind_masks d) (const_masks d) env /\ + valid_cases (ind_masks d) t + /\ is_expanded (ind_masks d) (const_masks d) t. +Proof. + unfold check_dearging_precond. + destruct closed_env => //. + unfold ExtractionCorrectness.compute_masks, Utils.timed. + destruct analyze_env eqn:eqm => //. + destruct is_expanded_env eqn:isex => //. + destruct valid_masks_env eqn:vm => //=. + destruct valid_cases eqn:vc => //=. + destruct is_expanded eqn:ise => //=. + intros [= <-]; cbn; intuition. +Qed. + Definition check_dearging_trans p := ((check_dearging_precond p.1 p.2, p.1), p.2). @@ -485,57 +526,69 @@ Next Obligation. cbn. intros. red. cbn. intros. exists v; split => //. Qed. -Definition dearg (p : (option dearg_set × global_env) * term) : global_context * term := - match p.1.1 with - | Some masks => (trans_env (dearg_env masks p.1.2), dearg_term masks p.2) - | None => (trans_env p.1.2, p.2) - end. +Section Dearging. + Import Optimize OptimizeCorrectness. -Program Definition dearging_transform {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} : - Transform.t _ _ EAst.term EAst.term _ _ (eval_typed_eprogram_masks opt_wcbv_flags) (eval_eprogram opt_wcbv_flags) := - {| name := "dearging"; - transform p _ := dearg p ; - pre p := post_dearging_checks efl p; - post p := wf_eprogram efl p /\ EEtaExpandedFix.expanded_eprogram p ; - obseq p hp p' v v' := v' = (dearg (p.1, v)).2 |}. + Definition dearg (p : (option dearg_set × global_env) * term) : global_context * term := + match p.1.1 with + | Some masks => (trans_env (dearg_env masks p.1.2), dearg_term masks p.2) + | None => (trans_env p.1.2, p.2) + end. -Next Obligation. -Proof. - cbn. intros. - unfold dearg. - destruct p. rewrite H. - destruct check_dearging_precond eqn:eqp; cbn => //. - split. - - split; cbn. clear H. unfold dearg_env. - all:todo "wf". - - todo "expanded". -Qed. + Program Definition dearging_transform (efl := all_env_flags) {hastrel : has_tRel} {hastbox : has_tBox} : + Transform.t _ _ EAst.term EAst.term _ _ (eval_typed_eprogram_masks opt_wcbv_flags) (eval_eprogram opt_wcbv_flags) := + {| name := "dearging"; + transform p _ := dearg p ; + pre p := post_dearging_checks efl p; + post p := wf_eprogram efl p /\ EEtaExpandedFix.expanded_eprogram p ; + obseq p hp p' v v' := v' = (dearg (p.1, v)).2 |}. -Next Obligation. - cbn. intros. red. - intros p v [he [wfe exp]]. unfold eval_typed_eprogram_masks. - intros [ev]. - unfold dearg. rewrite he. - destruct (check_dearging_precond) as [masks|] eqn:cpre. - * eapply (extract_correct_gen' _ _ _ masks) in ev as ev'. destruct ev' as [ev']. - eexists. split. red. sq. cbn. exact ev'. auto. - - destruct wfe. now eapply wellformed_closed_env. - - destruct wfe. now eapply wellformed_closed. - - move: cpre. unfold check_dearging_precond. destruct closed_env => //. - destruct ExtractionCorrectness.compute_masks => //. - destruct (_ && _) => //. congruence. - - move: cpre. rewrite /check_dearging_precond. - destruct closed_env => //. - destruct ExtractionCorrectness.compute_masks => //. - destruct valid_cases eqn:vc => //. cbn. - destruct is_expanded => //. now intros [= ->]. - - move: cpre. rewrite /check_dearging_precond. - destruct closed_env => //. - destruct ExtractionCorrectness.compute_masks => //. - destruct valid_cases eqn:vc => //. cbn. - destruct is_expanded eqn:ise => //. now intros [= ->]. - * exists v. cbn. split => //. -Qed. + Next Obligation. + Proof. + cbn. intros. + unfold dearg. + destruct p. rewrite H. + destruct check_dearging_precond eqn:eqp; cbn => //. + destruct input as [[masks env] t]. cbn -[trans_env Optimize.dearg_env] in *. + subst masks. destruct H0 as [wf exp]. + eapply check_dearging_precond_spec in eqp. intuition. + - split; cbn. + unfold dearg_env. + eapply wf_glob_debox. + eapply wf_glob_dearg; eauto. + eapply wf. + rewrite /dearg_env. rewrite -trans_env_debox. + eapply wellformed_dearg; eauto. + eapply wf. + - rewrite /dearg_env -trans_env_debox. split; cbn. + todo "expanded". + Qed. + + Next Obligation. + cbn. intros. red. + intros p v [he [wfe exp]]. unfold eval_typed_eprogram_masks. + intros [ev]. + unfold dearg. rewrite he. + destruct (check_dearging_precond) as [masks|] eqn:cpre. + * eapply (extract_correct_gen' _ _ _ masks) in ev as ev'. destruct ev' as [ev']. + eexists. split. red. sq. cbn. exact ev'. auto. + - destruct wfe. now eapply wellformed_closed_env. + - destruct wfe. now eapply wellformed_closed. + - move: cpre. unfold check_dearging_precond. destruct closed_env => //. + destruct ExtractionCorrectness.compute_masks => //. + destruct (_ && _) => //. congruence. + - move: cpre. rewrite /check_dearging_precond. + destruct closed_env => //. + destruct ExtractionCorrectness.compute_masks => //. + destruct valid_cases eqn:vc => //. cbn. + destruct is_expanded => //. now intros [= ->]. + - move: cpre. rewrite /check_dearging_precond. + destruct closed_env => //. + destruct ExtractionCorrectness.compute_masks => //. + destruct valid_cases eqn:vc => //. cbn. + destruct is_expanded eqn:ise => //. now intros [= ->]. + * exists v. cbn. split => //. + Qed. Definition extends_eprogram (p p' : eprogram) := extends p.1 p'.1 /\ p.2 = p'.2. diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v index 91b749cec..6c7387167 100644 --- a/erasure-plugin/theories/Erasure.v +++ b/erasure-plugin/theories/Erasure.v @@ -163,9 +163,8 @@ Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EW eta_expand (K _ T3) ▷ (* Casts are removed, application is binary, case annotations are inferred from the global environment *) template_to_pcuic_transform (K _ T2). - Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : - Transform.t _ _ +Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ Ast.term EAst.term _ _ TemplateProgram.eval_template_program (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) := diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v index e72727ef2..f3ed54f6c 100644 --- a/erasure/theories/EEtaExpandedFix.v +++ b/erasure/theories/EEtaExpandedFix.v @@ -946,6 +946,7 @@ Proof. eapply isEtaExp_mkApps_intro; auto; solve_all. Qed. + Lemma decompose_app_tApp_split f a hd args : decompose_app (tApp f a) = (hd, args) -> f = mkApps hd (remove_last args) /\ a = last args a. Proof. @@ -1456,11 +1457,11 @@ Proof. unfold isStuckFix', cunfold_fix. destruct nth_error => //. Qed. -Lemma isEtaExp_FixApp {Σ mfix idx l} : +Lemma isEtaExp_FixApp {Σ mfix idx Γ l} : isEtaExp_fixapp mfix idx #|l| -> - forallb (λ d : def EAst.term, isLambda d.(dbody) && isEtaExp Σ (rev_map (λ d0 : def term, 1 + rarg d0) mfix ++ []) (dbody d)) mfix -> - forallb (isEtaExp Σ []) l -> - isEtaExp Σ [] (mkApps (tFix mfix idx) l). + forallb (λ d : def EAst.term, isLambda d.(dbody) && isEtaExp Σ (rev_map (λ d0 : def term, 1 + rarg d0) mfix ++ Γ) (dbody d)) mfix -> + forallb (isEtaExp Σ Γ) l -> + isEtaExp Σ Γ (mkApps (tFix mfix idx) l). Proof. intros hmfix hm hl. funelim (isEtaExp Σ _ _) => //; solve_discr. noconf H. diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v index cab43751d..0fb577261 100644 --- a/erasure/theories/EOptimizePropDiscr.v +++ b/erasure/theories/EOptimizePropDiscr.v @@ -795,6 +795,7 @@ Proof. unfold expanded_constant_decl => /=. apply remove_match_on_box_expanded_irrel. Qed. + Lemma remove_match_on_box_wellformed {efl : EEnvFlags} {Σ : GlobalContextMap.t} n t : has_tBox -> has_tRel -> wf_glob Σ -> EWellformed.wellformed Σ n t -> EWellformed.wellformed Σ n (remove_match_on_box Σ t). @@ -1001,3 +1002,103 @@ Proof. eapply remove_match_on_box_expanded_irrel => //. now apply remove_match_on_box_expanded, isEtaExp_expanded. Qed. + + +Section ExpandedFix. + Import EEtaExpandedFix. + + Lemma expanded_mkApps_expanded Σ Γ t l : expanded Σ Γ t -> All (expanded Σ Γ) l -> expanded Σ Γ (mkApps t l). + Proof. + move/expanded_isEtaExp => ht ha. apply isEtaExp_expanded. + eapply isEtaExp_mkApps_intro; eauto; solve_all. now eapply expanded_isEtaExp. + Qed. + + Lemma remove_match_on_box_expanded_fix {Σ : GlobalContextMap.t} t : expanded Σ [] t -> expanded Σ [] (remove_match_on_box Σ t). + Proof. + induction 1 using expanded_ind. + all:try solve[constructor; eauto; solve_all]. + all:rewrite ?remove_match_on_box_mkApps. + - cbn. eapply expanded_tRel_app; tea. now len. solve_all. + - eapply expanded_mkApps_expanded; eauto; solve_all. + - cbn -[GlobalContextMap.inductive_isprop_and_pars]. unfold isprop_ind. + rewrite GlobalContextMap.inductive_isprop_and_pars_spec. + destruct inductive_isprop_and_pars as [[[|] _]|] => /= //. + 2-3:constructor; eauto; solve_all. + destruct branches eqn:heq. + constructor; eauto; solve_all. cbn. + destruct l => /=. + depelim H0. depelim H2. subst branches. + eapply isEtaExp_expanded. + eapply expanded_isEtaExp in H2. + eapply isEtaExp_substl; tea. len. eapply forallb_repeat => //. + destruct branches as [|[]]; cbn in heq; noconf heq. + cbn -[isEtaExp] in *. depelim H1. cbn in H1. + constructor; eauto; solve_all. + depelim H0. depelim H0. depelim H2. do 2 (constructor; intuition auto). + solve_all. + - cbn -[GlobalContextMap.inductive_isprop_and_pars]. + rewrite GlobalContextMap.inductive_isprop_and_pars_spec. + destruct inductive_isprop_and_pars as [[[|] _]|] => /= //. + constructor. all:constructor; auto. + - cbn. eapply expanded_tFix. 4:{ rewrite nth_error_map H4 //. } + all:eauto; solve_all. + rewrite isLambda_remove_match_on_box //. + rewrite !rev_map_spec in b *; rewrite map_map /= //. + - eapply expanded_tConstruct_app; tea. + now len. solve_all. + Qed. + + Lemma remove_match_on_box_expanded_fix_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} Γ t : wf_glob Σ -> expanded Σ Γ t -> expanded (remove_match_on_box_env Σ) Γ t. + Proof. + intros wf; induction 1 using expanded_ind. + all:try solve[constructor; eauto; solve_all]. + eapply expanded_tRel_app; tea. + eapply expanded_tFix; eauto. solve_all. + eapply expanded_tConstruct_app. + destruct H as [[H ?] ?]. + split => //. split => //. red. + red in H. rewrite lookup_env_remove_match_on_box // /= H //. 1-2:eauto. auto. solve_all. + Qed. + + Lemma remove_match_on_box_expanded_fix_decl {Σ : GlobalContextMap.t} t : expanded_decl Σ t -> expanded_decl Σ (remove_match_on_box_decl Σ t). + Proof. + destruct t as [[[]]|] => /= //. + unfold expanded_constant_decl => /=. + apply remove_match_on_box_expanded_fix. + Qed. + + Lemma remove_match_on_box_expanded_fix_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ -> expanded_decl Σ t -> expanded_decl (remove_match_on_box_env Σ) t. + Proof. + destruct t as [[[]]|] => /= //. + unfold expanded_constant_decl => /=. + apply remove_match_on_box_expanded_fix_irrel. + Qed. + + Lemma remove_match_on_box_env_expanded_fix {efl : EEnvFlags} {Σ : GlobalContextMap.t} : + wf_glob Σ -> expanded_global_env Σ -> expanded_global_env (remove_match_on_box_env Σ). + Proof. + unfold expanded_global_env; move=> wfg. + rewrite remove_match_on_box_env_eq //. + destruct Σ as [Σ map repr wf]. cbn in *. + clear map repr. + induction 1; cbn; constructor; auto. + cbn in IHexpanded_global_declarations. + unshelve eapply IHexpanded_global_declarations. now depelim wfg. cbn. + set (Σ' := GlobalContextMap.make _ _). + rewrite -(remove_match_on_box_env_eq Σ'). cbn. now depelim wfg. + eapply (remove_match_on_box_expanded_fix_decl_irrel (Σ := Σ')). now depelim wfg. + now unshelve eapply (remove_match_on_box_expanded_fix_decl (Σ:=Σ')). + Qed. + + Definition remove_match_on_box_program_expanded_fix {efl} (p : eprogram_env) : + wf_eprogram_env efl p -> + expanded_eprogram_env p -> expanded_eprogram (remove_match_on_box_program p). + Proof. + unfold expanded_eprogram_env. + move=> [wfe wft] [etae etat]. split. + cbn. eapply remove_match_on_box_env_expanded_fix => //. + eapply remove_match_on_box_expanded_fix_irrel => //. + now apply remove_match_on_box_expanded_fix. + Qed. + +End ExpandedFix. diff --git a/erasure/theories/ErasureFunctionProperties.v b/erasure/theories/ErasureFunctionProperties.v index e617fc6fd..f921232a3 100644 --- a/erasure/theories/ErasureFunctionProperties.v +++ b/erasure/theories/ErasureFunctionProperties.v @@ -1590,7 +1590,7 @@ Lemma erase_constant_body_correct'' {X_type X} {cb} {decls normalization_in prf} {onc : forall Σ' : global_env_ext, abstract_env_ext_rel X' Σ' -> ∥ on_constant_decl (lift_typing typing) Σ' cb ∥} {body} deps : EAst.cst_body (fst (erase_constant_body X_type X' cb onc)) = Some body -> forall Σ' : global_env_ext, abstract_env_ext_rel X' Σ' -> - ∥ ∑ t T, (Σ' ;;; [] |- t : T) * (Σ' ;;; [] |- t ⇝ℇ body) * + ∥ ∑ t T, (cst_body cb = Some t) * (Σ' ;;; [] |- t : T) * (Σ' ;;; [] |- t ⇝ℇ body) * (term_global_deps body = snd (erase_constant_body X_type X' cb onc)) * wellformed (efl:=all_env_flags) (erase_global_deps X_type (KernameSet.union deps (term_global_deps body)) X decls normalization_in prf).1 0 body ∥. Proof. diff --git a/erasure/theories/Typed/ErasureCorrectness.v b/erasure/theories/Typed/ErasureCorrectness.v index df3370493..94a946048 100644 --- a/erasure/theories/Typed/ErasureCorrectness.v +++ b/erasure/theories/Typed/ErasureCorrectness.v @@ -106,16 +106,15 @@ Context {X_type : PCUICWfEnv.abstract_env_impl} {X : X_type.π1}. Context {normalising_in: forall Σ : global_env_ext, wf_ext Σ -> PCUICWfEnv.abstract_env_rel X Σ -> PCUICSN.NormalizationIn Σ}. -Lemma erase_global_decls_deps_recursive_correct decls univs retro wfΣ include ignore_deps : +Lemma erase_global_decls_deps_recursive_correct_gen decls univs retro wfΣ include ignore_deps : let Σ := mk_global_env univs decls retro in (forall k, ignore_deps k = false) -> - (forall k, KernameSet.In k include -> P.lookup_env Σ k <> None) -> - includes_deps Σ (trans_env (erase_global_decls_deps_recursive (X_type := X_type) (X := X) decls univs retro wfΣ include ignore_deps)) include. + forall include', KernameSet.Subset include' include -> + (forall k, KernameSet.In k include' -> P.lookup_env Σ k <> None) -> + includes_deps Σ (trans_env (erase_global_decls_deps_recursive (X_type := X_type) (X := X) decls univs retro wfΣ include ignore_deps)) include'. Proof. cbn. - cut (is_true (KernameSet.subset include include)); [|now apply KernameSet.subset_spec]. - generalize include at 1 3 5 as include'. - intros include' sub no_ignores all_in. + intros no_ignores include' sub all_in. induction decls as [|(kn, decl) Σ0 IH] in X_type, X, univs, decls, retro, wfΣ, all_in, include, include', sub |- *. { intros kn isin. cbn. now apply all_in in isin. } @@ -145,7 +144,6 @@ Proof. intros k kisin. specialize (all_in _ kisin). unfold eq_kername in *. - apply KernameSet.subset_spec in sub. apply sub in kisin. apply KernameSet.mem_spec in kisin. destruct (Kername.reflect_kername) as [k_eq H]. @@ -161,13 +159,10 @@ Proof. apply global_erases_with_deps_cons; auto. { pose proof (wfΣ _ hfull). now subst Σfull. } eapply (IH _ _ _ _ wfΣprev _ (KernameSet.singleton k)). - - apply KernameSet.subset_spec. - intros ? ?. + - intros ? ?. eapply KernameSet.singleton_spec in H; subst a. apply KernameSet.union_spec. - right. - apply KernameSet.subset_spec in sub. - now apply sub. + right. now apply sub. - specialize (all_in _ isin). intros isink <-%KernameSet.singleton_spec. apply KernameSet.mem_spec in isin. @@ -282,8 +277,7 @@ Proof. eapply (@erase_global_erases_deps (_, _)); eauto. now apply erases_erase. eapply IH. - ++ apply KernameSet.subset_spec. - intros ? isin'. + ++ intros ? isin'. apply KernameSet.union_spec; left. now apply KernameSet.union_spec; right. ++ intros ? isin'. @@ -297,4 +291,13 @@ Proof. apply erase_ind_correct. Qed. +Lemma erase_global_decls_deps_recursive_correct decls univs retro wfΣ include ignore_deps : + let Σ := mk_global_env univs decls retro in + (forall k, ignore_deps k = false) -> + (forall k, KernameSet.In k include -> P.lookup_env Σ k <> None) -> + includes_deps Σ (trans_env (erase_global_decls_deps_recursive (X_type := X_type) (X := X) decls univs retro wfΣ include ignore_deps)) include. +Proof. + intros; eapply erase_global_decls_deps_recursive_correct_gen; eauto. reflexivity. +Qed. + End EEnvCorrect. \ No newline at end of file diff --git a/erasure/theories/Typed/ExAst.v b/erasure/theories/Typed/ExAst.v index daaf1e38b..345111a3f 100644 --- a/erasure/theories/Typed/ExAst.v +++ b/erasure/theories/Typed/ExAst.v @@ -1,4 +1,5 @@ From Coq Require Import List. +From MetaCoq.Utils Require Import utils. From MetaCoq.Common Require Import Kernames. From MetaCoq.Common Require Import BasicAst. From MetaCoq.Erasure Require Export EAst. @@ -173,9 +174,8 @@ Inductive fresh_globals : global_env -> Prop := fresh_global kn g -> fresh_globals ((kn,b,d) :: g). - Definition trans_env (Σ : global_env) : EAst.global_context := - map (fun '(kn, _, decl) => (kn, trans_global_decl decl)) Σ. + map (fun d => (d.1.1, trans_global_decl d.2)) Σ. Definition print_term (Σ : global_env) (t : term) : bytestring.String.t := EPretty.print_program (trans_env Σ,t). diff --git a/erasure/theories/Typed/ExtractionCorrectness.v b/erasure/theories/Typed/ExtractionCorrectness.v index 99c279643..30683c4bd 100644 --- a/erasure/theories/Typed/ExtractionCorrectness.v +++ b/erasure/theories/Typed/ExtractionCorrectness.v @@ -335,6 +335,99 @@ Proof. - intros he => /=. eapply wf_trans_inductives. Qed. + +Import EEtaExpandedFix. + +Lemma includes_deps_equiv Σ Σ' deps deps' : + KernameSet.Equal deps deps' -> + includes_deps Σ Σ' deps -> + includes_deps Σ Σ' deps'. +Proof. + unfold includes_deps. + intros eq hn kn. now rewrite <-eq. +Qed. + +Lemma expanded_erase (cf := config.extraction_checker_flags) + (no := PCUICSN.normalizing_flags) + {X_type X} univs wfΣ t wtp ignored : + (forall kn, ignored kn = false) -> + forall Σ prf', abstract_env_rel X Σ -> PCUICEtaExpand.expanded Σ [] t -> + let X' := abstract_make_wf_env_ext X univs wfΣ in + forall normalization_in' : forall Σ, wf_ext Σ -> Σ ∼_ext X' -> PCUICSN.NormalizationIn Σ, + let et := (@erase X_type X' normalization_in' [] t wtp) in + let deps := EAstUtils.term_global_deps et in + expanded (trans_env (@Erasure.erase_global_decls_deps_recursive X_type X Σ.(PEnv.declarations) Σ.(PEnv.universes) Σ.(PEnv.retroknowledge) prf' deps ignored)) [] et. +Proof. + intros hign Σ heq wf hexp X' normalization_in'. + pose proof (abstract_env_wf _ wf) as [wf']. + pose proof (abstract_env_ext_exists X') as [[? wfmake]]. + pose proof (abstract_env_ext_wf _ wfmake) as []. + pose proof (abstract_make_wf_env_ext_correct X univs wfΣ _ _ wf wfmake). subst x. + eapply (expanded_erases (Σ := (Σ, univs))); tea. + eapply (erases_erase (X := X')); eauto. + destruct (wtp _ wfmake). + eapply (erase_global_erases_deps (Σ := (Σ, univs))); eauto. + eapply erases_erase; eauto. cbn. destruct Σ. + eapply erase_global_decls_deps_recursive_correct_gen => //=. + intros k H0. + eapply term_global_deps_spec in H0; tea. 2:eapply X0. + cbn in H0. destruct H0 as [[decl hl]]. now rewrite hl. + now eapply erases_erase. +Qed. + +Lemma expanded_erase_global_decl : + forall (H := EWellformed.all_env_flags) + X_type X + (k : kername) (g : PCUICAst.PCUICEnvironment.global_decl) + env prf w wt (Σex : global_env) prf' seeds ignored, + let eg := (@Erasure.erase_global_decl X_type + (abstract_make_wf_env_ext X (PCUICAst.PCUICLookup.universes_decl_of_decl g) prf) (env, PCUICAst.PCUICLookup.universes_decl_of_decl g) + w k g wt) in + (forall kn, ignored kn = false) -> + Σex = @Erasure.erase_global_decls_deps_recursive X_type X env.(PEnv.declarations) env.(PEnv.universes) env.(PEnv.retroknowledge) prf' + (KernameSet.union (Erasure.decl_deps eg) seeds) ignored -> + expanded_global_env (trans_env Σex) -> + PCUICEtaExpand.expanded_decl env g -> + expanded_decl (trans_env Σex) (trans_global_decl eg). +Proof. + intros H X_type X k g [univs decls retros] prf w wt Σex prf' seeds ignored eg hign eqex wf_global; cbn in *. + revert eqex. subst eg. + set (Σ := {| PEnv.universes := _ |}) in *. + pose proof (abstract_env_exists X) as [[Σ' hΣ]]. + pose proof (prf' _ hΣ). subst Σ'. destruct (prf _ hΣ) as [wfΣ]. + unfold Erasure.erase_global_decl. + destruct g. + - destruct (Erasure.erase_constant_decl) eqn:Hdecl. + * unfold Erasure.erase_constant_decl,Erasure.erase_constant_decl_clause_1 in *. + destruct (Erasure.flag_of_type), conv_ar; try congruence. + inversion Hdecl;subst;clear Hdecl. + unfold trans_global_decl,trans_cst. + cbn [EWellformed.wf_global_decl]. + unfold MCOption.option_default. + destruct EAst.cst_body eqn:heq => //. + set (deps := KernameSet.union _ _). + destruct c as [ty [b|] cunivs rel]. 2:cbn in heq => //. + intros eq []. cbn in expanded_body. move: eq. + unshelve eapply (erase_constant_body_correct'' (X_type := X_type) (decls := decls) seeds) in heq as [[t0' [T [[] ?]]]]. + shelve. 4:exact w. intros. eapply Erasure.fake_normalization; tea. + { intros. now rewrite (prf' _ H0). } + intros ->. cbn. destruct p as [[eq ?] ?]. cbn in eq. noconf eq. + eapply expanded_erases; tea. apply wfΣ. cbn. clear i. cbn. + eapply (erase_global_erases_deps (Σ := (Σ, cunivs))); eauto. cbn. + set (ert := Erasure.erase_type _ _ _ _) in deps. clearbody ert. + cbn in deps. clear wf_global. + eapply erase_global_decls_deps_recursive_correct_gen => //. + { subst deps. knset. } + intros. + cbn in e. + eapply term_global_deps_spec in H0; tea. 2:eapply wfΣ. + cbn in H0. destruct H0 as [[decl hl]]. now rewrite hl. + * intros ->. cbn. + destruct o => //=. cbn in Hdecl. cbn. + intros; constructor. + - intros he => //=. +Qed. + Transparent Erasure.flag_of_type. Ltac invert_wf := @@ -382,6 +475,34 @@ Proof. - apply IHdecls. Qed. +Lemma expanded_erase_global_decls_recursive (H := EWellformed.all_env_flags) : + forall X_type X decls univs retros w seeds (ignored : kername -> bool), + (forall k, ignored k = false) -> + let Σex := @Erasure.erase_global_decls_deps_recursive X_type X decls univs retros w seeds ignored in + PCUICEtaExpand.expanded_global_declarations univs retros decls -> + expanded_global_env (trans_env Σex). +Proof. + intros X_type X decls univs retros w seeds ignored hign ?. + subst Σex. + revert seeds. + induction decls in X_type, X, w |- *;intros seeds;auto;try constructor. + simpl. + destruct a;simpl. + destruct (KernameSet.mem _ _);cbn. + - unfold MCProd.test_snd;cbn. + constructor. + * unfold trans_env in *;cbn in *. + depelim H0. + now apply IHdecls. + * cbn. depelim H0. cbn in H1. + remember (KernameSet.union _ _) as kns. + rewrite hign in Heqkns. cbn in Heqkns. + remember (Erasure.erase_global_decls_deps_recursive decls univs _ _ _ _) as Σex. + eapply expanded_erase_global_decl; tea. cbn. erewrite <- Heqkns. exact HeqΣex. subst Σex. + eapply IHdecls; eauto. + - intros H0; depelim H0. eapply IHdecls; eauto. +Qed. + Lemma optimize_correct `{EWellformed.EEnvFlags} Σ fgΣ t v : ELiftSubst.closed t = true -> EGlobalEnv.closed_env (trans_env Σ) = true -> diff --git a/erasure/theories/Typed/Optimize.v b/erasure/theories/Typed/Optimize.v index 7d52b6110..a659f1272 100644 --- a/erasure/theories/Typed/Optimize.v +++ b/erasure/theories/Typed/Optimize.v @@ -276,7 +276,9 @@ Definition dearg_oib let ctor_mask := get_branch_mask mib_masks oib_index c in dearg_ctor (param_mask mib_masks) ctor_mask ctor) (ind_ctors oib); - ind_projs := ind_projs oib |}. + ind_projs := + let ctor_mask := get_branch_mask mib_masks oib_index 0 in + masked ctor_mask (ind_projs oib) |}. Definition dearg_mib (kn : kername) (mib : mutual_inductive_body) : mutual_inductive_body := match get_mib_masks kn with @@ -372,6 +374,21 @@ Fixpoint valid_cases (t : term) : bool := | _ => true end. +Fixpoint forallbi {A} (f : nat -> A -> bool) n l := + match l with + | [] => true + | hd :: tl => f n hd && forallbi f (S n) tl + end. + +Definition check_oib_masks masks i oib := + forallbi (fun c cb => #|get_branch_mask masks i c| == cb.2) 0 oib.(ind_ctors) && + match oib.(ind_projs) with + | [] => true + | _ :: _ => + let mask := get_branch_mask masks i 0 in + #|mask| == #|oib.(ind_projs)| + end. + Definition valid_masks_decl (p : kername * bool * global_decl) : bool := match p with | (kn, _, ConstantDecl {| cst_body := Some body |}) => @@ -379,7 +396,8 @@ Definition valid_masks_decl (p : kername * bool * global_decl) : bool := | (kn, _, TypeAliasDecl typ) => #|get_const_mask kn| =? 0 | (kn, _, InductiveDecl mib) => match get_mib_masks kn with - | Some mask => #|mask.(param_mask)| =? mib.(ind_npars) + | Some mask => (#|mask.(param_mask)| =? mib.(ind_npars)) && + forallbi (check_oib_masks mask) 0 mib.(ind_bodies) | _ => false end | _ => true diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v index 5f7d180ca..aa607a222 100644 --- a/erasure/theories/Typed/OptimizeCorrectness.v +++ b/erasure/theories/Typed/OptimizeCorrectness.v @@ -6,7 +6,7 @@ From MetaCoq.Erasure.Typed Require Import Transform. From MetaCoq.Erasure.Typed Require Import WcbvEvalAux. From Coq Require Import Btauto. From Coq Require Import List. -From Coq Require Import ssrbool. +From Coq Require Import ssreflect ssrbool. From Coq Require Import PeanoNat. From Equations Require Import Equations. From MetaCoq.Erasure Require Import EPrimitive EAstUtils. @@ -14,7 +14,7 @@ From MetaCoq.Erasure Require Import ECSubst. From MetaCoq.Erasure Require Import EInduction. From MetaCoq.Erasure Require Import ELiftSubst. From MetaCoq.Erasure Require Import EWcbvEval. -From MetaCoq.Erasure Require Import EGlobalEnv. +From MetaCoq.Erasure Require Import EGlobalEnv EWellformed. From MetaCoq.Utils Require Import MCList. From MetaCoq.Utils Require Import MCPrelude. From MetaCoq.Utils Require Import utils. @@ -24,6 +24,8 @@ Import ExAst. Import Kernames. Import ListNotations. +Unset SsrRewrite. + Local Set Firstorder Solver auto. Ltac Tauto.intuition_solver ::= auto with *. @@ -112,6 +114,69 @@ Ltac refold := | [ |- context[filter _ ?Γ]] => progress (fold (vasses Γ) in * ) end. +(* +From Equations Require Import Equations. +Import EEtaExpandedFix EOptimizePropDiscr ESpineView. +Import TermSpineView EInduction. + +Lemma list_size_pos {A} (l : list A) (h : l <> []) (size : A -> nat) : list_size size l > 0. +Proof. + induction l; cbn; try lia. now elim h. +Qed. +Section DeargAuxDecomp. + +Context (ind_masks : list (kername * mib_masks)). +Context (const_masks : list (kername * bitmask)). +Notation get_ctor_mask := (get_ctor_mask ind_masks). +Notation get_mib_masks := (get_mib_masks ind_masks). +Notation get_const_mask := (get_const_mask const_masks). + +Set Equations Debug. +Equations? dearg_aux_decomp (t : term) : term by wf t (fun x y : EAst.term => size x < size y) := + dearg_aux_decomp t with TermSpineView.view t := { + | tRel i => EAst.tRel i + | tVar v => EAst.tVar v + | tBox => EAst.tBox + | tEvar ev l => EAst.tEvar ev (map_In l (fun x H => dearg_aux_decomp x)) + | tLambda na t => EAst.tLambda na (dearg_aux_decomp t) + | tLetIn na b t => EAst.tLetIn na (dearg_aux_decomp b) (dearg_aux_decomp t) + | tApp f args napp nempty with f := { + | EAst.tConstruct ind c cargs => dearg_single (get_ctor_mask ind c) (EAst.tConstruct ind c cargs) (map_In args (fun x H => dearg_aux_decomp x)) + | EAst.tConst kn => dearg_single (get_const_mask kn) (EAst.tConst kn) (map_In args (fun x H => dearg_aux_decomp x)) + | EAst.tCase (ind, npars) discr brs := + let discr := dearg_aux_decomp discr in + let brs := map_In brs (fun br hin => (br.1, dearg_aux_decomp br.2)) in + EAst.mkApps (dearg_case ind_masks ind npars discr brs) (map_In args (fun x H => dearg_aux_decomp x)) + | EAst.tProj (mkProjection ind npars arg) t => + mkApps (dearg_proj ind_masks ind npars arg (dearg_aux_decomp t)) (map_In args (fun x H => dearg_aux_decomp x)) + | hd => mkApps (dearg_aux_decomp hd) (map_In args (fun x H => dearg_aux_decomp x)) } + | tConstruct ind c cargs => dearg_single (get_ctor_mask ind c) (EAst.tConstruct ind c cargs) [] + | tConst kn => dearg_single (get_const_mask kn) (EAst.tConst kn) [] + | tCase (ind, npars) discr brs := + let discr := dearg_aux_decomp discr in + let brs := map_In brs (fun br hin => (br.1, dearg_aux_decomp br.2)) in + dearg_case ind_masks ind npars discr brs + | tProj (mkProjection ind npars arg) t => + dearg_proj ind_masks ind npars arg (dearg_aux_decomp t) + | tFix mfix idx => + EAst.tFix (map_In mfix (fun d hin => {| dname := d.(dname); dbody := dearg_aux_decomp d.(dbody); rarg := d.(rarg) |})) idx + | tCoFix mfix idx => + EAst.tCoFix (map_In mfix (fun d hin => {| dname := d.(dname); dbody := dearg_aux_decomp d.(dbody); rarg := d.(rarg) |})) idx + | tPrim p => EAst.tPrim (map_primIn p (fun x H => dearg_aux_decomp x)) }. +Proof. + all:try subst discr; try subst brs; clear dearg_aux_decomp. + all: cbn. + all: try lia. + all:rewrite ?size_mkApps; cbn [size]. + all:(try match goal with H : In ?x ?l |- _ => try (let H' := fresh in assert (H' := In_size id size H); unfold id in H'; change (fun x => size x) with size in H') end); eauto. + all:(try match goal with H : ?l <> [] |- context [ list_size ?size ?l ] => try (let H' := fresh in assert (H' := list_size_pos l H size)) end); eauto; try lia. + pose proof (H0 := In_size snd size hin); cbn in H0. lia. + pose proof (H0 := In_size snd size hin); cbn in H0. lia. + pose proof (H0 := In_size dbody size hin); cbn in H0. lia. + pose proof (H0 := In_size dbody size hin); cbn in H0. lia. + now apply InPrim_size. +Qed. *) + Lemma decompose_body_masked_spec mask Γ t t' : valid_dearg_mask mask t -> (Γ, t') = decompose_body_masked mask t -> @@ -821,7 +886,7 @@ Proof. - repeat (try destruct (_ <=? _) eqn:?; propify; try destruct (_ =? _) eqn:?; propify; - cbn in *); + cbn in * ); lia. - easy. - induction X; [easy|]. @@ -1160,7 +1225,7 @@ Proof. - repeat (try destruct (_ <=? _) eqn:?; propify; try destruct (_ =? _) eqn:?; propify; - cbn in *); + cbn in * ); lia. - induction X; [easy|]. cbn in *. @@ -2090,6 +2155,60 @@ Proof. now propify. Qed. +Import EWellformed. + +Lemma wellformed_dearg_single (efl := all_env_flags) Σ k t args mask : + wellformed Σ k t -> + Forall (wellformed Σ k) args -> + wellformed Σ k (dearg_single mask t args). +Proof. + intros clos_t clos_args. + induction mask as [|[] mask IH] in k, t, args, mask, clos_t, clos_args |- *; cbn in *. + - apply forallb_Forall in clos_args. + now rewrite wellformed_mkApps. + - depelim clos_args; [|easy]. + cbn in *. cbn. + apply IH; [|easy]. + pose proof (wellformed_lift 1 k 0 _ clos_t). + now rewrite Nat.add_1_r in H. + - depelim clos_args. + + cbn. + apply IH; [|easy]. + cbn. + rewrite Bool.andb_true_r. + pose proof (wellformed_lift 1 k 0 _ clos_t). + now rewrite Nat.add_1_r in H. + + apply IH; [|easy]. + cbn. + now propify. +Qed. +(* From Coq Require Import ssreflect. +Lemma wellformed_dearg_single' (efl := all_env_flags) Σ k t args mask : + wellformed (trans_env (dearg_env Σ)) k t -> + Forall (wellformed (trans_env (dearg_env Σ)) k) args -> + wellformed (trans_env (dearg_env Σ)) k (dearg_single mask t args). +Proof. + intros clos_t clos_args. + induction mask as [|[] mask IH] in k, t, args, mask, clos_t, clos_args |- *; cbn in *. + - eapply forallb_Forall in clos_args. + now rewrite wellformed_mkApps //. + - depelim clos_args; [|easy]. + cbn in *. cbn. + apply IH; [|easy]. + pose proof (wellformed_lift 1 k 0 _ clos_t). + now rewrite Nat.add_1_r in H. + - depelim clos_args. + + cbn. + apply IH; [|easy]. + cbn. + rewrite Bool.andb_true_r. + pose proof (wellformed_lift 1 k 0 _ clos_t). + now rewrite Nat.add_1_r in H. + + apply IH; [|easy]. + cbn. + now propify. +Qed. *) + Lemma closedn_dearg_lambdas k mask t : closedn k t -> closedn k (dearg_lambdas mask t). @@ -2103,6 +2222,19 @@ Proof. - now propify. Qed. +Lemma wellformed_dearg_lambdas {efl : EEnvFlags} Σ k mask t : + has_tBox -> + wellformed Σ k t -> + wellformed Σ k (dearg_lambdas mask t). +Proof. + intros clos. + induction t in k, mask, t, clos |- *; auto; cbn in *. + - destruct mask; [easy|]. rtoProp; intuition auto. + destruct b; eauto. + apply wellformed_subst; eauto; + cbn; rewrite ?Nat.add_1_r; eauto. cbn. rewrite H0. eauto. + - now propify. +Qed. (* NOTE: borrowed from MetaCoq (where it's commented out) and fixed *) Lemma closedn_subst s k k' t : @@ -2162,6 +2294,49 @@ Proof. easy. Qed. +Lemma wellformed_dearg_case_branch_body_rec (efl := all_env_flags) Σ i k mask t : + wellformed Σ (i + #|mask| + k) t -> + wellformed Σ (i + count_zeros mask + k) (dearg_branch_body_rec i mask t).2. +Proof. + intros clos. + induction mask in mask, i, k, t, clos |- *; cbn in *. + - eauto. + - destruct a. + * cbn in *. + eapply IHmask. + unfold subst1. + replace (i + #|mask| + k) with (k + #|mask| + i) by lia. + eapply wellformed_subst_eq;eauto. cbn. + now replace (k + #|mask| + i + 1) with (i + S #|mask| + k). + * cbn. + replace (i + S #|filter negb mask| + k) with (S i + #|filter negb mask| + k) by lia. + replace (i + S #|mask| + k) with (S i + #|mask| + k) in * by lia. + easy. +Qed. + +Import EEtaExpandedFix. + +Lemma isEtaExp_dearg_case_branch_body_rec (efl := all_env_flags) Σ i k mask t : + isEtaExp Σ (repeat 0 i ++ repeat 0 #|mask| ++ k) t -> + isEtaExp Σ (repeat 0 i ++ repeat 0 (count_zeros mask) ++ k) (dearg_branch_body_rec i mask t).2. +Proof. + intros clos. + induction mask in mask, i, k, t, clos |- *; cbn in *. + - eauto. + - destruct a. + * cbn in *. + eapply IHmask. + unfold subst1. + rewrite <- closed_subst; auto. + eapply etaExp_csubst'. now len. now simp_eta. exact clos. + * cbn. fold (dearg_branch_body_rec (S i) mask t). + pose proof (repeat_app 0 i 1). cbn in H. + replace (repeat 0 i ++ 0 :: repeat 0 #|filter negb mask| ++ k) with + (repeat 0 (S i) ++ repeat 0 #|filter negb mask| ++ k). + 2:{ rewrite Nat.add_1_r in H. now rewrite H; cbn; rewrite <- app_assoc; cbn. } + eapply IHmask. now rewrite <- Nat.add_1_r, repeat_app, <- app_assoc; cbn. +Qed. + Lemma closedn_dearg_aux k args t : closedn k t -> Forall (closedn k) args -> @@ -2242,6 +2417,25 @@ Proof. - rewrite closedn_mkApps; cbn; rtoProp; intuition solve_all. solve_all_k 6. Qed. +Lemma Alli_map {A B P n} {f : A -> B} l : + Alli (fun n x => P n (f x)) n l -> + Alli P n (map f l). +Proof. + induction 1; constructor; eauto. +Qed. + + +Lemma lookup_env_dearg_env Σ kn : + lookup_env (dearg_env Σ) kn = option_map (dearg_decl kn) (lookup_env Σ kn). +Proof. + unfold lookup_env. + induction Σ as [|((kn', has_deps), decl) Σ IH]; [easy|]. + cbn. + unfold eq_kername. + destruct Kername.reflect_kername as [eq Heq]. + destruct (Heq kn kn');subst;[easy| apply IH]. +Qed. + Hint Resolve closedn_subst0 closed_mkApps closedn_dearg_aux closed_iota_red is_expanded_aux_subst is_expanded_aux_mkApps @@ -2426,11 +2620,44 @@ Proof. now destruct get_const_mask. Qed. +Definition check_oib_masks_trans masks i oib := + forallbi (fun c cb => #|get_branch_mask masks i c| == cb.(cstr_nargs)) 0 oib.(EAst.ind_ctors) && + match oib.(EAst.ind_projs) with + | [] => true + | _ :: _ => + let mask := get_branch_mask masks i 0 in + #|mask| == #|oib.(EAst.ind_projs)| + end. + +Lemma forallbi_nth_error {A} n k {l : list A} p x : nth_error l n = Some x -> forallbi p k l -> p (n + k) x. +Proof. + induction l in x, n, k |- *; cbn => //. + - now rewrite nth_error_nil. + - destruct n; cbn. + + intros [= <-]. move/andP=> [ha hf]. exact ha. + + intros hn. move/andP=> [hp hf]. + eapply IHl in hn; tea. now rewrite Nat.add_succ_r in hn. +Qed. + + +Require Import ssreflect. + +Lemma forallbi_Alli {A} (f : nat -> A -> bool) n l : + Alli f n l <~> forallbi f n l. +Proof. + split. + - induction 1; cbn; auto. + - induction l in n |- *; cbn; auto. + * constructor. + * move/andP => [] hf hl. constructor; eauto. +Qed. + + Lemma valid_ind_mask_inductive Σ ind mib oib : valid_masks_env Σ -> EGlobalEnv.declared_inductive (trans_env Σ) ind mib oib -> ∑ mask, get_mib_masks (inductive_mind ind) = Some mask /\ - #|mask.(param_mask)| =? mib.(EAst.ind_npars). + (#|mask.(param_mask)| =? mib.(EAst.ind_npars)) /\ check_oib_masks_trans mask (inductive_ind ind) oib. Proof. intros valid_env decl_ind. apply forallb_Forall in valid_env. @@ -2444,7 +2671,17 @@ Proof. destruct cst;cbn in *;try congruence. inversion H0;subst;clear H0;cbn in *. destruct get_mib_masks;try congruence. - eexists;eauto. + eexists;eauto. split; eauto. + move/andP: Hb => [] -> hf. + rewrite nth_error_map in nth. + destruct nth_error eqn:hnth => //. eapply forallbi_nth_error in hf; tea. + rewrite Nat.add_0_r in hf. cbn in nth. noconf nth. + destruct o; cbn. split => //. unfold check_oib_masks in hf; cbn in hf. + move/andP: hf => [] oncs onps. apply/andP. split. + - cbn. move/forallbi_Alli: oncs => oncs. eapply forallbi_Alli, Alli_map, Alli_impl; tea; cbn. + now intros n [[kn tys] nargs]; cbn. + - unfold check_oib_masks_trans. cbn in *. destruct ind_projs; cbn in * => //. + now rewrite map_length. Qed. Ltac invert_facts := @@ -2567,17 +2804,6 @@ Proof with auto with dearg. solve_all. depelim H0; constructor; cbn; intuition eauto. solve_all. Qed. -Lemma lookup_env_dearg_env Σ kn : - lookup_env (dearg_env Σ) kn = option_map (dearg_decl kn) (lookup_env Σ kn). -Proof. - unfold lookup_env. - induction Σ as [|((kn', has_deps), decl) Σ IH]; [easy|]. - cbn. - unfold eq_kername. - destruct Kername.reflect_kername as [eq Heq]. - destruct (Heq kn kn');subst;[easy| apply IH]. -Qed. - Lemma declared_constant_dearg Σ k cst : declared_constant (trans_env Σ) k cst -> ∑ cst', @@ -2857,6 +3083,8 @@ Ltac facts := assert (is_expanded v) by (unshelve eapply (eval_is_expanded_aux _ _ _ 0 _ H); trivial) end). +Ltac bool := rtoProp; intuition eauto. + Lemma count_zeros_le : forall mask, count_zeros mask <= #|mask|. Proof. induction mask;cbn;auto. destruct a;cbn; unfold count_zeros in *; lia. @@ -2896,6 +3124,49 @@ Proof. destruct b;rewrite app_length;cbn; lia. Qed. + +Lemma masked_length {X} m (xs : list X) : + #|m| <= #|xs| -> + #|masked m xs| = count_zeros m + #|xs| - #|m|. +Proof. + intros len. + induction m in xs, len |- *; cbn in *. + - now destruct xs. + - destruct xs; cbn in *; [easy|]. + destruct a; cbn in *. + + rewrite IHm by easy. + now unfold count_zeros. + + rewrite IHm by easy. + now unfold count_zeros. +Qed. + + + +Import EEtaExpandedFix. + +Hint Resolve dearg_elim : core. + +Lemma isEtaExp_lift Σ Γ Γ' t : isEtaExp Σ Γ t -> isEtaExp Σ (Γ' ++ Γ) (lift0 #|Γ'| t). +Proof using. + todo "lift". +Qed. + +Lemma isEtaExp_dearg_single Σ Γ t m l : + isEtaExp Σ Γ t -> + forallb (isEtaExp Σ Γ) l -> + isEtaExp Σ Γ (dearg_single m t l). +Proof. + induction m in Γ, l, t |- *; intros etat etal. + - cbn. eapply isEtaExp_mkApps_intro; solve_all. + - cbn. destruct a; destruct l; simp_eta; eauto. eapply IHm; eauto. + now eapply (isEtaExp_lift _ _ [_]). + eapply IHm; eauto. now move/andP: etal. + eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]). + now eapply (isEtaExp_lift _ _ [_]). constructor; eauto. simp_eta. + eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]); eauto. constructor; eauto. + all:now move/andP: etal. +Qed. + Section dearg. Context {wfl : WcbvFlags}. Context (n : nat). @@ -3106,7 +3377,7 @@ Section dearg. eapply lookup_ctor_lookup_env;eauto. apply e0. eapply lookup_ctor_lookup_env;eauto. subst; apply e0. } - specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask Hparams]]. + specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask [Hparams _]]]. set (trans_mib (dearg_mib ind_masks (inductive_mind ind) mib)) as mib_dearg. set (trans_oib (dearg_oib mask (inductive_ind ind) oib)) as oib_dearg. set (dearg_ctor (param_mask mask) (get_branch_mask mask (inductive_ind ind) c) ctor) as ctor_dearg. @@ -3263,6 +3534,334 @@ Section dearg. - now apply Forall_snoc in valid_args. - now apply Forall_snoc in exp_args. Qed. + + Set SsrRewrite. + Lemma count_zeros_nth_error l : + count_zeros l = 0 -> + (forall n x, nth_error l n = Some x -> x = true). + Proof using. + clear. + unfold count_zeros. + induction l; cbn => //. + - intros _ n x; rewrite nth_error_nil //. + - destruct a => //=. intros hl n x. + destruct n => //=. + + intros [= <-] => //. + + intros hnth. eapply IHl; eauto. + Qed. + + Lemma wellformed_dearg_aux (efl := all_env_flags) k args t : + valid_cases t -> + wellformed (trans_env Σ) k t -> + Forall (wellformed (trans_env (dearg_env Σ)) k) args -> + wellformed (trans_env (dearg_env Σ)) k (dearg_aux args t). + Proof. + clear IH. + intros valid_t clos_t clos_args. + induction t in k, args, valid_t, clos_t, clos_args |- * using term_forall_list_ind; + cbn -[EGlobalEnv.lookup_projection EGlobalEnv.lookup_inductive EGlobalEnv.lookup_constructor] in *; intros; + try solve [intros; rewrite ?wellformed_mkApps; try easy; intros; repeat (rtoProp; cbn; intuition eauto; solve_all)]; + repeat (rtoProp; cbn; intuition eauto; solve_all). + - intros. eapply wellformed_dearg_single; eauto. cbn. + rewrite !lookup_env_trans_env in clos_t |- *. + rewrite lookup_env_dearg_env. destruct lookup_env => //=. cbn in clos_t. + destruct g => //. + - intros. eapply wellformed_dearg_single; eauto. + cbn -[EGlobalEnv.lookup_constructor]; eauto. move: H. + destruct EGlobalEnv.lookup_constructor as [[[mib oib] cb]|] eqn:hc => //= _. + eapply lookup_ctor_trans_env in hc as hc'; destruct hc' as [mib' [oib' [ctor' []]]]. intuition subst. + assert (decl_ind :declared_inductive (trans_env Σ) i (trans_mib mib') (trans_oib oib')). + { unfold declared_inductive,declared_minductive. + eapply lookup_ctor_lookup_env;eauto. } + specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask Hparams]]. + eapply lookup_ctor_dearg in H; tea. + erewrite lookup_ctor_trans_env_inv; tea. + - destruct p. rewrite wellformed_mkApps; try easy. + unfold dearg_case. + destruct (EGlobalEnv.lookup_inductive _ _) as [[mib oib]|] eqn:hl => //. + assert (decl_ind :declared_inductive (trans_env Σ) i mib oib). + { move: hl. unfold EGlobalEnv.lookup_inductive. cbn. + unfold declared_inductive,declared_minductive. destruct EGlobalEnv.lookup_env => //. + destruct g => //. destruct nth_error eqn:hnth => //. intros [= <- <-]. split; eauto. } + specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask Hparams]]. + rewrite Hmask. + rtoProp; intuition eauto; solve_all. + cbn [wellformed]. rtoProp; intuition eauto. + { unfold EGlobalEnv.lookup_inductive. cbn. + move: hl. cbn. + rewrite !lookup_env_trans_env lookup_env_dearg_env. + destruct lookup_env => //=. destruct g => //=. + rewrite !nth_error_map. unfold dearg_mib. rewrite Hmask. cbn. + rewrite nth_error_mapi. destruct nth_error => //. } + cbn. + unfold mapi. clear clos_args IHt. + unfold valid_case_masks in H3. rewrite Hmask in H3. + move/andP: H3 => [] _ hbrs. + eapply alli_Alli in hbrs. + eapply Alli_All_mix in hbrs; tea. clear H0. + generalize 0. + induction hbrs; [easy|]; intros n'. + cbn in p. + cbn [map mapi_rec forallb]. rtoProp. + split. + * unfold dearg_case_branch,dearg_branch_body. + destruct (_ <=? _) eqn:Hmask';[|cbn;easy]. + remember (complete_ctx_mask _ _) as mm. cbn. + assert (#|mm| = #|hd.1|) by now subst;propify;apply complete_ctx_mask_length. + rewrite masked_count_zeros. lia. + specialize (wellformed_dearg_case_branch_body_rec (trans_env (dearg_env Σ)) 0 ((#|hd.1| - #|mm|) + k) mm ((dearg_aux [] hd.2))) as b. + cbn in b. + replace (#|mm| + (#|hd.1| - #|mm| + k)) with (#|hd.1| + k) in * by lia. + rewrite <- Nat.add_assoc. + apply b. + now apply p. + * destruct p. eapply IHhbrs. + - destruct s. rewrite wellformed_mkApps; rtoProp; intuition auto; solve_all. + destruct lookup_projection as [[[[mib oib] cb] pb]|] eqn:hl => //. + assert (decl_ind :declared_inductive (trans_env Σ) proj_ind mib oib). + { move: hl. unfold EGlobalEnv.lookup_inductive. cbn. + unfold declared_inductive,declared_minductive. destruct EGlobalEnv.lookup_env => //. + destruct g => //. destruct nth_error eqn:hnth => //. + destruct EAst.ind_ctors => //. destruct (nth_error _ proj_arg) => //. now intros [= <- <- <- <-]. } + specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask [Hparams Hprojs]]]. + unfold dearg_proj. cbn -[lookup_projection] in *. + rtoProp; intuition auto. + revert hl; cbn. + rewrite !lookup_env_trans_env !lookup_env_dearg_env. + destruct lookup_env => //=. + destruct g => //=. rewrite !nth_error_map /dearg_mib //=. + destruct nth_error eqn:hi => //=; eauto. + destruct o; cbn. destruct ind_ctors eqn:hcs => //=. + rewrite nth_error_map. destruct (nth_error _ proj_arg) eqn:hp => //=. + intros [= <- <- <- <-]. rewrite Hmask /=. + rewrite nth_error_mapi hi //= /= nth_error_map. + rewrite /check_oib_masks_trans /= in Hprojs. + destruct ind_projs; [now rewrite nth_error_nil in hp|]; + rewrite /= map_length in Hprojs. + move: H2. rewrite /valid_proj. rewrite Hmask. + set (cm := get_branch_mask _ _ _) in *. + move/andP=> [] _. rewrite nth_nth_error. + eapply nth_error_Some_length in hp. clearbody cm. + destruct (nth_error (masked _ _) _) eqn:h' => //=. + eapply nth_error_None in h'. + move: h'. move/andP: Hprojs => [] _ Hprojs. + apply eqb_eq in Hprojs. + destruct (nth_error cm proj_arg) eqn:hmp. + 2:{ cbn. eapply nth_error_None in hmp. cbn in hp. lia. } + destruct b => //. intros hm _. + move: hm. + rewrite masked_count_zeros. cbn; lia. cbn. + intros. assert (count_zeros cm + (S #|ind_projs| - #|cm|) = count_zeros cm) by lia. + rewrite {}H2 in hm. cbn in hp. rewrite -Hprojs in hp. + pose proof (count_ones_zeros (firstn proj_arg cm)). + assert (count_ones (firstn proj_arg cm) = #|firstn proj_arg cm| - count_zeros (firstn proj_arg cm)). lia. + rewrite {}H3 in hm. + rewrite -{1}(firstn_skipn proj_arg cm) in hm. + rewrite count_zeros_distr_app in hm. + assert (#|firstn proj_arg cm| = proj_arg). rewrite firstn_length. lia. + rewrite H3 in hm. move: hm. + assert (proj_arg - (proj_arg - count_zeros (firstn proj_arg cm)) = proj_arg - proj_arg + count_zeros (firstn proj_arg cm)) as ->. lia. + rewrite Nat.sub_diag /=. intros. + assert (count_zeros (skipn proj_arg cm) = 0) by lia. + have hc:= (count_zeros_nth_error _ H4 0 false) => //. + forward hc. + rewrite nth_error_skipn Nat.add_0_r //. + by noconf hc. + - rewrite wellformed_mkApps; cbn; rtoProp; intuition eauto; solve_all. + destruct (dbody x); cbn in *; eauto; try congruence. + revert H0. unfold wf_fix. + rewrite map_length. + rtoProp; intuition eauto. unfold test_def in *; solve_all. + - rewrite wellformed_mkApps; cbn; rtoProp; intuition eauto; solve_all. + revert clos_t. unfold wf_fix. + rewrite map_length. + rtoProp; intuition eauto. unfold test_def in *; solve_all. + - rewrite wellformed_mkApps; cbn; rtoProp; intuition solve_all. solve_all_k 7. + Qed. + + Lemma wellformed_dearg (efl := all_env_flags) k t : + valid_cases t -> + wellformed (trans_env Σ) k t -> + wellformed (trans_env (dearg_env Σ)) k (dearg t). + Proof. + intros vt wf. + eapply wellformed_dearg_aux; tea; constructor. + Qed. + + Lemma All_masked {A} {P : A -> Type} m l : All P l -> All P (masked m l). + Proof. + induction 1 in m |- *; cbn; destruct m; try constructor; eauto. + cbn. destruct b; eauto. + Qed. + + Lemma isEtaExp_dearg_single_construct Γ ind i block_args l mib oib : + is_nil block_args -> + forall mask, get_mib_masks (inductive_mind ind) = Some mask -> + declared_inductive (trans_env Σ) ind mib oib -> + #|param_mask mask| = mib.(EAst.ind_npars) -> + isEtaExp_app (trans_env Σ) ind i #|l| -> + forallb (isEtaExp (trans_env (dearg_env Σ)) Γ) l -> + #|get_ctor_mask ind i| <= #|l| -> + isEtaExp (trans_env (dearg_env Σ)) Γ (dearg_single (get_ctor_mask ind i) (tConstruct ind i block_args) l). + Proof. + destruct block_args => //. intros _ mask getm decli hpars. + intros etsal etak hml. + rewrite dearg_single_masked; auto. + rewrite isEtaExp_Constructor. rewrite masked_length; auto. bool. + 2:solve_all. + move: etsal hml. + unfold isEtaExp_app. rewrite /get_ctor_mask getm app_length. + unfold lookup_constructor_pars_args. + destruct EGlobalEnv.lookup_constructor as [[[mib' oib'] cb]|]eqn:hl => //=. + assert (decl_ind :declared_inductive (trans_env Σ) ind mib' oib'). + { move: hl. unfold EGlobalEnv.lookup_inductive. cbn. + unfold declared_inductive,declared_minductive. destruct EGlobalEnv.lookup_env => //. + destruct g => //. destruct nth_error eqn:hnth => //. + destruct (nth_error _ i) eqn:hnth' => //. now intros [= <- <- <-]. } + specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask' [Hmask [Hparams Hprojs]]]. + rewrite Hmask in getm. noconf getm. + assert (oib = oib' /\ mib = mib'). + {move: decli decl_ind. rewrite /declared_inductive /declared_minductive. intuition congruence. } + destruct H; subst oib' mib'. + pose proof hl as hl'. + eapply lookup_ctor_trans_env in hl as [mib' [oib' [ctor' []]]]. intuition subst. + eapply lookup_ctor_dearg in H; tea. cbn in etsal. + eapply lookup_ctor_trans_env_inv in H as ->. cbn. + move/andP: Hprojs => [] Hcs _. + destruct decli. + destruct mib'; unfold dearg_mib. rewrite Hmask. cbn in *. + apply Nat.leb_le in etsal. apply Nat.leb_le. + unfold dearg_ctor. destruct ctor' as [[cna ctys] cnargs]. cbn in *. + rewrite count_zeros_distr_app. + move: hml. + intros hl. + assert (cnargs = #|get_branch_mask mask (inductive_ind ind) i|). + { destruct decl_ind. red in H1. rewrite H1 H0 in hl'. destruct (nth_error _ i) eqn:hnth. noconf hl'. + unfold trans_ctors in Hcs. destruct oib'; cbn in *. + eapply forallbi_nth_error in hnth; tea. cbn in hnth. rewrite Nat.add_0_r in hnth. now apply eqb_eq in hnth. noconf hl'. } + clear hl'. subst cnargs. + set (bm := get_branch_mask _ _ _) in *. + rewrite -{1}(count_ones_zeros bm). + replace (count_zeros bm + count_ones bm - count_ones bm) with (count_zeros bm) by lia. lia. + now eapply All_masked. + Qed. + + Lemma expanded_dearg_aux (efl := all_env_flags) Γ t : + valid_cases t -> + isEtaExp (trans_env Σ) Γ t -> + forall args, forallb (isEtaExp (trans_env (dearg_env Σ)) Γ) args -> + isEtaExp (trans_env (dearg_env Σ)) Γ (dearg_aux args t). + Proof. + clear IH. + apply_funelim (isEtaExp (trans_env Σ) Γ t); intros. + all:match goal with H : is_true (valid_cases _) |- _ => cbn in H; bool end; intros; simp_eta. + all:cbn; simp_eta; toAll; bool; try rewrite -> forallb_InP_spec in *. + all:try solve [solve_all]. + all:try solve [eapply isEtaExp_mkApps_intro; simp_eta; eauto; bool; solve_all]. + - eapply isEtaExp_dearg_single; simp_eta. + - eapply isEtaExp_dearg_single; simp_eta => //. + unfold is_nil. + rewrite H andb_true_r. + move: H0. rewrite /isEtaExp_app. + unfold lookup_constructor_pars_args. + destruct EGlobalEnv.lookup_constructor as [[[mib oib] cb]|]eqn:hl => //=. + assert (decl_ind :declared_inductive (trans_env Σ) ind mib oib). + { move: hl. unfold EGlobalEnv.lookup_inductive. cbn. + unfold declared_inductive,declared_minductive. destruct EGlobalEnv.lookup_env => //. + destruct g => //. destruct nth_error eqn:hnth => //. + destruct (nth_error _ i) eqn:hnth' => //. now intros [= <- <- <-]. } + specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask [Hparams Hprojs]]]. + eapply lookup_ctor_trans_env in hl as [mib' [oib' [ctor' []]]]. intuition subst. + eapply lookup_ctor_dearg in H0; tea. + eapply lookup_ctor_trans_env_inv in H0; rewrite H0. clear H0. cbn in *. + destruct mib'; cbn in *. unfold dearg_mib. rewrite Hmask /=. + eapply Nat.leb_le in H4. assert (ind_npars = 0) by lia. subst ind_npars. + apply Nat.eqb_eq in Hparams. destruct (param_mask) => //. cbn. + unfold dearg_ctor. destruct ctor'; cbn in *. destruct p. cbn. assert (n0 = 0) by lia. apply Nat.leb_le. lia. + - destruct ind. bool. eapply isEtaExp_mkApps_intro; simp_eta; eauto; bool; solve_all. + unfold dearg_case. cbn. simp_eta. bool. solve_all. + unfold valid_case_masks in H5. destruct get_mib_masks eqn:cm => //. + unfold dearg_case_branches. simp_eta. eapply All_mapi, Alli_map. + bool. eapply alli_Alli in H5. eapply Alli_All_mix in H5; tea. + eapply Alli_impl; tea; cbn. intuition eauto. destruct x. bool. cbn in *. + unfold dearg_case_branch. cbn. rewrite H6. + unfold dearg_branch_body. cbn. apply Nat.leb_le in H6. + rewrite masked_length. rewrite complete_ctx_mask_length //. + replace (count_zeros (complete_ctx_mask (get_branch_mask m (inductive_ind i) n1) l) + #|l| - #|complete_ctx_mask (get_branch_mask m (inductive_ind i) n1) l|) with + (count_zeros (complete_ctx_mask (get_branch_mask m (inductive_ind i) n1) l) + (#|l| - #|complete_ctx_mask (get_branch_mask m (inductive_ind i) n1) l|)). + 2:{ rewrite complete_ctx_mask_length; lia. } + rewrite complete_ctx_mask_length //. rewrite Nat.sub_diag Nat.add_0_r. + eapply (isEtaExp_dearg_case_branch_body_rec _ 0). + rewrite complete_ctx_mask_length //. + unfold dearg_case_branches. solve_all. + unfold dearg_case_branches. solve_all. + - destruct p. eapply isEtaExp_mkApps_intro; simp_eta; eauto; bool; solve_all. + bool. unfold dearg_proj. now simp_eta. + - rewrite test_primIn_spec in H1. eapply InPrim_primProp in H. + eapply isEtaExp_mkApps_intro; simp_eta; eauto; bool; solve_all. + solve_all. + eapply primProp_map, primProp_impl; solve_all. + - rewrite dearg_aux_mkApps. cbn. + eapply valid_cases_mkApps_inv in H0 as []. + move: H1. rewrite /isEtaExp_app /lookup_constructor_pars_args. + destruct EGlobalEnv.lookup_constructor as [[[mib oib] cb]|]eqn:hl => //=. + assert (decl_ind :declared_inductive (trans_env Σ) ind mib oib). + { move: hl. unfold EGlobalEnv.lookup_inductive. cbn. + unfold declared_inductive,declared_minductive. destruct EGlobalEnv.lookup_env => //. + destruct g => //. destruct nth_error eqn:hnth => //. + destruct (nth_error _ i) eqn:hnth' => //. now intros [= <- <- <-]. } + specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask [Hparams Hprojs]]]. + pose proof hl as hl'. + eapply lookup_ctor_trans_env in hl as [mib' [oib' [ctor' []]]]. intuition subst. + eapply lookup_ctor_dearg in H1; tea. + cbn. + eapply Nat.eqb_eq in Hparams. + eapply isEtaExp_dearg_single_construct; tea. + + len. unfold isEtaExp_app. + rewrite /lookup_constructor_pars_args hl' //=. eapply Nat.leb_le in H7. cbn in H7. apply Nat.leb_le. lia. + + rewrite forallb_app; bool; solve_all. + + len. rewrite /get_ctor_mask Hmask. len. rewrite Hparams. + move/andP: Hprojs => [] hc _. + destruct decl_ind. red in H6. + unfold EGlobalEnv.lookup_constructor in hl'. + rewrite /EGlobalEnv.lookup_inductive /EGlobalEnv.lookup_minductive H6 //= H8 in hl'. + destruct (nth_error _ i) eqn:nthc => //. noconf hl'. + eapply forallbi_nth_error in hc; tea. rewrite Nat.add_0_r /= in hc. cbn in H7. + apply Nat.eqb_eq in hc. apply Nat.leb_le in H7. rewrite -hc in H7. cbn. lia. + - rewrite dearg_aux_mkApps. eapply valid_cases_mkApps_inv in H1 as[]. + cbn in H1. cbn. + rewrite mkApps_app. eapply isEtaExp_mkApps_intro; solve_all. + eapply isEtaExp_FixApp. + + move: H2. unfold isEtaExp_fixapp. rewrite nth_error_map. + destruct nth_error eqn:hnth => //=; now len. + + rewrite forallb_InP_spec in H5. + cbn. clear H6. + replace (rev_map (fun d0 : def term => S (rarg d0)) (map (map_def (dearg_aux [])) mfix) ++ Γ0) with + (rev_map (fun d0 : def term => S (rarg d0)) mfix ++ Γ0). + 2:{ f_equal. rewrite !rev_map_spec. f_equal. now rewrite map_map_compose /=. } + set (rargs := rev_map _ _) in *. clearbody rargs. solve_all. bool. destruct (dbody x) => //. + + solve_all. + - rewrite dearg_aux_mkApps /=. + destruct nth_error eqn:hnth => //=. cbn in H1. + eapply expanded_isEtaExp. eapply expanded_tRel_app; tea. len. apply Nat.leb_le in H1. lia. + eapply valid_cases_mkApps_inv in H0 as []. + eapply All_Forall, All_app_inv. solve_all. eapply isEtaExp_expanded. eauto. + solve_all. now eapply isEtaExp_expanded. + + - apply valid_cases_mkApps_inv in H1 as []. + specialize (H H1 H2). + rewrite dearg_aux_mkApps. eapply H. rewrite forallb_app. bool. + solve_all. + Qed. + + Lemma expanded_dearg (efl := all_env_flags) Γ t : + valid_cases t -> + isEtaExp (trans_env Σ) Γ t -> + isEtaExp (trans_env (dearg_env Σ)) Γ (dearg t). + Proof. + intros vc ise. eapply expanded_dearg_aux; eauto. + Qed. + End dearg. Lemma env_closed_dearg Σ : @@ -3283,6 +3882,95 @@ Proof. now destruct o. Qed. +Lemma wf_glob_dearg (efl := all_env_flags) Σ : + valid_masks_env Σ -> + wf_glob (trans_env Σ) -> + wf_glob (trans_env (dearg_env Σ)). +Proof. + intros val clos. revert val. + induction Σ as [|((kn & has_deps) & decl) Σ IH]; [easy|]. + rewrite /valid_masks_env /=; move/andP => [] hd he. + depelim clos. cbn. + constructor; eauto. + destruct decl; cbn in *. + - destruct c as [ty []]; [|easy]. + cbn in *. unfold dearg. + move/andP: hd => [] vm vc. + eapply wellformed_dearg_aux; auto. + now eapply valid_cases_dearg_lambdas. + eapply wellformed_dearg_lambdas; auto. + - cbn in *. + unfold dearg_mib. + destruct get_mib_masks => //=. + solve_all. eapply All_mapi. + move/andP: hd => [] _ hf. + eapply forallbi_Alli in hf. + eapply Alli_All_mix in hf; tea. clear H. + eapply Alli_impl; tea; cbn. + intros n []; rewrite /trans_oib /dearg_oib //= /wf_inductive /wf_projections /=. + rewrite /check_oib_masks /=. + destruct ind_projs => //=; rewrite ?masked_nil //=. + move=> [] hl; apply eqb_eq in hl. + destruct ind_ctors => //=. destruct ind_ctors => //=. len. + destruct map eqn:hm; destruct p0 as [[pn pars] k] => //=. + intros h % eqb_eq. subst k. + rewrite masked_length. now (cbn; lia). + cbn. rewrite hl. + apply/Nat.eqb_spec. + pose proof (count_ones_zeros (get_branch_mask m0 n 0)). lia. + - now destruct o; cbn. + - clear hd. clear -H0. + move: H0; induction Σ; cbn; auto. + intros h; depelim h; constructor; cbn; eauto. + now destruct a as [[kn' b] d]; cbn in *. + solve_all. +Qed. + +Lemma trans_env_debox Σ : trans_env Σ = trans_env (debox_env_types Σ). +Proof. + unfold debox_env_types. + generalize Σ at 2. + induction Σ; cbn; auto. intros Σ0. + f_equal. f_equal. + - destruct a as [[kn d] []]; cbn. + * destruct c as [? []]; cbn => //. + * destruct m. unfold trans_mib, debox_type_mib; cbn. + f_equal. f_equal. + rewrite map_map_compose. eapply map_ext. + intros []; unfold trans_oib; cbn. f_equal. + rewrite map_map_compose. eapply map_ext => //. + intros [[] ?] => //. + now rewrite map_map_compose. + * destruct o => //=. destruct p => //. + - apply IHΣ. +Qed. + +Lemma wf_glob_debox (efl := all_env_flags) Σ : + wf_glob (trans_env Σ) -> + wf_glob (trans_env (debox_env_types Σ)). +Proof. + now rewrite trans_env_debox. +Qed. + +Section EtaFix. + Import EEtaExpandedFix. + Lemma expanded_dearg_env (efl := all_env_flags) Σ : + (* valid_masks_env Σ -> *) + expanded_global_env (trans_env Σ) -> + expanded_global_env (trans_env (dearg_env Σ)). + Proof. + induction Σ; intros exp; depelim exp. + - constructor. + - cbn. constructor; eauto. now apply IHΣ. + destruct a as [[kn ?] []]; cbn => //. + + destruct c as [? []]; cbn => //. + cbn in H. + + destruct o; cbn; constructor. + + + +Unset SsrRewrite. + Lemma valid_dearg_mask_dearg_aux mask t : valid_dearg_mask mask t -> valid_dearg_mask mask (dearg t). @@ -3297,21 +3985,6 @@ Proof. now rewrite is_dead_dearg_aux. Qed. -Lemma masked_length {X} m (xs : list X) : - #|m| <= #|xs| -> - #|masked m xs| = count_zeros m + #|xs| - #|m|. -Proof. - intros len. - induction m in xs, len |- *; cbn in *. - - now destruct xs. - - destruct xs; cbn in *; [easy|]. - destruct a; cbn in *. - + rewrite IHm by easy. - now unfold count_zeros. - + rewrite IHm by easy. - now unfold count_zeros. -Qed. - Lemma masked_app {X} m m' (xs : list X) : masked (m ++ m') xs = firstn (count_zeros m) (masked m xs) ++ masked m' (skipn #|m| xs). Proof. @@ -3803,7 +4476,7 @@ Proof. split. subst. eapply lookup_ctor_lookup_env;eauto. eapply lookup_ctor_lookup_env;eauto. subst; apply ctor_look. } - specialize (valid_ind_mask_inductive _ _ _ _ valid_env decl_ind) as [mask [Hmask Hparams]]. + specialize (valid_ind_mask_inductive _ _ _ _ valid_env decl_ind) as [mask [Hmask [Hparams Hprojs]]]. set (trans_mib (dearg_mib ind_masks (inductive_mind ind) mib)) as mib_dearg. set (trans_oib (dearg_oib mask (inductive_ind ind) oib)) as oib_dearg. set (dearg_ctor (param_mask mask) (get_branch_mask mask (inductive_ind ind) c) ctor) as ctor_dearg. @@ -3861,7 +4534,7 @@ Proof. { unfold declared_inductive,declared_minductive. split. rewrite lookup_env_trans_env. now rewrite Hg. unfold trans_mib;cbn. rewrite nth_error_map. now rewrite Hoib. } - specialize (valid_ind_mask_inductive _ _ _ _ valid_env decl_ind) as [mask [Hmask Hparams]]. + specialize (valid_ind_mask_inductive _ _ _ _ valid_env decl_ind) as [mask [Hmask [Hparams Hprojs]]]. set (dearg_case_branch mask ind c (on_snd dearg br)) as br_dearg. eapply (eval_iota _ _ _ _ _ c (masked (get_ctor_mask ind c) (map dearg args)) _ br_dearg);eauto. @@ -4177,7 +4850,7 @@ Proof. { unfold declared_inductive,declared_minductive. split. rewrite lookup_env_trans_env. now rewrite Hg. unfold trans_mib;cbn. rewrite nth_error_map. now rewrite Hoib. } - specialize (valid_ind_mask_inductive _ _ _ _ valid_env decl_ind) as [mask [Hmask Hparams]]. + specialize (valid_ind_mask_inductive _ _ _ _ valid_env decl_ind) as [mask [Hmask [Hparams Hprojs]]]. unfold get_ctor_mask,valid_proj in *. rewrite Hmask in *; cbn in *;propify. rewrite masked_count_zeros by (rewrite map_length;lia). @@ -4200,7 +4873,7 @@ Proof. { unfold declared_inductive,declared_minductive. split. rewrite lookup_env_trans_env. now rewrite Hg. unfold trans_mib;cbn. rewrite nth_error_map. now rewrite Hoib. } - specialize (valid_ind_mask_inductive _ _ _ _ valid_env decl_ind) as [mask [Hmask Hparams]]. + specialize (valid_ind_mask_inductive _ _ _ _ valid_env decl_ind) as [mask [Hmask [Hparams Hprojs]]]. unfold get_ctor_mask, valid_proj in *. rewrite Hmask in *;cbn in *;propify. destruct (nth_error args _) eqn:nth; [|now depelim ev2]. diff --git a/erasure/theories/Typed/OptimizePropDiscr.v b/erasure/theories/Typed/OptimizePropDiscr.v index b5036ae65..947efe2c0 100644 --- a/erasure/theories/Typed/OptimizePropDiscr.v +++ b/erasure/theories/Typed/OptimizePropDiscr.v @@ -1,5 +1,7 @@ (** Pass that removes discrimination (matches and projections) on things in Prop. This uses MetaCoq's optimization but adapted to run on our environments. *) + +From MetaCoq.Utils Require Import utils. From MetaCoq.Erasure.Typed Require Import ExAst. From MetaCoq.Erasure Require Import EOptimizePropDiscr. @@ -17,7 +19,7 @@ Lemma trans_env_fresh_global : forall (kn : Kernames.kername) (g : global_env), fresh_globals g -> fresh_global kn g -> - EnvMap.EnvMap.fresh_global kn (List.map (fun '(kn0, _, decl) => (kn0, trans_global_decl decl)) g). + EnvMap.EnvMap.fresh_global kn (List.map (fun d => (d.1.1, trans_global_decl d.2)) g). Proof. intros kn g fg H. induction H. From f1a445bc3a1e557ee65cbe3d34e433152c39537f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 13 Dec 2023 11:17:20 +0100 Subject: [PATCH 7/7] Finish the proof of preservation of eta-expansion by dearging --- erasure-plugin/src/g_metacoq_erasure.mlg | 8 ++- erasure-plugin/theories/ETransform.v | 10 ++- erasure-plugin/theories/Erasure.v | 2 +- erasure/theories/EEtaExpandedFix.v | 60 ++++++++++++++++++ erasure/theories/Typed/OptimizeCorrectness.v | 67 ++++++++++---------- pcuic/theories/PCUICEtaExpand.v | 1 + utils/theories/MCList.v | 12 +++- utils/theories/MCUtils.v | 1 + 8 files changed, 121 insertions(+), 40 deletions(-) diff --git a/erasure-plugin/src/g_metacoq_erasure.mlg b/erasure-plugin/src/g_metacoq_erasure.mlg index 6f10e648b..be1defda1 100644 --- a/erasure-plugin/src/g_metacoq_erasure.mlg +++ b/erasure-plugin/src/g_metacoq_erasure.mlg @@ -46,12 +46,18 @@ VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY let (c, _) = Constrintern.interp_constr env evm c in check ~bypass:true ~fast:false env evm c } -| [ "MetaCoq" "Typed" "Erase" constr(c) ] -> { +| [ "MetaCoq" "Bypass" "Typed" "Erase" constr(c) ] -> { let env = Global.env () in let evm = Evd.from_env env in let (c, _) = Constrintern.interp_constr env evm c in check ~bypass:true ~fast:false ~with_types:true env evm c } +| [ "MetaCoq" "Typed" "Erase" constr(c) ] -> { + let env = Global.env () in + let evm = Evd.from_env env in + let (c, _) = Constrintern.interp_constr env evm c in + check ~bypass:false ~fast:false ~with_types:true env evm c + } | [ "MetaCoq" "Erase" constr(c) ] -> { let env = Global.env () in let evm = Evd.from_env env in diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v index a9247e437..ab431bf18 100644 --- a/erasure-plugin/theories/ETransform.v +++ b/erasure-plugin/theories/ETransform.v @@ -412,7 +412,7 @@ Proof. destruct p; cbn. clear. intros h; depind h. - destruct g; noconf H. constructor. - - destruct g0; noconf H0. destruct p as [[kn' b] d']. noconf H0. + - destruct g0; noconf H0. destruct p as [[kn' b] d']. constructor; eauto. now eapply fresh_global_trans. Qed. @@ -535,7 +535,7 @@ Section Dearging. | None => (trans_env p.1.2, p.2) end. - Program Definition dearging_transform (efl := all_env_flags) {hastrel : has_tRel} {hastbox : has_tBox} : + Program Definition dearging_transform (efl := all_env_flags) : Transform.t _ _ EAst.term EAst.term _ _ (eval_typed_eprogram_masks opt_wcbv_flags) (eval_eprogram opt_wcbv_flags) := {| name := "dearging"; transform p _ := dearg p ; @@ -561,7 +561,9 @@ Section Dearging. eapply wellformed_dearg; eauto. eapply wf. - rewrite /dearg_env -trans_env_debox. split; cbn. - todo "expanded". + eapply expanded_dearg_env; tea. apply exp. + eapply EEtaExpandedFix.isEtaExp_expanded, expanded_dearg; eauto. + apply EEtaExpandedFix.expanded_isEtaExp, exp. Qed. Next Obligation. @@ -590,6 +592,8 @@ Section Dearging. * exists v. cbn. split => //. Qed. +End Dearging. + Definition extends_eprogram (p p' : eprogram) := extends p.1 p'.1 /\ p.2 = p'.2. diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v index 6c7387167..5b55c8016 100644 --- a/erasure-plugin/theories/Erasure.v +++ b/erasure-plugin/theories/Erasure.v @@ -227,7 +227,7 @@ Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl} remove_match_on_box_typed_transform (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ (* Check if the preconditions for dearging are valid, otherwise dearging will be the identity *) dearging_checks_transform (hastrel := eq_refl) (hastbox := eq_refl) ▷ - dearging_transform (hastrel := eq_refl) (hastbox := eq_refl) ▷ + dearging_transform ▷ rebuild_wf_env_transform true true ▷ verified_lambdabox_typed_pipeline. diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v index f3ed54f6c..77adc689d 100644 --- a/erasure/theories/EEtaExpandedFix.v +++ b/erasure/theories/EEtaExpandedFix.v @@ -1980,4 +1980,64 @@ Proof. * intros [_ [_ [_ H]]]. move/andP: H => [] _. rewrite forallb_app. move=> /andP[] //=. now rewrite andb_true_r. * now move/and4P => []. +Qed. + +Lemma isEtaExp_lift Σ Γ Γ' Γ'' t : isEtaExp Σ (Γ'' ++ Γ) t -> isEtaExp Σ (Γ'' ++ Γ' ++ Γ) (lift #|Γ'| #|Γ''| t). +Proof using. + funelim (isEtaExp Σ _ t); cbn; simp_eta; try now easy; intros; solve_all. + all:cbn; simp_eta; toAll; bool; try rewrite -> forallb_InP_spec in *. + all:try solve [solve_all]. + + - destruct nth_error eqn:hnth => //=. move: hnth. + destruct (PCUICLiftSubst.nth_error_appP Γ'' Γ0 i) => h; noconf h; destruct (Nat.leb_spec #|Γ''| i); try lia; simp_eta. + * rewrite nth_error_app_lt //= e //=. + * rewrite nth_error_app_ge; try lia. + rewrite nth_error_app_ge; try lia. + replace (#|Γ'| + i - #|Γ''| - #|Γ'|) with (i - #|Γ''|) by lia. + now rewrite e. + - simp_eta. eapply (H Γ0 Γ' (0 :: Γ'')); trea. + - eapply (H0 Γ0 Γ' (0 :: Γ'')); trea. + - destruct block_args => //. + - solve_all. + specialize (a Γ0 Γ' (repeat 0 #|x.1| ++ Γ'') x.2). + rewrite -!app_assoc in a. len in a. now apply a. + - solve_all. + specialize (a Γ0 Γ' (repeat 0 #|mfix| ++ Γ'') (dbody x)). + rewrite -!app_assoc in a. len in a. now apply a. + - eapply InPrim_primProp in H. + solve_all. eapply primProp_map, primProp_impl; tea; cbn. + intros x [a exp]. + specialize (a Γ0 Γ' Γ'' x). + now apply a. + - rewrite lift_mkApps /=. + rewrite isEtaExp_mkApps //=. bool. + + now len. + + solve_all. + + destruct block_args => //. + - rewrite lift_mkApps /=. + rewrite isEtaExp_mkApps //=. bool. + + len. + move: H1. rewrite /isEtaExp_fixapp nth_error_map. + destruct nth_error => //. + + solve_all. bool. + * destruct (dbody x) => //. + * set (rm := rev_map _ _). + specialize (a Γ0 Γ' (rm ++ Γ'') (dbody x)). + rewrite -!app_assoc in a. len in a. + rewrite /rm !rev_map_spec in H0 a *; len in a. len. eapply a; trea; rewrite map_map_compose //=. + + solve_all. + - rewrite lift_mkApps /=. + rewrite isEtaExp_mkApps //=; case: Nat.leb_spec => //= hn; bool; solve_all. + + move: H1. + destruct (PCUICLiftSubst.nth_error_appP Γ'' Γ0 n) => //= /Nat.leb_le hx. + * do 2 (rewrite nth_error_app_ge; [lia|]). lia. + * do 2 (rewrite nth_error_app_ge; [lia|]). + replace (#|Γ'| + n - #|Γ''| - #|Γ'|) with (n - #|Γ''|) by lia. + rewrite e //=. now apply Nat.leb_le. + + move: H1. + rewrite !nth_error_app_lt //=. + - rewrite lift_mkApps. + destruct (expanded_head_viewc u) => //. + bool. + eapply isEtaExp_mkApps_intro; eauto. solve_all. Qed. \ No newline at end of file diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v index aa607a222..201b4a68d 100644 --- a/erasure/theories/Typed/OptimizeCorrectness.v +++ b/erasure/theories/Typed/OptimizeCorrectness.v @@ -2877,6 +2877,21 @@ Proof. now apply valid_cases_subst. Qed. +Lemma isEtaExp_dearg_lambdas Σ Γ mask t : + isEtaExp Σ Γ t -> + isEtaExp Σ Γ (dearg_lambdas mask t). +Proof. + intros valid. + induction t in Γ, mask, valid |- * using term_forall_list_ind; cbn in *; try easy. + - simp_eta in valid. + destruct mask as [|[] mask]; try easy. + + now simp_eta. + + cbn. unfold subst1. rewrite <- closed_subst; try easy. + eapply (isEtaExp_substl _ [0] _ [_]); easy. + + simp_eta. now eapply IHt. + - simp_eta. simp_eta in valid. rtoProp; intuition eauto. +Qed. + Lemma dearg_dearg_lambdas mask t : valid_dearg_mask mask t -> valid_cases t -> @@ -3083,8 +3098,6 @@ Ltac facts := assert (is_expanded v) by (unshelve eapply (eval_is_expanded_aux _ _ _ 0 _ H); trivial) end). -Ltac bool := rtoProp; intuition eauto. - Lemma count_zeros_le : forall mask, count_zeros mask <= #|mask|. Proof. induction mask;cbn;auto. destruct a;cbn; unfold count_zeros in *; lia. @@ -3146,11 +3159,6 @@ Import EEtaExpandedFix. Hint Resolve dearg_elim : core. -Lemma isEtaExp_lift Σ Γ Γ' t : isEtaExp Σ Γ t -> isEtaExp Σ (Γ' ++ Γ) (lift0 #|Γ'| t). -Proof using. - todo "lift". -Qed. - Lemma isEtaExp_dearg_single Σ Γ t m l : isEtaExp Σ Γ t -> forallb (isEtaExp Σ Γ) l -> @@ -3159,14 +3167,15 @@ Proof. induction m in Γ, l, t |- *; intros etat etal. - cbn. eapply isEtaExp_mkApps_intro; solve_all. - cbn. destruct a; destruct l; simp_eta; eauto. eapply IHm; eauto. - now eapply (isEtaExp_lift _ _ [_]). + now eapply (isEtaExp_lift _ _ [_] []). eapply IHm; eauto. now move/andP: etal. eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]). - now eapply (isEtaExp_lift _ _ [_]). constructor; eauto. simp_eta. + now eapply (isEtaExp_lift _ _ [_] []). constructor; eauto. simp_eta. eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]); eauto. constructor; eauto. all:now move/andP: etal. Qed. +Unset Strict Universe Declaration. Section dearg. Context {wfl : WcbvFlags}. Context (n : nat). @@ -3296,7 +3305,7 @@ Section dearg. clear IHev1 IHev2 IHev3. revert ev3 ev_len. cbn in *. - rewrite !closed_subst; [|now apply closedn_dearg_aux|easy]. + rewrite !closed_subst; eauto. 2:now apply closedn_dearg_aux. intros. rewrite <- (dearg_subst [a']) by easy. unshelve eapply (IH _ _ _ _ _ ev3)... @@ -3910,12 +3919,13 @@ Proof. intros n []; rewrite /trans_oib /dearg_oib //= /wf_inductive /wf_projections /=. rewrite /check_oib_masks /=. destruct ind_projs => //=; rewrite ?masked_nil //=. - move=> [] hl; apply eqb_eq in hl. + move=> [] /andP[] hcs /Nat.eqb_eq hps. destruct ind_ctors => //=. destruct ind_ctors => //=. len. + intros h % eqb_eq. destruct map eqn:hm; destruct p0 as [[pn pars] k] => //=. - intros h % eqb_eq. subst k. + cbn in h. subst k. rewrite masked_length. now (cbn; lia). - cbn. rewrite hl. + cbn. rewrite hps. apply/Nat.eqb_spec. pose proof (count_ones_zeros (get_branch_mask m0 n 0)). lia. - now destruct o; cbn. @@ -3955,19 +3965,25 @@ Qed. Section EtaFix. Import EEtaExpandedFix. Lemma expanded_dearg_env (efl := all_env_flags) Σ : - (* valid_masks_env Σ -> *) + valid_masks_env Σ -> expanded_global_env (trans_env Σ) -> expanded_global_env (trans_env (dearg_env Σ)). Proof. - induction Σ; intros exp; depelim exp. + induction Σ; intros vm exp; depelim exp. - constructor. - - cbn. constructor; eauto. now apply IHΣ. + - cbn in *. constructor; eauto. move/andP: vm => [] va vΣ. now apply IHΣ. destruct a as [[kn ?] []]; cbn => //. + destruct c as [? []]; cbn => //. cbn in H. + move/andP: vm => [] /andP[] vdm vc vΣ. + eapply expanded_isEtaExp in H. + eapply isEtaExp_expanded. + eapply expanded_dearg; eauto. + now eapply valid_cases_dearg_lambdas. + now eapply isEtaExp_dearg_lambdas. + destruct o; cbn; constructor. - - + Qed. +End EtaFix. Unset SsrRewrite. @@ -4009,21 +4025,6 @@ Proof. f_equal; apply IH. Qed. -Lemma filter_length {X} (f : X -> bool) (xs : list X) : - #|filter f xs| <= #|xs|. -Proof. - induction xs; [easy|]. - cbn. - destruct (f a); cbn; lia. -Qed. - -Lemma map_repeat {X Y} (f : X -> Y) x n : - map f (repeat x n) = repeat (f x) n. -Proof. - induction n; [easy|]. - now cbn; rewrite IHn. -Qed. - Lemma nth_error_masked {X} m (xs : list X) n : nth n m false = false -> nth_error (masked m xs) (n - count_ones (firstn n m)) = diff --git a/pcuic/theories/PCUICEtaExpand.v b/pcuic/theories/PCUICEtaExpand.v index 75e6e8d67..940990cc7 100644 --- a/pcuic/theories/PCUICEtaExpand.v +++ b/pcuic/theories/PCUICEtaExpand.v @@ -233,6 +233,7 @@ Inductive expanded_global_declarations (univs : ContextSet.t) retro : forall (Σ | expanded_global_cons decl Σ : expanded_global_declarations univs retro Σ -> expanded_decl {| universes := univs; declarations := Σ; retroknowledge := retro |} decl.2 -> expanded_global_declarations univs retro (decl :: Σ). +Derive Signature for expanded_global_declarations. Definition expanded_global_env (g : global_env) := expanded_global_declarations g.(universes) g.(retroknowledge) g.(declarations). diff --git a/utils/theories/MCList.v b/utils/theories/MCList.v index 27e54ef68..f7a238fe7 100644 --- a/utils/theories/MCList.v +++ b/utils/theories/MCList.v @@ -1447,6 +1447,14 @@ Proof. induction n; cbn; congruence. Qed. +Lemma filter_length {X} (f : X -> bool) (xs : list X) : + #|filter f xs| <= #|xs|. +Proof. + induction xs; [easy|]. + cbn. + destruct (f a); cbn; lia. +Qed. + Lemma map2_length : forall {A B C : Type} (f : A -> B -> C) (l : list A) (l' : list B), #| map2 f l l'| = min #|l| #|l'|. Proof. @@ -1503,8 +1511,8 @@ Proof. { move => [->|[n H]]; [ exists 0 | exists (S n) ]; rewrite ?skipn_0 ?skipn_S => //=. } Qed. - + Lemma nth_error_firstn A n m (l:list A) x : nth_error (firstn n l) m = Some x -> nth_error l m = Some x. Proof. revert n l. induction m; intros n l H; destruct n, l; cbn in *; try solve [inversion H]; eauto. -Qed. \ No newline at end of file +Qed. \ No newline at end of file diff --git a/utils/theories/MCUtils.v b/utils/theories/MCUtils.v index 7de56e2b4..d066b02e4 100644 --- a/utils/theories/MCUtils.v +++ b/utils/theories/MCUtils.v @@ -147,6 +147,7 @@ Ltac rtoProp := | |- context [is_true (_ && _)] => rewrite andb_and end. +Ltac bool := rtoProp; intuition eauto. Class Fuel := fuel : nat.