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
dvd_trans
term
a
has type
ℤ
but is expected to have type
bar


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):

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

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: May 08 2021 at 19:11 UTC