default proofs

Stream: mathlib4

[Jireh Loreaux]

I don't understand why the first of these works, but the second fails. An explanation would be most welcome.

class Foo where
  X : ℕ

class Bar extends Foo where
  X := 5
  hX : X = 5 := by rfl  -- works

class Baz extends Foo where
  X := 5
  hX : X = 5 := rfl -- fails

[David Renshaw]

I think this is related to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/when.20are.20struct.20field.20defaults.20evaluated.3F/near/290407486

[David Renshaw]

The := by syntax means that the field is evaluated lazily as a tactic. In particular, it's not evaluated until an instance of the class is defined (if I understand correctly).

[David Renshaw]

In the second case, my understanding is that the plain := syntax means that the term should be evaluated immediately.

[David Renshaw]

Note that your example doesn't work if you do this:

class Bar extends Foo where
  X := 5
  hX : X = 5 := let () := (); by rfl

[David Renshaw]

That avoids the special syntax overload for := by and therefore causes the term to be evaluated eagerly.

[David Renshaw]

My feeling is that it would be better if we had actually clearly different syntax to distinguish these two different things.

[Jireh Loreaux]

Hmmm... okay. This behavior is a bit strange to me. I would have expected that the default proof would use the value from the default field. So I would have expected the eagerly evaluated one to work too.

[Jireh Loreaux]

But if this is the behavior, certainly a special syntax other than by would be preferable to highlight the distinction.

[Mario Carneiro]

:= by is a special keyword in this context

[David Renshaw]

I think you don't have enough information here to prove that X = 5 eagerly.

[Mario Carneiro]

I usually use := (by ... if I want to disable it

[Mario Carneiro]

yes, by rfl is the right solution in this example

[David Renshaw]

Like, it's a default value for X, right? and a different value for X could be supplied by an instance?

[Jireh Loreaux]

Sure, I understand that, but I would have expected the eager evaluation to use the default value when compiling the class declaration and then when defining an instance of this class if the default value is overridden then the proof field needs to be supplied.

[Mario Carneiro]

this is also the syntax for auto params BTW, def foo (x : 0 < y := by simp) : Nat := 0

[Mario Carneiro]

Yes it is something to be aware of but I think it is a reasonable syntax. It makes more sense than lean 3's x : Ty . tac stylistically