enforcing a type with show

Stream: general

[Sebastien Gouezel]

Sometimes, you want to tell Lean that a term has some type, but even type annotations are not enough because Lean sees them but it discards them right away as it has its own opinion on what the type is, so why should it listen to you. I've just seen a trick in Yury's PR #4199 where Lean has no choice but listen to you. Maybe it's a standard trick, but it was new to me so I thought I could share it here. The idea is to first give the type with show, and then the term:

theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
  set.range (show ℕ → α, from λ n, nat.rec x f n) =
    {x} ∪ set.range (λ n, nat.rec (f 0 x) (f ∘ succ) n) :=

Lean is happy with this, while I don't know how to make it happy only with type annotations.

[Sebastien Gouezel]

In fact, I can do it with type annotations:

theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
  (set.range (λ n, nat.rec x f n) : set α) =
    {x} ∪ set.range (λ n, nat.rec (f 0 x) (f ∘ succ) n) :=

But still it's a good trick to know.

[Mario Carneiro]

Note that show leaves "junk" (an identity function) in the term, unlike type annotations. This is actually the reason behind the difference in behavior

[Mario Carneiro]

so you should be careful doing this in things like simp lemmas