peano_naturals.v: get rid of universe N

[jdchristensen]

This is trying to address #1722. peano_naturals.v builds fine with the changes in this PR, but the build of Classes/theory/naturals.v fails, as it can't find lots of instances. For example, ?Azero0 : "Zero nat". This is similar to what I found in #1721 , where Coq couldn't find instances for IsHProp Unit after some things were minimized to set.

The issue can be reproduced in isolation as follows:

From HoTT Require Import Basics.Logic.

Class MyZero A := myzero : A.

Inductive MyUnit : Set := mytt : MyUnit.

Global Instance zero_unit : MyZero MyUnit := mytt.

Set Printing Universes.

Definition test1@{u} : MyZero@{u} MyUnit.
Proof.
  Fail exact _.
Abort.

Definition test2 : MyZero@{Set} MyUnit.
Proof.
  exact _.
Defined.

I don't plan to work on this unless someone suggests an easy fix, but I at least thought I'd record the needed changes to peano_naturals.v. It's also possible that I removed too many universe annotations there.

[JasonGross]

The issue can be reproduced in isolation as follows:

This can be fixed with Typeclasses Transparent MyZero or by making MyZero a cumulative inductive class. I will open an issue on Coq that "Cumulative" should have a meaning for definitional classes.

Edit: Issue opened at coq/coq#18147

[jdchristensen]

@JasonGross Your Typeclasses Transparent suggestion fixes the isolated example I gave, but unfortunately does not fix the real issue. I rebased the original commit, and then added a new commit which shows that Coq can't find the instance of Lt@{U U} nat, even when Lt is marked with Typeclasses Transparent (which it already is in canonical_names; I added it here to be sure). Any chance you can checkout this branch and see what is going on?

[JasonGross]

Try

Suggested change

	Global Instance nat_le: Le nat := Nat.Core.leq.
	Global Instance nat_lt: Lt nat := Nat.Core.lt.
	Global Instance nat_le@{u}: Le@{Set u} nat := Nat.Core.leq.
	Global Instance nat_lt@{u}: Lt@{Set u} nat := Nat.Core.lt.

?

[JasonGross]

This makes at least some of the files compile, and I'm out of time for now:

diff --git a/theories/Classes/implementations/peano_naturals.v b/theories/Classes/implementations/peano_naturals.v
index 45da6a7dd9..e1b41cf88d 100644
--- a/theories/Classes/implementations/peano_naturals.v
+++ b/theories/Classes/implementations/peano_naturals.v
@@ -223,8 +223,8 @@ induction b as [|b IHb];intros [|c];simpl_nat;intros a Ea E.
 Qed.

 (* Order *)
-Global Instance nat_le: Le nat := Nat.Core.leq.
-Global Instance nat_lt: Lt nat := Nat.Core.lt.
+Global Instance nat_le@{u}: Le@{Set u} nat := Nat.Core.leq.
+Global Instance nat_lt@{u}: Lt@{Set u} nat := Nat.Core.lt.

 Lemma le_plus : forall n k, n <= k + n.
 Proof.
diff --git a/theories/Classes/interfaces/naturals.v b/theories/Classes/interfaces/naturals.v
index f6212d7ca1..8f53ff01ac 100644
--- a/theories/Classes/interfaces/naturals.v
+++ b/theories/Classes/interfaces/naturals.v
@@ -2,6 +2,8 @@ Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders.

+#[local] Set Polymorphic Inductive Cumulativity.
+
 Class NaturalsToSemiRing@{i j} (A : Type@{i}) :=
   naturals_to_semiring: forall (B : Type@{j}) `{IsSemiRing B}, A -> B.

diff --git a/theories/Classes/interfaces/orders.v b/theories/Classes/interfaces/orders.v
index 4e1b63c099..85f1254582 100644
--- a/theories/Classes/interfaces/orders.v
+++ b/theories/Classes/interfaces/orders.v
@@ -1,6 +1,7 @@
 Require Import HoTT.Classes.interfaces.abstract_algebra.

 Generalizable Variables A.
+#[local] Set Polymorphic Inductive Cumulativity.

 (*
 In this file we describe interfaces for ordered structures. Since we are in a
@@ -28,7 +29,7 @@ Class PartialOrder `(Ale : Le A) :=
   po_hset
   po_hprop
   po_preorder
