From 66e14a0506d88492925b218de937bdab60a148de Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Fri, 26 Jan 2024 10:41:59 +0100 Subject: [PATCH 1/2] strengthen principal_type_ind --- pcuic/theories/PCUICPrincipality.v | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/pcuic/theories/PCUICPrincipality.v b/pcuic/theories/PCUICPrincipality.v index 4f3da8802..81654c126 100644 --- a/pcuic/theories/PCUICPrincipality.v +++ b/pcuic/theories/PCUICPrincipality.v @@ -358,13 +358,14 @@ Section Principality. End Principality. -Lemma principal_type_ind {cf:checker_flags} {Σ Γ c ind u u' args args'} {wfΣ: wf_ext Σ} : +Lemma principal_type_ind {cf:checker_flags} {Σ Γ c ind ind' u u' args args'} {wfΣ: wf_ext Σ} : Σ ;;; Γ |- c : mkApps (tInd ind u) args -> - Σ ;;; Γ |- c : mkApps (tInd ind u') args' -> + Σ ;;; Γ |- c : mkApps (tInd ind' u') args' -> (∑ ui', cmp_ind_universes Σ ind #|args| ui' u * - cmp_ind_universes Σ ind #|args'| ui' u') * - ws_cumul_pb_terms Σ Γ args args'. + cmp_ind_universes Σ ind' #|args'| ui' u') * + ws_cumul_pb_terms Σ Γ args args' * + (ind = ind'). Proof. intros h h'. destruct (common_typing _ wfΣ h h') as [C [l [r ty]]]. @@ -374,11 +375,9 @@ Proof. eapply invert_red_mkApps_tInd in redl as [args'' [-> eq0]]; auto. eapply invert_red_mkApps_tInd in redr as [args''' [eqnf eq1]]; auto. solve_discr. - split. + repeat split; eauto. assert (#|args| = #|args'|). now rewrite -(All2_length eqargs) -(All2_length eqargs') (All2_length a) (All2_length a0). - exists ui'. split; auto. - transitivity l'. now symmetry. transitivity args'' => //. now apply red_terms_ws_cumul_pb_terms. transitivity l''. symmetry. auto using red_terms_ws_cumul_pb_terms. @@ -647,7 +646,7 @@ Proof. eapply eq_context_upto_inst_case_context => //. eapply All2_app. 2:constructor; pcuic. specialize (X3 _ _ scrut_ty (eq_term_empty_leq_term X10)). - unshelve epose proof (principal_type_ind scrut_ty X3) as [_ indconv]; tea. + unshelve epose proof (principal_type_ind scrut_ty X3) as [[_ indconv] _]; tea. split; auto. eapply All2_app_inv in indconv as [convpars convinds] => //. exact (All2_length eqpars). @@ -658,7 +657,7 @@ Proof. specialize (X3 _ _ a0 (eq_term_empty_leq_term X4)). eapply eq_term_empty_eq_term in X4. assert (wf_ext Σ) by (split; assumption). - pose proof (principal_type_ind X3 a0) as [Ruu' X3']. + pose proof (principal_type_ind X3 a0) as [[Ruu' X3'] _]. eapply (type_ws_cumul_pb (pb:=Conv)). * clear a0. econstructor; eauto. From 807fc508553158b8ed831fa748f57d0c63b391c7 Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Fri, 26 Jan 2024 10:42:43 +0100 Subject: [PATCH 2/2] verified_erasure_pipeline_lookup_env_in for all decls --- erasure-plugin/theories/ErasureCorrectness.v | 55 +++++++++++--------- 1 file changed, 31 insertions(+), 24 deletions(-) diff --git a/erasure-plugin/theories/ErasureCorrectness.v b/erasure-plugin/theories/ErasureCorrectness.v index 9d2f538a6..fbeac012c 100644 --- a/erasure-plugin/theories/ErasureCorrectness.v +++ b/erasure-plugin/theories/ErasureCorrectness.v @@ -292,17 +292,27 @@ Section PCUICProof. lookup_env Σ kn = Some (PCUICAst.PCUICEnvironment.InductiveDecl decl') -> decl = erase_mutual_inductive_body decl'). + Definition erase_decl_equal cmp decl decl' := + match decl, decl' with + EAst.InductiveDecl decl , InductiveDecl decl' => decl = cmp decl' + | EAst.ConstantDecl _ , ConstantDecl _ => True + | _ , _ => False + end. + Lemma lookup_env_in_erase_global_deps X_type X deps decls kn normalization_in prf decl : EnvMap.EnvMap.fresh_globals decls -> - EGlobalEnv.lookup_env (erase_global_deps X_type deps X decls normalization_in prf).1 kn = Some (EAst.InductiveDecl decl) -> - exists decl', lookup_global decls kn = Some (InductiveDecl decl') /\ decl = erase_mutual_inductive_body decl'. + EGlobalEnv.lookup_env (erase_global_deps X_type deps X decls normalization_in prf).1 kn = Some decl -> + exists decl', lookup_global decls kn = Some decl' /\ + erase_decl_equal erase_mutual_inductive_body decl decl'. Proof. induction decls in deps, X, normalization_in, prf |- *; cbn [erase_global_deps] => //. destruct a => //. destruct g => //. - case: (knset_mem_spec k deps) => // hdeps. cbn [EGlobalEnv.lookup_env fst lookup_env lookup_global]. { destruct (eqb_spec kn k) => //. - intros hl. eapply IHdecls. now depelim hl. } + intro hl; depelim hl; cbn. intro e; noconf e. + eexists; split; eauto. cbn; eauto. + intros hl. cbn. eapply IHdecls. now depelim hl. } { intros hl. depelim hl. intros hl'. eapply IHdecls in hl. destruct hl. @@ -311,12 +321,12 @@ Section PCUICProof. destruct (eqb_spec kn k) => //. subst k. destruct H0. now eapply PCUICWeakeningEnv.lookup_global_Some_fresh in H0. - exact hl'. } + exact hl'. } - intros hf; depelim hf. case: (knset_mem_spec k deps) => // hdeps. cbn [EGlobalEnv.lookup_env fst lookup_env lookup_global]. - { destruct (eqb_spec kn k) => //. - intros hl. noconf hl. subst k. eexists; split; cbn; eauto. + { destruct (eqb_spec kn k) => //; cbn. + intros hl. noconf hl. subst k. eexists; split; cbn; eauto. cbn; eauto. intros hl'. eapply IHdecls => //. tea. } { intros hl'. eapply IHdecls in hf; tea. destruct hf. exists x. @@ -1663,15 +1673,15 @@ Section pipeline_theorem. Import PCUICWfEnv. Lemma verified_erasure_pipeline_lookup_env_in kn decl (efl := EInlineProjections.switch_no_params all_env_flags) {has_rel : has_tRel} {has_box : has_tBox} : - EGlobalEnv.lookup_env Σ_v kn = Some (EAst.InductiveDecl decl) -> + EGlobalEnv.lookup_env Σ_t kn = Some decl -> exists decl', PCUICAst.PCUICEnvironment.lookup_global (PCUICExpandLets.trans_global_decls - (PCUICAst.PCUICEnvironment.declarations - Σ.1)) kn = Some (PCUICAst.PCUICEnvironment.InductiveDecl decl') - /\ decl = ERemoveParams.strip_inductive_decl (erase_mutual_inductive_body decl'). + (PCUICAst.PCUICEnvironment.declarations Σ.1)) kn = Some decl' + /\ erase_decl_equal (fun decl => ERemoveParams.strip_inductive_decl (erase_mutual_inductive_body decl)) + decl decl'. Proof. Opaque compose. - unfold Σ_v, verified_erasure_pipeline. + unfold Σ_t, verified_erasure_pipeline. repeat rewrite -transform_compose_assoc. destruct_compose; intro. cbn. destruct_compose; intro. cbn. @@ -1713,21 +1723,18 @@ Section pipeline_theorem. intro. set (EAstUtils.term_global_deps _). set (build_wf_env_from_env _ _). - epose proof - (lookup_env_in_erase_global_deps optimized_abstract_env_impl w t0 - _ kn _ Hyp0). set (EGlobalEnv.lookup_env _ _). case_eq o. 2: { intros ?. inversion 1. } - destruct g3; intro Ho; [inversion 1|]. - cbn. inversion 1. - specialize (H8 m). forward H8. - epose proof (wf_fresh_globals _ HΣ). clear - H10. - revert H10. cbn. set (Σ.1). induction 1; econstructor; eauto. - cbn. clear -H. induction H; econstructor; eauto. - unfold o in Ho; rewrite Ho in H8. - specialize (H8 eq_refl). - destruct H8 as [decl' [? ?]]. exists decl'; split ; eauto. - rewrite <- H10. now destruct decl, m. + intros decl' Heq. + unshelve epose proof + (Hlookup := lookup_env_in_erase_global_deps optimized_abstract_env_impl w t0 + _ kn _ Hyp0 decl' _ Heq). + { epose proof (wf_fresh_globals _ HΣ). clear - H8. + revert H8. cbn. set (Σ.1). induction 1; econstructor; eauto. + cbn. clear -H. induction H; econstructor; eauto. } + destruct Hlookup as [decl'' [? ?]]. exists decl''; split ; eauto. + cbn in H10. inversion H10. + now destruct decl' , decl''. Qed. Lemma verified_erasure_pipeline_firstorder_evalue_block :