Zulip Chat Archive

Stream: general

Topic: unhygienic calc

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
has type
but is expected to have type

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

Yury G. Kudryashov (May 17 2020 at 10:37):

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

Yury G. Kudryashov (May 17 2020 at 10:38):


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

Mario Carneiro (May 17 2020 at 10:49):

making pnat.dvd_trans protected solves the issue

Last updated: Aug 03 2023 at 10:10 UTC