-  po_antisym.
+  po_antisym.

 Class TotalOrder `(Ale : Le A) :=
   { total_order_po : PartialOrder (≤)
diff --git a/theories/Classes/theory/naturals.v b/theories/Classes/theory/naturals.v
index e3811f9326..a1c24722d4 100644
--- a/theories/Classes/theory/naturals.v
+++ b/theories/Classes/theory/naturals.v
@@ -81,7 +81,7 @@ Section retract_is_nat.
     Context (h :  SR -> R) `{!IsSemiRingPreserving h}.

     Lemma same_morphism x : (naturals_to_semiring N R ∘ f^-1) x = h x.
-    Proof.
+    Proof using H IsSemiRingPreserving0 IsSemiRingPreserving2.
     transitivity ((h ∘ (f ∘ f^-1)) x).
     - symmetry. apply (to_semiring_unique (h ∘ f)).
     - unfold Compose. apply ap, eisretr.
@@ -90,7 +90,7 @@ Section retract_is_nat.

   (* If we make this an instance, instance resolution will loop *)
   Lemma retract_is_nat : Naturals SR (U:=retract_is_nat_to_sr).
-  Proof.
+  Proof using FullPseudoSemiRingOrder0 H H0 IsSemiRingPreserving0 IsSemiRingPreserving1.
   split;try apply _.
   - unfold naturals_to_semiring, retract_is_nat_to_sr. apply _.
   - intros;apply same_morphism;apply _.
