add constraints between monomorphic sorts to udecl (#687)

* add constraints between monomorphic sorts to udecl
adapts safechecker and implements the check and its spec in wGraph

* list lemmas

* fill the gaps in uGraph and safechecker

* fixing trivial instances of invariants on polymorphic universes

* fix plugin compilation

* completeness of consistent_on in uGraph

* fill the completeness part of polymorphic constraints on global levels

* fix plugin compilation in erasure

* Cleanup and lemma moving

* fix * -> /\ and computational content of ReflectEq

* tweak reflectEq instance for performance

* no more opaque reflectEq instances

erasure/_PluginProject.in

@@ -10,6 +10,8 @@
 # src/canonicalTries.ml
 src/ssrbool.ml
 src/ssrbool.mli
+src/ssreflect.ml
+src/ssreflect.mli
 src/uGraph0.ml
 src/uGraph0.mli
 src/wGraph.ml

erasure/src/metacoq_erasure_plugin.mlpack

@@ -1,6 +1,7 @@
 MSetWeakList
 EqdepFacts
 Ssrbool
+Ssreflect
 Utils
 
 WGraph

pcuic/theories/Conversion/PCUICUnivSubstitutionConv.v

@@ -614,15 +614,6 @@ Proof.
   destruct c as [[[] ?] []]; cbnr; discriminate.
 Qed.
 
-Lemma satisfies_union v φ1 φ2 :
-  satisfies v (CS.union φ1 φ2)
-  <-> (satisfies v φ1 /\ satisfies v φ2).
-Proof.
-  unfold satisfies. split.
-  - intros H; split; intros c Hc; apply H; now apply CS.union_spec.
-  - intros [H1 H2] c Hc; apply CS.union_spec in Hc; destruct Hc; auto.
-Qed.
-
 Lemma equal_subst_instance_cstrs_mono u cstrs :
   CS.For_all is_monomorphic_cstr cstrs ->
   CS.Equal (subst_instance_cstrs u cstrs) cstrs.

pcuic/theories/PCUICTyping.v

@@ -441,6 +441,10 @@ Existing Class wf.
 #[global]
 Hint Mode wf + + : typeclass_intances.
 
+Lemma wf_env_non_var_levels (Σ : global_env) `{checker_flags} (hΣ : ∥ wf Σ ∥) :
+  LS.For_all (negb ∘ Level.is_var) (PCUICLookup.global_levels Σ).
+Proof. now destruct hΣ as [[[_ [? _]] _]]. Qed.
+
 Definition wf_ext `{checker_flags} := on_global_env_ext (lift_typing typing).
 Existing Class wf_ext.
 #[global]
@@ -456,7 +460,7 @@ Hint Resolve wf_ext_wf : core.
 
 Lemma wf_ext_consistent {cf:checker_flags} Σ :
   wf_ext Σ -> consistent Σ.
-Proof. intros [? [? [? ?]]]; assumption. Qed.
+Proof. intros [_ [_ [_ [? _]]]]; assumption. Qed.
 #[global]
 Hint Resolve wf_ext_consistent : core.
 

safechecker/_PluginProject.in

@@ -8,6 +8,8 @@
 # From template
 src/ssrbool.ml
 src/ssrbool.mli
+src/ssreflect.ml
+src/ssreflect.mli
 src/uGraph0.ml
 src/uGraph0.mli
 src/wGraph.ml

safechecker/src/metacoq_safechecker_plugin.mlpack

@@ -1,5 +1,6 @@
 Utils
 Ssrbool
+Ssreflect
 WGraph
 UGraph0
 EnvMap

safechecker/theories/PCUICConsistency.v

@@ -133,18 +133,17 @@ Proof.
     constructor; auto.
     - apply wfΣ.
     - apply make_fresh_name_fresh.
-    - red.
-      cbn.
-      split.
-      { now intros ? ?%LevelSet.empty_spec. }
-      split.
-      { now intros ? ?%ConstraintSet.empty_spec. }
-      destruct wfΣ as (?&(?&?&[val sat])).
-      exists val.
-      intros l isin.
-      apply sat; auto.
-      apply ConstraintSet.union_spec.
-      apply ConstraintSet.union_spec in isin as [?%ConstraintSet.empty_spec|]; auto.
+    - split; first now intros ? ?%LevelSet.empty_spec.
+      split; first now intros ? ?%ConstraintSet.empty_spec.
+      destruct wfΣ as (?&(?&?&[val sat]&monoval)); split.
+      1: { 
+        exists val.
+        intros l isin.
+        apply sat; auto.
+        apply ConstraintSet.union_spec.
+        apply ConstraintSet.union_spec in isin as [?%ConstraintSet.empty_spec|]; auto.
+      }
+      intros v hv; exists v; split; [intros ? []%CS.empty_spec| now intros ??].
     - hnf.
       constructor.
       + constructor.

safechecker/theories/PCUICSafeChecker.v

@@ -209,7 +209,7 @@ Section OnUdecl.
       rewrite [mapi_rec _ _ _]mapi_unfold forallb_unfold /= //.
       intros x Hx. apply In_Var_global_ext_poly. len.
     - destruct wfext as [onX onu]. simpl in *.
-      destruct onu as [_ [_ sat]].
+      destruct onu as [_ [_ [sat _]]].
       do 2 red in sat.
       unfold PCUICLookup.global_ext_constraints in sat. simpl in sat.
       red. destruct check_univs => //.
@@ -238,7 +238,7 @@ Section OnUdecl.
       rewrite [mapi_rec _ _ _]mapi_unfold forallb_unfold /= //.
       intros x Hx. apply In_Var_global_ext_poly. len.
     - destruct wfext as [onX onu]. simpl in *.
-      destruct onu as [_ [_ sat]].
+      destruct onu as [_ [_ [sat _]]].
       do 2 red in sat.
       unfold PCUICLookup.global_ext_constraints in sat. simpl in sat.
       red. destruct check_univs => //.
@@ -324,13 +324,22 @@ Section CheckEnv.
   Section UniverseChecks.
   Obligation Tactic := idtac.
 
+  Lemma consistent_extension_on_global Σ uctx :
+    consistent_extension_on (global_uctx Σ) uctx ->
+    consistent_extension_on Σ uctx.
+  Proof.
+    move=> hext v {}/hext [v' [satv' eqv']].
+    exists v'; split=> // x hx; apply: eqv'.
+    apply/LevelSet.union_spec; by left.
+  Qed.
+
   Program Definition check_udecl id X (udecl : universes_decl)
     : EnvCheck X_env_ext_type (∑ uctx', gc_of_uctx (uctx_of_udecl udecl) = Some uctx' /\
                          forall Σ : global_env, abstract_env_rel X Σ -> ∥ on_udecl Σ udecl ∥) :=
     let levels := levels_of_udecl udecl in
     let global_levels := global_levels (abstract_env_univ X) in
     let all_levels := LevelSet.union levels global_levels in
-    check_eq_true_lazy (LevelSet.for_all (fun l => negb (LevelSet.mem l global_levels)) levels)
+    check_eq_true_lazy (LevelSet.for_all (fun l => Level.is_var l) levels)
        (fun _ => (abstract_env_empty_ext X, IllFormedDecl id (Msg ("non fresh level in " ^ print_lset levels))));;
     check_eq_true_lazy (ConstraintSet.for_all (fun '(l1, _, l2) => LevelSet.mem l1 all_levels && LevelSet.mem l2 all_levels) (constraints_of_udecl udecl))
        (fun _ => (abstract_env_empty_ext X, IllFormedDecl id (Msg ("non declared level in " ^ print_lset levels ^
@@ -348,50 +357,45 @@ Section CheckEnv.
     rewrite <- Huctx.
     split; auto.
     assert (HH: ConstraintSet.For_all
-                  (fun '(l1, _, l2) =>
-                     LevelSet.In l1 (LevelSet.union (levels_of_udecl udecl) (global_levels (abstract_env_univ X))) /\
-                     LevelSet.In l2 (LevelSet.union (levels_of_udecl udecl) (global_levels (abstract_env_univ X))))
-                  (constraints_of_udecl udecl)). {
+                  (declared_cstr_levels (LS.union (levels_of_udecl udecl) (global_levels (abstract_env_univ X))))
+                  (constraints_of_udecl udecl)).
+    {
       clear -H0. apply ConstraintSet.for_all_spec in H0.
       2: now intros x y [].
       intros [[l ct] l'] Hl. specialize (H0 _ Hl). simpl in H0.
       apply andb_true_iff in H0. destruct H0 as [H H0].
       apply LevelSet.mem_spec in H. apply LevelSet.mem_spec in H0.
       now split. }
-   repeat split.
+    intros Σ H1; split; last (split; last split).
     - clear -H H1. apply LevelSet.for_all_spec in H.
       2: now intros x y [].
-      intros l Hl. specialize (H l Hl).
-      apply negb_true_iff in H. 
-      erewrite <- abstract_env_univ_correct in H; eauto.
-      now apply LevelSetFact.not_mem_iff in H.
-    - erewrite <- abstract_env_univ_correct in HH; eauto. 
-    - clear - HH Huctx H1 H2. unfold gc_of_uctx, uctx_of_udecl in *.
-      simpl in *.
-      unfold satisfiable_udecl.
-      change (consistent ((Σ , udecl) : global_env_ext)).
-      pose (abstract_env_wf _ H1). sq. 
-      erewrite abstract_env_is_consistent_uctx_correct; eauto.
-      + rename s into HΣ.
-        apply wf_global_uctx_invariants in HΣ.
-        split.
-        * clear -HΣ. cbn. apply LevelSet.union_spec; right.
-          apply HΣ.
-        * intros [[l ct] l'] Hl.
-          apply ConstraintSet.union_spec in Hl. destruct Hl.
-        erewrite <- abstract_env_univ_correct in HH; eauto. 
-        apply (HH _ H). clear -H HΣ ct. destruct HΣ as [_ HΣ].
-        specialize (HΣ (l, ct, l') H).
-        split; apply LevelSet.union_spec; right; apply HΣ.
-  Qed. 
+      intros l Hl Hlglob.
+      move: (wf_env_non_var_levels Σ (heΣ _ _ H1) l Hlglob).
+      now rewrite (H l Hl).
+    - erewrite <- abstract_env_univ_correct in HH; eauto.
+    - pose (HΣ := abstract_env_wf _ H1); sq.
+      apply wf_global_uctx_invariants in HΣ.
+      enough (satisfiable_udecl Σ udecl /\ valid_on_mono_udecl (global_uctx Σ) udecl).
+      1: case: H3; split=> //; apply: consistent_extension_on_global=> //.
+
+      eapply abstract_env_is_consistent_uctx_correct; eauto=> //.
+      split.
+      * apply LevelSet.union_spec; right ; apply HΣ.
+      * intros [[l ct] l'] [Hl|Hl]%CS.union_spec.
+        + erewrite <- abstract_env_univ_correct in HH; eauto.
+          apply (HH _ Hl).
+        + clear -Hl HΣ ct. destruct HΣ as [_ HΣ].
+          specialize (HΣ (l, ct, l') Hl).
+          split; apply LevelSet.union_spec; right; apply HΣ.
+  Defined.
 
-  Definition check_wf_env_ext_prop X X_ext ext := 
+  Definition check_wf_env_ext_prop X X_ext ext :=
       (forall Σ : global_env, abstract_env_rel X Σ -> abstract_env_ext_rel X_ext (Σ, ext))
       /\ (forall Σ : global_env_ext, abstract_env_ext_rel X_ext Σ -> abstract_env_rel X Σ.1).
-  
+
   Program Definition make_abstract_env_ext X (id : kername) (ext : universes_decl)
     :
-    EnvCheck X_env_ext_type ({ X_ext | check_wf_env_ext_prop X X_ext ext})  :=  
+    EnvCheck X_env_ext_type ({ X_ext | check_wf_env_ext_prop X X_ext ext})  :=
     match ext with
     | Monomorphic_ctx => ret (exist (abstract_env_empty_ext X) _)
     | Polymorphic_ctx _ =>

safechecker/theories/PCUICWfEnv.v

@@ -118,9 +118,12 @@ Class abstract_env_prop {cf:checker_flags} (abstract_env_impl abstract_env_ext_i
     consistent udecl.2 <-> abstract_env_is_consistent uctx ;
   abstract_env_is_consistent_uctx_correct X Σ uctx udecl :
     abstract_env_rel X Σ ->
+    global_uctx_invariants (global_uctx Σ) ->
     global_uctx_invariants (global_ext_uctx (Σ, udecl)) ->
     gc_of_uctx (uctx_of_udecl udecl) = Some uctx ->
-    consistent ((Σ,udecl):global_env_ext) <-> abstract_env_is_consistent_uctx X uctx ;
+    (consistent ((Σ,udecl):global_env_ext) /\
+       consistent_extension_on (global_uctx Σ) (uctx_of_udecl udecl).2)
+    <-> abstract_env_is_consistent_uctx X uctx ;
   abstract_env_univ_correct X {Σ} (wfΣ : abstract_env_rel X Σ) :
     (Σ:ContextSet.t) = abstract_env_univ X
   }.

safechecker/theories/PCUICWfEnvImpl.v

@@ -59,9 +59,10 @@ Proof.
   repeat split; cbn.
   - intros i; rewrite LevelSetFact.empty_iff //.
   - intros i; rewrite ConstraintSetFact.empty_iff //.
-  - red. rewrite /univs_ext_constraints /=. 
+  - red. rewrite /univs_ext_constraints /=.
     rewrite CS_union_empty.
     apply wfΣ.
+  - apply consistent_extension_on_empty.
 Qed.
 
 Record referenced_impl_ext {cf:checker_flags} := {
@@ -153,7 +154,10 @@ Program Global Instance canonical_abstract_env_struct {cf:checker_flags} :
  abstract_env_univ X := X ;
  abstract_env_global_declarations X := declarations X;
  abstract_env_is_consistent uctx := wGraph.is_acyclic (make_graph uctx);
- abstract_env_is_consistent_uctx X uctx := wGraph.is_acyclic (add_uctx uctx (referenced_impl_graph X)) ;
+ abstract_env_is_consistent_uctx X uctx :=
+   let G := referenced_impl_graph X in
+   let G' := add_uctx uctx G in
+   wGraph.is_acyclic G' && wGraph.is_full_subgraph G G' ;
  abstract_env_add_uctx X uctx udecl Hdecl Hglobal := {| referenced_impl_env_ext := (X.(referenced_impl_env) , udecl);
  |} ;
  abstract_env_rel := fun X Σ => Σ = referenced_impl_env X
@@ -164,10 +168,10 @@ Next Obligation. pose proof (referenced_impl_wf X) as [[? ?]]; sq; destruct H.
   econstructor; eauto. econstructor; eauto.  Qed.
 Next Obligation. pose proof (referenced_impl_wf X) as [?]. sq. split; eauto.
   apply on_udecl_mono.
-Qed.   
+Qed.
 Next Obligation.
   pose proof (referenced_impl_wf X). now sq.
-Qed.  
+Qed.
 
 (* We pack up all the information required on the global environment and graph in a
 single record. *)
@@ -390,6 +394,7 @@ Next Obligation. now rewrite (abstract_env_compare_global_instance_correct X.(wf
 Next Obligation. now rewrite (abstract_env_check_constraints_correct X.(wf_env_ext_referenced)); eauto. Defined.
 Next Obligation. apply fake_guard_correct. Defined.
 
+
 Program Global Instance canonical_abstract_env_prop {cf:checker_flags} :
   @abstract_env_prop _ _ _ canonical_abstract_env_ext_struct canonical_abstract_env_struct.
 Next Obligation. now sq. Qed.
@@ -399,39 +404,77 @@ Next Obligation. now split. Qed.
 Next Obligation. unshelve epose proof (is_consistent_spec udecl _) as Hconsistent; eauto.
   unfold is_consistent in Hconsistent; now rewrite H0 in Hconsistent.
   Qed.
-Next Obligation. 
-  rename H1 into Huctx. unfold referenced_impl_graph.
+Next Obligation.
+  rename H2 into Hudecl. unfold referenced_impl_graph; rewrite andb_and.
   pose proof (referenced_impl_graph_wf X) as HG.
-  set (gph := (graph_of_wf X).π1) in *. clearbody gph. simpl in HG.  
-  unfold is_graph_of_uctx in HG. unfold gc_of_uctx in *.
-  case_eq (gc_of_constraints (global_uctx X).2).
-  2:{ intro XX. rewrite XX in HG. inversion HG. }
-  intros Σctrs HΣctrs.
-  rewrite HΣctrs in HG. simpl in HG.
-  case_eq (gc_of_constraints (constraints_of_udecl udecl));
-    [|intro XX; rewrite XX in Huctx; discriminate Huctx].
-  intros ctrs Hctrs. rewrite Hctrs in Huctx. simpl in *.
+  set (gph := (graph_of_wf X).π1) in *. clearbody gph. simpl in HG.
+  move: HG=> /on_SomeP [[uctx1 uctx2] [Huctx HG]].
+  pose proof (gcinv := gc_of_uctx_invariants _ _ Huctx H0).
+  pose proof (invG := make_graph_invariants _ gcinv).
+  destruct (gc_of_uctx_union _ _ _ _ Hudecl Huctx) as [gcsExt [uctxExtEq hgcs]].
+  pose proof (HG' := add_uctx_make_graph t uctx1 t0 uctx2).
+  set (uctxExt := (LS.union t uctx1, GCS.union t0 uctx2)) in HG'.
+  have gcExtinv : global_gc_uctx_invariants uctxExt.
+  { rewrite /uctxExt /global_gc_uctx_invariants /=; rewrite <- hgcs.
+    apply: (gc_of_uctx_invariants _ _ uctxExtEq). }
+  pose proof (invG' := make_graph_invariants _ gcExtinv).
+  move: (Huctx); rewrite /gc_of_uctx.
+  case_eq (gc_of_constraints (global_uctx X).2) => //=.
+  intros Σctrs HΣctrs [=]; subst.
+  unfold gc_of_uctx in Hudecl; move: Hudecl.
+  case_eq (gc_of_constraints (constraints_of_udecl udecl)); last by move=> ->.
+  move=> ctrs /= /[dup] Hctrs -> [=]??; subst. simpl in *.
   rewrite - (is_consistent_spec (global_ext_uctx (X, udecl))).
   pose proof (gc_of_constraints_union (constraints_of_udecl udecl) (global_constraints X)).
-  rewrite {}HΣctrs {}Hctrs in H. simpl in H.
-  unfold is_consistent, global_ext_uctx, gc_of_uctx, global_ext_constraints. simpl. 
+  rewrite HΣctrs Hctrs in H. simpl in H.
+  unfold is_consistent, global_ext_uctx, gc_of_uctx, global_ext_constraints. simpl.
   destruct (gc_of_constraints (ConstraintSet.union (constraints_of_udecl udecl)
-  (global_constraints X))).
-  - simpl in H. inversion Huctx; subst; clear Huctx. 
-  clear -H H0 cf HG.   
-  rewrite -HG add_uctx_make_graph. 
-  unfold global_ext_levels, global_levels in *. simpl.
-  assert (make_graph
-  (LevelSet.union (levels_of_udecl udecl)
-     (LevelSet.union (ContextSet.levels X) (LevelSet.singleton Level.lzero)),
-  t1) =_g make_graph
-  (LevelSet.union (levels_of_udecl udecl)
-     (LevelSet.union (ContextSet.levels X) (LevelSet.singleton Level.lzero)),
-     GoodConstraintSet.union t0 Σctrs)).
-  { apply make_graph_proper. now split; eauto. }     
-  now erewrite is_acyclic_proper.
-  - inversion H. 
-  Qed.   
+                                                   (global_constraints X))).
+  2: inversion H.
+  simpl in H.
+  assert (H45 : make_graph (global_ext_levels (X, udecl) , t) =_g make_graph uctxExt).
+  { apply make_graph_proper. now split; eauto. }
+  erewrite is_acyclic_proper; last eassumption.
+  clear H1 H0 H45; split.
+  + move=> [] h consistent_ext ; split; first by rewrite -{1}HG HG'.
+    apply/wGraph.is_full_subgraph_spec.
+    symmetry in HG.
+    refine (@consistent_on_full_subgraph _ (global_uctx X) (uctx_of_udecl udecl)
+                                        (global_levels X, uctx2)
+                                        (levels_of_udecl udecl, t0)
+                                        gph
+                                        _
+                                        _
+                                        gcinv
+                                        Huctx
+                                        (gc_of_constraints_of_uctx (uctx_of_udecl udecl) _ Hctrs)
+                                        HG
+           ).
+    * move: h=> /wGraph.is_acyclic_spec.
+      rewrite -HG' -HG.
+      apply: acyclic_no_loop_add_uctx.
+    * apply: consistent_extension_on_union.
+      pose proof (referenced_impl_wf X); sq.
+      apply: PCUICUnivSubstitutionConv.levels_global_constraint.
+      unfold uctx_of_udecl=> /=.
+      exact consistent_ext.
+  + move=> [acG'] /wGraph.is_full_subgraph_spec H1; split; first by rewrite -HG' HG.
+    rewrite  -HG' HG in invG'.
+    move: acG' => /wGraph.is_acyclic_correct acG'.
+    intros v [gΣ [gcΣeq Σsat]]%gc_of_constraints_spec%on_SomeP.
+    symmetry in HG. rewrite -HG in HG'.
+    move: gcΣeq; rewrite HΣctrs => [=]?; subst.
+    destruct (graph_extend gph _ H1 acG' _ _ gcinv gcExtinv HG HG' v Σsat) as [vext [vextsat extendsv]].
+    simpl in vextsat.
+    exists vext; split.
+    * apply gc_of_constraints_spec.
+      rewrite Hctrs /=.
+      apply GoodConstraintSet.for_all_spec; first by move=> ?? ->.
+      move=> ??; apply GoodConstraintSet.for_all_spec in vextsat; last by move=> ??->.
+      apply: vextsat; apply/GoodConstraintSet.union_spec; by left.
+    * move=> l Hl; apply extendsv.
+      case: HG=> eq1 _ ; rewrite eq1 //=.
+  Qed.
 
 Program Global Instance optimized_abstract_env_prop {cf:checker_flags} :
   @abstract_env_prop _ _ _ optimized_abstract_env_ext_struct optimized_abstract_env_struct.