Use just-defined instance of substructure in superstructure?

Stream: lean4

[Thomas Murrills]

Consider the following #mwe:

class Foo (α : Type) where
  x : Bool

def f (α) [Foo α] : Nat := 0

class Bar (α : Type) extends Foo α where
  y : f α = 0

theorem fIsZero (α) [Foo α] : f α = 0 := rfl

def baz : Bar Nat := { x := true, y := fIsZero Nat} -- failed to synthesize instance
  Foo ℕ

We've just defined an instance of Foo Nat by providing x, but fIsZero can't see it.

How do we get something like fIsZero to use the Foo α we've just defined? Is there a better option than just "precariously" inlining an instance of Foo Nat which happens to be equal to the one we're defining?

[Adam Topaz]

you could do this:

def baz : Bar Nat :=
  let t : Foo Nat := ⟨true⟩
  { t with y := fIsZero Nat}

[Thomas Murrills]

Nice, thanks!

[Jireh Loreaux]

Don't you want to use letI so that it actually gets inlined?

[Thomas Murrills]

Ok, sounds good—but just wondering, what's the actual difference, there? Why would I want let to not inline sometimes? (Or when can it not?)

[Reid Barton]

Usually you don't want let to inline, to avoid computing something more than once, or to avoid blowing up the term size.

[Adam Topaz]

Jireh Loreaux said:

Don't you want to use letI so that it actually gets inlined?

Yes, letI would be better here. I only used let because I wasn't sure whether Thomas wanted to rely on std4 (which is where letI is defined)