if_true

Stream: lean4

[Marcus Rossel]

In statement of docs4#if_true, the argument h : Decidable True is an implicit argument:

@[simp] theorem if_true {h : Decidable True} (t e : α) : ite True t e = t := ...

Seeing as Decidable _ is a typeclass, why isn't this a typeclass argument?

And how then does Lean manage to fill in that argument in the following proof?

theorem thm : if True then true else false = true :=
  if_true true false

[Marcus Rossel]

Ah, I guess in thm it can fill in the typeclass argument by unification which is already synthesized when elaborating the type of the theorem:

set_option pp.explicit true in
#print thm
/-
theorem thm : @Eq Bool (@ite Bool True instDecidableTrue true false) true :=
@if_true Bool instDecidableTrue true false
-/

[Yaël Dillies]

Yes exactly. That saves an instance search and, since Lean 4 is very petty about ensuring that typeclass arguments are the ones synthesized by TC inference, means we can apply the theorem to non-canonical instances of Decidable True

[Marcus Rossel]

Is this approach used in other theorems (about other things than ite) as well?

[Eric Wieser]

In general the approach is pretty fragile, as usually you need both the {} and[] versions of the theorem

[Eric Wieser]

The {} approach only works when the term is about @func someInst where someInst : Foo, not @func someInst.toFoo where someInst : Bar

[Kim Morrison]

Some relevant incoming changes to lean: lean#3507, lean#3509

[Eric Wieser]

Oh that's big news!

[Eric Wieser]

I thought there was some principled stance that rw and simp shouldn't be allowed to work on non-canonical instances (in the same way as everything else is not supposed to); is that stance shifting globally, or is this just a pragmatic local change?

[Eric Wieser]

(the remaining one that comes to mind is that {} notation for structures is not permitted to infer its instance arguments by unification, and so sometimes cannot be used)

[Kyle Miller]

Is that last comment of yours documented somewhere @Eric Wieser? Something I'm going to look at is getting structure instance notation to be able to infer more instances automatically, and this sounds like a good to know about