Merge pull request #536 from yforster/8.11_into_8.12

Merge again 8.11 into 8.12

Author: mattam82

Makefile

@@ -72,7 +72,7 @@ erasure: template-coq safechecker pcuic
 checker: template-coq
 	$(MAKE) -C checker
 
-examples: template-coq checker
+examples: checker safechecker
 	$(MAKE) -C examples
 
 test-suite: template-coq checker safechecker erasure

README.md

@@ -4,8 +4,7 @@
 <img src="https://raw.githubusercontent.com/MetaCoq/metacoq.github.io/master/assets/LOGO.png" alt="MetaCoq" width="50px"/>
 </p>
 
-[![Build status](https://github.com/MetaCoq/metacoq/workflows/Test%20compilation/badge.svg?branch=coq-8.12)](https://github.com/MetaCoq/metacoq/actions)
-[![MetaCoq Chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com)
+[![Build status](https://github.com/MetaCoq/metacoq/workflows/Test%20compilation/badge.svg?branch=coq-8.12)](https://github.com/MetaCoq/metacoq/actions) [![MetaCoq Chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com)
 
 MetaCoq is a project formalizing Coq in Coq and providing tools for
 manipulating Coq terms and developing certified plugins

TODO.md

@@ -2,6 +2,8 @@
 
 - `assumption_context` should be a boolean function.
 
+- remove duplication of eq_context / eq_context_upto  and eq_decl / eq_decl_upto
+
 - Rename `mkApps_nested` into `mkApps_app` (et inverser la direction de la
   règle)
 
@@ -34,6 +36,20 @@
 
 # Big projects
 
+- Refine the longest-simple-path algorithm on universes with the 
+  Bender & al algorithm used in Coq, extended with edges of negative weight.
+  Alternatively prove the spec for that algorithm. Refinement might be easier:
+  it amounts to show that the new algorithm calculates the longest simple
+  path between two universes. 
+
+- Verify parsing and printing of terms / votour
+
+- Primivite projections: we could be more relaxed on the elimination sort of the 
+  inductive. If it is e.g. InProp, then all projections to types in Prop should
+  be definable. Probably not very useful though because if the elimination is 
+  restricted then it means some Type is in the constructor and won't be projectable.
+  
+
 ## Website
 
 Put a demo using JS-coq on the webiste
@@ -55,10 +71,3 @@ into β-redexes, hence it is only β-convertible and not a syntactical equality.
 
 - Deduce that we have weakening and substitution lemmas in Template from those of
   PCUIC.
-
-
-## Finish Safechecker correctness
-
-- `valid_btys`
-
-- `check_one_body`

checker/theories/Closed.v

@@ -289,6 +289,24 @@ Proof.
     now rewrite andb_true_r in b.
 Qed.
 
+Lemma sorts_local_ctx_Pclosed Σ Γ Δ s :
+  sorts_local_ctx (lift_typing Pclosed) Σ Γ Δ s ->
+  Alli (fun i d => closed_decl (#|Γ| + i) d) 0 (List.rev Δ).
+Proof.
+  induction Δ in s |- *; simpl; auto; try constructor.  
+  destruct a as [? [] ?]; intuition auto.
+  - apply Alli_app_inv; eauto. constructor. simpl.
+    rewrite List.rev_length. 2:constructor.
+    unfold closed_decl. unfold Pclosed in b0. simpl.
+    rewrite app_context_length in b0. now rewrite Nat.add_comm.
+  - destruct s; auto. destruct X.
+    apply Alli_app_inv; eauto. constructor. simpl.
+    rewrite List.rev_length. 2:constructor.
+    unfold closed_decl. unfold Pclosed in i. simpl.
+    rewrite app_context_length in i. rewrite Nat.add_comm.
+    now rewrite andb_true_r in i.
+Qed.
+
 Lemma All_local_env_Pclosed Σ Γ :
   All_local_env ( lift_typing Pclosed Σ) Γ ->
   Alli (fun i d => closed_decl i d) 0 (List.rev Γ).
@@ -413,7 +431,7 @@ Proof.
   eapply closedn_lift.
   clear -parslen isdecl Heq' onpars X.
   rename X into args.
-  apply type_local_ctx_Pclosed in args.
+  apply sorts_local_ctx_Pclosed in args.
   red in onpars.
   eapply All_local_env_Pclosed in onpars.
   eapply (Alli_impl (Q:=fun i d => closed_decl (#|ind_params mdecl| + i + #|arities_context (ind_bodies mdecl)|) d)) in args.

checker/theories/WeakeningEnv.v

@@ -102,15 +102,23 @@ Proof.
   - simpl. apply ConstraintSet.union_spec. right; eauto.
 Qed.
 
+Lemma satisfies_subset φ φ' val :
+  ConstraintSet.Subset φ φ' ->
+  satisfies val φ' ->
+  satisfies val φ.
+Proof.
+  intros sub sat ? isin.
+  apply sat, sub; auto.
+Qed.
+
 Lemma leq_universe_subset {cf:checker_flags} ctrs ctrs' t u
   : ConstraintSet.Subset ctrs ctrs'
     -> leq_universe ctrs t u -> leq_universe ctrs' t u.
 Proof.
   intros Hctrs H. unfold leq_universe in *.
   destruct check_univs; [|trivial].
   intros v Hv. apply H.
-  intros ctr Hc. apply Hv.
-  apply Hctrs; eauto.
+  eapply satisfies_subset; eauto.
 Qed.
 
 Lemma eq_universe_subset {cf:checker_flags} ctrs ctrs' t u
@@ -120,8 +128,7 @@ Proof.
   intros Hctrs H. unfold eq_universe in *.
   destruct check_univs; [|trivial].
   intros v Hv. apply H.
-  intros ctr Hc. apply Hv.
-  apply Hctrs; eauto.
+  eapply satisfies_subset; eauto.
 Qed.
 
 
@@ -204,6 +211,22 @@ Proof.
   - econstructor 3; eauto. eapply weakening_env_red1; eauto. exists Σ''; eauto.
 Qed.
 
+Lemma weakening_env_is_allowed_elimination `{CF:checker_flags} Σ Σ' φ u allowed :
+  wf Σ' -> extends Σ Σ' ->
+  is_allowed_elimination (global_ext_constraints (Σ, φ)) u allowed ->
+  is_allowed_elimination (global_ext_constraints (Σ', φ)) u allowed.
+Proof.
+  intros wfΣ [Σ'' ->] al.
+  unfold is_allowed_elimination in *.
+  destruct check_univs; auto.
+  intros val sat.
+  unshelve epose proof (al val _) as al.
+  { eapply satisfies_subset; eauto.
+    apply global_ext_constraints_app. }
+  destruct allowed; auto; cbn in *; destruct ?; auto.
+Qed.
+Hint Resolve weakening_env_is_allowed_elimination : extends.
+
 Lemma weakening_env_declared_constant `{CF:checker_flags}:
   forall (Σ : global_env) cst (decl : constant_body),
     declared_constant Σ cst decl ->
@@ -436,8 +459,10 @@ Proof.
       intros decl cs []. unshelve econstructor; eauto.
       red in on_ctype |- *. eauto.
       clear on_cindices cstr_eq cstr_args_length cstr_concl_head.
-      induction (cshape_args cs); simpl in *; auto.
-      ** eapply (extends_wf_universe (Σ:=(Σ,φ)) Σ'); auto.
+      revert on_cargs.
+      generalize (cshape_sorts cs).
+      induction (cshape_args cs); destruct l; simpl in *; auto.
+      ** destruct a as [na [b|] ty]; simpl in *; intuition eauto.
       ** destruct a as [na [b|] ty]; simpl in *; intuition eauto.
       ** clear on_ctype on_cargs.
         revert on_cindices.
@@ -448,32 +473,34 @@ Proof.
         simpl in *. move: on_ctype_variance.
         unfold cstr_respects_variance. destruct variance_universes as [[[univs u] u']|]; auto.
         intros [args idxs]. split.
-        eapply (All2_local_env_impl args); intros.
+        eapply (context_relation_impl args); intros.
+        inversion X; constructor; auto.
+        eapply weakening_env_cumul; eauto.
+        eapply weakening_env_conv; eauto.
         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.
-          intros. eapply leq_universe_subset; tea.
-          apply weakening_env_global_ext_constraints; tea.
-          destruct indices_matter; [|trivial]. clear -ind_sorts HPΣ wfΣ' Hext.
-          induction ind_indices; simpl in *; auto.
-          ** eapply (extends_wf_universe (Σ:=(Σ,φ)) Σ'); auto.
-          ** destruct a as [na [b|] ty]; simpl in *; intuition eauto.
-      --- split; [apply fst in ind_sorts|apply snd in ind_sorts].
-          eapply Forall_impl; tea; cbn.
-          intros. eapply leq_universe_subset; tea.
-          apply weakening_env_global_ext_constraints; tea.
-          destruct indices_matter; [|trivial]. clear -ind_sorts HPΣ wfΣ' Hext.
-          induction ind_indices; simpl in *; auto.
-          ** eapply (extends_wf_universe (Σ:=(Σ,φ)) Σ'); auto.
-          ** destruct a as [na [b|] ty]; simpl in *; intuition eauto.
+    -- unfold check_ind_sorts in *.
+       destruct Universe.is_prop; auto.
+       destruct Universe.is_sprop; auto.
+       split; [apply fst in ind_sorts|apply snd in ind_sorts].
+       eapply Forall_impl; tea; cbn.
+       intros. eapply Forall_impl; eauto; simpl.
+       intros; eapply leq_universe_subset; tea.
+       apply weakening_env_global_ext_constraints; tea.
+       destruct indices_matter; [|trivial]. clear -ind_sorts HPΣ wfΣ' Hext.
+       induction ind_indices; simpl in *; auto.
+       ** eapply (extends_wf_universe (Σ:=(Σ,φ)) Σ'); auto.
+       ** destruct a as [na [b|] ty]; simpl in *; intuition eauto.
       -- intros v onv.
           move: (onIndices v onv). unfold ind_respects_variance.
          destruct variance_universes as [[[univs u] u']|] => //.
-         intros idx; eapply (All2_local_env_impl idx); simpl.
-         intros par par' t t'. eapply weakening_env_cumul; eauto.
+         intros idx; eapply (context_relation_impl idx); simpl.
+         intros par par' t t'.
+         intros d. inv d; constructor; auto.
+         eapply weakening_env_cumul; eauto.
+         eapply weakening_env_conv; eauto.
+         eapply weakening_env_cumul; eauto.
   - red in onP |- *. eapply All_local_env_impl; eauto.
 Qed.
 

erasure/theories/EAst.v

@@ -171,7 +171,7 @@ Notation " Γ ,, d " := (snoc Γ d) (at level 20, d at next level).
 Record one_inductive_body : Set := {
   ind_name : ident;
   ind_propositional : bool; (* True iff the inductive lives in Prop *)
-  ind_kelim : sort_family; (* Top allowed elimination sort *)
+  ind_kelim : allowed_eliminations; (* Allowed eliminations *)
   ind_ctors : list (ident * nat (* arity, w/o lets, w/o parameters *));
   ind_projs : list (ident) (* names of projections, if any. *) }.
 

erasure/theories/Erasure.v

@@ -58,50 +58,63 @@ Program Fixpoint check_wf_env_only_univs (Σ : global_env)
         end
     end.
   Next Obligation.
-    repeat constructor. apply graph_eq; try reflexivity.
-    cbn. symmetry. apply wGraph.VSetProp.singleton_equal_add.
+    repeat constructor.
   Qed.
   Next Obligation.
     sq. unfold is_graph_of_uctx, gc_of_uctx; simpl.
     unfold gc_of_uctx in e. simpl in e.
     case_eq (gc_of_constraints (constraints_of_udecl (universes_decl_of_decl g)));
       [|intro HH; rewrite HH in e; discriminate e].
-    intros ctrs' Hctrs'. rewrite Hctrs' in *.
+    intros ctrs' Hctrs'. rewrite Hctrs' in e.
     cbn in e. inversion e; subst; clear e.
     unfold global_ext_constraints; simpl.
-    rewrite gc_of_constraints_union. rewrite Hctrs'.
+    pose proof (gc_of_constraints_union 
+      (constraints_of_udecl (universes_decl_of_decl g)) (global_constraints Σ)).
+    rewrite Hctrs' in H0. simpl in H0.
     red in i. unfold gc_of_uctx in i; simpl in i.
     case_eq (gc_of_constraints (global_constraints Σ));
       [|intro HH; rewrite HH in i; cbn in i; contradiction i].
-    intros Σctrs HΣctrs; rewrite HΣctrs in *; simpl in *.
-    subst G. unfold global_ext_levels; simpl. rewrite no_prop_levels_union.
-    symmetry; apply add_uctx_make_graph.
+    intros Σctrs HΣctrs; rewrite HΣctrs in H0, i; simpl in *.
+    destruct (gc_of_constraints (ConstraintSet.union _ _)).
+    simpl in H0. 
+    subst G. unfold global_ext_levels; simpl.
+    symmetry. rewrite add_uctx_make_graph.
+    apply graph_eq. simpl. reflexivity.
+    simpl. now rewrite H0. simpl. reflexivity.
+    now simpl in H0.
   Qed.
   Next Obligation.
     split; sq. 2: constructor; tas.
     unfold is_graph_of_uctx, gc_of_uctx; simpl.
     unfold gc_of_uctx in e. simpl in e.
     case_eq (gc_of_constraints (constraints_of_udecl (universes_decl_of_decl g)));
       [|intro HH; rewrite HH in e; discriminate e].
-    intros ctrs' Hctrs'. rewrite Hctrs' in *.
+    intros ctrs' Hctrs'. rewrite Hctrs' in e.
     cbn in e. inversion e; subst; clear e.
     unfold global_ext_constraints; simpl.
-    rewrite gc_of_constraints_union.
+    pose proof (gc_of_constraints_union 
+      (constraints_of_udecl (universes_decl_of_decl g)) (global_constraints Σ)).
+    rewrite Hctrs' in H1; simpl in H1.
+    red in i. unfold gc_of_uctx in i; simpl in i.
     assert (eq: monomorphic_constraints_decl g
                 = constraints_of_udecl (universes_decl_of_decl g)). {
       destruct g. destruct c, cst_universes; try discriminate; reflexivity.
       destruct m, ind_universes; try discriminate; reflexivity. }
-    rewrite eq; clear eq. rewrite Hctrs'.
-    red in i. unfold gc_of_uctx in i; simpl in i.
+    rewrite eq; clear eq. 
     case_eq (gc_of_constraints (global_constraints Σ));
       [|intro HH; rewrite HH in i; cbn in i; contradiction i].
-    intros Σctrs HΣctrs; rewrite HΣctrs in *; simpl in *.
-    subst G. unfold global_ext_levels; simpl. rewrite no_prop_levels_union.
+    intros Σctrs HΣctrs; rewrite HΣctrs in H1, i; simpl in *.
+    destruct (gc_of_constraints (ConstraintSet.union _ _)).
+    simpl in H1.
+    subst G. unfold global_ext_levels; simpl.
     assert (eq: monomorphic_levels_decl g
                 = levels_of_udecl (universes_decl_of_decl g)). {
       destruct g. destruct c, cst_universes; try discriminate; reflexivity.
       destruct m, ind_universes; try discriminate; reflexivity. }
-    rewrite eq. symmetry; apply add_uctx_make_graph.
+    rewrite eq. simpl. rewrite add_uctx_make_graph.
+    apply graph_eq; try reflexivity.
+    simpl. now rewrite H1.
+    now simpl in H1.
   Qed.
   Next Obligation.
     split; sq. 2: constructor; tas.
@@ -114,7 +127,7 @@ Program Fixpoint check_wf_env_only_univs (Σ : global_env)
       destruct g. destruct c, cst_universes; try discriminate; reflexivity.
       destruct m, ind_universes; try discriminate; reflexivity. }
     rewrite eq1; clear eq1.
-    assumption.
+    now rewrite levelset_union_empty, constraintset_union_empty.
   Qed.
 
 (* This is the total erasure function + the optimization that removes all 

erasure/theories/ErasureCorrectness.v

@@ -79,26 +79,26 @@ Lemma wf_local_rel_conv:
   forall Σ : global_env × universes_decl,
     wf Σ.1 ->
     forall Γ Γ' : context,
-      PCUICContextRelation.context_relation (PCUICContextConversion.conv_decls Σ) Γ Γ' ->
+      context_relation (conv_decls Σ) Γ Γ' ->
       forall Γ0 : context, wf_local Σ Γ' -> wf_local_rel Σ Γ Γ0 -> wf_local_rel Σ Γ' Γ0.
 Proof.
   intros Σ wfΣ Γ Γ' X1 Γ0 ? w0. induction w0.
   - econstructor.
   - econstructor; eauto. cbn in *.
     destruct t0. exists x. eapply PCUICContextConversion.context_conversion with (Γ ,,, Γ0); eauto.
-    eapply conv_context_app; eauto.
-    eapply typing_wf_local; eauto.
-    eapply PCUICSafeChecker.wf_local_app_inv; eauto.
+    * eapply PCUICSafeChecker.wf_local_app_inv; eauto.
+    * eapply conv_context_app; eauto.
+      eapply typing_wf_local; eauto.
   - econstructor; eauto.
     + cbn in *.
       destruct t0. exists x. eapply PCUICContextConversion.context_conversion with (Γ ,,, Γ0); eauto.
-      eapply conv_context_app; eauto.
-      eapply typing_wf_local; eauto.
-      eapply PCUICSafeChecker.wf_local_app_inv; eauto.
+      * eapply PCUICSafeChecker.wf_local_app_inv; eauto.
+      * eapply conv_context_app; eauto.
+        eapply typing_wf_local; eauto.
     + cbn in *. eapply PCUICContextConversion.context_conversion with (Γ ,,, Γ0); eauto.
-      eapply conv_context_app; eauto.
-      eapply typing_wf_local; eauto.
-      eapply PCUICSafeChecker.wf_local_app_inv; eauto.
+      * eapply PCUICSafeChecker.wf_local_app_inv; eauto.
+      * eapply conv_context_app; eauto.
+        eapply typing_wf_local; eauto.
 Qed.
 
 Hint Resolve Is_type_conv_context : core.
@@ -150,17 +150,15 @@ Proof.
     eapply All_local_env_impl; eauto. simpl; intros.
     destruct T. simpl in *.
     eapply PCUICContextConversion.context_conversion with (Γ ,,, Γ0); eauto.
-    eapply conv_context_app; auto. eapply typing_wf_local; eauto.
+    2:{ eapply conv_context_app; auto. eapply typing_wf_local; eauto. }
     eapply typing_wf_local in X3.
     eapply PCUICSafeChecker.wf_local_app_inv.
     eauto. eapply wf_local_rel_local in X3.
     eapply wf_local_rel_app in X3 as []. rewrite app_context_nil_l in w0.
-
-
     eapply wf_local_rel_conv; eauto.
     destruct X3. exists x0.
     eapply PCUICContextConversion.context_conversion with (Γ ,,, Γ0); eauto.
-    eapply conv_context_app; auto. eapply typing_wf_local; eauto.
+    2:{ eapply conv_context_app; auto. eapply typing_wf_local; eauto. }
 
     eapply typing_wf_local in t0.
     eapply PCUICSafeChecker.wf_local_app_inv.
@@ -185,7 +183,7 @@ Proof.
     eapply All_local_env_impl; eauto. simpl; intros.
     destruct T. simpl in *.
     eapply PCUICContextConversion.context_conversion with (Γ ,,, Γ0); eauto.
-    eapply conv_context_app; auto. eapply typing_wf_local; eauto.
+    2:{ eapply conv_context_app; auto. eapply typing_wf_local; eauto. }
     eapply typing_wf_local in X3.
     eapply PCUICSafeChecker.wf_local_app_inv.
     eauto. eapply wf_local_rel_local in X3.
@@ -195,7 +193,7 @@ Proof.
     eapply wf_local_rel_conv; eauto.
     destruct X3. exists x0.
     eapply PCUICContextConversion.context_conversion with (Γ ,,, Γ0); eauto.
-    eapply conv_context_app; auto. eapply typing_wf_local; eauto.
+    2:{ eapply conv_context_app; auto. eapply typing_wf_local; eauto. }
 
     eapply typing_wf_local in t0.
     eapply PCUICSafeChecker.wf_local_app_inv.