Merge pull request #475 from MetaCoq/merge-coq-8.11

Merge coq 8.11

Makefile

@@ -82,5 +82,6 @@ ci-local:
 	$(MAKE) all test-suite
 
 ci-opam:
-	opam install -y .
+	# Use -v so that regular output is produced
+	opam install -v -y .
 	opam remove -y coq-metacoq coq-metacoq-template

README.md

@@ -3,7 +3,6 @@ MetaCoq
 
 <img src="https://raw.githubusercontent.com/MetaCoq/metacoq.github.io/master/assets/LOGO.png" alt="MetaCoq" width="50px"/>
 
-<<<<<<< HEAD
 [![Build Status](https://travis-ci.com/MetaCoq/metacoq.svg?branch=coq-8.12)](https://travis-ci.com/MetaCoq/metacoq)
 [![MetaCoq Chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com)
 
@@ -72,12 +71,9 @@ basic `OCaml` `4.07.1` compiler, and puts you in the right environment
 
 Once in the right switch, you can install `Coq` and the `Equations` package using:
 
-    # opam pin add coq 8.12.0
-    # opam pin add coq-equations 1.2.3+8.12
+    # opam install . --deps-only
 
-Pinning the packages prevents opam from trying to upgrade it afterwards, in
-this switch. If the commands are successful you should have `coq`
-available (check with `coqc -v`). 
+If the commands are successful you should have `coq` available (check with `coqc -v`). 
 
 Installing from GitHub repository (for developers)
 ------------------------------
@@ -104,7 +100,7 @@ Requirements
 
 To compile the library, you need:
 
-- The `Coq` version corrsponding to your branch (you can use the `coq.dev` package 
+- The `Coq` version corresponding to your branch (you can use the `coq.dev` package 
   for the `master` branch).
 - `OCaml` (tested with `4.07.1` and `4.09.1`, beware that `OCaml 4.06.0`
   can produce linking errors on some platforms)

checker/theories/Checker.v

@@ -827,7 +827,7 @@ Lemma lookup_constant_type_is_declared Σ cst u T :
            subst_instance_constr u decl.(cst_type) = fst T }.
 Proof.
   unfold lookup_constant_type_cstrs, lookup_env, declared_constant.
-  destruct Typing.lookup_env eqn:Hlook; try discriminate.
+  destruct Ast.lookup_env eqn:Hlook; try discriminate.
   destruct g eqn:Hg; intros; try discriminate. destruct c.
   injection H as eq. subst T. simpl.
   eexists. split; eauto.

checker/theories/WcbvEval.v

@@ -158,8 +158,8 @@ Section Wcbv.
       eval (tCase (ind, pars) p discr brs) res
 
   (** Proj *)
-  | eval_proj i pars arg discr args k u a res :
-      eval discr (mkApps (tConstruct i k u) args) ->
+  | eval_proj i pars arg discr args u a res :
+      eval discr (mkApps (tConstruct i 0 u) args) ->
       nth_error args (pars + arg) = Some a ->
       eval a res ->
       eval (tProj (i, pars, arg) discr) res
@@ -238,10 +238,10 @@ Section Wcbv.
           eval discr (mkApps (tConstruct ind c u) args) ->
           P discr (mkApps (tConstruct ind c u) args) ->
           eval (iota_red pars c args brs) res -> P (iota_red pars c args brs) res -> P (tCase (ind, pars) p discr brs) res) ->
-      (forall (i : inductive) (pars arg : nat) (discr : term) (args : list term) (k : nat) (u : Instance.t)
+      (forall (i : inductive) (pars arg : nat) (discr : term) (args : list term) (u : Instance.t)
               (a res : term),
-          eval discr (mkApps (tConstruct i k u) args) ->
-          P discr (mkApps (tConstruct i k u) args) ->
+          eval discr (mkApps (tConstruct i 0 u) args) ->
+          P discr (mkApps (tConstruct i 0 u) args) ->
           nth_error args (pars + arg) = Some a -> eval a res -> P a res -> P (tProj (i, pars, arg) discr) res) ->
       (forall (f : term) (mfix : mfixpoint term) (idx : nat) (fixargsv args argsv : list term)
              (narg : nat) (fn res : term),

checker/theories/Weakening.v

@@ -1078,9 +1078,8 @@ Proof.
       split; auto.
       apply All_local_env_app_inv; intuition auto.
       clear -wf a.
-      induction ctx; try constructor.
-      depelim a.
-      -- rewrite lift_context_snoc.
+      induction ctx; try constructor; depelim a.
+      -- rewrite lift_context_snoc.         
          constructor; auto.
          eapply IHctx. eapply a.
          simpl. destruct tu as [u tu]. exists u.

checker/theories/WeakeningEnv.v

@@ -163,6 +163,14 @@ Proof.
     repeat split; eauto using eq_term_upto_univ_morphism0.
 Qed.
 
+Lemma eq_term_subset {cf:checker_flags} φ φ' t t'
+  : ConstraintSet.Subset φ φ'
+    -> eq_term φ t t' ->  eq_term φ' t t'.
+Proof.
+  intro H. apply eq_term_upto_univ_morphism.
+  all: intros u u'; eapply eq_universe_subset; assumption.
+Qed.
+
 Lemma leq_term_subset {cf:checker_flags} ctrs ctrs' t u
   : ConstraintSet.Subset ctrs ctrs' -> leq_term ctrs t u -> leq_term ctrs' t u.
 Proof.
@@ -172,6 +180,21 @@ Proof.
 Qed.
 
 
+Lemma weakening_env_conv `{CF:checker_flags} Σ Σ' φ Γ M N :
+  wf Σ' ->
+  extends Σ Σ' ->
+  conv (Σ, φ) Γ M N ->
+  conv (Σ', φ) Γ M N.
+Proof.
+  intros wfΣ [Σ'' ->].
+  induction 1; simpl.
+  - econstructor. eapply eq_term_subset.
+    + eapply global_ext_constraints_app.
+    + assumption. 
+  - econstructor 2; eauto. eapply weakening_env_red1; eauto. exists Σ''; eauto.
+  - econstructor 3; eauto. eapply weakening_env_red1; eauto. exists Σ''; eauto.
+Qed.
+
 Lemma weakening_env_cumul `{CF:checker_flags} Σ Σ' φ Γ M N :
   wf Σ' -> extends Σ Σ' ->
   cumul (Σ, φ) Γ M N -> cumul (Σ', φ) Γ M N.
@@ -252,14 +275,6 @@ Proof.
   apply global_ext_constraints_app.
 Qed.
 
-Lemma eq_term_subset {cf:checker_flags} φ φ' t t'
-  : ConstraintSet.Subset φ φ'
-    -> eq_term φ t t' ->  eq_term φ' t t'.
-Proof.
-  intro H. apply eq_term_upto_univ_morphism.
-  all: intros u u'; eapply eq_universe_subset; assumption.
-Qed.
-
 Lemma eq_decl_subset {cf:checker_flags} φ φ' d d'
   : ConstraintSet.Subset φ φ'
     -> eq_decl φ d d' ->  eq_decl φ' d d'.
@@ -379,6 +394,15 @@ Proof.
       revert on_cindices.
       generalize (List.rev (LiftSubst.lift_context #|cshape_args cs| 0 ind_indices)).
       generalize (cshape_indices cs). induction 1; constructor; eauto.
+      simpl.
+      intros v indv. specialize (on_ctype_variance v indv).
+      simpl in *. move: on_ctype_variance.
+      unfold respects_variance. destruct variance_universes as [[[univs u] u']|]; auto.
+      intros [args idxs]. split.
+      eapply (All2_local_env_impl args); intros.
+      eapply weakening_env_cumul; eauto.
+      eapply (All2_impl idxs); intros.
+      eapply weakening_env_conv; eauto.
     -- unfold check_ind_sorts in *. destruct universe_family; auto.
       --- split; [apply fst in ind_sorts|apply snd in ind_sorts].
           eapply Forall_impl; tea; cbn.

erasure/theories/EArities.v

@@ -4,7 +4,7 @@ From MetaCoq.Template Require Import config utils monad_utils.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils 
   PCUICClosed PCUICTyping PCUICWcbvEval PCUICLiftSubst PCUICInversion PCUICArities
   PCUICSR PCUICPrincipality PCUICGeneration PCUICSubstitution PCUICElimination
-  PCUICContextConversion PCUICConversion.
+  PCUICContextConversion PCUICConversion PCUICCanonicity.
 
 From Equations Require Import Equations.
 Local Open Scope string_scope.
@@ -61,35 +61,6 @@ Lemma isWfArity_prod_inv:
     unfold snoc, app_context in *. rewrite <- app_assoc in *. eassumption.
 Qed.
 
-Lemma isArity_subst:
-  forall x2 : term, forall s n, isArity x2 -> isArity (subst s n x2).
-Proof.
-  induction x2; cbn in *; try tauto; intros; eauto.
-Qed.
-
-Lemma isArity_typing_spine:
-  forall (Σ : global_env_ext) (Γ : context) (L : list term) (T x4 : term),
-    wf Σ -> wf_local Σ Γ ->
-    Is_conv_to_Arity Σ Γ x4 -> typing_spine Σ Γ x4 L T -> Is_conv_to_Arity Σ Γ T.
-Proof.
-  intros.
-  depind X1.
-  - destruct H as (? & ? & ?). sq.
-    eapply PCUICCumulativity.red_cumul_inv in H.
-    eapply (cumul_trans _ _ _ _ _) in c; tea.
-    eapply invert_cumul_arity_l in c; eauto.
-  - eapply IHX1.
-    destruct H as (? & ? & ?). sq.
-    eapply PCUICCumulativity.red_cumul_inv in H.
-    eapply (cumul_trans _ _ _ _ _) in c; tea.
-    eapply invert_cumul_arity_l in c; eauto.
-    destruct c as (? & H1 & H2). sq.
-    eapply invert_red_prod in H1 as (? & ? & [] & ?); eauto; subst.
-    exists (x2 {0 := hd}). split; sq.
-    eapply (PCUICSubstitution.substitution_red Σ Γ [_] [] [_]). eauto. econstructor. econstructor.
-    rewrite subst_empty. eassumption. eauto. cbn. eassumption. cbn in H2.
-    now eapply isArity_subst.
-Qed.
 
 Lemma inds_nth_error ind u l n t :
   nth_error (inds ind u l) n = Some t -> exists n, t = tInd {| inductive_mind := ind ; inductive_ind := n |} u.
@@ -547,14 +518,12 @@ Qed.
 
 Lemma Is_type_eval (Σ : global_env_ext) t v:
   wf Σ ->
+  axiom_free Σ ->
   eval Σ t v ->
   isErasable Σ [] t ->
   isErasable Σ [] v.
 Proof.
   intros; eapply Is_type_red. eauto.
-  eapply wcbeval_red; eauto.
   red in X1. destruct X1 as [T [HT _]].
-  eapply typecheck_closed in HT as [_ HT]; auto. 
-  apply andP in HT. now destruct HT.
-  eauto.
+  eapply wcbeval_red; eauto. assumption.
 Qed.