cannot infer universe when declaring instances

Stream: new members

[LizBonn]

I'm trying to achieve something like peano axioms in Lean. More precisely, I create a type class called NatLike and NatLike α means that α satisfies peano axioms. The definition of NatLike is as follows:

class NatLike.{u, v} (α : Type u) where
  zero : α
  succ : α → α
  eq_iff_succ_eq_succ : ∀ {b c : α}, b = c ↔ succ b = succ c
  zero_ne_succ : ∀ a : α, zero ≠ succ a
  inductionLike : {motive : α → Sort v} → motive zero → ((a : α) → motive a → motive (succ a)) → (a : α) → motive a

Similar to Nat.le, I also define the le relationship on a type α with instance NatLike α:

inductive NatLike.le.{u} {α : Type u} [NatLike α] : α → α → Prop where
  | refl (n : α) : le n n
  | step (n m : α) : le n m → le n (NatLike.succ m)

Then I want to prove NatLike.zero_le : (n : α) → le zero n using inductionLike:

theorem NatLike.zero_le.{u} {α : Type u} [h : NatLike α] (n : α) : NatLike.le NatLike.zero n :=
  inductionLike (motive := fun x : α => le zero x)
    (le.refl zero) (fun n hle => le.step zero n hle) n

But there're some errors!! Lean complains that it fails to synthesize NatLike α. So I provide all the implicit parameters:

theorem NatLike.zero_le'.{u} {α : Type u} [h : NatLike α] (n : α) : NatLike.le NatLike.zero n :=
  @NatLike.inductionLike α h (motive := fun n : α => @NatLike.le α h (@NatLike.zero α h) n)
    (@NatLike.le.refl α h (@NatLike.zero α h)) (fun n hle => @NatLike.le.step α h (@NatLike.zero α h) n hle) n

After that, Lean finds a type mismatch:

type mismatch
  le zero n
has type
  Prop : Type
but is expected to have type
  Sort u_1 : Type u_1

However, when I #check the same expression, the errors miraculously disappear:

section
universe u
variable {α : Type u} [h : NatLike α] (n : α)

#check @NatLike.inductionLike α h (motive := fun n : α => @NatLike.le α h (@NatLike.zero α h) n) (@NatLike.le.refl α h (@NatLike.zero α h)) (fun n hle => @NatLike.le.step α h (@NatLike.zero α h) n hle) n
end

This makes me really confused. I guess it's probably because I introduce an arbitrary universe v when defining NatLike and Lean cannot infer what v is from a given instance like NatLike α. When I change the type of the motive to α → Prop, everything is OK as expected. But on one hand, I want to define the induction to be some general like Nat.rec and on the other hand, when I try to prove the decidability of the le relationship, I need to do induction on Decidable which is not a Prop.

So, is my guess right? And if I want to eliminate a type α with instance NatLike α to any other universe, how should I define the type of inductionLike? I mean, how to express "for any motive : α → Sort v, ..."? Or does such an expression make no sense at all?

Any explanation will be appreciated. Thanks in advance!

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

No sorry, I am confused

[Riccardo Brasca]

Yeah, it is something subtle about universes. Your NatLike.{u, v} fixes v. If you write set_option pp.universes true before your theorem you see that h has type NatLike.{u, u_1} α, so if u_1 is not Prop is not good.

[Riccardo Brasca]

I am not sure how this can be fixed in general.

[Riccardo Brasca]

I mean

theorem NatLike.zero_le.{u} {α : Type u} [h : NatLike.{u, 0} α] (n : α) : NatLike.le NatLike.zero n :=
  inductionLike (motive := fun x : α => le zero x)
    (le.refl zero) (fun n hle => le.step zero n hle) n

works. The problem is that you want NatLike to work for an arbitrary v, but it is impossible to quantify over universes.

[LizBonn]

Yeah, I get this. But as stated above, when I want to do induction on Decidable, I may need an instance like NatLike.{u, 1} α because Decidable has type Type. So now my question is, given a concrete type α : Type u, as long as I give an instance NatLike.{u, v} α for any universe v, can we directly derive instances such as NatLike.{u, 0} α and NatLike.{u, 1} α from it?

[LizBonn]

Or do I have to give different instances separately when in difference universes v?

[Riccardo Brasca]

But then the various zero would be different, right?

[Eric Wieser]

Yes, you'd need

class NatLike.{u} (α : Type u) where
  zero : α
  succ : α → α
  eq_iff_succ_eq_succ : ∀ {b c : α}, b = c ↔ succ b = succ c
  zero_ne_succ : ∀ a : α, zero ≠ succ a

class NatLikeRec.{v, u} (α : Type u) [NatLike α] where
  inductionLike : {motive : α → Sort v} → motive NatLike.zero → ((a : α) → motive a → motive (NatLike.succ a)) → (a : α) → motive a

[Eric Wieser]

(note that NatLikeRec also needs that inductionLike p0 psucc zero = p0 and inductionLike p0 psucc (succ n) = ...)

[LizBonn]

Uh, sorry, I'm stupid. I can only give an instance for a fixed universe v, as what we talked above.

[LizBonn]

I understand that. Thank you very much!!

[Riccardo Brasca]

Yeah, that's the problem with your approach (and in general this is the reason why we try to avoid using universal properties like that in definitions). I think you may be able to define an instance NatLike.{u, v_1} α → NatLike.{u, v_2} α → NatLike.{u, max v_1 v_2} α playing with Ulift, but I am not 100% sure.

[LizBonn]

That sounds reasonable, I'll try it.

[Eric Wieser]

What you can do here is just have the recursor go into Type, and then use the real Nat to lift it to other universes