@@ -118,16 +118,18 @@ Context `{Funext} `{Univalence} {N : Type@{U} } `{Naturals@{U U U U U U U U} N}.
 Lemma from_nat_stmt  (N':Type@{U}) `{Naturals@{U U U U U U U U} N'}
   : forall (P : SemiRings.Operations -> Type),
   P (SemiRings.BuildOperations N') -> P (SemiRings.BuildOperations N).
-Proof.
+Proof using H H0 H1.
 apply SemiRings.iso_leibnitz with (naturals_to_semiring N' N);apply _.
 Qed.

+#[local] Typeclasses Transparent Apart NaturalsToSemiRing.
+
 Section borrowed_from_nat.

   Lemma induction
     : forall (P: N -> Type),
     P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P n.
-  Proof.
+  Proof using H H0 H1.
   pose (Q := fun s : SemiRings.Operations =>
     forall P : s -> Type, P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P n).
   change (Q (SemiRings.BuildOperations N)).
@@ -138,58 +140,59 @@ Section borrowed_from_nat.
   Qed.

   Lemma case : forall x : N, x = 0 |_| exists y : N, (x = 1 + y)%mc.
-  Proof.
+  Proof using H H0 H1.
   refine (from_nat_stmt nat
     (fun s => forall x : s, x = 0 |_| exists y : s, (x = 1 + y)%mc) _).
   simpl. intros [|x];eauto.
   Qed.

   Global Instance: Biinduction N.
-  Proof.
+  Proof using H H0 H1.
   hnf. intros P E0 ES.
   apply induction;trivial.
   apply ES.
   Qed.

   Global Instance nat_plus_cancel_l : forall z : N, LeftCancellation (+) z.
-  Proof.
+  Proof using H H0 H1.
   refine (from_nat_stmt@{i U}
     nat (fun s => forall z : s, LeftCancellation plus z) _).
-  simpl. first [exact nat_plus_cancel_l@{U i}|exact nat_plus_cancel_l@{U}].
+  simpl. first [exact nat_plus_cancel_l@{U i}|exact nat_plus_cancel_l@{U}|exact nat_plus_cancel_l@{}].
   Qed.

   Global Instance: forall z : N, RightCancellation (+) z.
-  Proof. intro. apply (right_cancel_from_left (+)). Qed.
+  Proof using H H0 H1. intro. apply (right_cancel_from_left (+)). Qed.

   Global Instance: forall z : N, PropHolds (z <> 0) -> LeftCancellation (.*.) z.
-  Proof.
+  Proof using H H0 H1.
   refine (from_nat_stmt nat (fun s =>
     forall z : s, PropHolds (z <> 0) -> LeftCancellation mult z) _).
   simpl. apply nat_mult_cancel_l.
   Qed.

   Global Instance: forall z : N, PropHolds (z <> 0) -> RightCancellation (.*.) z.
-  Proof. intros ? ?. apply (right_cancel_from_left (.*.)). Qed.
+  Proof using H H0 H1. intros ? ?. apply (right_cancel_from_left (.*.)). Qed.

   Instance nat_nontrivial: PropHolds ((1:N) <> 0).
-  Proof.
-  refine (from_nat_stmt nat (fun s => PropHolds ((1:s) <> 0)) _).
-  apply _.
+  Proof using H H0 H1.
+    refine (from_nat_stmt nat (fun s => PropHolds ((1:s) <> 0)) _).
+    #[local] Typeclasses Transparent PropHolds not SR_carrier one zero.
+    apply _.
   Qed.

   Instance nat_nontrivial_apart `{Apart N} `{!TrivialApart N} :
     PropHolds ((1:N) ≶ 0).
-  Proof. apply apartness.ne_apart. solve_propholds. Qed.
+  Proof using H H0 H1. apply apartness.ne_apart. solve_propholds. Qed.

   Lemma zero_sum : forall (x y : N), x + y = 0 -> x = 0 /\ y = 0.
-  Proof.
+  Proof using H H0 H1.
   refine (from_nat_stmt nat
     (fun s => forall x y : s, x + y = 0 -> x = 0 /\ y = 0) _).
   simpl. apply plus_eq_zero.
   Qed.

   Lemma one_sum : forall (x y : N), x + y = 1 -> (x = 1 /\ y = 0) |_| (x = 0 /\ y = 1).
-  Proof.
+  Proof using H H0 H1.
   refine (from_nat_stmt nat (fun s =>
     forall (x y : s), x + y = 1 -> (x = 1 /\ y = 0) |_| (x = 0 /\ y = 1)) _).
   simpl.
@@ -203,19 +206,19 @@ Section borrowed_from_nat.
   Qed.

   Global Instance: ZeroProduct N.
-  Proof.
+  Proof using H H0 H1.
   refine (from_nat_stmt nat (fun s => ZeroProduct s) _).
   simpl. red. apply mult_eq_zero.
   Qed.
 End borrowed_from_nat.

 Lemma nat_1_plus_ne_0 x : 1 + x <> 0.
-Proof.
+Proof using H H0 H1.
 intro E. destruct (zero_sum 1 x E). apply nat_nontrivial. trivial.
 Qed.

 Global Instance slow_naturals_dec : DecidablePaths N.
-Proof.
+Proof using H1.
 apply decidablepaths_equiv with nat (naturals_to_semiring nat N);apply _.
 Qed.

@@ -224,7 +227,7 @@ Section with_a_ring.

   Lemma to_ring_zero_sum x y :
     -f x = f y -> x = 0 /\ y = 0.
-  Proof.
+  Proof using H H0 H1 H2 IsInjective0 IsSemiRingPreserving0.
   intros E. apply zero_sum, (injective f).
   rewrite rings.preserves_0, rings.preserves_plus, <-E.
   apply plus_negate_r.
@@ -232,7 +235,7 @@ Section with_a_ring.

   Lemma negate_to_ring x y :
     -f x = f y -> f x = f y.
-  Proof.
+  Proof using H H0 H1 H2 IsInjective0 IsSemiRingPreserving0.
   intros E. destruct (to_ring_zero_sum x y E) as [E2 E3].
   rewrite E2, E3. reflexivity.
   Qed.

(The Proof using is not necessary, I just haven't bothered to strip it from the diff, sorry.)

[jdchristensen]

Thanks, @JasonGross, that helps! I applied the relevant parts of that diff and there's good progress with only minor changes. But I don't see how to solve the next issue myself.

Would you like me to push my changes (which don't include the Proof using parts)? Or will that interfere with your WIP?

[JasonGross]

Yes, feel free to apply it

[JasonGross]

But I don't see how to solve the next issue myself.

The next issue is not spurious. The issue is that natdistance_default is taking in N : Type0, but here is required to prove NatDistance N for N : Type. This constraint comes from naturals_to_semiring N nat x and where we have

naturals_to_semiring@{i j} =
fun A : Type@{i} => idmap
     : forall A : Type@{i},
       NaturalsToSemiRing@{i j} A ->
       forall (B : Type@{j}) (Aplus : Plus@{j} B) (Amult : Mult@{j} B) (Azero : Zero@{j} B) (Aone : One@{j} B),
       @IsSemiRing@{j} B Aplus Amult Azero Aone -> A -> B
(* i j |=  *)

NaturalsToSemiRing@{i j} =
fun A : Type@{i} =>
forall (B : Type@{j}) (Aplus : Plus@{j} B) (Amult : Mult@{j} B) (Azero : Zero@{j} B) (Aone : One@{j} B),
@IsSemiRing@{j} B Aplus Amult Azero Aone -> A -> B
     : Type@{i} -> Type@{max(i,j+1)}
(* i j |=  *)

to_semiring_involutive@{u u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11} :
forall (N : Type@{u11}) {Aap : Apart@{u11 u7} N} {Aplus : Plus@{u11} N} {Amult : Mult@{u11} N}
{Azero : Zero@{u11} N} {Aone : One@{u11} N} {Ale : Le@{u11 u9} N} {Alt : Lt@{u11 u10} N}
{U : NaturalsToSemiRing@{u11 u11} N} {H : Naturals@{u5 u6 u7 u8 u9 u10 u11 u11} N} (N2 : Type@{u11})
{Aap0 : Apart@{u11 u1} N2} {Aplus0 : Plus@{u11} N2} {Amult0 : Mult@{u11} N2} {Azero0 : Zero@{u11} N2}
{Aone0 : One@{u11} N2} {Ale0 : Le@{u11 u3} N2} {Alt0 : Lt@{u11 u4} N2} {U0 : NaturalsToSemiRing@{u11 u11} N2}
{H0 : Naturals@{u u0 u1 u2 u3 u4 u11 u11} N2} (x : N),
naturals_to_semiring@{u11 u11} N2 N (naturals_to_semiring@{u11 u11} N N2 x) = x

Notably, it is not conservative to minimize NaturalsToSemiRing@{_ i} to NaturalsToSemiRing@{_ Set}, since the latter says strictly less than the former. But when we fill in the arguments to naturals_to_semiring with the instances from nat, unless we somehow force the universes to be strictly above Set, the universes get dropped down to Set and then we are sad.

(Now again out of time to look at this.)

[jdchristensen]

I think it's fine it leave this unfinished. It's not worth much time.

[JasonGross]

Sure, I agree. I do think it's an interesting case study that might suggest a better heuristic for minimization to Set (cc @SkySkimmer @mattam82 ?), namely that if universe cumulativity and variance is extended from inductives to constants, then it always makes sense to minimize irrelevant universes to Set, and when you know a universe is only going to be used covariantly in a top-level definition, then it's okay to minimize to Set. I think this means in proof mode we should only ever minimize universes to Set if the universe is irrelevant for the goal and context, and most minimization to Set should happen at definition closing time? (Maybe an easy intermediate heuristic would be Set Minimization ToSet In Non Proof Mode Only or something?)