From 462f3abaab68e5ca3fd861fcee29c660a2570b5b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 22 Jul 2024 14:46:51 +0200 Subject: [PATCH] Proof that reordering of constructors is correct (#1095) * WIP on reordering constructors * New/old tag reasoning * WIP correctness of constructor reordering. main lemma proven * Reordering preserves well-formedness * Reorderin * Admit free proofs of preservation for wf and substitution * WIP adapting to an additional mapping argument for transforms and stronger wellformedness property on extracted terms * Full composed pipeline with mapping of constructors * Fixes due to removal of useless -fast flag and change for reordering of constructors, now verified * Remove option to reorder constructors, now safely done always * Fix metacoq_tour * Fix a remaining todo * Remove generated files --- .vscode/metacoq.code-workspace | 1 + erasure-plugin/clean_extraction.sh | 2 +- erasure-plugin/src/g_metacoq_erasure.mlg | 15 +- erasure-plugin/theories/ETransform.v | 69 +- erasure-plugin/theories/Erasure.v | 890 ++++++++-- erasure/theories/ECoInductiveToInductive.v | 3 +- erasure/theories/EConstructorsAsBlocks.v | 2 +- erasure/theories/EDeps.v | 46 +- erasure/theories/EGenericGlobalMap.v | 2 +- erasure/theories/EGenericMapEnv.v | 2 +- erasure/theories/EImplementBox.v | 3 +- erasure/theories/EInlineProjections.v | 14 +- erasure/theories/EOptimizePropDiscr.v | 6 +- erasure/theories/EProgram.v | 3 + erasure/theories/ERemoveParams.v | 5 +- erasure/theories/EReorderCstrs.v | 1541 ++++++++++++++++- .../EWcbvEvalCstrsAsBlocksFixLambdaInd.v | 1 - erasure/theories/EWcbvEvalCstrsAsBlocksInd.v | 1 + erasure/theories/EWcbvEvalNamed.v | 9 +- erasure/theories/EWellformed.v | 26 +- erasure/theories/ErasureCorrectness.v | 9 +- erasure/theories/ErasureFunction.v | 1 + erasure/theories/ErasureFunctionProperties.v | 12 +- erasure/theories/ErasureProperties.v | 35 +- erasure/theories/Extract.v | 1 + erasure/theories/Typed/OptimizeCorrectness.v | 10 +- examples/metacoq_tour.v | 2 +- safechecker-plugin/clean_extraction.sh | 2 +- template-coq/_PluginProject | 248 --- template-coq/_TemplateCoqProject | 32 - test-suite/erasure_live_test.v | 15 +- 31 files changed, 2456 insertions(+), 552 deletions(-) delete mode 100644 template-coq/_PluginProject delete mode 100644 template-coq/_TemplateCoqProject diff --git a/.vscode/metacoq.code-workspace b/.vscode/metacoq.code-workspace index f69bd9643..acfd61685 100644 --- a/.vscode/metacoq.code-workspace +++ b/.vscode/metacoq.code-workspace @@ -106,5 +106,6 @@ "**/.DS_Store": true, "**/Thumbs.db": true }, + "coq-lsp.check_only_on_request": true, } } diff --git a/erasure-plugin/clean_extraction.sh b/erasure-plugin/clean_extraction.sh index 4187f6ddc..562a941fa 100755 --- a/erasure-plugin/clean_extraction.sh +++ b/erasure-plugin/clean_extraction.sh @@ -9,7 +9,7 @@ fi shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files -files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/` +files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/` if [[ ! -f "src/metacoq_erasure_plugin.cmxs" || "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]] diff --git a/erasure-plugin/src/g_metacoq_erasure.mlg b/erasure-plugin/src/g_metacoq_erasure.mlg index 3efd45e9e..84d490c08 100644 --- a/erasure-plugin/src/g_metacoq_erasure.mlg +++ b/erasure-plugin/src/g_metacoq_erasure.mlg @@ -25,7 +25,6 @@ type erasure_command_args = | Time | Typed | BypassQeds - | Fast let pr_char c = str (Char.escaped c) @@ -46,24 +45,19 @@ type erasure_config = { unsafe : bool; time : bool; typed : bool; - bypass_qeds : bool; - fast : bool; - } + bypass_qeds : bool } let default_config = { unsafe = false; time = false; typed = false; - bypass_qeds = false; - fast = false } + bypass_qeds = false } let make_erasure_config config = let open Erasure0 in { enable_unsafe = if config.unsafe then all_unsafe_passes else no_unsafe_passes ; enable_typed_erasure = config.typed; - enable_fast_remove_params = config.fast; dearging_config = default_dearging_config; - inductives_mapping = []; inlined_constants = Kernames.KernameSet.empty } let time_opt config str fn arg = @@ -76,8 +70,9 @@ let check config env evm c = let time str f arg = time_opt config str f arg in let term = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass:config.bypass_qeds env evm) (EConstr.to_constr evm c) in let erasure_config = make_erasure_config config in + let mapping = [] in let erase = - time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config) term + time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config mapping) term in Feedback.msg_notice (pr_char_list erase) @@ -92,7 +87,6 @@ let interp_erase args env evm c = | Time -> aux {config with time = true} args | Typed -> aux {config with typed = true} args | BypassQeds -> aux {config with bypass_qeds = true} args - | Fast -> aux {config with fast = true} args in aux default_config args in check config env evm c @@ -123,7 +117,6 @@ ARGUMENT EXTEND erase_args | [ "-time" ] -> { Time } | [ "-typed" ] -> { Typed } | [ "-bypass-qeds" ] -> { BypassQeds } -| [ "-fast" ] -> { Fast } END VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v index 06a08372a..1e58c8f01 100644 --- a/erasure-plugin/theories/ETransform.v +++ b/erasure-plugin/theories/ETransform.v @@ -1020,42 +1020,59 @@ Qed. From MetaCoq.Erasure Require Import EReorderCstrs. -Axiom trust_reorder_cstrs_wf : - forall efl : EEnvFlags, - WcbvFlags -> - forall (m : inductives_mapping) (input : Transform.program E.global_context term), - wf_eprogram efl input -> wf_eprogram efl (reorder_program m input). -Axiom trust_reorder_cstrs_pres : - forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping) (p : Transform.program E.global_context term) - (v : term), - wf_eprogram efl p -> - eval_eprogram wfl p v -> exists v' : term, eval_eprogram wfl (reorder_program m p) v' /\ v' = reorder m v. +Definition eval_eprogram_mapping (wfl : WcbvFlags) (p : inductives_mapping * eprogram) t := + eval_eprogram wfl p.2 t. -Program Definition reorder_cstrs_transformation (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping) : - Transform.t _ _ EAst.term EAst.term _ _ - (eval_eprogram wfl) (eval_eprogram wfl) := - {| name := "reoder inductive constructors "; - transform p _ := EReorderCstrs.reorder_program m p ; - pre p := wf_eprogram efl p ; - post p := wf_eprogram efl p ; - obseq p hp p' v v' := v' = EReorderCstrs.reorder m v |}. +Definition eval_eprogram_env_mapping (wfl : WcbvFlags) (p : inductives_mapping * eprogram_env) t := + eval_eprogram_env wfl p.2 t. + +Definition to_program (e : eprogram_env) : eprogram := + (e.1, e.2). + +Program Definition reorder_cstrs_transformation {efl : EEnvFlags} {wca : cstr_as_blocks = false} {has_app : has_tApp} + (wfl : WcbvFlags) {wcon : with_constructor_as_block = false} : + Transform.t _ _ _ EAst.term _ _ + (eval_eprogram_env_mapping wfl) (eval_eprogram wfl) := + {| name := "reorder inductive constructors "; + transform p _ := EReorderCstrs.reorder_program p.1 (to_program p.2) ; + pre p := [/\ wf_eprogram_env efl p.2, EEtaExpandedFix.expanded_eprogram_env p.2 & wf_inductives_mapping p.2.1 p.1] ; + post p := wf_eprogram efl p /\ EEtaExpandedFix.expanded_eprogram p; + obseq p hp p' v v' := v' = EReorderCstrs.reorder p.1 v |}. Next Obligation. - move=> efl wfl m. cbn. now apply trust_reorder_cstrs_wf. + move=> efl wca hasapp wfl wcb [m p] [wfp exp wfm]. split => //. + now unshelve eapply reorder_program_wf. cbn. + now eapply reorder_program_expanded_fix. Qed. Next Obligation. - red. eapply trust_reorder_cstrs_pres. + red. intros efl wca hasapp wfl wcb [m p] v [wfp wfm] evp. + destruct evp as [ev]. + unshelve eapply EReorderCstrs.optimize_correct in ev; trea. + 2,3:apply wfp. + exists (reorder m v). split => //. Qed. #[global] -Axiom trust_reorder_cstrs_transformation_ext : forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping), - TransformExt.t (reorder_cstrs_transformation efl wfl m) - (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1). +Instance reorder_cstrs_transformation_ext {efl : EEnvFlags} (wca : cstr_as_blocks = false) (has_app : has_tApp) (wfl : WcbvFlags) + {wcon : with_constructor_as_block = false} : + TransformExt.t (reorder_cstrs_transformation (wca := wca) (has_app := has_app) wfl (wcon:=wcon)) + (fun p p' => p.1 = p'.1 /\ extends p.2.1 p'.2.1) (fun p p' => extends p.1 p'.1). +Proof. + red. intros p p' pr pr' [eq ext]. + red; cbn. rewrite -eq. eapply EReorderCstrs.optimize_extends_env; eauto. + move: pr'; cbn. now intros []. apply pr. apply pr'. +Qed. #[global] -Axiom trust_reorder_cstrs_transformation_ext' : forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping), - TransformExt.t (reorder_cstrs_transformation efl wfl m) - extends_eprogram extends_eprogram. +Instance reorder_cstrs_transformation_ext' {efl : EEnvFlags} (wca : cstr_as_blocks = false) (has_app : has_tApp) (wfl : WcbvFlags) + {wcon : with_constructor_as_block = false} : + TransformExt.t (reorder_cstrs_transformation (wca := wca) (has_app := has_app) wfl (wcon:=wcon)) + (fun p p' => p.1 = p'.1 /\ extends_eprogram_env p.2 p'.2) extends_eprogram. +Proof. + red. intros p p' pr pr' [eq [ext eq']]. cbn. + red. cbn. rewrite -eq -eq'. split => //. eapply EReorderCstrs.optimize_extends_env; eauto. + move: pr'; cbn. now intros []. apply pr. apply pr'. +Qed. From MetaCoq.Erasure Require Import EUnboxing. diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v index a36fbe6da..83d2ed7d6 100644 --- a/erasure-plugin/theories/Erasure.v +++ b/erasure-plugin/theories/Erasure.v @@ -34,7 +34,6 @@ Local Obligation Tactic := program_simpl. Record unsafe_passes := { cofix_to_lazy : bool; - reorder_constructors : bool; inlining : bool; unboxing : bool; betared : bool }. @@ -42,9 +41,7 @@ Record unsafe_passes := Record erasure_configuration := { enable_unsafe : unsafe_passes; enable_typed_erasure : bool; - enable_fast_remove_params : bool; dearging_config : dearging_config; - inductives_mapping : EReorderCstrs.inductives_mapping; inlined_constants : KernameSet.t }. @@ -56,7 +53,6 @@ Definition default_dearging_config := Definition make_unsafe_passes b := {| cofix_to_lazy := b; - reorder_constructors := b; inlining := b; unboxing := b; betared := b |}. @@ -65,12 +61,10 @@ Definition no_unsafe_passes := make_unsafe_passes false. Definition all_unsafe_passes := make_unsafe_passes true. (* This runs the cofix -> fix/lazy translation as well as inlining and - beta-redex simplification, which are not verified. It does not change - representation by reordering constructors or unboxing. *) + beta-redex simplification, which are not verified. It does do unboxing. *) Definition default_unsafe_passes := {| cofix_to_lazy := true; - reorder_constructors := false; inlining := true; unboxing := false; betared := true |}. @@ -79,17 +73,13 @@ Definition default_erasure_config := {| enable_unsafe := default_unsafe_passes; dearging_config := default_dearging_config; enable_typed_erasure := true; - enable_fast_remove_params := true; - inductives_mapping := []; inlined_constants := KernameSet.empty |}. (* This runs only the verified phases without the typed erasure and "fast" remove params *) Definition safe_erasure_config := {| enable_unsafe := no_unsafe_passes; enable_typed_erasure := false; - enable_fast_remove_params := false; dearging_config := default_dearging_config; - inductives_mapping := []; inlined_constants := KernameSet.empty |}. Axiom assume_welltyped_template_program_expansion : @@ -135,8 +125,6 @@ Program Definition optional_unsafe_transforms econf := (* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *) coinductive_to_inductive_transformation efl (has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl)) ▷ - ETransform.optional_self_transform passes.(reorder_constructors) - (reorder_cstrs_transformation efl final_wcbv_flags econf.(inductives_mapping)) ▷ ETransform.optional_self_transform passes.(unboxing) (rebuild_wf_env_transform (efl := efl) false false ▷ unbox_transformation efl final_wcbv_flags) ▷ @@ -149,26 +137,22 @@ Program Definition optional_unsafe_transforms econf := betared_transformation efl final_wcbv_flags). Next Obligation. - destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto. + destruct (enable_unsafe econf) as [[] [] [] []]; cbn in * => //; intuition auto. Qed. Next Obligation. - destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto. + destruct (enable_unsafe econf) as [[] [] [] []]; cbn in * => //; intuition auto. Qed. Next Obligation. - destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto. -Qed. -Next Obligation. - destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto. + destruct (enable_unsafe econf) as [[] [] [] []]; cbn in * => //; intuition auto. Qed. Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) - : Transform.t _ _ EAst.term EAst.term _ _ + : Transform.t _ _ _ EAst.term _ _ (* Standard evaluation, with cases on prop, guarded fixpoints, applied constructors *) - (EProgram.eval_eprogram_env default_wcbv_flags) + (eval_eprogram_env default_wcbv_flags) (* Target evaluation, with no more cases on prop, unguarded fixpoints, constructors as block *) (EProgram.eval_eprogram final_wcbv_flags) := - (* 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. *) @@ -203,9 +187,276 @@ Next Obligation. now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs. Qed. +Program Definition verified_lambdabox_pipeline_mapping {guard : abstract_guard_impl} + (efl := EWellformed.all_env_flags) + : Transform.t _ _ _ EAst.term _ _ + (* Standard evaluation, with cases on prop, guarded fixpoints, applied constructors *) + (eval_eprogram_env_mapping default_wcbv_flags) + (* Target evaluation, with no more cases on prop, unguarded fixpoints, constructors as block *) + (EProgram.eval_eprogram final_wcbv_flags) := + (* Reorder constructors according to the mapping *) + reorder_cstrs_transformation (wca := eq_refl) (has_app := eq_refl) default_wcbv_flags (wcon := eq_refl) ▷ + (* Rebuild the efficient lookup table *) + rebuild_wf_env_transform (efl := efl) true true ▷ + (* Extract as usual *) + verified_lambdabox_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 + 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. + +Definition eval_pcuic_program_mapping (p : inductives_mapping * pcuic_program) t := + PCUICTransform.eval_pcuic_program p.2 t. + +Import EReorderCstrs (wf_tags_list). + +Definition wf_pcuic_inductive_mapping (Σ : PCUICAst.PCUICEnvironment.global_env) (m : inductive_mapping) : bool := + let '(ind, (_, cstrs)) := m in + match PCUICAst.PCUICLookup.lookup_inductive Σ ind with + | Some (mib, oib) => wf_tags_list cstrs #|oib.(PCUICAst.PCUICEnvironment.ind_ctors)| + | None => true + end. + +Definition wf_pcuic_inductives_mapping Σ m := forallb (wf_pcuic_inductive_mapping Σ) m. + +Import ErasureFunction ErasureFunctionProperties. + +Import PCUICAst.PCUICEnvironment Extract EReorderCstrs EDeps EGlobalEnv. + +Lemma lookup_env_filter Σ f kn : + fresh_global kn Σ -> + lookup_env (filter f Σ) kn = None. +Proof. + induction 1; cbn => //. + destruct f. cbn. case: eqb_spec. intros ->. contradiction. + eauto. eauto. +Qed. + +Lemma lookup_env_filter_deps {efl : EEnvFlags} {Σ f i p} : + wf_glob Σ -> + lookup_env Σ i = Some p -> + lookup_env (filter f Σ) i = Some p \/ + lookup_env (filter f Σ) i = None. +Proof. + move=> wfΣ. + induction Σ in wfΣ |- *; cbn => //. + case: eqb_spec. + - intros -> [= <-]. destruct f. left. cbn. now rewrite eqb_refl. + right. depelim wfΣ. cbn. now apply lookup_env_filter. + - intros diff hl. + destruct f. cbn. case: eqb_spec. + intros ->. contradiction. intros _. depelim wfΣ. + now specialize (IHΣ wfΣ hl). + depelim wfΣ. + now specialize (IHΣ wfΣ hl). +Qed. + +Lemma lookup_env_filter_deps_None {efl : EEnvFlags} {Σ f i} : + wf_glob Σ -> + lookup_env Σ i = None -> + lookup_env (filter f Σ) i = None. +Proof. + move=> wfΣ. + induction Σ in wfΣ |- *; cbn => //. + case: eqb_spec. + - intros -> [= <-]. + - intros diff hl. + destruct f. cbn. case: eqb_spec. + intros ->. contradiction. intros _. depelim wfΣ. + now specialize (IHΣ wfΣ hl). + depelim wfΣ. + now specialize (IHΣ wfΣ hl). +Qed. + +Lemma lookup_inductive_filter_deps_Some {efl : EEnvFlags} {Σ f i p} : + wf_glob Σ -> + lookup_inductive Σ i = Some p -> + lookup_inductive (filter f Σ) i = Some p \/ + lookup_inductive (filter f Σ) i = None. +Proof. + move => wfΣ. + rewrite /lookup_inductive /lookup_minductive. + destruct lookup_env eqn:hle => //=. + eapply lookup_env_filter_deps in hle as [-> | ->] => //; destruct g => //=. now left. + now right. +Qed. + +Lemma lookup_inductive_filter_deps_None {efl : EEnvFlags} {Σ f i} : + wf_glob Σ -> + lookup_inductive Σ i = None -> + lookup_inductive (filter f Σ) i = None. +Proof. + move => wfΣ. + rewrite /lookup_inductive /lookup_minductive. + destruct lookup_env eqn:hle => //=; try destruct g => //=. + eapply (lookup_env_filter_deps) in hle as [-> | ->] => //; destruct g => //=. + eapply (lookup_env_filter_deps) in hle as [-> | ->] => //; destruct g => //=. + eapply (lookup_env_filter_deps_None) in hle as -> => //; destruct g => //=. +Qed. + +Lemma erases_global_lookup_env_constant Σ Σ' kn : + erases_global Σ Σ' -> + forall d, PCUICAst.PCUICEnvironment.lookup_env Σ kn = Some (ConstantDecl d) -> + exists d', lookup_env Σ' kn = Some (EAst.ConstantDecl d'). +Proof. + destruct Σ as [? ? ?]. rewrite /erases_global //=. + induction 1; cbn => //. + - intros d. case: eqb_spec. + + intros ->. intros [=]; subst. now eexists. + + intros diff. cbn in *. eauto. + - intros d. case: eqb_spec. + + intros ->. intros [=]; subst. + + intros diff. cbn in *. eauto. +Qed. + +Lemma erases_global_lookup_env_inductive Σ Σ' kn : + erases_global Σ Σ' -> + forall d, PCUICAst.PCUICEnvironment.lookup_env Σ kn = Some (InductiveDecl d) -> + exists d', lookup_env Σ' kn = Some (EAst.InductiveDecl d') /\ erases_mutual_inductive_body d d'. +Proof. + destruct Σ as [? ? ?]. rewrite /erases_global //=. + induction 1; cbn => //. + - intros d. case: eqb_spec. + + intros ->. intros [=]; subst. + + intros diff. cbn in *. eauto. + - intros d. case: eqb_spec. + + intros ->. intros [=]; subst. now eexists. + + intros diff. cbn in *. eauto. +Qed. + +Lemma erases_global_lookup_env_none Σ Σ' kn : + erases_global Σ Σ' -> + PCUICAst.PCUICEnvironment.lookup_env Σ kn = None -> + lookup_env Σ' kn = None. +Proof. + destruct Σ as [? ? ?]. rewrite /erases_global //=. + induction 1; cbn => //. + - case: eqb_spec. + + intros ->. intros [=]; subst. + + intros diff. cbn in *. eauto. + - case: eqb_spec. + + intros ->. intros [=]; subst. + + intros diff. cbn in *. eauto. +Qed. + +Lemma erases_wf_inductives_mapping {Σ : global_env_ext} {Σ' deps m} : + PCUICTyping.wf_ext Σ -> + erases_global Σ Σ' -> + wf_pcuic_inductives_mapping Σ m -> + EReorderCstrs.wf_inductives_mapping (filter_deps deps Σ') m. +Proof. + move=> wfΣ er. + have wfΣ' := ErasureCorrectness.erases_global_wf_glob _ (fst wfΣ) er. + rewrite /wf_pcuic_inductives_mapping /wf_inductives_mapping. + solve_all. move: H. + rewrite /wf_pcuic_inductive_mapping /wf_inductive_mapping. + destruct x as [ind [na tags]]. + have eral := EDeps.erases_global_all_deps _ _ (PCUICElimination.wf_ext_wf _ wfΣ) er. + have trind := ErasureProperties.trans_lookup_inductive eral ind. + destruct PCUICAst.PCUICLookup.lookup_inductive as [[mib oib]|] eqn:li. + specialize (trind _ _ eq_refl). + - intros wftags. + destruct trind as [mib' [oib' [hli' hctors]]]. + rewrite (filter_deps_filter (efl := all_env_flags)) //. + set (f := fun x => _). + eapply (lookup_inductive_filter_deps_Some (efl := all_env_flags) (f:=f)) in hli' as [H|H] => //; rewrite H //. + congruence. + - intros _. clear trind. + destruct (lookup_inductive (filter_deps deps Σ') ind) eqn:li' => //. + apply False_rect. move: li'. + rewrite (filter_deps_filter (efl:=all_env_flags)) //. + generalize (fun x : KernameSet.elt × EAst.global_decl => flip KernameSet.mem (global_deps Σ' deps) x.1). + intros f li'. + have nli : lookup_inductive Σ' ind = None. + { clear -wfΣ wfΣ' er li. + move: li. rewrite /PCUICAst.PCUICLookup.lookup_inductive /lookup_inductive. + rewrite /PCUICAst.PCUICLookup.lookup_inductive_gen /lookup_minductive. + rewrite /PCUICAst.PCUICLookup.lookup_minductive_gen /lookup_minductive. + destruct PCUICAst.PCUICEnvironment.lookup_env eqn:hle => //=. destruct g => //. + eapply erases_global_lookup_env_constant in hle as [? ->]; tea => //. + eapply erases_global_lookup_env_inductive in hle as [? [-> ?]]; tea => //=. + depelim H. + destruct nth_error eqn:hnth => // _. + destruct (nth_error (EAst.ind_bodies _) _) eqn:hnth' => //=. + eapply nth_error_Some_length in hnth'. eapply nth_error_None in hnth. eapply Forall2_length in H. lia. + intros _. + eapply erases_global_lookup_env_none in hle as ->; tea => //. } + now rewrite (lookup_inductive_filter_deps_None wfΣ' nli) in li'. +Qed. + + +Program Definition erase_transform_mapping {guard : abstract_guard_impl} : Transform.t _ _ _ _ PCUICAst.term EAst.term + eval_pcuic_program_mapping (eval_eprogram_env_mapping EWcbvEval.default_wcbv_flags) := + {| name := "erasure"; + pre p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ pre erase_transform p.2 ; + transform p hp := let nhs := proj2 hp in + (p.1, transform erase_transform p.2 nhs) ; + post p := EReorderCstrs.wf_inductives_mapping p.2.1.(EEnvMap.GlobalContextMap.global_decls) p.1 /\ post erase_transform p.2; + obseq p hp p' := obseq erase_transform p.2 (proj2 hp) p'.2 |}. + +Local Obligation Tactic := idtac. +Next Obligation. + cbn -[erase_transform]. intros. + split. 2:eapply (correctness erase_transform). + destruct input as [m prog]; cbn [fst snd] in *. + destruct p. + unfold erase_transform; cbn [transform]. + unfold erase_program, erase_pcuic_program; + set (egf := erase_global_fast _ _ _ _ _); + set (ef := ErasureFunction.erase _ _ _ _ _); + cbn -[egf ef]; unfold erase_global_fast in egf; rewrite /egf; clear egf ef; + set (deps := EAstUtils.term_global_deps _); clearbody deps; + match goal with + |- context [erase_global_deps_fast ?deps ?X_type ?X ?decls (normalization_in:=?normalization_in) ?hprefix ] => + have heq := @erase_global_deps_fast_erase_global_deps deps X_type X decls normalization_in hprefix + end; cbn in heq; specialize (heq (fun Σ eq => f_equal declarations eq)); + destruct heq as [nin' eq]; rewrite eq; clear eq. + rewrite erase_global_deps_erase_global. + cbn -[ErasureFunction.erase_global]. + match goal with + |- context [@erase_global ?X_type ?X ?decls ?SN ?eq] => + have erg := @erases_global_erase_global X_type X _ _ SN eq + end. + cbn in erg. specialize (erg _ eq_refl). + cbn in p. destruct p as [[wt] ?]. + set (eg := erase_global _ _ _) in erg |- *. clearbody eg. + have := erases_wf_inductives_mapping (Σ' := eg) (fst wt) erg i. + intros h. eauto. +Qed. + +Next Obligation. + intros g p v pr ev. cbn. + now apply (preservation erase_transform). +Qed. + +Program Definition pcuic_expand_lets_transform_mapping {cf : checker_flags} K : Transform.t _ _ _ _ PCUICAst.term PCUICAst.term + eval_pcuic_program_mapping eval_pcuic_program_mapping := + {| name := "let expansion in constructors"; + pre p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ pre (pcuic_expand_lets_transform K) p.2 ; + transform p hp := let nhs := proj2 hp in + (p.1, transform (pcuic_expand_lets_transform K) p.2 nhs) ; + post p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ post (pcuic_expand_lets_transform K) p.2; + obseq p hp p' := obseq (pcuic_expand_lets_transform K) p.2 (proj2 hp) p'.2 |}. +Next Obligation. + cbn. intros cf K input []. split => //. + - move: H; rewrite /wf_pcuic_inductives_mapping. + solve_all. move: H; rewrite /wf_pcuic_inductive_mapping. + destruct x as [ind [na tags]]. + rewrite /PCUICAst.PCUICLookup.lookup_inductive /PCUICAst.PCUICLookup.lookup_inductive_gen /PCUICAst.PCUICLookup.lookup_minductive_gen. + rewrite PCUICExpandLetsCorrectness.trans_lookup. destruct PCUICAst.PCUICEnvironment.lookup_env => //. destruct g => //=. + rewrite nth_error_mapi. destruct nth_error => //=. now len. + - unshelve eapply (correctness (pcuic_expand_lets_transform K)). apply H0. +Qed. +Next Obligation. + intros cf K p v pr ev. now eapply (preservation (pcuic_expand_lets_transform K)). +Qed. + Program Definition verified_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : - Transform.t _ _ - PCUICAst.term EAst.term _ _ + Transform.t _ _ _ EAst.term _ _ PCUICTransform.eval_pcuic_program (EProgram.eval_eprogram final_wcbv_flags) := (* a bunch of nonsense for normalization preconditions *) @@ -219,6 +470,37 @@ Program Definition verified_erasure_pipeline {guard : abstract_guard_impl} (efl (* Erasure of proofs terms in Prop and types *) erase_transform ▷ verified_lambdabox_pipeline. +Next Obligation. + intros guard efl K T1 p. + cbn. intuition eauto. now eapply H2. now eapply H2. +Qed. +Next Obligation. + intros guard efl K T1 p. cbn. intuition auto. +Qed. + +Program Definition verified_erasure_pipeline_mapping {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : + Transform.t _ _ _ EAst.term _ _ + eval_pcuic_program_mapping + (EProgram.eval_eprogram final_wcbv_flags) := + (* 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_mapping (K _ T1) ▷ + (* Erasure of proofs terms in Prop and types *) + erase_transform_mapping ▷ + verified_lambdabox_pipeline_mapping. +Next Obligation. + intros guard efl K T1 p. + cbn. intuition eauto. now eapply H3. now eapply H3. +Qed. +Next Obligation. + intros guard efl K T1 p. cbn. intuition auto. + split; eauto. +Qed. Import EGlobalEnv EWellformed. @@ -236,24 +518,143 @@ Proof. eexists;reflexivity. 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) - (EEnvMap.GlobalContextMap.global_decls p'.1)) (fun p p' => extends p.1 p'.1). +Instance 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) (EEnvMap.GlobalContextMap.global_decls p'.1)) (fun p p' => extends p.1 p'.1). Proof. unfold verified_lambdabox_pipeline. tc. Qed. +Instance verified_lambdabox_pipeline_mapping_extends {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : + TransformExt.t verified_lambdabox_pipeline_mapping + (fun p p' => + p.1 = p'.1 /\ + extends (EEnvMap.GlobalContextMap.global_decls p.2.1) (EEnvMap.GlobalContextMap.global_decls p'.2.1)) (fun p p' => extends p.1 p'.1). +Proof. + unfold verified_lambdabox_pipeline_mapping. 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. Proof. unfold verified_lambdabox_pipeline. tc. Qed. -Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : +Lemma verified_lambdabox_pipeline_mapping_extends' {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : + TransformExt.t verified_lambdabox_pipeline_mapping (fun p p' => p.1 = p'.1 /\ extends_eprogram_env p.2 p'.2) extends_eprogram. +Proof. + unfold verified_lambdabox_pipeline_mapping. tc. +Qed. + +Definition eval_template_program_mapping (p : inductives_mapping * template_program) t := + TemplateProgram.eval_template_program p.2 t. + +Definition eval_template_program_env_mapping (p : inductives_mapping * template_program_env) t := + TemplateProgram.eval_template_program_env p.2 t. + +Definition wf_template_inductive_mapping (Σ : Env.global_env) (m : inductive_mapping) : bool := + let '(ind, (_, cstrs)) := m in + match Template.Ast.lookup_inductive Σ ind with + | Some (mib, oib) => wf_tags_list cstrs #|oib.(Env.ind_ctors)| + | None => true + end. + +Definition wf_template_inductives_mapping Σ m := forallb (wf_template_inductive_mapping Σ) m. + +Program Definition build_template_program_env_mapping {cf : checker_flags} K : + Transform.t _ _ _ _ _ _ eval_template_program_mapping eval_template_program_env_mapping := + {| name := name (build_template_program_env K); + pre p := wf_template_inductives_mapping p.2.1 p.1 /\ pre (build_template_program_env K) p.2 ; + transform p hp := let nhs := proj2 hp in + (p.1, transform (build_template_program_env K) p.2 nhs) ; + post p := wf_template_inductives_mapping p.2.1 p.1 /\ post (build_template_program_env K) p.2; + obseq p hp p' := obseq (build_template_program_env K) p.2 (proj2 hp) p'.2 |}. +Next Obligation. + cbn; intros cf K input [? []]. intuition auto. +Qed. +Next Obligation. + cbn; intros cf K ? ? [? []] ev. cbn. + now unshelve eapply (preservation (build_template_program_env K)). +Qed. + +Lemma lookup_lookup_global_env_None (Σ : GlobalEnvMap.t) kn : + Env.lookup_env Σ kn = None -> + Env.lookup_global (eta_global_declarations Σ (Env.declarations Σ)) kn = None. +Proof. + intros hl. + induction Σ => // /=. induction env => //=. cbn in hl. + rewrite /eta_global_declarations. cbn in *. rewrite lookup_global_map_on_snd hl //. +Qed. + +Lemma eta_lookup_inductive_ctors (Σ : GlobalEnvMap.t) ind : + option_map (fun '(mib, oib) => #|Env.ind_ctors oib|) (Ast.lookup_inductive Σ ind) = option_map (fun '(mib, oib) => #|Env.ind_ctors oib|) (Ast.lookup_inductive (eta_expand_global_env Σ) ind). +Proof. + rewrite /Ast.lookup_inductive /eta_expand_global_env /lookup_inductive_gen /lookup_minductive_gen. + destruct Env.lookup_env eqn:le => //. + cbn. eapply eta_lookup_global in le. rewrite le /=. + destruct g => //=. rewrite nth_error_map. destruct nth_error => //=. len. + cbn. now eapply lookup_lookup_global_env_None in le as ->. +Qed. + +Program Definition eta_expand_mapping K : + Transform.t _ _ _ _ _ _ eval_template_program_env_mapping eval_template_program_mapping := + {| name := name (eta_expand K); + pre p := wf_template_inductives_mapping p.2.1 p.1 /\ pre (eta_expand K) p.2 ; + transform p hp := let nhs := proj2 hp in + (p.1, transform (eta_expand K) p.2 nhs) ; + post p := wf_template_inductives_mapping p.2.1 p.1 /\ post (eta_expand K) p.2; + obseq p hp p' := obseq (eta_expand K) p.2 (proj2 hp) p'.2 |}. +Next Obligation. + cbn; intros K input [? ?]. split. 2:now unshelve eapply (correctness (eta_expand K)). + move: H. rewrite /wf_template_inductives_mapping. + solve_all. move: H. + rewrite /wf_template_inductive_mapping. + destruct x as [ind [na tags]]. + have eqe := eta_lookup_inductive_ctors input.2.1 ind. + do 2 destruct Ast.lookup_inductive as [[? ?]|]; cbn in *; congruence. +Qed. +Next Obligation. + cbn; intros K ? ? [? []] ev. cbn. + now unshelve eapply (preservation (eta_expand K)). +Qed. + +Program Definition template_to_pcuic_mapping K : + Transform.t _ _ _ _ _ _ eval_template_program_mapping eval_pcuic_program_mapping := + {| name := name (template_to_pcuic_transform K); + pre p := wf_template_inductives_mapping p.2.1 p.1 /\ pre (template_to_pcuic_transform K) p.2 ; + transform p hp := let nhs := proj2 hp in + (p.1, transform (template_to_pcuic_transform K) p.2 nhs) ; + post p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ post (template_to_pcuic_transform K) p.2; + obseq p hp p' := obseq (template_to_pcuic_transform K) p.2 (proj2 hp) p'.2 |}. +Next Obligation. + cbn; intros K input [wfm pre]. + pose proof (correctness (template_to_pcuic_transform K) _ pre) as post. + split. 2:now unshelve eapply (correctness (template_to_pcuic_transform K)). + move: wfm. rewrite /wf_template_inductives_mapping. + solve_all. move: H. + rewrite /wf_template_inductive_mapping /wf_pcuic_inductive_mapping. + unfold Ast.lookup_inductive, PCUICAst.PCUICLookup.lookup_inductive, Ast.lookup_inductive_gen, + PCUICAst.PCUICLookup.lookup_inductive_gen, + PCUICAst.PCUICLookup.lookup_minductive_gen, + Ast.lookup_minductive_gen, lookup_minductive_gen. + cbn. destruct post as [[[wtr _]] _]. cbn in wtr. + destruct x as [ind [na tags]]. + destruct pre as [[wta] _]. + have trl := TemplateToPCUICCorrectness.trans_lookup input.2.1 (inductive_mind ind) wta.1 wtr.1. + destruct Env.lookup_env; cbn in *; rewrite trl //. + destruct g => //=. rewrite nth_error_map. destruct nth_error => //=. len. +Qed. +Next Obligation. + cbn; intros K ? ? [? []] ev. cbn. + now unshelve eapply (preservation (template_to_pcuic_transform K)). +Qed. + +Program Definition pre_erasure_pipeline (efl := EWellformed.all_env_flags) : Transform.t _ _ - Ast.term PCUICAst.term _ _ - TemplateProgram.eval_template_program - PCUICTransform.eval_pcuic_program := + _ _ _ _ + eval_template_program + PCUICTransform.eval_pcuic_program := (* a bunch of nonsense for normalization preconditions *) let K ty (T : ty -> _) p := let p := T p in @@ -261,7 +662,7 @@ Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EW (PCUICTyping.wf_ext p -> PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn p) in let T1 (p:global_env_ext_map) := p in let T2 (p:global_env_ext_map) := T1 (build_global_env_map (PCUICExpandLets.trans_global_env p.1), p.2) in - let T3 (p:global_env) := T2 (TemplateToPCUIC.trans_global_env p, Monomorphic_ctx) in + let T3 (p:Env.global_env) := T2 (TemplateToPCUIC.trans_global_env p, Monomorphic_ctx) in let T4 (p:GlobalEnvMap.t) := T3 (eta_expand_global_env p) in (* Build an efficient lookup map for the following eta-expansion phase *) build_template_program_env (K _ T4) ▷ @@ -269,22 +670,75 @@ 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). +Next Obligation. + intros efl K T1 T2 T3 T4 p. cbn. intuition eauto. +Qed. +Next Obligation. + intros efl K T1 T2 T3 T4 p. cbn. intuition eauto. +Qed. -Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ - Ast.term EAst.term _ _ - TemplateProgram.eval_template_program +Program Definition pre_erasure_pipeline_mapping (efl := EWellformed.all_env_flags) : + Transform.t _ _ + _ _ _ _ + eval_template_program_mapping + eval_pcuic_program_mapping := + (* 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 + let T2 (p:global_env_ext_map) := T1 (build_global_env_map (PCUICExpandLets.trans_global_env p.1), p.2) in + let T3 (p:Env.global_env) := T2 (TemplateToPCUIC.trans_global_env p, Monomorphic_ctx) in + let T4 (p:GlobalEnvMap.t) := T3 (eta_expand_global_env p) in + (* Build an efficient lookup map for the following eta-expansion phase *) + build_template_program_env_mapping (K _ T4) ▷ + (* Eta-expand constructors and fixpoint *) + eta_expand_mapping (K _ T3) ▷ + (* Casts are removed, application is binary, case annotations are inferred from the global environment *) + template_to_pcuic_mapping (K _ T2). +Next Obligation. + intros efl K T1 T2 T3 T4 p. cbn. intuition eauto. +Qed. +Next Obligation. + intros efl K T1 T2 T3 T4 p. cbn. intuition eauto. +Qed. + +Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ _ _ _ _ + eval_template_program (EProgram.eval_eprogram final_wcbv_flags) := pre_erasure_pipeline ▷ verified_erasure_pipeline. -Program Definition verified_lambdabox_typed_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) econf : - Transform.t _ _ EAst.term EAst.term _ _ - (EProgram.eval_eprogram_env {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |}) +Next Obligation. + intros guard efl p; cbn. intuition auto. +Qed. + +Program Definition erasure_pipeline_mapping {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ _ _ _ _ + eval_template_program_mapping + (EProgram.eval_eprogram final_wcbv_flags) := + pre_erasure_pipeline_mapping ▷ + verified_erasure_pipeline_mapping. + +Next Obligation. + intros guard efl p; cbn. intuition auto. +Qed. + +Local Obligation Tactic := program_simpl. + +Program Definition verified_lambdabox_typed_pipeline (efl := EWellformed.all_env_flags) + (wfl := {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |}) econf : + Transform.t _ _ _ EAst.term _ _ + (eval_eprogram_env_mapping wfl) (EProgram.eval_eprogram final_wcbv_flags) := + (* Reorder constructors according to the mapping *) + reorder_cstrs_transformation (wca := eq_refl) (has_app := eq_refl) wfl (wcon := eq_refl) ▷ + (* Rebuild the efficient lookup table *) + rebuild_wf_env_transform (efl := efl) true 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 ▷ + 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 *) @@ -319,12 +773,254 @@ Qed. Local Obligation Tactic := intros; eauto. +Definition eval_typed_eprogram_mapping (wfl : WcbvFlags) (p : inductives_mapping × (ExAst.global_env × EAst.term)) t := + eval_typed_eprogram wfl p.2 t. + +Lemma wf_inductive_mapping_trans {Σ Σ' m} : + (forall kn decl, ExAst.lookup_inductive Σ' kn = Some decl -> + exists decl', PCUICAst.lookup_inductive Σ kn = Some decl' /\ #|ind_ctors decl'.2| = #|ExAst.ind_ctors decl|) -> + wf_pcuic_inductive_mapping Σ m -> + wf_inductive_mapping (ExAst.trans_env Σ') m. +Proof. + intros hkn. + rewrite /wf_pcuic_inductive_mapping /wf_inductive_mapping. + destruct m as [ind [na tags]]. + destruct lookup_inductive as [decl|]eqn:hl => //. + have [pdecl [hl' htr]] : exists p, ExAst.lookup_inductive Σ' ind = Some p /\ ExAst.trans_oib p = decl.2. + { move: hl; rewrite /lookup_inductive /ExAst.lookup_inductive. + rewrite /lookup_minductive /= /ExAst.lookup_minductive. + rewrite OptimizeCorrectness.lookup_env_trans_env. + destruct ExAst.lookup_env => //=. destruct g => //=. + rewrite nth_error_map //=. destruct nth_error => //=. intros [= <-]. + now eexists. } + eapply hkn in hl' as [decl' [hl''hct]]. + rewrite hl''hct. destruct decl'; cbn in *. destruct decl. cbn in *. subst o0. + rewrite H. rewrite /ExAst.trans_oib /=. + rewrite /ExAst.trans_ctors. now rewrite map_length. +Qed. + +From Equations Require Import Equations. + +Lemma nth_error_map_In {A B} (l : list A) (f : forall x, In x l -> B) n o : + nth_error (map_In l f) n = Some o -> + exists a (ha : In a l), nth_error l n = Some a /\ o = f a ha. +Proof. + funelim (map_In l f); cbn. + - rewrite nth_error_nil => //. + - destruct n; cbn. + * intros [= <-]; now eexists. + * intros h. have [a [hin []]]:= H _ _ h. + intros -> ->. exists a. exists (or_intror hin). split => //. +Qed. + +Lemma map_In_length {A B} (l : list A) (f : forall x, In x l -> B) : + #|map_In l f| = #|l|. +Proof. funelim (map_In l f); cbn; auto; lia. Qed. + +Lemma lookup_inductive_erase_global_decls_deps {X_type X} {decls : global_env} {prop incl ignore} {kn} {decl} : + ExAst.lookup_inductive (@Erasure.erase_global_decls_deps_recursive X_type X (declarations decls) (universes decls) (retroknowledge decls) prop incl ignore) kn = Some decl -> + exists decl', PCUICAst.lookup_inductive decls kn = Some decl' /\ #|ind_ctors decl'.2| = #|ExAst.ind_ctors decl|. +Proof. + rewrite /ExAst.lookup_inductive /ExAst.lookup_minductive. + destruct decls as [univs' decls retro]. + cbn. unfold ExAst.lookup_env. + induction decls as [|[kn' []]] in X, prop, incl |- *. cbn => //. + - cbn [Erasure.erase_global_decls_deps_recursive] => //. + destruct KernameSet.mem; cbn [ExAst.lookup_env Erasure.erase_global_decl]; + try destruct Erasure.erase_constant_decl => //=; + unfold PCUICAst.lookup_inductive; + unfold PCUICAst.PCUICEnvironment.lookup_env; cbn; + unfold PCUICAst.lookup_inductive_gen, PCUICAst.lookup_minductive_gen. + * unfold ExAst.lookup_env. cbn. + case: eqb_spec. + + intros <-. now cbn. + + intros diff. cbn in IHdecls. eapply IHdecls. + * case: eqb_spec. + + intros <-. now cbn. + + intros diff. eapply IHdecls. + * case: eqb_spec. + + intros heq. + pose proof (PCUICWfEnv.abstract_env_exists X) as [[Σ abs]]. + pose proof (PCUICWfEnv.abstract_env_wf _ abs) as []. + pose proof (prop _ abs). subst Σ. cbn in X0. + eapply wf_fresh_globals in X0. cbn in X0. + depelim X0. clear abs. + match goal with + |- context [@Erasure.erase_global_decls_deps_recursive ?X_type ?X ?decls ?univs ?retro ?prop ?incl ?ignore ] => + set (iprop := prop); set (iincl := incl) + (* have hcor := @ErasureCorrectness.erase_global_decls_deps_recursive_correct X_type X decls univs retro prop incl ignore (fun _ => eq_refl) *) + end. + intros h; specialize (IHdecls _ iprop iincl h). + destruct IHdecls as [decl'' []]. + subst kn'. move: H0. + rewrite /PCUICAst.lookup_inductive /PCUICAst.lookup_inductive_gen. + rewrite /PCUICAst.lookup_minductive /PCUICAst.lookup_minductive_gen. cbn. + destruct lookup_global eqn:hl => //=. + eapply PCUICAst.fresh_global_iff_lookup_global_None in H. rewrite H in hl. congruence. + + intros diff. eapply IHdecls. + - cbn [Erasure.erase_global_decls_deps_recursive] => //. + destruct KernameSet.mem; cbn [ExAst.lookup_env Erasure.erase_global_decl]; + unfold PCUICAst.lookup_inductive; + unfold PCUICAst.PCUICEnvironment.lookup_env; cbn; + unfold PCUICAst.lookup_inductive_gen, PCUICAst.lookup_minductive_gen. + * unfold ExAst.lookup_env. cbn. + case: eqb_spec. + + intros <-. cbn. + destruct nth_error eqn:hmi => //. intros [= <-]. + eapply nth_error_map_In in hmi as [oib [hin [hnth ->]]]. + exists (m, oib); rewrite hnth. split => //=. + now rewrite /Erasure.erase_ind_body map_In_length. + + intros diff. eapply IHdecls. + * case: eqb_spec. + + intros heq. + pose proof (PCUICWfEnv.abstract_env_exists X) as [[Σ abs]]. + pose proof (PCUICWfEnv.abstract_env_wf _ abs) as []. + pose proof (prop _ abs). subst Σ. cbn in X0. + eapply wf_fresh_globals in X0. cbn in X0. + depelim X0. clear abs. + match goal with + |- context [@Erasure.erase_global_decls_deps_recursive ?X_type ?X ?decls ?univs ?retro ?prop ?incl ?ignore ] => + set (iprop := prop); set (iincl := incl) + (* have hcor := @ErasureCorrectness.erase_global_decls_deps_recursive_correct X_type X decls univs retro prop incl ignore (fun _ => eq_refl) *) + end. + intros h; specialize (IHdecls _ iprop iincl h). + destruct IHdecls as [decl'' []]. + subst kn'. move: H0. + rewrite /PCUICAst.lookup_inductive /PCUICAst.lookup_inductive_gen. + rewrite /PCUICAst.lookup_minductive /PCUICAst.lookup_minductive_gen. cbn. + destruct lookup_global eqn:hl => //=. + eapply PCUICAst.fresh_global_iff_lookup_global_None in H. rewrite H in hl. congruence. + + intros diff. eapply IHdecls. +Qed. + +Local Obligation Tactic := program_simpl. + +Program Definition typed_erase_transform_mapping : + Transform.t _ _ _ _ _ _ eval_pcuic_program_mapping (eval_typed_eprogram_mapping default_wcbv_flags) := + {| name := name typed_erase_transform; + pre p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ pre typed_erase_transform p.2 ; + transform p hp := let nhs := proj2 hp in + (p.1, transform typed_erase_transform p.2 nhs) ; + post p := wf_inductives_mapping (ExAst.trans_env p.2.1) p.1 /\ post typed_erase_transform p.2; + obseq p hp p' := obseq typed_erase_transform p.2 (proj2 hp) p'.2 |}. + +Next Obligation. +Proof. + destruct s. cbn -[ExAst.trans_env typed_erase_transform]. split => //. + 2:{ eapply (correctness typed_erase_transform). } + move: i; rewrite /wf_pcuic_inductives_mapping /wf_inductives_mapping. + solve_all. + destruct w as [wf wt]. + eapply wf_inductive_mapping_trans; tea. + intros kn d. + eapply lookup_inductive_erase_global_decls_deps. +Qed. +Next Obligation. + cbn. intros p v pr. eapply (preservation typed_erase_transform). +Qed. + +Lemma lookup_inductive_map_on_snd_remove_decl Σ Σ' kn : + lookup_inductive (map (on_snd (EOptimizePropDiscr.remove_match_on_box_decl Σ')) Σ) kn = lookup_inductive Σ kn. +Proof. + rewrite /lookup_inductive /lookup_minductive. + rewrite EGenericGlobalMap.lookup_env_map_snd. destruct lookup_env => //=. + destruct g => //. +Qed. + +Program Definition remove_match_on_box_typed_transform_mapping {fl} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} : + Transform.t _ _ _ _ _ _ (eval_typed_eprogram_mapping fl) (eval_typed_eprogram_mapping (disable_prop_cases fl)) := + let tr := (remove_match_on_box_typed_transform (fl:=fl) (wcon := wcon) (hastrel := hastrel) (hastbox := hastbox)) in + {| name := name tr; + pre p := wf_inductives_mapping (ExAst.trans_env p.2.1) p.1 /\ pre tr p.2 ; + transform p hp := let nhs := proj2 hp in (p.1, transform tr p.2 nhs) ; + post p := wf_inductives_mapping (ExAst.trans_env p.2.1) p.1 /\ post tr p.2; + obseq p hp p' := obseq tr p.2 (proj2 hp) p'.2 |}. + +Next Obligation. +Proof. + split. 2:{ cbn. now unshelve eapply (correctness remove_match_on_box_typed_transform). } + cbn. + move: i; rewrite /wf_inductives_mapping; solve_all. + move: H; rewrite /wf_inductive_mapping. + rewrite /remove_match_on_box_typed_env. + rewrite -map_trans_env. + destruct x as [ind [na tags]]. now rewrite lookup_inductive_map_on_snd_remove_decl. +Qed. +Next Obligation. + intros p v pr ev. + now unshelve eapply (preservation remove_match_on_box_typed_transform). +Qed. + +Definition eval_typed_eprogram_masks_mapping (fl : WcbvFlags) (p : inductives_mapping × ((option Optimize.dearg_set × ExAst.global_env) × EAst.term)) t := + eval_typed_eprogram_masks fl p.2 t. + +Program Definition dearging_checks_transform_mapping {efl : EEnvFlags} (cf : ETransform.dearging_config) {hastrel : has_tRel} {hastbox : has_tBox} : + Transform.t _ _ _ _ _ _ (eval_typed_eprogram_mapping opt_wcbv_flags) (eval_typed_eprogram_masks_mapping opt_wcbv_flags) := + let tr := (dearging_checks_transform (efl:=efl) cf (hastrel := hastrel) (hastbox := hastbox)) in + {| name := name tr; + pre p := wf_inductives_mapping (ExAst.trans_env p.2.1) p.1 /\ pre tr p.2 ; + transform p hp := let nhs := proj2 hp in (p.1, transform tr p.2 nhs) ; + post p := wf_inductives_mapping (ExAst.trans_env p.2.1.2) p.1 /\ post tr p.2; + obseq p hp p' := obseq tr p.2 (proj2 hp) p'.2 |}. +Next Obligation. +Proof. + split => //. +Qed. +Next Obligation. +Proof. + intros p v pr ev. now unshelve eapply (preservation (dearging_checks_transform cf)). +Qed. + +Program Definition dearging_transform_mapping (cf : ETransform.dearging_config) : + Transform.t _ _ _ _ _ _ (eval_typed_eprogram_masks_mapping opt_wcbv_flags) (eval_eprogram_mapping opt_wcbv_flags) := + let tr := (dearging_transform cf) in + {| name := name tr; + pre p := wf_inductives_mapping (ExAst.trans_env p.2.1.2) p.1 /\ pre tr p.2 ; + transform p hp := let nhs := proj2 hp in (p.1, transform tr p.2 nhs) ; + post p := wf_inductives_mapping p.2.1 p.1 /\ post tr p.2; + obseq p hp p' := obseq tr p.2 (proj2 hp) p'.2 |}. +Next Obligation. +Proof. + split => //. + 2:{ now unshelve eapply (correctness (dearging_transform cf)). } + move: H; rewrite /wf_inductives_mapping; solve_all. + move: H; rewrite /wf_inductive_mapping. destruct x as [ind [na tags]]. + rewrite /dearg. destruct input.2.1.1 => //. + rewrite /OptimizeCorrectness.dearg_env. + rewrite /lookup_inductive /lookup_minductive /=. + rewrite !OptimizeCorrectness.lookup_env_trans_env. + rewrite OptimizeCorrectness.lookup_env_debox_env_types option_map_two /=. + rewrite OptimizeCorrectness.lookup_env_dearg_env option_map_two /=. + destruct ExAst.lookup_env => //=; destruct g => //=. + rewrite !nth_error_map option_map_two /=. + rewrite /Optimize.dearg_mib /=. destruct Optimize.get_mib_masks => //=. + rewrite !nth_error_mapi. + 1-2:destruct nth_error eqn:hnth => //=; len. + intros _. destruct o => //=. destruct p => //. +Qed. +Next Obligation. +Proof. + intros p v pr ev. now unshelve eapply (preservation (dearging_transform cf)). +Qed. + +Program Definition rebuild_wf_env_transform_mapping {fl : WcbvFlags} {efl : EEnvFlags} (with_exp with_fix : bool) : + Transform.t _ _ _ _ _ _ (eval_eprogram_mapping fl) (eval_eprogram_env_mapping fl) := + let tr := @rebuild_wf_env_transform fl efl with_exp with_fix in + {| name := name tr; + pre p := wf_inductives_mapping p.2.1 p.1 /\ pre tr p.2 ; + transform p hp := let nhs := proj2 hp in (p.1, transform tr p.2 nhs) ; + post p := wf_inductives_mapping p.2.1.(EEnvMap.GlobalContextMap.global_decls) p.1 /\ post tr p.2; + obseq p hp p' := obseq tr p.2 (proj2 hp) p'.2 |}. +Next Obligation. +Proof. + intros p v pr ev. now unshelve eapply (preservation (rebuild_wf_env_transform _ _)). +Qed. + Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) econf : - Transform.t _ _ - PCUICAst.term EAst.term _ _ - PCUICTransform.eval_pcuic_program + Transform.t _ _ _ _ _ _ + eval_pcuic_program_mapping (EProgram.eval_eprogram final_wcbv_flags) := (* a bunch of nonsense for normalization preconditions *) let K ty (T : ty -> _) p @@ -333,32 +1029,30 @@ Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl} (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) ▷ + pcuic_expand_lets_transform_mapping (K _ T1) ▷ (* Erasure of proofs terms in Prop and types *) - typed_erase_transform ▷ + typed_erase_transform_mapping ▷ (* Remove match on box early for dearging *) - remove_match_on_box_typed_transform (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷ + remove_match_on_box_typed_transform_mapping (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 econf.(dearging_config) (hastrel := eq_refl) (hastbox := eq_refl) ▷ - dearging_transform econf.(dearging_config) ▷ - rebuild_wf_env_transform true true ▷ + dearging_checks_transform_mapping econf.(dearging_config) (hastrel := eq_refl) (hastbox := eq_refl) ▷ + dearging_transform_mapping econf.(dearging_config) ▷ + rebuild_wf_env_transform_mapping true true ▷ verified_lambdabox_typed_pipeline econf. Next Obligation. - cbn in H. split; cbn; intuition eauto. + unfold pre_remove_match_on_box_typed. split; intuition eauto. Qed. Next Obligation. - cbn in H |- *; intuition eauto. + split; intuition auto. Qed. Program Definition typed_erasure_pipeline {guard : abstract_guard_impl} - (efl := EWellformed.all_env_flags) - econf : - Transform.t _ _ - Ast.term EAst.term _ _ - TemplateProgram.eval_template_program + (efl := EWellformed.all_env_flags) econf : + Transform.t _ _ _ _ _ _ + eval_template_program_mapping (EProgram.eval_eprogram final_wcbv_flags) := - pre_erasure_pipeline ▷ + pre_erasure_pipeline_mapping ▷ verified_typed_erasure_pipeline econf. (* At the end of erasure we get a well-formed program (well-scoped globally and localy), without @@ -369,61 +1063,6 @@ Program Definition typed_erasure_pipeline {guard : abstract_guard_impl} Import EGlobalEnv EWellformed. -Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) econf := - (* 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 - let T2 (p:global_env_ext_map) := T1 (build_global_env_map (PCUICExpandLets.trans_global_env p.1), p.2) in - let T3 (p:global_env) := T2 (TemplateToPCUIC.trans_global_env p, Monomorphic_ctx) in - let T4 (p:GlobalEnvMap.t) := T3 (eta_expand_global_env p) in - build_template_program_env (K _ T4) ▷ - eta_expand (K _ T3) ▷ - template_to_pcuic_transform (K _ T2) ▷ - pcuic_expand_lets_transform (K _ T1) ▷ - 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 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 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 false ▷ - constructors_as_blocks_transformation (efl := efl) (has_app := eq_refl) (has_pars := eq_refl) (has_rel := eq_refl) (has_box := eq_refl) (has_cstrblocks := eq_refl) ▷ - optional_unsafe_transforms econf. -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. unfold optional_unsafe_transforms. - cbn. - destruct enable_unsafe as [[] ? ? ? ?]=> //. -Qed. -Next Obligation. - cbn in H. split; cbn; intuition eauto. -Qed. - -Definition run_erase_program_fast {guard : abstract_guard_impl} (econf : erasure_configuration) := - run (erasure_pipeline_fast econf). - Local Open Scope string_scope. Axiom fake_guard_impl_properties : @@ -447,6 +1086,8 @@ Global Existing Instance fake_normalization. the environment is wellformed and the term well-typed (e.g. when it comes directly from a Coq definition). *) +Axiom assume_that_we_only_erase_on_wellformed_inductive_mappings : forall {cf : checker_flags}, + forall (p : Ast.Env.program) (m : inductives_mapping), wf_template_inductives_mapping p.1 m. Axiom assume_that_we_only_erase_on_welltyped_programs : forall {cf : checker_flags}, forall (p : Ast.Env.program), squash (TemplateProgram.wt_template_program p). @@ -454,19 +1095,19 @@ Axiom assume_that_we_only_erase_on_welltyped_programs : forall {cf : checker_fla (* This also optionally runs the cofix to fix translation *) Program Definition run_erase_program {guard : abstract_guard_impl} econf := if econf.(enable_typed_erasure) then run (typed_erasure_pipeline econf) - else if econf.(enable_fast_remove_params) then - run (erasure_pipeline_fast econf) - else run (erasure_pipeline ▷ (optional_unsafe_transforms econf)). + else run (erasure_pipeline_mapping ▷ (optional_unsafe_transforms econf)). Next Obligation. Proof. unfold optional_unsafe_transforms; cbn. destruct enable_unsafe as [[] ? ? ? ?]=> //. Qed. -Program Definition erase_and_print_template_program econf (p : Ast.Env.program) : string := - let p' := run_erase_program econf p _ in +Program Definition erase_and_print_template_program econf (m : inductives_mapping) (p : Ast.Env.program) : string := + let p' := run_erase_program econf (m, p) _ in time "Pretty printing" EPretty.print_program p'. Next Obligation. + split. + now eapply assume_that_we_only_erase_on_wellformed_inductive_mappings. split. now eapply assume_that_we_only_erase_on_welltyped_programs. cbv [PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn]. @@ -474,26 +1115,13 @@ Next Obligation. split; typeclasses eauto. Qed. -Definition erasure_fast_config := - {| enable_unsafe := no_unsafe_passes; - dearging_config := default_dearging_config; - enable_typed_erasure := false; - enable_fast_remove_params := true; - inductives_mapping := []; - inlined_constants := KernameSet.empty |}. - -Program Definition erase_fast_and_print_template_program (p : Ast.Env.program) : string := - erase_and_print_template_program erasure_fast_config p. - Definition typed_erasure_config := {| enable_unsafe := no_unsafe_passes; dearging_config := default_dearging_config; enable_typed_erasure := true; - enable_fast_remove_params := true; - inductives_mapping := []; inlined_constants := KernameSet.empty |}. -(* Parameterized by a configuration for dearging, allowing to, e.g., override masks. *) +(* TODO: Parameterize by a configuration for dearging, allowing to, e.g., override masks. *) Program Definition typed_erase_and_print_template_program (p : Ast.Env.program) : string := - erase_and_print_template_program typed_erasure_config p. + erase_and_print_template_program typed_erasure_config [] p. diff --git a/erasure/theories/ECoInductiveToInductive.v b/erasure/theories/ECoInductiveToInductive.v index 485284539..602321dcb 100644 --- a/erasure/theories/ECoInductiveToInductive.v +++ b/erasure/theories/ECoInductiveToInductive.v @@ -383,6 +383,7 @@ Proof. unfold lookup_inductive in hl. destruct lookup_minductive => //. } - rewrite !GlobalContextMap.lookup_inductive_kind_spec. + move: H2; rewrite /wf_brs. destruct lookup_inductive as [[mdecl idecl]|] eqn:hl => //. assert (map (on_snd (trans Σ)) l = map (on_snd (trans Σ')) l) as -> by solve_all. rewrite (extends_lookup_inductive_kind H0 H1) //. @@ -1013,7 +1014,7 @@ Proof. destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto. destruct g eqn:hg => /= //; intros; rtoProp; eauto. repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; len; eauto. 1: solve_all. - - rewrite lookup_env_trans //. + - rewrite /wf_brs; cbn; rewrite lookup_env_trans //. destruct lookup_env eqn:hl => // /=. destruct g eqn:hg => /= //. subst g. destruct nth_error => /= //. diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v index c4453bbae..63f188d20 100644 --- a/erasure/theories/EConstructorsAsBlocks.v +++ b/erasure/theories/EConstructorsAsBlocks.v @@ -738,7 +738,7 @@ Proof. rewrite /lookup_constructor_pars_args in H3. destruct lookup_constructor as [[[] ?]|]=> //. cbn in H3. eapply Nat.leb_le in H3. intuition auto. apply/eqb_spec. lia. - - now rewrite lookup_inductive_transform_blocks. + - len. move: H2. rewrite /wf_brs. now rewrite lookup_inductive_transform_blocks. - now rewrite lookup_constructor_transform_blocks. - unfold wf_fix in *. rtoProp. solve_all. solve_all. now eapply isLambda_transform_blocks. - unfold wf_fix in *. rtoProp. solve_all. diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v index 7bee22452..cfd1c70e3 100644 --- a/erasure/theories/EDeps.v +++ b/erasure/theories/EDeps.v @@ -61,9 +61,10 @@ Proof. - depelim er. econstructor; eauto. - depelim er. - econstructor; eauto. + econstructor; eauto. now len. + clear H3. induction X; [easy|]. - depelim H3. + depelim H4. constructor; [|easy]. now cbn. - depelim er. @@ -115,9 +116,9 @@ Proof. - depelim er. econstructor; eauto. - depelim er. - econstructor; eauto. + econstructor; eauto. now len. clear H3. induction X; [easy|]. - depelim H3. + depelim H4. constructor; [|easy]. now cbn. - depelim er. @@ -175,9 +176,10 @@ Proof. - depelim er. cbn. econstructor; eauto. - depelim er. - econstructor; [easy|easy|easy|easy|easy|]. + econstructor; [easy|easy|easy|easy|easy| | ]. + now len. clear H3. induction X; [easy|]. - depelim H3. + depelim H4. constructor; [|easy]. now cbn. - depelim er. @@ -290,14 +292,14 @@ Proof. unfold EGlobalEnv.iota_red. apply erases_deps_substl. + intuition auto. - apply erases_deps_mkApps_inv in H4. + apply erases_deps_mkApps_inv in H5. now apply Forall_rev, Forall_skipn. + eapply nth_error_forall in e2; [|now eauto]. assumption. - congruence. - depelim er. subst brs; cbn in *. - depelim H3. + depelim H4. cbn in *. apply IHev2. apply erases_deps_substl; [|easy]. @@ -325,9 +327,9 @@ Proof. - depelim er. specialize (IHev1 er). apply erases_deps_mkApps_inv in IHev1 as (? & ?). - depelim H4. + depelim H5. apply IHev2. - econstructor; [easy|easy|easy|easy| |easy]. + econstructor; [easy|easy|easy|easy| |easy|easy ]. apply erases_deps_mkApps; [|easy]. now eapply erases_deps_cunfold_cofix; eauto. - depelim er. @@ -398,6 +400,7 @@ Lemma erases_deps_forall_ind Σ Σ' erases_one_inductive_body idecl idecl' -> erases_deps Σ Σ' discr -> P discr -> + #|idecl'.(ind_ctors)| = #|brs| -> Forall (fun br : _ × Extract.E.term => erases_deps Σ Σ' br.2) brs -> Forall (fun br => P br.2) brs -> P (Extract.E.tCase p discr brs)) @@ -438,7 +441,7 @@ Proof. - eauto. - eapply Hcase; try eassumption. + now apply f. - + revert brs H3. + + clear H3; revert brs H4. fix f' 2. intros brs []; [now constructor|]. constructor; [now apply f|now apply f']. @@ -622,6 +625,14 @@ Proof. repeat eapply conj; try eassumption. cbn in *. now rewrite H8, H9. Qed. +Lemma Forall2_nth_error_left {A B} {P} {l : list A} {l' : list B} : Forall2 P l l' -> + forall n x, nth_error l n = Some x -> + exists x', nth_error l' n = Some x' /\ P x x'. +Proof. + induction 1; destruct n; simpl; auto; try discriminate. + intros x' [= ->]. eexists; eauto. +Qed. + Lemma erases_deps_single Σ Σ' Γ t T et : wf_ext Σ -> Σ;;; Γ |- t : T -> @@ -653,6 +664,11 @@ Proof. econstructor; eauto. destruct H2. destruct x1; eauto. destruct H1. eapply Forall2_All2 in H2. eapply All2_nth_error in H2; eauto. + { eapply Forall2_length in H0. eapply All2i_length in brs_ty. + eapply All2_length in X. rewrite <- H0. + depelim H2. destruct H1 as []. + destruct x1 as []. eapply Forall2_nth_error_left in H2 as [x' []]; tea. + rewrite H4 in H2; noconf H2. depelim H7. eapply Forall2_length in H2. lia. } clear -wf brs_ty X H0 Σer. subst predctx ptm. clear X. @@ -711,14 +727,6 @@ Proof. depelim H0; depelim p1; depelim X; cbn in *; try constructor; cbn; intuition eauto. solve_all. Qed. -Lemma Forall2_nth_error_left {A B} {P} {l : list A} {l' : list B} : Forall2 P l l' -> - forall n x, nth_error l n = Some x -> - exists x', nth_error l' n = Some x' /\ P x x'. -Proof. - induction 1; destruct n; simpl; auto; try discriminate. - intros x' [= ->]. eexists; eauto. -Qed. - Lemma erases_global_all_deps Σ Σ' : wf Σ -> erases_global Σ Σ' -> diff --git a/erasure/theories/EGenericGlobalMap.v b/erasure/theories/EGenericGlobalMap.v index 797eedcf3..d209122f9 100644 --- a/erasure/theories/EGenericGlobalMap.v +++ b/erasure/theories/EGenericGlobalMap.v @@ -324,7 +324,7 @@ Proof. destruct g eqn:hg => /= //; intros; rtoProp; eauto. rewrite gen_transform_inductive_decl_id. repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; eauto. solve_all. - - rewrite lookup_env_gen_transform //. + - rewrite /wf_brs. cbn. rewrite lookup_env_gen_transform //. destruct lookup_env eqn:hl => // /=. destruct g eqn:hg => /= //. subst g. rewrite gen_transform_inductive_decl_id. diff --git a/erasure/theories/EGenericMapEnv.v b/erasure/theories/EGenericMapEnv.v index c5a0b4853..1fa0d2bed 100644 --- a/erasure/theories/EGenericMapEnv.v +++ b/erasure/theories/EGenericMapEnv.v @@ -279,7 +279,7 @@ Proof. destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto. destruct g eqn:hg => /= //; intros; rtoProp; eauto. repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; eauto. solve_all. - - rewrite lookup_env_gen_transform //. + - rewrite /wf_brs; cbn. rewrite lookup_env_gen_transform //. destruct lookup_env eqn:hl => // /=. destruct g eqn:hg => /= //. subst g. destruct nth_error => /= //. diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v index 0817566d3..f87ee87fb 100644 --- a/erasure/theories/EImplementBox.v +++ b/erasure/theories/EImplementBox.v @@ -481,7 +481,8 @@ Proof. all: destruct cstr_as_blocks; rtoProp; try split; eauto. + solve_all. + destruct block_args; cbn in *; eauto. - - rewrite lookup_inductive_implement_box. intuition auto. solve_all. + - rewrite /wf_brs; cbn -[lookup_inductive implement_box]. + rewrite lookup_inductive_implement_box. intuition auto. solve_all. solve_all. replace (#|x.1| + S m) with ((#|x.1| + m) + 1) by lia. eapply wellformed_lift. eauto. - rewrite lookup_constructor_implement_box. intuition auto. diff --git a/erasure/theories/EInlineProjections.v b/erasure/theories/EInlineProjections.v index 302b57bc3..c1f930195 100644 --- a/erasure/theories/EInlineProjections.v +++ b/erasure/theories/EInlineProjections.v @@ -74,7 +74,7 @@ Qed. Lemma wellformed_projection_args {efl : EEnvFlags} {Σ p mdecl idecl cdecl pdecl} : wf_glob Σ -> lookup_projection Σ p = Some (mdecl, idecl, cdecl, pdecl) -> - p.(proj_arg) < cdecl.(cstr_nargs). + #|idecl.(ind_ctors)| = 1 /\ p.(proj_arg) < cdecl.(cstr_nargs). Proof. intros wfΣ. rewrite /lookup_projection /lookup_constructor /lookup_inductive. @@ -161,10 +161,10 @@ Section optimize. - rewrite GlobalContextMap.lookup_projection_spec. destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl; auto => //. simpl. - have arglen := wellformed_projection_args wfΣ hl. + have [ncstrs arglen] := wellformed_projection_args wfΣ hl. apply lookup_projection_lookup_constructor, lookup_constructor_lookup_inductive in hl. - rewrite hl /= andb_true_r. - rewrite IHt //=; len. apply Nat.ltb_lt. + rewrite /wf_brs hl /= andb_true_r. + rewrite IHt //=; len. rewrite ncstrs. apply Nat.ltb_lt. lia. - len. rtoProp; solve_all. solve_all. now eapply isLambda_optimize. solve_all. @@ -795,9 +795,11 @@ Proof. rewrite GlobalContextMap.lookup_projection_spec. destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl'; auto => //. simpl. + rewrite /wf_brs. rewrite (lookup_constructor_lookup_inductive (lookup_projection_lookup_constructor hl')) /=. rewrite hrel IHt //= andb_true_r. - have hargs' := wellformed_projection_args wfΣ hl'. + have [-> hargs'] := wellformed_projection_args wfΣ hl'. + rtoProp; intuition auto. apply Nat.ltb_lt. len. - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_optimize. - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. @@ -823,7 +825,7 @@ Proof. destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto. destruct g eqn:hg => /= //; intros; rtoProp; eauto. repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; eauto. solve_all. - - rewrite lookup_env_optimize //. + - rewrite /wf_brs; cbn; rewrite lookup_env_optimize //. destruct lookup_env eqn:hl => // /=. destruct g eqn:hg => /= //. subst g. destruct nth_error => /= //. diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v index 449e36dc8..8c0f5bd2f 100644 --- a/erasure/theories/EOptimizePropDiscr.v +++ b/erasure/theories/EOptimizePropDiscr.v @@ -378,7 +378,9 @@ Proof. - destruct cstr_as_blocks; rtoProp; eauto. f_equal. solve_all. destruct args; inv H2. reflexivity. - rewrite !GlobalContextMap.inductive_isprop_and_pars_spec. assert (map (on_snd (remove_match_on_box Σ)) l = map (on_snd (remove_match_on_box Σ')) l) as -> by solve_all. - rewrite (extends_inductive_isprop_and_pars H0 H1 H2). + assert (iss : isSome (lookup_inductive Σ p.1)). + { move: H2; rewrite /wf_brs; destruct lookup_inductive => //. } + rewrite (extends_inductive_isprop_and_pars H0 H1 iss). destruct inductive_isprop_and_pars as [[[]]|]. destruct map => //. f_equal; eauto. destruct l0 => //. destruct p0 => //. f_equal; eauto. @@ -849,7 +851,7 @@ Proof. destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto. destruct g eqn:hg => /= //; intros; rtoProp; eauto. repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; len; eauto. 1: solve_all. - - rewrite lookup_env_remove_match_on_box //. + - rewrite /wf_brs; cbn. rewrite lookup_env_remove_match_on_box //. destruct lookup_env eqn:hl => // /=. destruct g eqn:hg => /= //. subst g. destruct nth_error => /= //. diff --git a/erasure/theories/EProgram.v b/erasure/theories/EProgram.v index 925bc9f76..e05c56212 100644 --- a/erasure/theories/EProgram.v +++ b/erasure/theories/EProgram.v @@ -18,6 +18,9 @@ Local Obligation Tactic := program_simpl. Import EGlobalEnv EWellformed. +Definition inductive_mapping : Set := Kernames.inductive * (bytestring.string * list nat). +Definition inductives_mapping := list inductive_mapping. + Definition eprogram := (EAst.global_context * EAst.term). Definition eprogram_env := (EEnvMap.GlobalContextMap.t * EAst.term). diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v index 9780299a8..f1a992987 100644 --- a/erasure/theories/ERemoveParams.v +++ b/erasure/theories/ERemoveParams.v @@ -1094,9 +1094,10 @@ Proof. destruct g eqn:hg => /= //. subst g. destruct nth_error => //. destruct nth_error => //. - cbn -[strip]. + rtoProp. move: H2. rewrite /wf_brs; cbn -[strip]. rewrite lookup_env_strip. cbn in H1. destruct lookup_env eqn:hl => // /=. destruct g eqn:hg => /= //. subst g. - destruct nth_error => //. rtoProp; intuition auto. + destruct nth_error => //. rtoProp; intuition auto. len. simp_strip. toAll; solve_all. toAll. solve_all. - cbn -[strip] in H0 |- *. @@ -1142,7 +1143,7 @@ Proof. destruct cstr_as_blocks => //; repeat split; eauto. destruct nth_error => /= //. destruct nth_error => /= //. - - rewrite lookup_env_strip //. + - rewrite /wf_brs; cbn; rewrite lookup_env_strip //. destruct lookup_env eqn:hl => // /=. destruct g eqn:hg => /= //. subst g. destruct nth_error => /= //. diff --git a/erasure/theories/EReorderCstrs.v b/erasure/theories/EReorderCstrs.v index 3e029f23e..71f288ea0 100644 --- a/erasure/theories/EReorderCstrs.v +++ b/erasure/theories/EReorderCstrs.v @@ -1,37 +1,81 @@ -From Coq Require Import List String Arith Lia. +From Coq Require Import List String Arith Lia ssreflect ssrbool Morphisms. Import ListNotations. From Equations Require Import Equations. Set Equations Transparent. From MetaCoq.PCUIC Require Import PCUICAstUtils. From MetaCoq.Utils Require Import MCList bytestring utils monad_utils. -From MetaCoq.Erasure Require Import EPrimitive EAst ESpineView EEtaExpanded EInduction ERemoveParams Erasure EGlobalEnv. +From MetaCoq.Erasure Require Import EProgram EPrimitive EAst ESpineView EEtaExpanded EInduction ERemoveParams Erasure EGlobalEnv + EAstUtils ELiftSubst EWellformed ECSubst EWcbvEval. Import Kernames. Import MCMonadNotation. -Definition inductive_mapping : Set := Kernames.inductive * (bytestring.string * list nat). -Definition inductives_mapping := list inductive_mapping. +Lemma lookup_declared_constructor {Σ id mdecl idecl cdecl} : + lookup_constructor Σ id.1 id.2 = Some (mdecl, idecl, cdecl) -> + declared_constructor Σ id mdecl idecl cdecl. +Proof. + rewrite /lookup_constructor /declared_constructor. + rewrite /declared_inductive /lookup_inductive. + rewrite /declared_minductive /lookup_minductive. + destruct lookup_env => //=. destruct g => //=. + destruct nth_error eqn:hn => //. destruct (nth_error _ id.2) eqn:hn' => //. + intros [= <- <- <-]. intuition auto. +Qed. -Fixpoint lookup_inductive {A} (Σ : list (inductive × A)) (kn : inductive) {struct Σ} : option A := +Fixpoint lookup_inductive_assoc {A} (Σ : list (inductive × A)) (kn : inductive) {struct Σ} : option A := match Σ with | [] => None - | d :: tl => if kn == d.1 then Some d.2 else lookup_inductive tl kn + | d :: tl => if kn == d.1 then Some d.2 else lookup_inductive_assoc tl kn end. -Section Reorder. - Context (Σ : global_declarations). - Context (mapping : inductives_mapping). +Section Tags. - Definition lookup_constructor_mapping i m := - '(tyna, tags) <- lookup_inductive mapping i ;; - List.nth_error tags m. - - Definition lookup_constructor_ordinal i m := - match lookup_constructor_mapping i m with - | None => m - | Some m' => m' + Fixpoint find_tag (l : list nat) (idx : nat) (tag : nat) : option nat := + match l with + | [] => None + | tag' :: tags => if tag == tag' then Some idx + else find_tag tags (S idx) tag end. + (* e.g. for bool: [ 1 0 ], i.e true (0 in Coq) is mapped to 1 and false (1 in Coq) is mapped to 0 *) + Definition new_tag tags tag := find_tag tags 0 tag. + Definition old_tag (tags : list nat) tag := nth_error tags tag. + + (*Lemma old_of_new tags oldidx : + old_tag tags oldidx >>= new_tag tags = Some oldidx. + Proof. + rewrite /old_tag /new_tag. + destruct nth_error eqn:hnth => //=. 2:admit. + revert hnth. + rewrite -{2}[oldidx]Nat.add_0_r. generalize 0. + induction tags in oldidx, n |- *. + - intros n0. now rewrite nth_error_nil. + - cbn. intros n0 hnth. case: eqb_spec. + intros ->. destruct oldidx => //. (* tags are unique *) admit. + intros neq. + destruct oldidx. + * cbn in hnth. now noconf hnth. + * cbn in hnth. rewrite (IHtags oldidx) //. f_equal. lia. + Qed.*) + + Lemma new_tag_spec tags newidx oldidx : + new_tag tags newidx = Some oldidx -> + old_tag tags oldidx = Some newidx. + Proof. + rewrite /old_tag /new_tag. + rewrite -{2}[oldidx]Nat.sub_0_r. generalize 0. + induction tags in oldidx |- *. + - intros n0. now rewrite nth_error_nil. + - cbn. intros n0. case: eqb_spec. + * move=> -> [= ->]. now rewrite Nat.sub_diag. + * intros neq h. specialize (IHtags _ _ h). + case H: (oldidx - n0) => [|n]. + + cbn. assert (oldidx - S n0 = 0). lia. rewrite H0 in IHtags. + destruct tags; cbn in * => //. + noconf IHtags. rewrite eqb_refl in h. noconf h. lia. + + cbn. destruct oldidx; try lia. rewrite Nat.sub_succ in IHtags. + assert (oldidx - n0 = n) by lia. now rewrite H0 in IHtags. + Qed. Definition reorder_list_opt {A} tags (brs : list A) : option (list A) := mapopt (nth_error brs) tags. @@ -39,8 +83,277 @@ Section Reorder. Definition reorder_list {A} tags (l : list A) := option_get l (reorder_list_opt tags l). + Fixpoint one_to_one_map n l := + match n with + | 0 => l == nil + | S n => + existsb (fun x => x == n) l && one_to_one_map n (remove Nat.eq_dec n l) + end. + + Definition wf_tags (l : list nat) := + forallb (fun n => n + Forall (fun tag => tag <> idx) tags. + Proof. + induction tags in n |- *; cbn; auto. + case: eqb_spec => [->|neq] // h. + specialize (IHtags _ h). constructor; auto. + Qed. + + Lemma one_to_one_map_spec l : one_to_one_map #|l| l -> + forall i, i < #|l| <-> In i l. + Proof. + move: (Nat.le_refl #|l|). + generalize #|l| at 2 3 4 as n. induction n in l |- *; cbn. + - move=> hl _ i; split => //. lia. move: l hl; case => //=; try lia. + - move=> hl /andP[] /existsb_exists => [[x [inx xeqn]]] hone i. + specialize (IHn (remove Nat.eq_dec n l)). + apply eqb_eq in xeqn. subst x. + forward IHn. + have hlt := remove_length_lt Nat.eq_dec l n inx. lia. + specialize (IHn hone). + case: (eqb_spec i n) => [->|neq]. intuition auto. + split => hi. assert (i < n) by lia. + now have := proj1 (IHn _) H => /(in_remove Nat.eq_dec). + suff: i < n by lia. apply <- IHn. + apply (in_in_remove Nat.eq_dec) => //. + Qed. + + Lemma find_tag_wf tags idx : + wf_tags tags -> + new_tag tags idx = None -> + #|tags| <= idx. + Proof. + rewrite /wf_tags => /andP[] /forallb_All hwf. + move => /one_to_one_map_spec hone /find_tag_None /Forall_forall hdiff. + case: (Nat.leb_spec #|tags| idx) => // hlt. + elim (hdiff idx). apply hone, hlt. reflexivity. + Qed. + + Lemma mapopt_spec {A B} (f : A -> option B) (l : list A) : + (forall i x, nth_error l i = Some x -> exists x', f x = Some x') -> + exists l', mapopt f l = Some l' /\ + (forall i x, nth_error l i = Some x -> exists x', f x = Some x' /\ nth_error l' i = f x). + Proof. + induction l; cbn. + - intros hf. exists []. split => // i x. rewrite nth_error_nil //. + - intros hf. forward IHl. + { intros i x hx. apply (hf (S i) x hx). } + destruct IHl as [l' [exl' hl']]. + specialize (hf 0 a eq_refl) as [x' eqx']. + destruct (f a) eqn:fa. + * noconf eqx'. rewrite exl'. + eexists; split => //. + intros i x hnth. destruct i; cbn in *. now noconf hnth. + now apply hl'. + * discriminate. + Qed. + + Lemma mapopt_inv_spec {B} (f : nat -> option B) (l : list nat) : + (forall i x, nth_error l i = Some x -> exists x', f x = Some x') -> + exists l', mapopt f l = Some l' /\ #|l| = #|l'| /\ + (forall i x, nth_error l' i = Some x -> exists x', nth_error l i = Some x' /\ f x' = Some x). + Proof. + induction l; cbn. + - intros hf. exists []. split => //; split => // i x. rewrite nth_error_nil //. + - intros hf. forward IHl. + { intros i x hx. apply (hf (S i) x hx). } + destruct IHl as [l' [exl' hl']]. + specialize (hf 0 a eq_refl) as [x' eqx']. + rewrite eqx' exl'. eexists; split => //= //. split => //. lia. + intros. + destruct hl' as [hl hl']. destruct i. cbn in *. noconf H. exists a. now split => //. + now apply hl'. + Qed. + + (*Lemma mapopt_spec' {B} (f : nat -> option B) (l : list nat) : + (forall i x, nth_error l i = Some x -> exists x', f x = Some x') -> + exists l', mapopt f l = Some l' /\ + (forall i x, nth_error l i = Some x -> exists b, f x = Some b /\ nth_error l' x = Some b). + Proof. + induction l; cbn. + - intros hf. exists []. split => // i x. rewrite nth_error_nil //. + - intros hf. forward IHl. + { intros i x hx. apply (hf (S i) x hx). } + destruct IHl as [l' [exl' hl']]. + pose proof (hf 0 a eq_refl) as [x' eqx']. + destruct (f a) eqn:fa => //. + noconf eqx'. rewrite exl'. + eexists; split => //. + intros i x hnth. destruct i; cbn in *. noconf hnth. + * exists x'. split => //. destruct a; cbn. congruence. + apply hl'. + * discriminate. + Qed. *) + + Lemma reorder_list_opt_spec {A} (l : list A) (tags : list nat) (htags : wf_tags tags) : + #|l| = #|tags| -> + exists l', reorder_list_opt tags l = Some l' /\ + (forall i k, old_tag tags i = Some k -> exists x, nth_error l k = Some x /\ nth_error l' i = nth_error l k). + Proof. + rewrite /reorder_list_opt. + rewrite /wf_tags in htags. + intros hlen. + move/andP: htags => [] htags _. + have optH := mapopt_spec (nth_error l) tags. + forward optH. + { intros i x hnth. solve_all. eapply All_nth_error in htags; tea. apply Nat.ltb_lt in htags. + rewrite -hlen in htags. + apply nth_error_Some in htags. destruct (nth_error l x) eqn:hnth'; try congruence. now eexists. } + destruct optH as [l' [heq hl']]. + setoid_rewrite heq. eexists; split => //. + Qed. + + Lemma reorder_list_opt_In {A} (l : list A) (tags : list nat) l' : + reorder_list_opt tags l = Some l' -> + (forall x, In x l' -> In x l). + Proof. + rewrite /reorder_list_opt. + induction tags in l, l' |- *; cbn. + - intros [= <-] x []. + - destruct nth_error eqn:hnth => //. + destruct mapopt eqn:hmap => //. + intros [= <-] x [->|]. + now eapply nth_error_In in hnth. + eapply IHtags; tea. + Qed. + + (* Lemma reorder_list_spec {A} (tags : list nat) (l : list A) n i : + wf_tags tags -> #|l| = #|tags| -> + nth_error tags i = Some n -> + nth_error (reorder_list tags l) i = nth_error l n. + Proof. + intros wft hlt hnth. + rewrite /reorder_list. + now have [l' [-> hnth']] := reorder_list_opt_spec l tags wft hlt. + Qed. *) + + (* Definition reorder_list_spec_maps {A} (l : list A) (tags : list nat) : + forall l', reorder_list_opt tags l = Some l' -> + (forall i k, maps_to tags i k -> nth_error l' k = nth_error l i). + Proof. + intros l'. + induction l; cbn. + - destruct l'; cbn. + intros [=] i k. now rewrite !nth_error_nil. + rewrite /reorder_list_opt /=. + destruct tags => //=. now rewrite nth_error_nil. + - rewrite /reorder_list_opt. *) + + Definition inj_tags (tags : list nat) := + forall i i' k, nth_error tags i = Some k -> nth_error tags i' = Some k -> i = i'. + + Lemma reorder_list_opt_spec' {A} (l : list A) (tags : list nat) (htags : wf_tags tags) : + #|l| = #|tags| -> + (* inj_tags tags -> *) + exists l', reorder_list_opt tags l = Some l' /\ + (forall oldidx a, nth_error l' oldidx = Some a -> + exists newidx, old_tag tags oldidx = Some newidx /\ nth_error l newidx = Some a). + Proof. + rewrite /reorder_list_opt. + rewrite /wf_tags in htags. + move: htags => /andP[] htags hone. + intros hlen. + have optH := mapopt_inv_spec (nth_error l) tags. + forward optH. + { intros i x hnth. solve_all. eapply All_nth_error in htags; tea. apply Nat.ltb_lt in htags. + rewrite -hlen in htags. + apply nth_error_Some in htags. destruct (nth_error l x) eqn:hnth'; try congruence. now eexists. } + destruct optH as [l' [heq hl']]. + setoid_rewrite heq. eexists; split => //. + destruct hl' as [hlen' hl']. + intros newidx a hnth. + specialize (hl' _ _ hnth). + destruct hl' as [x' [eqx' hl']]. exists x'. split => //. + Qed. + + Lemma reorder_list_spec' {A} (tags : list nat) (l : list A) n i x : + wf_tags tags -> #|l| = #|tags| -> + nth_error tags i = Some n -> (* tags[0] = 1 *) + nth_error l n = Some x -> (* l[1] = info *) + nth_error (reorder_list tags l) i = Some x. (* l'[0] = info*) + Proof. + intros wft hlt hnth hnth'. + rewrite /reorder_list. + have [l' [-> hnth'']] := reorder_list_opt_spec l tags wft hlt. + cbn. specialize (hnth'' _ _ hnth). destruct hnth'' as [? []]. congruence. + Qed. + + Lemma reorder_list_spec_inv {A} (tags : list nat) (l : list A) n x : + wf_tags tags -> #|l| = #|tags| -> + nth_error (reorder_list tags l) n = Some x -> (* n is a new index, i an old one *) + exists i, nth_error tags n = Some i /\ nth_error l i = Some x. + Proof. + intros wft hlt. + rewrite /reorder_list. + have [l' [eq hnth'']] := reorder_list_opt_spec' l tags wft hlt; rewrite eq /= => hnth. + specialize (hnth'' _ _ hnth) as [oldidx []]. exists oldidx; now split. + Qed. + + + Lemma reorder_list_old_tag {A} (tags : list nat) (l : list A) oldidx newidx : + wf_tags tags -> #|l| = #|tags| -> + old_tag tags newidx = Some oldidx -> + nth_error (reorder_list tags l) newidx = nth_error l oldidx. + Proof. + rewrite /old_tag. + intros wft hlen ht. + destruct (nth_error l) eqn:hl => //=. + eapply (reorder_list_spec' tags l) in ht; tea. + move: wft => /andP[] wft hone. + solve_all. eapply All_nth_error in wft; tea. + apply Nat.ltb_lt in wft. rewrite -hlen in wft. apply nth_error_None in hl. lia. + Qed. + +(* Lemma reorder_list_old_tag' {A} (tags : list nat) (l : list A) oldidx newidx : + wf_tags tags -> #|l| = #|tags| -> + old_tag tags oldidx = Some newidx -> + nth_error (reorder_list tags l) oldidx = nth_error l newidx. + Proof. + rewrite /old_tag. + intros wft hlen ht. + destruct (nth_error l) eqn:hl => //=. + eapply (reorder_list_spec' tags l) in ht; tea. + move/andP: wft => [] wft hone. + unfold wf_tags in wft. solve_all. eapply All_nth_error in wft; tea. + apply Nat.ltb_lt in wft. rewrite -hlen in wft. apply nth_error_None in hl. lia. + Qed. +*) + + (* Lemma reorder_list_old_tag_inv {A} (tags : list nat) (l : list A) oldidx newidx : + wf_tags tags -> #|l| = #|tags| -> + old_tag tags oldidx = Some newidx -> + nth_error (reorder_list tags l) newidx = nth_error l oldidx. + Proof. + rewrite /old_tag. + intros wft hlen ht. + destruct (nth_error l) eqn:hl => //=. + eapply (reorder_list_spec tags l) in ht; tea. + unfold wf_tags in wft. solve_all. eapply All_nth_error in wft; tea. + apply Nat.ltb_lt in wft. rewrite -hlen in wft. apply nth_error_None in hl. lia. + Qed. *) + + +End Tags. + +Section Reorder. + Context (Σ : global_declarations). + Context (mapping : inductives_mapping). + + Definition lookup_constructor_mapping i c := + '(tyna, tags) <- lookup_inductive_assoc mapping i ;; + new_tag tags c. + + Definition lookup_constructor_ordinal i c := + match lookup_constructor_mapping i c with + | None => c + | Some c' => c' + end. + Definition reorder_branches (i : inductive) (brs : list (list BasicAst.name × term)) : list (list BasicAst.name × term) := - match lookup_inductive mapping i with + match lookup_inductive_assoc mapping i with | None => brs | Some (tyna, tags) => reorder_list tags brs end. @@ -52,11 +365,11 @@ Section Reorder. | tApp fn arg => tApp (reorder fn) (reorder arg) | tConst nm => tConst nm | tConstruct i m args => tConstruct i (lookup_constructor_ordinal i m) (map reorder args) - | tCase i mch brs => tCase i mch (reorder_branches i.1 (map (on_snd reorder) brs)) + | tCase i mch brs => tCase i (reorder mch) (reorder_branches i.1 (map (on_snd reorder) brs)) | tFix mfix idx => tFix (map (map_def reorder) mfix) idx | tCoFix mfix idx => tCoFix (map (map_def reorder) mfix) idx - | tProj (Kernames.mkProjection ind i arg) bod => - tProj (Kernames.mkProjection ind i (lookup_constructor_ordinal ind arg)) (reorder bod) + | tProj p bod => + tProj p (reorder bod) | tPrim p => tPrim (map_prim reorder p) | tLazy t => tLazy (reorder t) | tForce t => tForce (reorder t) @@ -68,25 +381,26 @@ Section Reorder. {| cst_body := option_map reorder cb.(cst_body) |}. Definition reorder_one_ind kn i (oib : one_inductive_body) : one_inductive_body := - match lookup_inductive mapping {| inductive_mind := kn; inductive_ind := i |} with + match lookup_inductive_assoc mapping {| inductive_mind := kn; inductive_ind := i |} with | None => oib | Some (tyna, tags) => {| ind_name := oib.(ind_name); ind_propositional := oib.(ind_propositional); ind_kelim := oib.(ind_kelim); ind_ctors := reorder_list tags oib.(ind_ctors); - ind_projs := reorder_list tags oib.(ind_projs) |} + ind_projs := oib.(ind_projs) |} end. Definition reorder_inductive_decl kn idecl := - {| ind_finite := idecl.(ind_finite); ind_npars := 0; + {| ind_finite := idecl.(ind_finite); ind_npars := idecl.(ind_npars); ind_bodies := mapi (reorder_one_ind kn) idecl.(ind_bodies) |}. Definition reorder_decl d := - match d.2 with - | ConstantDecl cb => (d.1, ConstantDecl (reorder_constant_decl cb)) - | InductiveDecl idecl => (d.1, InductiveDecl (reorder_inductive_decl d.1 idecl)) - end. + let d' := match d.2 with + | ConstantDecl cb => ConstantDecl (reorder_constant_decl cb) + | InductiveDecl idecl => InductiveDecl (reorder_inductive_decl d.1 idecl) + end in + (d.1, d'). Definition reorder_env Σ := map (reorder_decl) Σ. @@ -95,3 +409,1174 @@ End Reorder. Definition reorder_program mapping (p : program) : program := (reorder_env mapping p.1, reorder mapping p.2). + +Definition wf_tags_list (tags : list nat) (n : nat) := + (#|tags| == n) && wf_tags tags. + +Lemma nth_error_reorder {A} {l : list A} {tags n newidx} : + wf_tags_list tags #|l| -> + old_tag tags newidx = Some n -> + nth_error (reorder_list tags l) newidx = nth_error l n. +Proof. + move=> /andP [] h. apply eqb_eq in h. move=> wft hnw. + pose proof (reorder_list_old_tag tags l n newidx wft). + now apply H. +Qed. + +Definition wf_reordering ncstrs cstrs := + (List.length cstrs == ncstrs) && + one_to_one_map ncstrs cstrs. + +Definition wf_inductive_mapping (Σ : global_declarations) (m : inductive_mapping) : bool := + let '(ind, (_, cstrs)) := m in + match EGlobalEnv.lookup_inductive Σ ind with + | Some (mib, oib) => wf_tags_list cstrs #|oib.(ind_ctors)| + | None => true + end. + +Definition wf_inductives_mapping Σ (m : inductives_mapping) : bool := + forallb (wf_inductive_mapping Σ) m. + +Section reorder_proofs. + Context {efl : EEnvFlags}. + Context {wca : cstr_as_blocks = false}. + Context (Σ : global_declarations) (m : inductives_mapping). + Context (wfm : wf_inductives_mapping Σ m). + + Notation optimize := (reorder m). + + Lemma optimize_mkApps f l : optimize (mkApps f l) = mkApps (optimize f) (map optimize l). + Proof using Type. + induction l using rev_ind; simpl; auto. + now rewrite mkApps_app /= IHl map_app /= mkApps_app /=. + Qed. + + Lemma map_optimize_repeat_box n : map optimize (repeat tBox n) = repeat tBox n. + Proof using Type. by rewrite map_repeat. Qed. + + (* move to globalenv *) + + Lemma isLambda_optimize t : isLambda t -> isLambda (optimize t). + Proof. destruct t => //. Qed. + Lemma isBox_optimize t : isBox t -> isBox (optimize t). + Proof. destruct t => //. Qed. + + Lemma lookup_env_reorder kn : lookup_env (reorder_env m Σ) kn = option_map (fun decl => snd (reorder_decl m (kn, decl))) (lookup_env Σ kn). + Proof. + clear wfm. induction Σ; cbn; auto. + case: eqb_spec => [->|hneq] //=. + Qed. + + Lemma lookup_constant_reorder c : option_map (reorder_constant_decl m) (lookup_constant Σ c) = lookup_constant (reorder_env m Σ) c. + Proof. + rewrite /lookup_constant lookup_env_reorder. + destruct lookup_env => //=. + destruct g => //. + Qed. + + Lemma lookup_inductive_reorder i : + lookup_inductive (reorder_env m Σ) i = option_map (fun '(mib, oib) => + (reorder_inductive_decl m i.(inductive_mind) mib, reorder_one_ind m i.(inductive_mind) i.(inductive_ind) oib)) + (lookup_inductive Σ i). + Proof. + unfold lookup_inductive, lookup_minductive. + unfold reorder_env. rewrite lookup_env_reorder. + destruct lookup_env => //=. + destruct g => //. + cbn. rewrite nth_error_mapi. + destruct nth_error => //=. + Qed. + + Lemma lookup_inductive_assoc_spec {ind p} : + wf_inductives_mapping Σ m -> + lookup_inductive_assoc m ind = Some p -> + wf_inductive_mapping Σ (ind, p). + Proof. + clear. rewrite /wf_inductives_mapping. + induction m; cbn -[lookup_inductive wf_inductive_mapping] => //. + destruct eq_inductive eqn:heq => //. + - move=> /andP[] wfa wfi. intros [= <-]. + apply eqb_eq in heq. subst ind. destruct a; apply wfa. + - move=> /andP[] wfa wfi. intros hl. now apply IHi. + Qed. + + Lemma lookup_inductive_assoc_wf_tags {ind mib oib p} : + lookup_inductive Σ ind = Some (mib, oib) -> + lookup_inductive_assoc m ind = Some p -> + wf_tags_list (snd p) #|oib.(ind_ctors)|. + Proof. + move=> hl. + move/(lookup_inductive_assoc_spec wfm). + rewrite /wf_inductive_mapping hl. + now destruct p. + Qed. + + Lemma ind_ctors_reorder {ind mib oib p} : + lookup_inductive Σ ind = Some (mib, oib) -> + lookup_inductive_assoc m ind = Some p -> + ind_ctors (reorder_one_ind m ind.(inductive_mind) ind.(inductive_ind) oib) = + reorder_list p.2 (ind_ctors oib). + Proof. + intros hli hia. + unfold reorder_one_ind. + destruct ind; rewrite hia. destruct p. now cbn. + Qed. + + Lemma ind_ctors_no_reorder {ind mib oib} : + lookup_inductive Σ ind = Some (mib, oib) -> + lookup_inductive_assoc m ind = None -> + ind_ctors (reorder_one_ind m ind.(inductive_mind) ind.(inductive_ind) oib) = + ind_ctors oib. + Proof. + intros hli hia. + unfold reorder_one_ind. + now destruct ind; rewrite hia. + Qed. + + Lemma nth_reorder_list_ctors {i mib oib na tags} : + lookup_inductive Σ i = Some (mib, oib) -> + lookup_inductive_assoc m i = Some (na, tags) -> + forall newidx n, old_tag tags newidx = Some n -> + nth_error (reorder_list tags oib.(ind_ctors)) newidx = nth_error oib.(ind_ctors) n. + Proof. + move=> hli hia idx hnew. + apply nth_error_reorder => //. + eapply (lookup_inductive_assoc_wf_tags (p:=(na, tags))); tea. + Qed. + + Lemma map_opt_length {A B} (f : A -> option B) l : + match mapopt f l with + | None => True + | Some l' => #|l'| = #|l| + end. + Proof. + induction l; cbn; auto. + destruct (f a) => //. + destruct (mapopt f l) => //=. now f_equal. + Qed. + + Lemma reorder_list_length {A} tags (l : list A): #|tags| = #|l| -> #|reorder_list tags l| = #|l|. + Proof. + move=> hl. rewrite /reorder_list. + case hr: reorder_list_opt => [l'|] //=. + move: hr; rewrite /reorder_list_opt. + have := map_opt_length (nth_error l) tags. + destruct mapopt => //. congruence. + Qed. + + Lemma lookup_inductive_assoc_None_reorder_one_ind i oib : + lookup_inductive_assoc m i = None -> + reorder_one_ind m (inductive_mind i) (inductive_ind i) oib = oib. + Proof. + rewrite /reorder_one_ind. destruct i; move => -> //. + Qed. +(* + Lemma lookup_inductive_assoc_None_reorder_inductive_decl i mib : + lookup_inductive_assoc m i = None -> + reorder_inductive_decl m (inductive_mind i) mib = mib. + Proof. + rewrite /reorder_inductive_decl. + intros hl. destruct mib; f_equal. + cbn; induction ind_bodies => //=. f_equal; eauto. + rewrite (lookup_inductive_assoc_None_reorder_one_ind {| inductive_mind := inductive_mind i; inductive_ind := 0 |}). //. + + Qed. *) + Arguments eqb_eq {A H x y}. + Lemma lookup_constructor_reorder i n : + option_map (fun '(mib, oib, c) => (reorder_inductive_decl m (inductive_mind i) mib, reorder_one_ind m (inductive_mind i) (inductive_ind i) oib, c)) (lookup_constructor Σ i n) = + lookup_constructor (reorder_env m Σ) i (lookup_constructor_ordinal m i n). + Proof. + rewrite /lookup_constructor lookup_inductive_reorder. + destruct lookup_inductive as [[mib oib]|] eqn:hind => //=. + destruct nth_error eqn:hnth => //=. + destruct (lookup_inductive_assoc m i) as [(na, tags)|] eqn:hl. + have /andP[] := lookup_inductive_assoc_wf_tags hind hl => //= /eqb_eq => hlen wft. + rewrite (ind_ctors_reorder hind hl). cbn. + destruct (nth_error _ (lookup_constructor_ordinal _ _ _)) eqn:hnth'. + rewrite /lookup_constructor_ordinal /lookup_constructor_mapping in hnth'. + rewrite hl /= in hnth'. + destruct (new_tag tags n) as [newidx|] eqn:ht. + - eapply new_tag_spec in ht. + now rewrite (nth_reorder_list_ctors hind hl _ n) in hnth'. + - move/nth_error_Some_length: hnth. + rewrite /new_tag in ht => hn. + eapply find_tag_wf in ht => //. lia. + - eapply nth_error_None in hnth'. + apply nth_error_Some_length in hnth. + rewrite reorder_list_length in hnth' => //. + move: hnth'. + rewrite /lookup_constructor_ordinal /lookup_constructor_mapping hl /=. + destruct (new_tag tags n) as [newidx|] eqn:ht. + eapply new_tag_spec in ht. + apply nth_error_Some_length in ht. lia. + rewrite /new_tag in ht => hn. + eapply find_tag_wf in ht => //. lia. + - rewrite /lookup_constructor_ordinal /lookup_constructor_mapping hl //=. + destruct i. + rewrite /reorder_one_ind hl //=. now rewrite hnth. + - apply nth_error_None in hnth. + rewrite /lookup_constructor_ordinal /lookup_constructor_mapping /=. + destruct lookup_inductive_assoc eqn:hl => //=. + have /andP[] := lookup_inductive_assoc_wf_tags hind hl => //= /(eqb_eq (A:=nat)) => hlen wft. + destruct p as [na tags]. + destruct (new_tag tags n) as [newidx|] eqn:ht. + + eapply new_tag_spec in ht. + move/andP: wft => [] ht' _. + eapply forallb_All in ht'. eapply All_nth_error in ht'; tea. apply Nat.ltb_lt in ht'. lia. + + rewrite /reorder_one_ind. destruct i; rewrite hl //=. + destruct nth_error eqn:hnth' => //. + apply nth_error_Some_length in hnth'. rewrite reorder_list_length in hnth'. cbn in hlen; lia. lia. + + rewrite lookup_inductive_assoc_None_reorder_one_ind //=. + destruct nth_error eqn:hnth' => //. + apply nth_error_Some_length in hnth'. lia. + Qed. + + Lemma ind_projs_reorder mind ind oib : + ind_projs (reorder_one_ind m mind ind oib) = ind_projs oib. + Proof. + rewrite /reorder_one_ind. destruct lookup_inductive_assoc as [[na tags]|]=> //. + Qed. + + Lemma wf_glob_ind_projs {p pinfo} : + wf_glob Σ -> + lookup_projection Σ p = Some pinfo -> + #|(ind_ctors pinfo.1.1.2)| = 1. + Proof. + intros wf. + rewrite /lookup_projection /lookup_constructor /lookup_inductive /lookup_minductive. + destruct lookup_env eqn:hl => //. + have := lookup_env_wellformed wf hl. + destruct g as [|mib] => //=. + destruct nth_error eqn:hind => //=. + destruct ind_ctors eqn:hctors => //=. + destruct (nth_error (ind_projs o) _) eqn:hprojs => //=. + intros wfmind [= <-]. cbn. + move: wfmind; rewrite /wf_minductive. + move/andP=> [] _ /forallb_All ha. + eapply All_nth_error in ha; tea. + move: ha; rewrite /wf_inductive /wf_projections. + destruct ind_projs => //. now rewrite nth_error_nil in hprojs. + rewrite hctors. destruct l => //. + Qed. + + + Lemma lookup_projection_ordinal p : + wf_glob Σ -> + isSome (lookup_projection Σ p) -> + lookup_constructor_ordinal m (proj_ind p) 0 = 0. + Proof. + move=> wf. + case hl: lookup_projection => [pro|] //= _. + have wfpro := wf_glob_ind_projs wf hl. move: hl. + rewrite /lookup_projection /lookup_constructor_ordinal. + destruct lookup_constructor as [[[mib oib] cb]|] eqn:hlc => //=. + destruct nth_error eqn:nthp => //=. intros [= <-]. cbn in wfpro. + rewrite /lookup_constructor_mapping. + destruct lookup_inductive_assoc as [[na tags]|] eqn:hla => //=. + destruct new_tag eqn:hnt => //=. + eapply new_tag_spec in hnt. + eapply lookup_inductive_assoc_spec in hla; tea. + rewrite /wf_inductive_mapping in hla. + eapply lookup_constructor_lookup_inductive in hlc. rewrite hlc in hla. + move/andP: hla. rewrite wfpro. rewrite /wf_tags => [] [] taglen /andP[] /forallb_All ht. + destruct tags as [|] => //. destruct tags as [|] => //. + destruct n => //. cbn in hnt. now rewrite nth_error_nil in hnt. + Qed. + + Lemma lookup_projection_reorder p : + wf_glob Σ -> + isSome (lookup_projection Σ p) -> + lookup_projection (reorder_env m Σ) p = option_map (fun '(((mib, oib), c), pb) => + (reorder_inductive_decl m p.(proj_ind).(inductive_mind) mib, + reorder_one_ind m p.(proj_ind).(inductive_mind) p.(proj_ind).(inductive_ind) oib, + c, pb)) + (lookup_projection Σ p). + Proof. + intros wf iss. unfold lookup_projection. + rewrite -{1}(lookup_projection_ordinal _ wf iss) -lookup_constructor_reorder. + destruct lookup_constructor eqn:hlc => //=. + destruct p0 as [[mib oib] cb] => //=. + rewrite ind_projs_reorder //=. + destruct nth_error eqn:nthp => //=. + Qed. + + Lemma All_reorder_list {A tags} {P : A -> Prop} {l} : + All P l -> + All P (reorder_list tags l). + Proof. + rewrite /reorder_list. + destruct reorder_list_opt as [l'|] eqn:hre => //=. + have hin := reorder_list_opt_In _ _ _ hre. + move/(All_Forall). + move/(Forall_forall _ _) => hl. + apply Forall_All, Forall_forall. intuition eauto. + Qed. + + Lemma wf_ind_mapping_wf_brs {ind n nas tags} : wf_brs Σ ind n -> + lookup_inductive_assoc m ind = Some (nas, tags) -> + #|tags| = n. + Proof. + rewrite /wf_brs. + destruct lookup_inductive as [[mib oib]|] eqn:hli => //. + move=> /eqb_eq hlen hla. + have := lookup_inductive_assoc_wf_tags hli hla. + rewrite /wf_tags_list /= => /andP[] /eqb_eq hlt _. lia. + Qed. + + Ltac rtoProp ::= + repeat match goal with + | H : is_true (_ && _) |- _ => apply andb_and in H; destruct H + | |- context [is_true (_ && _)] => rewrite andb_and + | H : is_true (_ || _) |- _ => move/orP: H => H; destruct H + | |- context [is_true (_ || _)] => apply/orP + end. + + + + Lemma wf_optimize t k : + wf_glob Σ -> + wellformed Σ k t -> wellformed (reorder_env m Σ) k (optimize t). + Proof using Type wfm wca. + intros wfΣ. + induction t in k |- * using EInduction.term_forall_list_ind; simpl; auto; + intros; try easy; + rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length; + unfold wf_fix_gen, test_def in *; + simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; bool; solve_all]; try easy. + - bool. rewrite -lookup_constant_reorder. destruct lookup_constant => //=; bool. + now destruct (cst_body c) => //=. + - rewrite wca in H *. move/andP: H => [] /andP[] -> iss isnil /=. + rewrite -lookup_constructor_reorder. + destruct lookup_constructor eqn:hl => //=. + destruct args => //. + - rtoProp; intuition auto; solve_all. + * rewrite /reorder_branches. + destruct lookup_inductive_assoc as [[na tags]|] eqn:hl => //=. + have lenreo := wf_ind_mapping_wf_brs H0 hl. + rewrite reorder_list_length. len. len. + move: H0. rewrite /wf_brs. destruct p as [[mind ind] i]. + rewrite lookup_inductive_reorder. destruct lookup_inductive as [[mib oib]|]=> //=. + rewrite /reorder_one_ind hl /=. move/eqb_eq => hl'. rewrite reorder_list_length //. lia. + now apply Nat.eqb_eq. len. + move: H0. rewrite /wf_brs. destruct p as [[mind ind] i]. + rewrite lookup_inductive_reorder. destruct lookup_inductive as [[mib oib]|]=> //=. + rewrite /reorder_one_ind hl /=. move/eqb_eq => hl'. now apply Nat.eqb_eq. + * rewrite /reorder_branches. + destruct lookup_inductive_assoc as [[nas tags]|]. + eapply All_reorder_list. + all:solve_all. + - rtoProp; intuition auto. + rewrite lookup_projection_reorder //. + destruct lookup_projection => //. + - rtoProp; intuition auto; solve_all. + destruct (dbody x) => //. + - rtoProp; intuition auto; solve_all. + depelim H1; constructor; eauto. intuition auto. + cbn; solve_all. + Qed. + + Instance mapopt_ext {A B} : + Proper (pointwise_relation A eq ==> eq ==> eq) (@mapopt A B). + Proof. + intros f g eqfg l ? <-. + induction l; cbn; auto. + rewrite (eqfg a). destruct (g a) => //. + now rewrite IHl. + Qed. + + Lemma mapopt_option_map {A B C} (f : A -> option B) (g : B -> C) l : + mapopt (fun x => option_map g (f x)) l = option_map (map g) (mapopt f l). + Proof. + induction l; cbn; auto. + destruct (f a) => //=. + rewrite IHl. destruct (mapopt f l) => //. + Qed. + + Lemma reorder_list_opt_map {A B} tags (f : A -> B) (l : list A) : + reorder_list_opt tags (map f l) = option_map (map f) (reorder_list_opt tags l). + Proof. + rewrite /reorder_list_opt. + have req : pointwise_relation nat eq (nth_error (map f l)) (fun x => option_map f (nth_error l x)). + { intros x. now rewrite nth_error_map. } + setoid_rewrite req. now rewrite mapopt_option_map. + Qed. + + Lemma reorder_branches_map i f brs : + reorder_branches m i (map f brs) = + map f (reorder_branches m i brs). + Proof. + rewrite /reorder_branches. + destruct lookup_inductive_assoc as [[na tags]|] eqn:hl => //. + rewrite /reorder_list. + rewrite reorder_list_opt_map. + destruct (reorder_list_opt tags brs) => //=. + Qed. + + Lemma optimize_csubst {a k b} n : + wf_glob Σ -> + wellformed Σ (k + n) b -> + optimize (ECSubst.csubst a k b) = ECSubst.csubst (optimize a) k (optimize b). + Proof using Type wfm wca. + intros wfΣ. + induction b in k |- * using EInduction.term_forall_list_ind; simpl; auto; + intros wft; try easy; + rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length; + unfold wf_fix, test_def in *; + simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy. + - destruct (k ?= n0)%nat; auto. + - f_equal. rtoProp. rewrite wca in H0. now destruct args; inv H0. + - move/andP: wft => [] hasc /andP[] /andP[] hi hb hl. rewrite IHb. f_equal. unfold on_snd; solve_all. + repeat toAll. f_equal. solve_all. + rewrite -!reorder_branches_map map_map_compose. cbn. f_equal. + unfold on_snd; cbn. + solve_all. f_equal. unfold optimize in *. + rewrite a0 //. red; rewrite -b0. lia_f_equal. + - move/andP: wft => [] /andP[] hasf hp /andP[] hb hwfm. + f_equal. solve_all. + rewrite /map_def; destruct x => //=. f_equal. + apply a0; cbn in *. red; rewrite -b0. lia_f_equal. + - move/andP: wft => [] hasco /andP[] hp hb. + f_equal. solve_all. + rewrite /map_def; destruct x => //=. f_equal. + apply a0; cbn in *. red; rewrite -b. lia_f_equal. + Qed. + + Lemma optimize_substl s t : + wf_glob Σ -> + forallb (wellformed Σ 0) s -> + wellformed Σ #|s| t -> + optimize (substl s t) = substl (map optimize s) (optimize t). + Proof using Type wfm wca. + intros wfΣ. induction s in t |- *; simpl; auto. + move/andP => [] cla cls wft. + rewrite IHs //. eapply wellformed_csubst => //. + f_equal. rewrite (optimize_csubst (S #|s|)) //. + Qed. + + Lemma optimize_iota_red pars args br : + wf_glob Σ -> + forallb (wellformed Σ 0) args -> + wellformed Σ #|skipn pars args| br.2 -> + optimize (EGlobalEnv.iota_red pars args br) = EGlobalEnv.iota_red pars (map optimize args) (on_snd optimize br). + Proof using Type wfm wca. + intros wfΣ wfa wfbr. + unfold EGlobalEnv.iota_red. + rewrite optimize_substl //. + rewrite forallb_rev forallb_skipn //. + now rewrite List.rev_length. + now rewrite map_rev map_skipn. + Qed. + + Lemma optimize_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def optimize) mfix) = map optimize (EGlobalEnv.fix_subst mfix). + Proof using Type. + unfold EGlobalEnv.fix_subst. + rewrite map_length. + generalize #|mfix|. + induction n; simpl; auto. + f_equal; auto. + Qed. + + Lemma optimize_cofix_subst mfix : EGlobalEnv.cofix_subst (map (map_def optimize) mfix) = map optimize (EGlobalEnv.cofix_subst mfix). + Proof using Type. + unfold EGlobalEnv.cofix_subst. + rewrite map_length. + generalize #|mfix|. + induction n; simpl; auto. + f_equal; auto. + Qed. + + Lemma optimize_cunfold_fix mfix idx n f : + wf_glob Σ -> + wellformed Σ 0 (tFix mfix idx) -> + cunfold_fix mfix idx = Some (n, f) -> + cunfold_fix (map (map_def optimize) mfix) idx = Some (n, optimize f). + Proof using Type wfm wca. + intros wfΣ hfix. + unfold cunfold_fix. + rewrite nth_error_map. + cbn in hfix. move/andP: hfix => [] /andP[] hasfix hlam /andP[] hidx hfix. + destruct nth_error eqn:hnth => //. + intros [= <- <-] => /=. f_equal. + rewrite optimize_substl //. eapply wellformed_fix_subst => //. + rewrite fix_subst_length. + eapply nth_error_forallb in hfix; tea. now rewrite Nat.add_0_r in hfix. + now rewrite optimize_fix_subst. + Qed. + + Lemma optimize_cunfold_cofix mfix idx n f : + wf_glob Σ -> + wellformed Σ 0 (tCoFix mfix idx) -> + cunfold_cofix mfix idx = Some (n, f) -> + cunfold_cofix (map (map_def optimize) mfix) idx = Some (n, optimize f). + Proof using Type wfm wca. + intros wfΣ hfix. + unfold cunfold_cofix. + rewrite nth_error_map. + cbn in hfix. move/andP: hfix => [] hasfix /andP[] hidx hfix. + destruct nth_error eqn:hnth => //. + intros [= <- <-] => /=. f_equal. + rewrite optimize_substl //. eapply wellformed_cofix_subst => //. + rewrite cofix_subst_length. + eapply nth_error_forallb in hfix; tea. now rewrite Nat.add_0_r in hfix. + now rewrite optimize_cofix_subst. + Qed. + +End reorder_proofs. + +Import EGlobalEnv EExtends. + +Lemma extends_lookup_projection {efl : EEnvFlags} {Σ Σ' p} : extends Σ Σ' -> wf_glob Σ' -> + isSome (lookup_projection Σ p) -> + lookup_projection Σ p = lookup_projection Σ' p. +Proof. + intros ext wf. + unfold lookup_projection. + destruct lookup_constructor as [[[mdecl idecl] cdecl]|] eqn:hl => //. + simpl. + rewrite (extends_lookup_constructor wf ext _ _ _ hl) //. +Qed. + +(* +Lemma wellformed_optimize_extends {wfl: EEnvFlags} {Σ} t : + forall n, EWellformed.wellformed Σ n t -> + forall {Σ'}, extends Σ Σ' -> wf_glob Σ' -> + optimize Σ t = optimize Σ' t. +Proof. + induction t using EInduction.term_forall_list_ind; cbn -[lookup_constant lookup_inductive + GlobalContextMap.lookup_projection]; intros => //. + all:unfold wf_fix_gen in *; rtoProp; intuition auto. + 5:{ destruct cstr_as_blocks; rtoProp. f_equal; eauto; solve_all. destruct args; cbn in *; eauto. } + all:f_equal; eauto; solve_all. + - rewrite !GlobalContextMap.lookup_projection_spec. + rewrite -(extends_lookup_projection H0 H1 H3). + destruct lookup_projection as [[[[]]]|]. f_equal; eauto. + now cbn in H3. +Qed. + +Lemma wellformed_reorder_decl_extends {wfl: EEnvFlags} {Σ} t : + wf_global_decl Σ t -> + forall {Σ' : GlobalContextMap.t}, extends Σ Σ' -> wf_glob Σ' -> + reorder_decl Σ t = reorder_decl Σ' t. +Proof. + destruct t => /= //. + intros wf Σ' ext wf'. f_equal. unfold optimize_constant_decl. f_equal. + destruct (cst_body c) => /= //. f_equal. + now eapply wellformed_optimize_extends. +Qed. + +Lemma lookup_env_reorder_env_Some {efl : EEnvFlags} {Σ} kn d : + wf_glob Σ -> + GlobalContextMap.lookup_env Σ kn = Some d -> + ∑ Σ' : GlobalContextMap.t, + [× extends_prefix Σ' Σ, wf_global_decl Σ' d & + lookup_env (reorder_env Σ) kn = Some (reorder_decl Σ' d)]. +Proof. + rewrite GlobalContextMap.lookup_env_spec. + destruct Σ as [Σ map repr wf]. + induction Σ in map, repr, wf |- *; simpl; auto => //. + intros wfg. + case: eqb_specT => //. + - intros ->. cbn. intros [= <-]. + exists (GlobalContextMap.make Σ (fresh_globals_cons_inv wf)). split. + now eexists [_]. + cbn. now depelim wfg. + f_equal. symmetry. eapply wellformed_reorder_decl_extends. cbn. now depelim wfg. + eapply extends_prefix_extends. + cbn. now exists [a]. now cbn. now cbn. + - intros _. + set (Σ' := GlobalContextMap.make Σ (fresh_globals_cons_inv wf)). + specialize (IHΣ (GlobalContextMap.map Σ') (GlobalContextMap.repr Σ') (GlobalContextMap.wf Σ')). + cbn in IHΣ. forward IHΣ. now depelim wfg. + intros hl. specialize (IHΣ hl) as [Σ'' [ext wfgd hl']]. + exists Σ''. split => //. + * destruct ext as [? ->]. + now exists (a :: x). + * rewrite -hl'. f_equal. + clear -wfg. + eapply map_ext_in => kn hin. unfold on_snd. f_equal. + symmetry. eapply wellformed_reorder_decl_extends => //. cbn. + eapply lookup_env_In in hin. 2:now depelim wfg. + depelim wfg. eapply lookup_env_wellformed; tea. + eapply extends_prefix_extends. + cbn. now exists [a]. now cbn. +Qed. + +Lemma lookup_env_map_snd Σ f kn : lookup_env (List.map (on_snd f) Σ) kn = option_map f (lookup_env Σ kn). +Proof. + induction Σ; cbn; auto. + case: eqb_spec => //. +Qed. + +Lemma lookup_env_reorder_env_None {efl : EEnvFlags} {Σ} kn : + GlobalContextMap.lookup_env Σ kn = None -> + lookup_env (reorder_env Σ) kn = None. +Proof. + rewrite GlobalContextMap.lookup_env_spec. + destruct Σ as [Σ map repr wf]. + cbn. intros hl. rewrite lookup_env_map_snd hl //. +Qed. +*) + +Section reorder_mapping. + Context {efl : EEnvFlags}. + Context {wca : cstr_as_blocks = false}. + + Context (mapping : inductives_mapping). + Context (Σ : global_context). + Context (wfm : wf_inductives_mapping Σ mapping). + Notation reorder := (reorder mapping). + Notation reorder_decl := (reorder_decl mapping). + Notation reorder_env := (reorder_env mapping). + +Lemma is_propositional_optimize ind : + wf_glob Σ -> + inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars (reorder_env Σ) ind. +Proof. + rewrite /inductive_isprop_and_pars => wf. + rewrite /lookup_inductive /lookup_minductive. + rewrite lookup_env_reorder. + destruct lookup_env as [[decl|]|] => //=. + rewrite nth_error_mapi. destruct nth_error => //=. + destruct o => //=. rewrite /reorder_one_ind /=. + destruct lookup_inductive_assoc as [[na tags]|]=> //=. +Qed. + +Lemma lookup_inductive_pars_optimize ind : + wf_glob Σ -> + EGlobalEnv.lookup_inductive_pars Σ ind = EGlobalEnv.lookup_inductive_pars (reorder_env Σ) ind. +Proof. + rewrite /lookup_inductive_pars => wf. + rewrite /lookup_inductive /lookup_minductive. + rewrite lookup_env_reorder. + destruct lookup_env as [[decl|]|] => //. +Qed. + +Lemma is_propositional_cstr_optimize ind c : + wf_glob Σ -> + constructor_isprop_pars_decl Σ ind c = constructor_isprop_pars_decl (reorder_env Σ) ind (lookup_constructor_ordinal mapping ind c). +Proof. + rewrite /constructor_isprop_pars_decl => wf. + rewrite -lookup_constructor_reorder //. + destruct lookup_constructor as [[[mib oib] cb]|] => //=. + rewrite /reorder_one_ind. + destruct lookup_inductive_assoc as [[na tags]|]=> //. +Qed. + +Lemma closed_iota_red pars c args brs br : + forallb (closedn 0) args -> + nth_error brs c = Some br -> + #|skipn pars args| = #|br.1| -> + closedn #|br.1| br.2 -> + closed (iota_red pars args br). +Proof. + intros clargs hnth hskip clbr. + rewrite /iota_red. + eapply ECSubst.closed_substl => //. + now rewrite forallb_rev forallb_skipn. + now rewrite List.rev_length hskip Nat.add_0_r. +Qed. + +Lemma isFix_mkApps t l : isFix (mkApps t l) = isFix t && match l with [] => true | _ => false end. +Proof. + induction l using rev_ind; cbn. + - now rewrite andb_true_r. + - rewrite mkApps_app /=. now destruct l => /= //; rewrite andb_false_r. +Qed. + +Lemma constructor_isprop_pars_decl_inductive {ind c} {prop pars cdecl} : + constructor_isprop_pars_decl Σ ind c = Some (prop, pars, cdecl) -> + inductive_isprop_and_pars Σ ind = Some (prop, pars). +Proof. + rewrite /constructor_isprop_pars_decl /inductive_isprop_and_pars /lookup_constructor. + destruct lookup_inductive as [[mdecl idecl]|]=> /= //. + destruct nth_error => //. congruence. +Qed. + +Lemma constructor_isprop_pars_decl_constructor {ind c} {mdecl idecl cdecl} : + lookup_constructor Σ ind c = Some (mdecl, idecl, cdecl) -> + constructor_isprop_pars_decl Σ ind c = Some (ind_propositional idecl, ind_npars mdecl, cdecl). +Proof. + rewrite /constructor_isprop_pars_decl. intros -> => /= //. +Qed. + +Lemma wf_mkApps {hasapp : has_tApp} k f args : + reflect (wellformed Σ k f /\ forallb (wellformed Σ k) args) (wellformed Σ k (mkApps f args)). +Proof. + rewrite wellformed_mkApps //. eapply andP. +Qed. + +Lemma substl_closed s t : closed t -> substl s t = t. +Proof. + induction s in t |- *; cbn => //. + intros clt. rewrite csubst_closed //. now apply IHs. +Qed. + +Lemma substl_rel s k a : + closed a -> + nth_error s k = Some a -> + substl s (tRel k) = a. +Proof. + intros cla. + induction s in k |- *. + - rewrite nth_error_nil //. + - destruct k => //=. + * intros [= ->]. rewrite substl_closed //. + * intros hnth. now apply IHs. +Qed. + +(* EEnvFlags is reorder_env_flags *) +Lemma optimize_correct {fl} t v {withc : with_constructor_as_block = false} : + has_tApp -> + wf_glob Σ -> + @eval fl Σ t v -> + wellformed Σ 0 t -> + @eval fl (reorder_env Σ) (reorder t) (reorder v). +Proof. + intros hastapp wfΣ ev. + induction ev; simpl in *. + + - move/andP => [] /andP[] hasapp cla clt. econstructor; eauto. + - move/andP => [] /andP[] hasapp clf cla. + eapply eval_wellformed in ev2; tea => //. + eapply eval_wellformed in ev1; tea => //. + econstructor; eauto. + move: ev1 => /= /andP[] hasl ev1. + rewrite -(optimize_csubst _ _ wfm 1) //. + apply IHev3. eapply wellformed_csubst => //. + + - move/andP => [] /andP[] haslet clb0 clb1. + intuition auto. + eapply eval_wellformed in ev1; tea => //. + forward IHev2 by eapply wellformed_csubst => //. + econstructor; eauto. rewrite -(optimize_csubst _ _ wfm 1) //. + + - move/andP => [] hascase /andP[] /andP[] hl wfd wfbrs. + rewrite optimize_mkApps in IHev1. + eapply eval_wellformed in ev1 => //. + move/(@wf_mkApps hastapp): ev1 => [] wfc' wfargs. + eapply nth_error_forallb in wfbrs; tea. + rewrite Nat.add_0_r in wfbrs. + forward IHev2. eapply wellformed_iota_red; tea => //. + rewrite (optimize_iota_red _ _ wfm) in IHev2 => //. now rewrite e4. + econstructor; eauto. + rewrite -is_propositional_cstr_optimize //. tea. + rewrite reorder_branches_map nth_error_map. + rewrite /reorder_branches. + rewrite /lookup_constructor_ordinal /lookup_constructor_mapping. + destruct lookup_inductive_assoc as [[na tags]|] eqn:hla => //=. + rewrite /wf_brs in hl. + destruct lookup_inductive as [[mib oib]|] eqn:li => //. apply Nat.eqb_eq in hl. + have wftags := lookup_inductive_assoc_wf_tags _ _ wfm li hla. + have wfmap := lookup_inductive_assoc_spec _ _ wfm hla. + have wfbrl : #|brs| = #|ind_ctors oib|. lia. + have wftbrs : wf_tags_list tags #|brs|. + { now move: wftags; rewrite /wf_tags_list -wfbrl. } + destruct new_tag eqn:hnewt => //=. + * eapply new_tag_spec in hnewt. + rewrite (nth_error_reorder wftbrs hnewt) e2 //. + * move: wftbrs => /andP[] htbrs wftag. + eapply find_tag_wf in wftag; tea. apply nth_error_Some_length in e2. + apply eqb_eq in htbrs. lia. + * rewrite e2 //. + * len. + * len. + + - congruence. + + - move/andP => [] hascase /andP[] /andP[] hl wfd wfbrs. + eapply eval_wellformed in ev1 => //. + move: hl; rewrite /wf_brs. + destruct lookup_inductive as [[mib oib]|] eqn:li => //. move/Nat.eqb_eq. + len. cbn in wfbrs. subst brs. cbn in wfbrs. rewrite Nat.add_0_r in wfbrs. + move/andP: wfbrs => [] wfbrs _. cbn; intros hlen. + forward IHev2. eapply wellformed_substl; tea => //. + rewrite forallb_repeat //. len. + eapply eval_iota_sing; eauto. + rewrite -is_propositional_optimize //. + rewrite /reorder_branches. + destruct lookup_inductive_assoc as [[na tags]|] eqn:hla => //=. + have wftags := lookup_inductive_assoc_wf_tags _ _ wfm li hla. + have wfmap := lookup_inductive_assoc_spec _ _ wfm hla. + have wftbrs : wf_tags_list tags #|[(n, f4)]|. + { move: wftags; rewrite /wf_tags_list //=. now rewrite hlen. } + rewrite //=. + move: wftbrs => /andP[] /Nat.eqb_eq //=. + destruct tags => //=. destruct tags => //= _. + rewrite /wf_tags => /andP[] ht _. move: ht => //= /andP[] /Nat.ltb_lt. + destruct n0 => //. destruct n0 => //. cbn -[substl]. + rewrite (optimize_substl Σ) in IHev2 => //. + * now rewrite forallb_repeat. + * now len. + * now rewrite map_repeat in IHev2. + + - move/andP => [] /andP[] hasapp clf cla. rewrite optimize_mkApps in IHev1. + simpl in *. + eapply eval_wellformed in ev1 => //. + move/(@wf_mkApps hastapp): ev1 => [] wff wfargs. + eapply eval_fix; eauto. + rewrite map_length. + unshelve (eapply optimize_cunfold_fix; tea); tea. + rewrite optimize_mkApps in IHev3. apply IHev3. + rewrite wellformed_mkApps // wfargs. + eapply eval_wellformed in ev2; tas => //. rewrite ev2 /= !andb_true_r. + rewrite hastapp. + eapply wellformed_cunfold_fix; tea. + + - move/andP => [] /andP[] hasapp clf cla. + eapply eval_wellformed in ev1 => //. + move/(@wf_mkApps hastapp): ev1 => [] clfix clargs. + eapply eval_wellformed in ev2; tas => //. + rewrite optimize_mkApps in IHev1 |- *. + simpl in *. eapply eval_fix_value. auto. auto. auto. + unshelve (eapply optimize_cunfold_fix; eauto); tea. + now rewrite map_length. + + - move/andP => [] /andP[] hasapp clf cla. + eapply eval_wellformed in ev1 => //. + eapply eval_wellformed in ev2; tas => //. + simpl in *. eapply eval_fix'. auto. auto. + unshelve (eapply optimize_cunfold_fix; eauto); tea. + eapply IHev2; tea. eapply IHev3. + apply/andP; split => //. + rewrite hastapp. + eapply wellformed_cunfold_fix; tea. + + - move/andP => [] hascase /andP[] /andP[] hl cd clbrs. specialize (IHev1 cd). + eapply eval_wellformed in ev1; tea => //. + move/(@wf_mkApps hastapp): ev1 => [] wfcof wfargs. + forward IHev2. + rewrite hl wellformed_mkApps // /= wfargs clbrs !andb_true_r. + rewrite hascase. + eapply wellformed_cunfold_cofix; tea => //. + rewrite !optimize_mkApps /= in IHev1, IHev2. + eapply eval_cofix_case. tea. + unshelve (eapply optimize_cunfold_cofix; tea); tea. + exact IHev2. + + - move/andP => [] /andP[] hasproj hl hd. + destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl' => //. + eapply eval_wellformed in ev1 => //. + move/(@wf_mkApps hastapp): ev1 => [] wfcof wfargs. + forward IHev2. + { rewrite /= wellformed_mkApps // wfargs andb_true_r hasproj andb_true_r. + eapply wellformed_cunfold_cofix; tea. } + rewrite optimize_mkApps /= in IHev1. + eapply eval_cofix_proj. eauto. + unshelve (eapply optimize_cunfold_cofix; tea); tea. + rewrite optimize_mkApps in IHev2 => //. + + - rewrite /declared_constant in isdecl. + rewrite /lookup_constant. rewrite isdecl /= => _. + destruct decl; cbn in e; subst cst_body. + econstructor. + rewrite /declared_constant. + rewrite lookup_env_reorder isdecl //=. cbn. reflexivity. + eapply IHev. + eapply lookup_env_wellformed in wfΣ; tea. + move: wfΣ. now rewrite /wf_global_decl /=. + + - move=> /andP[] /andP[] hasproj iss cld. + eapply eval_wellformed in ev1; tea => //. + move/(@wf_mkApps hastapp): ev1 => [] wfc wfargs. + destruct lookup_projection as [[[[mdecl idecl] cdecl'] pdecl]|] eqn:hl' => //. + pose proof (lookup_projection_lookup_constructor hl'). + rewrite (constructor_isprop_pars_decl_constructor H) in e1. noconf e1. + forward IHev1 by auto. + forward IHev2. eapply nth_error_forallb in wfargs; tea. + rewrite optimize_mkApps /= in IHev1. + have lp := lookup_projection_reorder _ _ wfm p wfΣ. + forward lp. now rewrite hl'. + rewrite hl' /= in lp. + have lpo := (lookup_projection_ordinal _ _ wfm p wfΣ). + forward lpo by now rewrite hl'. + rewrite lpo in IHev1. + eapply eval_proj; tea. + rewrite -lpo -is_propositional_cstr_optimize //. + rewrite /constructor_isprop_pars_decl // H //= // H0 H1 //. + len. rewrite nth_error_map e3 //. + + - congruence. + + - move/andP => [] /andP[] hasproj hl hd. + eapply eval_proj_prop; eauto. + rewrite -is_propositional_optimize //. + + - move/andP=> [] /andP[] hasapp clf cla. + rewrite optimize_mkApps. + eapply eval_construct; tea. + rewrite -lookup_constructor_reorder //. now rewrite e0 //=. + rewrite optimize_mkApps in IHev1. now eapply IHev1. + now len. + now eapply IHev2. + + - congruence. + + - move/andP => [] /andP[] hasapp clf cla. + specialize (IHev1 clf). specialize (IHev2 cla). + eapply eval_app_cong; eauto. + eapply eval_to_value in ev1. + destruct ev1; simpl in *; eauto. + * depelim a0. + + destruct t => //; rewrite optimize_mkApps /=. + + now rewrite /= !orb_false_r orb_true_r in i. + * destruct with_guarded_fix. + + move: i. + rewrite !negb_or. + rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps + !isLazyApp_mkApps. + destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //. + rewrite !andb_true_r. + rtoProp; intuition auto; destruct v => /= //. + + move: i. + rewrite !negb_or. + rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps. + destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //. + destruct v => /= //. + - intros; rtoProp; intuition eauto. + depelim X; repeat constructor. + eapply All2_over_undep in a. + eapply All2_Set_All2 in ev. eapply All2_All2_Set. primProp. + subst a0 a'; cbn in *. depelim H0; cbn in *. intuition auto; solve_all. + primProp; depelim H0; intuition eauto. + - move=> /andP[] haslazy wf. econstructor; eauto. eapply IHev2. + eapply eval_wellformed in ev1; tea. move/andP: ev1 => []; tea => //. + - destruct t => //. + all:constructor; eauto. + cbn [atom reorder] in i |- *. + rewrite -lookup_constructor_reorder //. + destruct args. 2:cbn in *; eauto. + cbn -[lookup_constructor]. rtoProp; intuition auto. + destruct lookup_constructor => //. +Qed. +End reorder_mapping. + +Lemma wf_inductive_mapping_inv {efl : EEnvFlags} d Σ m : + wf_glob (d :: Σ) -> + wf_inductives_mapping (d :: Σ) m -> + (match d.2 with + | InductiveDecl mib => + (forall i oib, nth_error mib.(ind_bodies) i = Some oib -> + match lookup_inductive_assoc m {| inductive_mind := d.1; inductive_ind := i |} with + | Some (na, tags) => wf_tags_list tags #|oib.(ind_ctors)| + | None => true + end) + | ConstantDecl _ => True + end) /\ wf_inductives_mapping Σ m. +Proof. + rewrite /wf_inductives_mapping. + intros wfΣ wfm. split; revgoals. solve_all. + move: H; rewrite /wf_inductive_mapping. + destruct x as [ind [na tags]]. + destruct lookup_inductive as [[mib oib]|] eqn:li => //=. + depelim wfΣ; cbn. + move: li. cbn. case: eqb_spec. + * intros <-. + destruct d0 => //. destruct nth_error eqn:hnth => //. + intros [= -> ->]. + destruct lookup_env eqn:hle. + have:= lookup_env_Some_fresh hle. contradiction. + auto. + * intros neq. destruct lookup_env => //=. destruct g => //. + destruct nth_error => //. now intros [= -> ->]. + * depelim wfΣ. move: li. cbn; case: eqb_spec. + + intros <-. destruct d0 => //. + destruct lookup_env eqn:hle => //. + have:= lookup_env_Some_fresh hle. contradiction. + destruct lookup_env eqn:hle => //. + have:= lookup_env_Some_fresh hle. contradiction. + + intros neq. destruct lookup_env => //=. destruct g => //. + destruct nth_error => //. + * depelim wfΣ; cbn. + destruct d0 => //. + intros i oib hnth. + destruct lookup_inductive_assoc as [[na tags]|] eqn:hla => //. + have hla' := lookup_inductive_assoc_wf_tags _ _ wfm _ hla. + eapply hla'. + rewrite /lookup_inductive /lookup_minductive /=. + rewrite eqb_refl. rewrite hnth. reflexivity. +Qed. + +From MetaCoq.Erasure Require Import EEtaExpanded. + +Lemma optimize_expanded {Σ m} t : + wf_inductives_mapping Σ m -> expanded Σ t -> expanded (reorder_env m Σ) (reorder m t). +Proof. + intros wfm. + induction 1 using expanded_ind. + all:try solve[constructor; eauto; solve_all]. + all:rewrite ?optimize_mkApps. + - eapply expanded_mkApps_expanded => //. solve_all. + - cbn. econstructor; eauto. + rewrite /reorder_branches. + destruct lookup_inductive_assoc => //; solve_all. + eapply All_reorder_list. solve_all. + - cbn. eapply expanded_tFix. solve_all. + rewrite isLambda_optimize //. + - cbn. + eapply declared_constructor_lookup in H. + have hl := lookup_constructor_reorder _ _ wfm ind idx. rewrite H /= in hl. + eapply expanded_tConstruct_app; tea. + eapply lookup_declared_constructor. now symmetry. + now len. now solve_all. +Qed. + +Lemma optimize_expanded_decl {Σ m kn t} : + wf_inductives_mapping Σ m -> + expanded_decl Σ t -> expanded_decl (reorder_env m Σ) (reorder_decl m (kn, t)).2. +Proof. + destruct t as [[[]]|] => /= //. + unfold expanded_constant_decl => /=. + intros. now apply optimize_expanded. +Qed. + +Lemma reorder_env_expanded {efl : EEnvFlags} {Σ m} : + wf_inductives_mapping Σ m -> + wf_glob Σ -> expanded_global_env Σ -> expanded_global_env (reorder_env m Σ). +Proof. + intros wfm. + unfold expanded_global_env; move=> wfg exp. + induction exp; cbn; constructor; auto. + cbn in IHexp. + unshelve eapply IHexp; tea. eapply wf_inductive_mapping_inv; tea. now depelim wfg. cbn. + unshelve eapply (optimize_expanded_decl). now eapply wf_inductive_mapping_inv. + now destruct decl. +Qed. + +From MetaCoq.Erasure Require Import EEtaExpandedFix. + +Lemma optimize_expanded_fix {Σ Γ m} t : + wf_inductives_mapping Σ m -> expanded Σ Γ t -> expanded (reorder_env m Σ) Γ (reorder m t). +Proof. + intros wfm. + induction 1 using expanded_ind. + all:try solve[constructor; eauto; solve_all]. + all:rewrite ?optimize_mkApps. + - cbn. eapply expanded_tRel_app; tea. len. solve_all. + - cbn. econstructor; eauto. + 2:solve_all. + destruct f3 => //. + - cbn. econstructor; eauto. + rewrite /reorder_branches. + destruct lookup_inductive_assoc => //; solve_all. + eapply All_reorder_list. solve_all. + - cbn. eapply expanded_tFix. solve_all. + rewrite isLambda_optimize //. + now rewrite rev_map_spec map_map_compose /= -rev_map_spec. + solve_all. destruct args => //. rewrite nth_error_map /= H4 //. + len. + - cbn. + eapply declared_constructor_lookup in H. + have hl := lookup_constructor_reorder _ _ wfm ind idx. rewrite H /= in hl. + eapply expanded_tConstruct_app; tea. + eapply lookup_declared_constructor. now symmetry. + now len. now solve_all. +Qed. + +Lemma optimize_expanded_decl_fix {Σ m kn t} : + wf_inductives_mapping Σ m -> + expanded_decl Σ t -> expanded_decl (reorder_env m Σ) (reorder_decl m (kn, t)).2. +Proof. + destruct t as [[[]]|] => /= //. + unfold expanded_constant_decl => /=. + intros. now apply optimize_expanded_fix. +Qed. + +Lemma reorder_env_expanded_fix {efl : EEnvFlags} {Σ m} : + wf_inductives_mapping Σ m -> + wf_glob Σ -> expanded_global_env Σ -> expanded_global_env (reorder_env m Σ). +Proof. + intros wfm. + unfold expanded_global_env; move=> wfg exp. + induction exp; cbn; constructor; auto. + cbn in IHexp. + unshelve eapply IHexp; tea. eapply wf_inductive_mapping_inv; tea. now depelim wfg. cbn. + unshelve eapply (optimize_expanded_decl_fix). now eapply wf_inductive_mapping_inv. + now destruct decl. +Qed. + +Lemma optimize_extends_env {efl : EEnvFlags} {Σ Σ'} m : + wf_inductives_mapping Σ' m -> + extends Σ Σ' -> + wf_glob Σ -> + wf_glob Σ' -> + extends (reorder_env m Σ) (reorder_env m Σ'). +Proof. + intros hast ext wf wf'. + rewrite /extends => kn decl. + rewrite !lookup_env_reorder. + specialize (ext kn). + destruct lookup_env eqn:hle => //. specialize (ext _ eq_refl). + rewrite ext. auto. +Qed. + +Lemma reorder_env_wf {efl : EEnvFlags} {Σ m} + {wcb : cstr_as_blocks = false} : + wf_inductives_mapping Σ m -> + wf_glob Σ -> wf_glob (reorder_env m Σ). +Proof. + intros wfg wfΣ. + induction wfΣ; cbn. constructor; eauto. + have wfdΣ : (wf_glob ((kn, d) :: Σ)) by constructor; auto. + have [wfd wfinv] := (wf_inductive_mapping_inv _ _ _ wfdΣ wfg). cbn in wfd. + constructor; eauto. destruct d; cbn. + - unfold wf_global_decl in H. cbn in H. + destruct (cst_body c) => //=. cbn in H. + unshelve (eapply wf_optimize); eauto. + - cbn in H. rewrite /wf_minductive in H. cbn in H. + rewrite /wf_minductive /=. + move/andP: H => [] -> H /=. solve_all. + have hfa := (forall_nth_error_Alli (fun i oib => + is_true (match lookup_inductive_assoc m {| inductive_mind := kn; inductive_ind := i |} with + | Some p => let (_, tags) := p in wf_tags_list tags #|ind_ctors oib| + | None => true + end)) 0 (ind_bodies m0) wfd). clear wfd. + eapply Alli_All_mix in hfa; tea. clear H. + eapply (Alli_All (P:=fun _ x => wf_inductive x) (n:=0)); eauto. + eapply (fst (Alli_mapi _ _ _)). + eapply Alli_impl; tea. cbn. + intros n x [hla wf]. + rewrite /reorder_one_ind. + destruct lookup_inductive_assoc as [[na tags]|] eqn:hla' => //. + move: wf. rewrite /wf_inductive /wf_projections /=. + destruct ind_projs => //. destruct ind_ctors => //. destruct l0 => //=. + move: hla; rewrite /wf_tags_list. destruct tags => //=. + destruct tags => //=. rewrite /wf_tags. move/andP=> [] hf _. + cbn in hf. rewrite andb_true_r in hf. apply Nat.leb_le in hf. + have -> : n0 = 0 by lia. now cbn. + - cbn. apply ErasureFunction.fresh_global_In. + rewrite map_map_compose /=. intros hin'. apply ErasureFunction.fresh_global_In in H0. + now apply H0. +Qed. + +From MetaCoq.Erasure Require Import EProgram. + +Definition reorder_program_wf {efl : EEnvFlags} {wca : cstr_as_blocks = false} (p : eprogram) m (wfm : wf_inductives_mapping p.1 m) : + wf_eprogram efl p -> wf_eprogram efl (reorder_program m p). +Proof. + intros []; split. + now unshelve eapply reorder_env_wf. + cbn. now eapply (@wf_optimize _ wca). +Qed. + +Definition reorder_program_expanded {efl : EEnvFlags} (p : eprogram) m (wfm : wf_inductives_mapping p.1 m) : + wf_eprogram efl p -> + expanded_eprogram_cstrs p -> expanded_eprogram_cstrs (reorder_program m p). +Proof. + unfold expanded_eprogram_env_cstrs. + move=> [wfe wft] /andP[] etae etat. + apply/andP; split. + cbn. eapply EEtaExpanded.expanded_global_env_isEtaExp_env, reorder_env_expanded => //. + now eapply isEtaExp_env_expanded_global_env. + eapply EEtaExpanded.expanded_isEtaExp. + now apply optimize_expanded, EEtaExpanded.isEtaExp_expanded. +Qed. + +Definition reorder_program_expanded_fix {efl : EEnvFlags} (p : eprogram) m (wfm : wf_inductives_mapping p.1 m) : + wf_eprogram efl p -> + expanded_eprogram p -> expanded_eprogram (reorder_program m p). +Proof. + unfold expanded_eprogram. + move=> [wfe wft] [] etae etat. + split. now eapply reorder_env_expanded_fix. + now eapply optimize_expanded_fix. +Qed. diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v index 47d73387e..5202cef2f 100644 --- a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v +++ b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v @@ -618,7 +618,6 @@ Proof. split; intros; rtoProp; intuition auto; solve_all. - red. move=> hascase n ci discr brs. simpl. - destruct lookup_inductive eqn:hl => /= //. intros; rtoProp; intuition auto; solve_all. - red. simpl. move=> hasproj n p discr wf discr' wf'. simpl. rtoProp; intuition auto. diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v index 955c25c0b..bfedd9f57 100644 --- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v +++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v @@ -517,6 +517,7 @@ Proof. split; intros; rtoProp; intuition auto; solve_all. - red. move=> hascase n ci discr brs. simpl. + rewrite /wf_brs. destruct lookup_inductive eqn:hl => /= //. intros; rtoProp; intuition auto; solve_all. - red. simpl. move=> hasproj n p discr wf discr' wf'. diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v index a3ac397de..8fcd94a95 100644 --- a/erasure/theories/EWcbvEvalNamed.v +++ b/erasure/theories/EWcbvEvalNamed.v @@ -1118,12 +1118,11 @@ Proof. repeat split. len. solve_all. destruct cstr_as_blocks; eauto. rtoProp; intuition eauto. solve_all. destruct args => //. - - destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto. + - move: H0; rewrite /wf_brs; cbn; destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto. erewrite lookup_annotate_env; eauto. cbn. - destruct nth_error as [ [] | ]; cbn in *; eauto. - - destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto. - destruct nth_error as [ [] | ]; cbn in *; eauto. - repeat split. eauto. + destruct nth_error as [ [] | ]; cbn in *; eauto. len. + - move: H0; rewrite /wf_brs; cbn; destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto. + destruct nth_error as [ [] | ]; cbn in *; eauto. intros eq. solve_all. rewrite map_length. rewrite <- app_length. eapply a; eauto. len. rewrite gen_many_fresh_length. eauto. - destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto. diff --git a/erasure/theories/EWellformed.v b/erasure/theories/EWellformed.v index 25037ce0e..84f333032 100644 --- a/erasure/theories/EWellformed.v +++ b/erasure/theories/EWellformed.v @@ -107,7 +107,8 @@ Section wf. - all occuring constructors are defined, - all occuring constants are defined, and - all occuring fixpoints have lambdas as bodies - - if has_axioms is false, all occuring constants have bodies *) + - if has_axioms is false, all occuring constants have bodies + - all cases are exhaustive w.r.t the global declaration *) Definition wf_fix_gen (wf : nat -> term -> bool) k mfix idx := let k' := List.length mfix + k in @@ -115,6 +116,12 @@ Section wf. Definition is_nil {A} (l : list A) := match l with [] => true | _ => false end. + Definition wf_brs ind brsl := + match lookup_inductive Σ ind with + | Some (mib, oib) => #|oib.(ind_ctors)| == brsl + | None => false + end. + Fixpoint wellformed k (t : term) : bool := match t with | tRel i => has_tRel && Nat.ltb i k @@ -124,7 +131,7 @@ Section wf. | tLetIn na b b' => has_tLetIn && wellformed k b && wellformed (S k) b' | tCase ind c brs => has_tCase && let brs' := List.forallb (fun br => wellformed (#|br.1| + k) br.2) brs in - isSome (lookup_inductive Σ ind.1) && wellformed k c && brs' + wf_brs ind.1 #|brs| && wellformed k c && brs' | tProj p c => has_tProj && isSome (lookup_projection Σ p) && wellformed k c | tFix mfix idx => has_tFix && List.forallb (isLambda ∘ dbody) mfix && wf_fix_gen wellformed k mfix idx | tCoFix mfix idx => has_tCoFix && wf_fix_gen wellformed k mfix idx @@ -440,6 +447,19 @@ Proof. intros wfΣ' Hl; apply Hl. Qed. + +Lemma extends_lookup_inductive {efl} {Σ Σ'} : + wf_glob Σ' -> extends Σ Σ' -> + forall ind b, lookup_inductive Σ ind = Some b -> + lookup_inductive Σ' ind = Some b. +Proof. + intros wf ex ind b. + rewrite /lookup_inductive /lookup_minductive. + destruct lookup_env eqn:lookup => //=. + now rewrite (extends_lookup wf ex lookup). +Qed. + + Lemma extends_lookup_constructor {efl} {Σ Σ'} : wf_glob Σ' -> extends Σ Σ' -> forall ind c b, lookup_constructor Σ ind c = Some b -> @@ -482,6 +502,8 @@ Proof. all:try destruct g => //. - destruct cstr_as_blocks; eauto; solve_all. destruct lookup_constructor_pars_args as [ [] | ]; rtoProp; repeat solve_all. + - move: H0. rewrite /wf_brs. destruct lookup_inductive eqn:hl => //. + now rewrite (extends_lookup_inductive wf ex _ _ hl). - move/andP: H0 => [] hn hf. unfold wf_fix. rewrite hn /=. solve_all. - move/andP: H0 => [] hn hf. unfold wf_fix. rewrite hn /=. solve_all. Qed. diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v index 4dcabe930..1dfd6fec1 100644 --- a/erasure/theories/ErasureCorrectness.v +++ b/erasure/theories/ErasureCorrectness.v @@ -195,9 +195,10 @@ Proof. eapply Construct_Ind_ind_eq in X0; tea. 2:{ eapply declared_constructor_from_gen; tea. } destruct X0 as (((([_ Ru] & cu) & cpu) & ?) & (parsubst & argsubst & parsubst' & argsubst' & [])). invs He. - + depelim Hed. + + depelim Hed. rename H5 into Hlen. rename H1 into decli. rename H2 into decli'. rename H3 into em. rename Hed into er. + rename H6 into H5. rename H7 into H6. rename H8 into H7. edestruct (IHeval1 _ scrut_ty) as (v' & Hv' & [He_v']); eauto. pose proof e0 as Hnth. assert (lenppars : ind_npars mdecl = #|pparams p|). @@ -838,7 +839,9 @@ Proof. 2:{ now eapply nth_error_all in a; tea. } invs He. * edestruct IHeval1 as (? & ? & ?); eauto. now depelim Hed. - depelim Hed. + depelim Hed. rename H5 into Hlen. + rename H6 into H5. rename H7 into H6. rename H8 into H7. + rename H9 into H8. rename H10 into H9. unshelve eapply declared_inductive_to_gen in H1, decli; eauto. destruct (declared_inductive_inj H1 decli). subst mdecl0 idecl0. rename H0 into decli'. rename H1 into decli''. rename H2 into er. rename H3 into H0. @@ -1368,7 +1371,7 @@ Proof. depelim etaΣ. eauto. depelim etaΣ. - solve_all. rewrite -b2. len. eapply H7 => //. + solve_all. rewrite -b2. len. eapply H8 => //. exact a0. - intros Γ0 v etaΣ. move=> /erases_mkApps_inv; intros [(?&?&?&?&_&?&?&?)|(?&?&?&?&?)]; subst. diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v index cbebb27ab..34c0e307a 100644 --- a/erasure/theories/ErasureFunction.v +++ b/erasure/theories/ErasureFunction.v @@ -169,6 +169,7 @@ Proof. - destruct p. rewrite KernameSet.union_spec knset_in_fold_left in H0. destruct H0. apply KernameSet.singleton_spec in H0. subst kn. cbn in *. + move: H1; rewrite /EWellformed.wf_brs; cbn. destruct (EGlobalEnv.lookup_env Σ _) eqn:E. destruct g => //. now eapply lookup_env_In in E. easy. clear H1. diff --git a/erasure/theories/ErasureFunctionProperties.v b/erasure/theories/ErasureFunctionProperties.v index c6b674c45..be6884594 100644 --- a/erasure/theories/ErasureFunctionProperties.v +++ b/erasure/theories/ErasureFunctionProperties.v @@ -245,6 +245,9 @@ Proof. eapply erases_deps_tCase; eauto. apply declared_inductive_from_gen; auto. split; eauto. split; eauto. + apply All2_length in X. rewrite -X. + destruct H5. apply Forall2_length in H5. rewrite -H5. + now apply Forall2_length in wf_brs. destruct H1. eapply In_Forall in H3. eapply All_Forall. eapply Forall_All in H3. @@ -350,6 +353,7 @@ Proof. eapply extends_decls_extends, strictly_extends_decls_extends_decls. econstructor; try reflexivity. eexists [(_, _)]; reflexivity. - econstructor; eauto. eapply declared_inductive_from_gen. + rename H3 into Hlen, H4 into H3, H5 into H4. inv wfΣ. inv X. assert (wf Σ) by (inversion H5;econstructor; eauto). unshelve eapply declared_inductive_to_gen in H; eauto. @@ -1451,11 +1455,11 @@ Proof. - cbn. red in H0. rewrite H0 //. - cbn -[lookup_constructor]. cbn. now destruct H0 as [[-> ->] ->]. - - cbn in *. move/andP: H5 => [] cld clbrs. + - cbn in *. move/andP: H6 => [] cld clbrs. cbn. apply/andP; split. apply/andP; split. - * now destruct H0 as [-> ->]. - * now move/andP: H6. - * move/andP: H6; PCUICAstUtils.solve_all. + * rewrite /wf_brs. cbn. destruct H0 as [-> ->]. now apply Nat.eqb_eq. + * now move/andP: H7. + * move/andP: H7; PCUICAstUtils.solve_all. - cbn -[lookup_projection] in *. apply/andP; split; eauto. now rewrite (declared_projection_lookup H0). - cbn in H, H0 |- *. rtoProp; intuition eauto. solve_all_k 7. diff --git a/erasure/theories/ErasureProperties.v b/erasure/theories/ErasureProperties.v index 125ca26b8..06b919b1a 100644 --- a/erasure/theories/ErasureProperties.v +++ b/erasure/theories/ErasureProperties.v @@ -475,6 +475,12 @@ Section wellscoped. Context (Σ : global_env). Import ssrbool. + Definition wf_brs ind brsl := + match lookup_inductive Σ ind with + | Some (mib, oib) => #|oib.(ind_ctors)| == brsl + | None => false + end. + Fixpoint wellformed (t : term) : bool := match t with | tRel i => true @@ -485,7 +491,7 @@ Section wellscoped. | tLetIn na b ty b' => wellformed b && wellformed ty && wellformed b' | tCase ind p c brs => let brs' := forallb (wellformed ∘ bbody) brs in - isSome (lookup_inductive Σ ind.(ci_ind)) && wellformed c && brs' + wf_brs ind.(ci_ind) #|brs| && wellformed c && brs' | tProj p c => isSome (lookup_projection Σ p) && wellformed c | tFix mfix idx => (idx isSome (EGlobalEnv.lookup_inductive Σ' kn). - Proof using g. - destruct g. - destruct (lookup_inductive Σ kn) as [[]|] eqn:hl => /= // _. + Lemma trans_lookup_inductive kn mib oib : + lookup_inductive Σ kn = Some (mib, oib) -> + exists mib' oib', EGlobalEnv.lookup_inductive Σ' kn = Some (mib', oib') /\ #|oib.(ind_ctors)| = #|oib'.(EAst.ind_ctors)|. + Proof. destruct g. + destruct (lookup_inductive Σ kn) as [[]|] eqn:hl => /= // [=]. intros -> ->. eapply lookup_inductive_declared in hl. eapply declared_inductive_from_gen in hl. - specialize (H0 kn m o hl) as [? [? [d _]]]. - now rewrite (EGlobalEnv.declared_inductive_lookup d). + specialize (H0 kn mib oib hl) as [? [? [d er]]]. + exists x, x0. + split. now rewrite (EGlobalEnv.declared_inductive_lookup d). + depelim er. depelim hl. depelim d. + eapply Forall2_nth_error_left in H4 as [x' []]; tea. + rewrite H3 in H4. noconf H4. depelim H6. now apply Forall2_length in H4. Qed. Lemma trans_lookup_constructor kn c : isSome (lookup_constructor Σ kn c) -> isSome (EGlobalEnv.lookup_constructor Σ' kn c). @@ -636,7 +649,11 @@ Proof. - eapply trans_lookup_constructor in wfa; tea. now rewrite wfa. - move/andP: wfa => [] /andP[] lookup wfc wfbrs. apply/andP. split. apply/andP. split; eauto. - eapply trans_lookup_inductive; tea. + { rewrite /wf_brs. + move: lookup. rewrite /ErasureProperties.wf_brs. + destruct lookup_inductive as [[mib oib]|] eqn:hli => //. + eapply trans_lookup_inductive in hli as [mib' [oib' [-> <-]]]; tea. + move/Nat.eqb_eq ->. apply All2_length in X1. now apply Nat.eqb_eq. } eapply All_forallb. unfold tCaseBrsProp_k in X0. eapply All2_All_mix_left in X1; eauto. eapply forallb_All in wfbrs. diff --git a/erasure/theories/Extract.v b/erasure/theories/Extract.v index 3a3f72ee9..ea9d49a2c 100644 --- a/erasure/theories/Extract.v +++ b/erasure/theories/Extract.v @@ -338,6 +338,7 @@ Inductive erases_deps (Σ : global_env) (Σ' : E.global_declarations) : E.term - erases_mutual_inductive_body mdecl mdecl' -> erases_one_inductive_body idecl idecl' -> erases_deps Σ Σ' discr -> + #|EAst.ind_ctors idecl'| = #|brs| -> Forall (fun br => erases_deps Σ Σ' br.2) brs -> erases_deps Σ Σ' (E.tCase p discr brs) | erases_deps_tProj p mdecl idecl cdecl pdecl mdecl' idecl' cdecl' pdecl' t : diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v index a8f685dfc..7850b06fc 100644 --- a/erasure/theories/Typed/OptimizeCorrectness.v +++ b/erasure/theories/Typed/OptimizeCorrectness.v @@ -3611,6 +3611,7 @@ Section dearg. erewrite lookup_ctor_trans_env_inv; tea. - destruct p. rewrite wellformed_mkApps; try easy. unfold dearg_case. + rewrite /wf_brs in H. 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. @@ -3619,15 +3620,18 @@ Section dearg. specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask Hparams]]. rewrite Hmask. rtoProp; intuition eauto; solve_all. - cbn [wellformed]. rtoProp; intuition eauto. + cbn [wellformed]. rtoProp; intuition eauto. len. + rewrite mapi_length map_length. rewrite /wf_brs. { 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 => //. } + rewrite nth_error_mapi. destruct nth_error => //=. + intros [= <- <-]. + move: H; cbn. now rewrite /trans_ctors !map_length !mapi_length. } cbn. - unfold mapi. clear clos_args IHt. + unfold mapi. clear clos_args IHt H. unfold valid_case_masks in H3. rewrite Hmask in H3. move/andP: H3 => [] _ hbrs. eapply alli_Alli in hbrs. diff --git a/examples/metacoq_tour.v b/examples/metacoq_tour.v index 3830aa3de..5b5ba9c1c 100644 --- a/examples/metacoq_tour.v +++ b/examples/metacoq_tour.v @@ -99,7 +99,7 @@ From MetaCoq.ErasurePlugin Require Import Erasure Loader. (** Running erasure live in Coq *) Definition test (p : Ast.Env.program) : string := - erase_and_print_template_program default_erasure_config p. + erase_and_print_template_program default_erasure_config [] p. MetaCoq Quote Recursively Definition zero := 0. diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh index 44164597f..85e2f761a 100755 --- a/safechecker-plugin/clean_extraction.sh +++ b/safechecker-plugin/clean_extraction.sh @@ -9,7 +9,7 @@ fi shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files -files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/` +files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/` if [[ ! -f "src/metacoq_safechecker_plugin.cmxs" || "src/metacoq_safechecker_plugin.cmxs" -ot "theories/Extraction.vo" ]] diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject deleted file mode 100644 index 314e020ac..000000000 --- a/template-coq/_PluginProject +++ /dev/null @@ -1,248 +0,0 @@ -# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh --R ../utils/theories MetaCoq.Utils -R ../common/theories MetaCoq.Common --I gen-src --Q gen-src MetaCoq.Template --R theories MetaCoq.Template -META.coq-metacoq-template-ocaml --I . - -# Generated Code by `ls -1 gen-src/*.ml gen-src/*.mli` in `template-coq/` after having compiled `Extraction.v` -gen-src/all_Forall.ml -gen-src/all_Forall.mli -gen-src/ascii.ml -gen-src/ascii.mli -gen-src/ast0.ml -gen-src/ast0.mli -gen-src/astUtils.ml -gen-src/astUtils.mli -gen-src/ast_denoter.ml -gen-src/ast_quoter.ml -gen-src/basicAst.ml -gen-src/basicAst.mli -gen-src/basics.ml -gen-src/basics.mli -gen-src/binInt.ml -gen-src/binInt.mli -gen-src/binNat.ml -gen-src/binNat.mli -gen-src/binNums.ml -gen-src/binNums.mli -gen-src/binPos.ml -gen-src/binPos.mli -gen-src/binPosDef.ml -gen-src/binPosDef.mli -gen-src/decidableClass.mli -gen-src/decidableClass.ml -gen-src/bool.ml -gen-src/bool.mli -gen-src/byte.ml -gen-src/byte.mli -gen-src/byte0.ml -gen-src/byte0.mli -gen-src/byteCompare.ml -gen-src/byteCompare.mli -gen-src/byteCompareSpec.ml -gen-src/byteCompareSpec.mli -gen-src/bytestring.ml -gen-src/bytestring.mli -gen-src/cRelationClasses.ml -gen-src/cRelationClasses.mli -gen-src/caml_byte.ml -gen-src/caml_byte.mli -gen-src/caml_bytestring.ml -gen-src/caml_nat.ml -gen-src/caml_nat.mli -gen-src/carryType.ml -gen-src/carryType.mli -gen-src/classes0.ml -gen-src/classes0.mli -gen-src/common0.ml -gen-src/common0.mli -gen-src/compare_dec.ml -gen-src/compare_dec.mli -gen-src/config0.ml -gen-src/config0.mli -gen-src/coreTactics.ml -gen-src/coreTactics.mli -gen-src/datatypes.ml -gen-src/datatypes.mli -gen-src/decidableType.ml -gen-src/decidableType.mli -gen-src/decimal.ml -gen-src/decimal.mli -gen-src/denoter.ml -gen-src/depElim.ml -gen-src/depElim.mli -gen-src/envMap.ml -gen-src/envMap.mli -gen-src/environment.ml -gen-src/environment.mli -gen-src/environmentTyping.ml -gen-src/environmentTyping.mli -gen-src/eqDec.ml -gen-src/eqDec.mli -gen-src/eqDecInstances.ml -gen-src/eqDecInstances.mli -gen-src/eqdepFacts.ml -gen-src/eqdepFacts.mli -gen-src/equalities.ml -gen-src/equalities.mli -gen-src/extractable.ml -gen-src/extractable.mli -gen-src/fMapAVL.ml -gen-src/fMapAVL.mli -gen-src/fMapFacts.ml -gen-src/fMapFacts.mli -gen-src/fMapInterface.ml -gen-src/fMapInterface.mli -gen-src/fMapList.ml -gen-src/fMapList.mli -gen-src/floatClass.ml -gen-src/floatClass.mli -gen-src/floatOps.ml -gen-src/floatOps.mli -gen-src/hexadecimal.ml -gen-src/hexadecimal.mli -# gen-src/hexadecimalString.ml -# gen-src/hexadecimalString.mli -gen-src/induction0.ml -gen-src/induction0.mli -gen-src/init.ml -gen-src/init.mli -gen-src/int0.ml -gen-src/int0.mli -gen-src/kernames.ml -gen-src/kernames.mli -gen-src/liftSubst.ml -gen-src/liftSubst.mli -gen-src/list0.ml -gen-src/list0.mli -gen-src/logic0.ml -gen-src/logic0.mli -gen-src/logic1.ml -gen-src/logic1.mli -gen-src/logic2.ml -gen-src/logic2.mli -gen-src/mCCompare.ml -gen-src/mCCompare.mli -gen-src/mCFSets.ml -gen-src/mCFSets.mli -gen-src/mCList.ml -gen-src/mCList.mli -gen-src/mCMSets.ml -gen-src/mCMSets.mli -gen-src/mCOption.ml -gen-src/mCOption.mli -gen-src/mCPrelude.ml -gen-src/mCPrelude.mli -gen-src/mCProd.ml -gen-src/mCProd.mli -gen-src/mCReflect.ml -gen-src/mCReflect.mli -gen-src/mCRelations.ml -gen-src/mCRelations.mli -gen-src/mCString.ml -gen-src/mCString.mli -gen-src/sint63.mli -gen-src/sint63.ml -gen-src/show.mli -gen-src/show.ml -# gen-src/mCUint63.ml -# gen-src/mCUint63.mli -gen-src/mCUtils.ml -gen-src/mCUtils.mli -gen-src/mSetAVL.ml -gen-src/mSetAVL.mli -gen-src/mSetDecide.ml -gen-src/mSetDecide.mli -gen-src/mSetFacts.ml -gen-src/mSetFacts.mli -gen-src/mSetInterface.ml -gen-src/mSetInterface.mli -gen-src/mSetList.ml -gen-src/mSetList.mli -gen-src/mSetProperties.ml -gen-src/mSetProperties.mli -gen-src/monad_utils.ml -gen-src/monad_utils.mli -gen-src/nat0.ml -gen-src/nat0.mli -gen-src/noConfusion.ml -gen-src/noConfusion.mli -gen-src/number.ml -gen-src/number.mli -gen-src/orderedType0.ml -gen-src/orderedType0.mli -gen-src/orderedTypeAlt.ml -gen-src/orderedTypeAlt.mli -gen-src/orders.ml -gen-src/orders.mli -gen-src/ordersAlt.ml -gen-src/ordersAlt.mli -gen-src/ordersFacts.ml -gen-src/ordersFacts.mli -gen-src/ordersLists.ml -gen-src/ordersLists.mli -gen-src/ordersTac.ml -gen-src/ordersTac.mli -gen-src/peanoNat.ml -gen-src/peanoNat.mli -gen-src/plugin_core.ml -gen-src/plugin_core.mli -gen-src/pretty.ml -gen-src/pretty.mli -gen-src/primFloat.ml -gen-src/primFloat.mli -gen-src/primInt63.ml -gen-src/primInt63.mli -gen-src/primitive.ml -gen-src/primitive.mli -gen-src/quoter.ml -gen-src/reflect.ml -gen-src/reflect.mli -gen-src/reflectEq.ml -gen-src/reflectEq.mli -gen-src/reification.ml -gen-src/relation.ml -gen-src/relation.mli -gen-src/run_extractable.ml -gen-src/run_extractable.mli -gen-src/signature.ml -gen-src/signature.mli -gen-src/specFloat.ml -gen-src/specFloat.mli -gen-src/specif.ml -gen-src/specif.mli -gen-src/string0.ml -gen-src/string0.mli -gen-src/sumbool.ml -gen-src/sumbool.mli -gen-src/templateEnvMap.ml -gen-src/templateEnvMap.mli -gen-src/templateProgram.ml -gen-src/templateProgram.mli -gen-src/termEquality.ml -gen-src/termEquality.mli -gen-src/tm_util.ml -gen-src/transform.ml -gen-src/transform.mli -gen-src/typing0.ml -gen-src/typing0.mli -gen-src/uint0.ml -gen-src/uint0.mli -gen-src/universes0.ml -gen-src/universes0.mli -gen-src/wf.ml -gen-src/wf.mli -gen-src/zArith_dec.ml -gen-src/zArith_dec.mli -gen-src/zbool.ml -gen-src/zbool.mli -gen-src/zeven.ml -gen-src/zeven.mli -gen-src/zpower.ml -gen-src/zpower.mli - -gen-src/metacoq_template_plugin.mlpack - -theories/ExtractableLoader.v diff --git a/template-coq/_TemplateCoqProject b/template-coq/_TemplateCoqProject deleted file mode 100644 index 05f7e2517..000000000 --- a/template-coq/_TemplateCoqProject +++ /dev/null @@ -1,32 +0,0 @@ -# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh --R ../utils/theories MetaCoq.Utils -R ../common/theories MetaCoq.Common --I src --Q src MetaCoq.Template --R theories MetaCoq.Template -META.coq-metacoq-template-coq --I . - -# the MetaCoq plugin -src/tm_util.ml - -src/reification.ml -src/quoter.ml -src/denoter.ml -src/constr_reification.ml -src/constr_quoter.ml -src/constr_denoter.ml - -src/g_template_coq.mlg -src/template_coq.mlpack -src/template_monad.mli -src/template_monad.ml -src/run_template_monad.mli -src/run_template_monad.ml -src/plugin_core.mli -src/plugin_core.ml - -theories/Loader.v -theories/All.v - -# A checker of well-formedness in MetaCoq and Coq -theories/TemplateCheckWf.v diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v index d9796c1f1..79d10fdfc 100644 --- a/test-suite/erasure_live_test.v +++ b/test-suite/erasure_live_test.v @@ -18,14 +18,11 @@ Unset MetaCoq Debug. #[local] Existing Instance config.extraction_checker_flags. Definition test (p : Ast.Env.program) : string := - erase_and_print_template_program default_erasure_config p. + erase_and_print_template_program default_erasure_config [] 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. - MetaCoq Quote Recursively Definition zero := 0. Definition zerocst := Eval lazy in test zero. @@ -53,12 +50,7 @@ Definition singlelim := ((fun (X : Set) (x : X) (e : x = x) => Definition erase {A} (a : A) : TemplateMonad unit := aq <- tmQuoteRec a ;; - s <- tmEval lazy (erase_and_print_template_program default_erasure_config aq) ;; - tmMsg s. - -Definition erase_fast {A} (a : A) : TemplateMonad unit := - aq <- tmQuoteRec a ;; - s <- tmEval lazy (erase_fast_and_print_template_program aq) ;; + s <- tmEval lazy (erase_and_print_template_program default_erasure_config [] aq) ;; tmMsg s. MetaCoq Run (erase 0). @@ -80,7 +72,6 @@ Definition vplus0123 := (vplus v01 v23). Set MetaCoq Timing. Time MetaCoq Run (tmEval hnf vplus0123 >>= erase). -Time MetaCoq Run (tmEval hnf vplus0123 >>= erase_fast). (** Cofix *) From Coq Require Import StreamMemo. @@ -352,7 +343,7 @@ MetaCoq Quote Recursively Definition cbv_provedCopyx := Definition ans_provedCopyx := Eval lazy in (test cbv_provedCopyx). MetaCoq Quote Recursively Definition p_provedCopyx := provedCopyx. (* program *) -Time Definition P_provedCopyx := Eval lazy in (test_fast cbv_provedCopyx). +Time Definition P_provedCopyx := Eval lazy in (test cbv_provedCopyx). (* We don't run this one every time as it is really expensive *) (*Time Definition P_provedCopyxvm := Eval vm_compute in (test p_provedCopyx).*)