From 2b710a41baea4ec3f66a9a6aa42ec55cf1806f09 Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Wed, 19 Apr 2023 10:13:09 +0200 Subject: [PATCH 1/2] consistency makes us of canonicity --- pcuic/theories/PCUICCanonicity.v | 4 ++-- pcuic/theories/PCUICConsistency.v | 29 +++++++++++++---------------- 2 files changed, 15 insertions(+), 18 deletions(-) diff --git a/pcuic/theories/PCUICCanonicity.v b/pcuic/theories/PCUICCanonicity.v index c4de646dd..84b881bb8 100644 --- a/pcuic/theories/PCUICCanonicity.v +++ b/pcuic/theories/PCUICCanonicity.v @@ -20,7 +20,7 @@ From MetaCoq.PCUIC Require Import PCUICTyping PCUICEquality PCUICAst PCUICAstUti Lemma pcuic_canonicity {cf:checker_flags} {nor : normalizing_flags} Σ {normalization_in: NormalizationIn Σ} t i u args : axiom_free Σ -> wf Σ -> Σ ;;; [] |- t : mkApps (tInd i u) args -> - { t':term & (Σ ;;; [] |- t =s t') * construct_cofix_discr (head t')}. + { t':term & (Σ ;;; [] |- t' : mkApps (tInd i u) args) * (Σ ;;; [] |- t =s t') * construct_cofix_discr (head t')}. Proof. intros axΣ wfΣ typ_ind. pose proof (_ ; typ_ind) as wt. eapply wh_normalization in wt ; eauto. @@ -29,7 +29,7 @@ Proof. pose proof (typ_ind' := typ_ind). eapply subject_reduction in typ_ind; eauto. eapply whnf_classification with (args := args) in typ_ind as ctor; auto. - exists t'; split; eauto. + exists t'; repeat split; eauto. eapply cumulAlgo_cumulSpec. eapply red_ws_cumul_pb. split; eauto. now eapply subject_is_open_term. diff --git a/pcuic/theories/PCUICConsistency.v b/pcuic/theories/PCUICConsistency.v index d5071b5a4..c649d80af 100644 --- a/pcuic/theories/PCUICConsistency.v +++ b/pcuic/theories/PCUICConsistency.v @@ -15,7 +15,7 @@ From MetaCoq.PCUIC Require Import PCUICTyping PCUICEquality PCUICAst PCUICAstUti PCUICParallelReductionConfluence PCUICWcbvEval PCUICClosed PCUICClosedTyp PCUICReduction PCUICCSubst PCUICOnFreeVars PCUICWellScopedCumulativity - PCUICWcbvEval PCUICClassification PCUICSN PCUICNormalization PCUICViews. + PCUICWcbvEval PCUICClassification PCUICCanonicity PCUICSN PCUICNormalization PCUICViews. From Equations Require Import Equations. @@ -46,28 +46,23 @@ Theorem pcuic_consistent {cf:checker_flags} {nor : normalizing_flags} Σ Σ ;;; [] |- t : tInd False_pcuic [] -> False. Proof. intros Hdecl wfΣ axΣ typ_false. - pose proof (_ ; typ_false) as wt. + destruct (pcuic_canonicity Σ t False_pcuic [] []) as [t' [[typ_false' eqtt'] ctor]]; eauto. destruct Hdecl as [Hdecl Hidecl]. destruct False_pcuic as [kn n]. destruct n; cbn in *; [| now rewrite nth_error_nil in Hidecl]. - eapply wh_normalization in wt ; eauto. destruct wt as [empty [Hnormal Hempty]]. - pose proof (Hempty_ := Hempty). - eapply subject_reduction in typ_false; eauto. - eapply ind_whnf_classification with (indargs := []) in typ_false as ctor; auto. - - unfold isConstruct_app in ctor. - destruct decompose_app eqn:decomp. - apply decompose_app_inv in decomp. - rewrite decomp in typ_false. - destruct t0; try discriminate ctor. - apply PCUICValidity.inversion_mkApps in typ_false as H; auto. + rewrite /construct_cofix_discr /head in ctor. + destruct decompose_app eqn:decomp. + apply decompose_app_inv in decomp; subst. + destruct t0; try discriminate ctor. + - apply PCUICValidity.inversion_mkApps in typ_false' as H; auto. destruct H as (?&typ_ctor&_). apply inversion_Construct in typ_ctor as (?&?&?&?&?&?&?); auto. - eapply Construct_Ind_ind_eq with (args' := []) in typ_false; tea. + eapply Construct_Ind_ind_eq with (args' := []) in typ_false'; tea. 2: eauto. destruct (on_declared_constructor d). destruct p. destruct s. destruct p. - destruct typ_false as (((((->&_)&_)&_)&_)&_). + destruct typ_false' as (((((->&_)&_)&_)&_)&_). clear -Hdecl d wfΣ. destruct wfΣ. cbn in *. destruct d as ((?&?)&?). @@ -77,7 +72,9 @@ Proof. cbn in H0. noconf H0. cbn in H1. rewrite nth_error_nil in H1. discriminate. - - unfold notCoInductive, check_recursivity_kind. destruct wfΣ. + - eapply @typing_cofix_coind with (indargs := []) in typ_false'; eauto. + unfold check_recursivity_kind in typ_false'. destruct wfΣ. unshelve eapply declared_minductive_to_gen in Hdecl; eauto. - red in Hdecl. cbn. rewrite Hdecl; cbn. auto. + red in Hdecl. rewrite Hdecl in typ_false'. + cbn in typ_false'. inversion typ_false'. Qed. \ No newline at end of file From 74f668a2f30bc1fda1f5d5c417d6638df5299a31 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 20 Apr 2023 16:32:53 +0200 Subject: [PATCH 2/2] Update INSTALL.md --- INSTALL.md | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index f50f8ad86..1070c62e8 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -67,10 +67,10 @@ to have a dedicated `opam` switch (see below). To get the source code: # git clone https://github.com/MetaCoq/metacoq.git - # git checkout -b coq-8.14 origin/coq-8.14 + # git checkout -b coq-8.16 origin/coq-8.16 # git status -This checks that you are indeed on the `coq-8.14` branch. +This checks that you are indeed on the `coq-8.16` branch. ### Setting up an `opam` switch @@ -109,14 +109,12 @@ the sources directory. Then use: - `make` to compile the `template-coq` plugin, the `pcuic` - development and the `safechecker` and `erasure` plugins. + development and the `safechecker` and `erasure` plugins, + along with the `test-suite`, `translations`, `examples` + and `quotation` libraries. You can also selectively build each target. -- `make translations` to compile the translation plugins - -- `make test-suite` to compile the test suite - -- `make install` to install the plugin in `Coq`'s `user-contrib` local +- `make install` to install the plugins in `Coq`'s `user-contrib` local library. Then the `MetaCoq` namespace can be used for `Require Import` statements, e.g. `From MetaCoq.Template Require Import All.`.