Zulip Chat Archive

Stream: general

Topic: unhygienic calc


view this post on Zulip Mario Carneiro (May 17 2020 at 09:31):

I found this bug in 3.13, the MWE might need some small variation to work on earlier versions, but apparently calc doesn't pay attention to name scoping when using @[trans] theorems:

class ring (α : Type) := mk
instance foo.dvd {α} [ring α] : has_dvd α := sorry
@[trans] theorem dvd_trans {α} [ring α] {a b c : α} :
  a  b  b  c  a  c := sorry
instance : ring  := sorry

def bar : Type := sorry

namespace bar

instance bar.dvd {α} [ring α] : has_dvd bar := sorry
@[trans] theorem dvd_trans {a b c : bar} :
  a  b  b  c  a  c := sorry

example {a b c : } (h1 : a  b) (h2 : b  c) : a  c :=
calc a  b : h1
   ...  c : h2

end bar
type mismatch at application
  dvd_trans
term
  a
has type
  
but is expected to have type
  bar

view this post on Zulip Mario Carneiro (May 17 2020 at 09:34):

Oh, actually in my original example bar.dvd_trans was not marked as @[trans], but I see that the example depends on this. So maybe it's not bad name resolution but rather some kind of @[trans] shadowing

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 10:37):

It seens that calc supports only one @[trans] per relation

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 10:38):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60subset.60.20on.20.60finset.60

view this post on Zulip Mario Carneiro (May 17 2020 at 10:48):

I'm still not really sure what's happening here. The actual example is pnat.dvd_trans, which AFAICT is not marked @[trans], yet it still interferes with the calc proof

view this post on Zulip Mario Carneiro (May 17 2020 at 10:49):

making pnat.dvd_trans protected solves the issue


Last updated: May 08 2021 at 19:11 UTC