From 2fc21e55c94b0725812b3f95c30c7d6ee2d3e4d7 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 27 Nov 2023 18:11:53 +0100 Subject: [PATCH] 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, _).