Zulip Chat Archive

Stream: general

Topic: enforcing a type with show


view this post on Zulip Sebastien Gouezel (Sep 24 2020 at 08:57):

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.

view this post on Zulip Sebastien Gouezel (Sep 24 2020 at 09:00):

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.

view this post on Zulip Mario Carneiro (Sep 24 2020 at 14:40):

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

view this post on Zulip Mario Carneiro (Sep 24 2020 at 14:41):

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


Last updated: May 09 2021 at 20:11 UTC