Zulip Chat Archive

In the following mwe, let works but set gives an "invalid definev tactic, value has type {x_1 // x_1 ∈ algebra.adjoin R {x}} but is expected to have type algebra.adjoin R {x}" error. Is this the expected behaviour, and if so, could you explain why?

import ring_theory.adjoin.basic

example {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S] (x : S): false :=
begin
  let y : algebra.adjoin R ({x} : set S) := ⟨x, algebra.self_mem_adjoin_singleton R x⟩, -- works
  set y : algebra.adjoin R ({x} : set S) := ⟨x, algebra.self_mem_adjoin_singleton R x⟩, -- error
  sorry
end

Alex J. Best (May 31 2022 at 13:31):

Looks like a bug to me, I made a branch that might fix it, but we'll have to watch CI and make sure no other uses of set break https://github.com/leanprover-community/mathlib/runs/6671547585?check_suite_focus=true

María Inés de Frutos Fernández (May 31 2022 at 13:33):

Thanks!

Eric Wieser (May 31 2022 at 14:04):

I feel like we've run into this bug before in another tactic, but I can't remember which one. How does docs#tactic.interactive.let avoid the problem?

Eric Wieser (May 31 2022 at 14:05):

Ah, it was leanprover-community/lean#555 (and https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/let.20fails.20with.20coe_sort/near/230488843)

Alex J. Best (May 31 2022 at 14:07):

Ah, so the issue is that let was fixed but set wasn't analogously, that makes more sense how they ended up being different, essentially all my fix does is make the behaviour uniform between the two

Alex J. Best (May 31 2022 at 14:11):

Ah this is great, this also gives me a minimal test case that I couldn't come up with :smile:

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib