Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generalize lemmas for coq malfunction #1046

Merged
merged 2 commits into from
Jan 26, 2024
Merged

Generalize lemmas for coq malfunction #1046

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
66e14a0
strengthen principal_type_ind
tabareau Jan 26, 2024
807fc50
verified_erasure_pipeline_lookup_env_in for all decls
tabareau Jan 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 31 additions & 24 deletions erasure-plugin/theories/ErasureCorrectness.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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 :
Expand Down
17 changes: 8 additions & 9 deletions pcuic/theories/PCUICPrincipality.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]]].
Expand All @@ -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.
Expand Down Expand Up @@ -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).
Expand All @@ -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.
Expand Down
Loading