working with universal typeclass instances

Stream: lean4

[Colin S. Gordon]

I'm fiddling around with typeclasses in Lean 4, and recently (via Lars König's very cool MS thesis learned about Lean 4's support for universal quantification in typeclass constraints. I'm fiddling with this, and I've found a case where I suspect there's a way to make something work, but I'm not having any luck getting it to work.

As a simple example, consider

  class isNum (i:Nat) where
    p : even i ∨ odd i
  class hasP (P:Nat -> Prop) where
    p : ∀ i, P i
  instance hasNum : [∀ i, isNum i] -> hasP (fun x => even x ∨ odd x) where
    p := by intro i
            apply isNum.p

Here the universal version of isNum is automatically found and instantiated in tactic mode when using isNum.p. But this seems to only work because the i from the the type of hasP.p is in the tactic context explicitly. If I try a slight variation on this:

  class proveUniv (P:Nat -> Prop) where
    p := Prop
  instance hasUniv : [∀ i, isNum i] -> proveUniv (fun x => even x ∨ odd x) where
    p := (∀ (y:Nat), isNum.p (i:=y)) -- <-- Doesn't check

I cannot get anything I've tried for this last instance body to work. Because the universal typeclass constraint is after the colon, I can't name it and refer back to it (I can name it, but I can't use the name in the term given for hasUniv.p). Moving it before the colon (i.e., instance hasUniv [inst:∀ i, isNum i] : provUniv ...) results in a complaint that there is no forward dependency on i. Attempting to stick a by tactic block inside the ∀ (y:Nat), ... body doesn't seem to get anything working.

It seems the issue is trying to use this universal instance under a new binder introduced in the typeclass member definition. Is this expected to work via some means I have yet to figure out? Or is there a reason this shouldn't/can't work (either an engineering reason or a theoretical reason)?

[Sebastian Ullrich]

Do you have a self-contained version? even and odd are missing, and if I add them I get "type expected" at the last instance, which makes sense because isNum.p is a proof, while a Type is expected at that position. I can't reproduce the forward dependency error either.

[Colin S. Gordon]

oops, sorry, I had forgotten I'd defined these rather than importing them

def odd (n:Nat) : Bool :=
  match n with
  | Nat.zero => false
  | Nat.succ Nat.zero => true
  | Nat.succ (Nat.succ x) => odd x
def even (n:Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ Nat.zero => false
  | Nat.succ (Nat.succ x) => even x

[Colin S. Gordon]

I had forgotten I'd hit this with booleans, but this variant that sticks to Prop has the same symptoms

  def fakeEven (i:Nat) : Prop := True
  def fakeOdd (i:Nat) : Prop := False
  class isNum (i:Nat) where
    p : fakeEven i ∨ fakeOdd i
  class hasP (P:Nat -> Prop) where
    p : ∀ i, P i
  instance hasNum : [∀ i, isNum i] -> hasP (fun x => fakeEven x ∨ fakeOdd x) where
    p := by intro i
            apply isNum.p -- <-- works
  class proveUniv (P:Nat -> Prop) where
    p := Prop
  instance hasUniv : [∀ i, isNum i] -> proveUniv (fun x => fakeEven x ∨ fakeOdd x) where
    p := (∀ (y:Nat), isNum.p (i:=y)) -- <-- fails

[Colin S. Gordon]

...and curiously I can no longer reproduce the complaint about no forward dependencies either

[Sebastian Ullrich]

I still get only "type expected" with that. I suspect you meant p : Prop in proveUniv, but even then isNum.p still isn't a Prop regardless of typeclass resolution.

[Colin S. Gordon]

ah, you're right, that's the heart of the issue here... I may have mis-distilled my minimal example