@@ -151,101 +151,3 @@ def testVirtualParentFixed {G : Type} [AddCommGroup G] (s : MySub₂ G) (x : s)
151151 myOp x
152152
153153end VirtualParentAbuse
154-
155- section ZeroInstanceAbuse
156- /-! ### Zero instance mismatch during `rw`
157-
158- In Mathlib, `rw [sub_nonneg]` on `ℤ` failed because the lemma (for generic
159- `[OrderedAddCommGroup α]`) has `0` elaborated as `@Zero.zero α ...` while the
160- goal's `0` is `@OfNat.ofNat ℤ 0 ...` (which reduces to `Int.ofNat 0`). These are
161- definitionally equal, but not at instance transparency. Detecting it with `#defeq_abuse`
162- looked like:
163-
164- ```lean
165- example (a b : ℤ) : 0 ≤ a - b ↔ b ≤ a := by
166- #defeq_abuse in rw [sub_nonneg]
167- -- reported: ❌️ Zero.zero =?= Int.ofNat 0
168- ```
169-
170- Matthew Jasper's Mathlib-free minimization
171- (https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/near/576388498)
172- reproduces this pattern below. -/
173-
174- class Zo' (α : Type _) where
175- zo : α
176-
177- class Num' (α : Type _) (n : Nat) where
178- fromNat : α
179-
180- class Gr' (α : Type _) extends Zo' α where
181- add : α → α → α
182- inv : α → α
183-
184- class Sm' (α : Type _) extends Zo' α where
185- inv : α → α
186-
187- instance {α} [h : Gr' α] : Sm' α := { h with }
188-
189- instance : Zo' Int where
190- zo := 0
191-
192- instance {n} : Num' Int n where
193- fromNat := Int.ofNat n
194-
195- instance {α} [Zo' α] : Num' α 0 where
196- fromNat := Zo'.zo
197-
198- instance : Gr' Int where
199- add a b := a + b
200- inv a := -a
201-
202- theorem zo_eq_iff {α} [Gr' α] (a : α) : Num'.fromNat 0 = a ↔ a = Gr'.add a a := test_sorry
203-
204- /--
205- warning: #defeq_abuse: tactic fails with `backward.isDefEq.respectTransparency true` but succeeds with `false`.
206- The following isDefEq checks are the root causes of the failure:
207- ❌️ Int.ofNat 0 =?= Zo'.zo
208- -/
209- #guard_msgs in
210- example (a : Int) : Num'.fromNat 0 = a ↔ a = Gr'.add a a := by
211- #defeq_abuse in rw [zo_eq_iff]
212-
213- -- Command-level test: same abuse should be detected for a theorem with `by rw`.
214- /--
215- warning: #defeq_abuse: command fails with `backward.isDefEq.respectTransparency true` but succeeds with `false`.
216- The following isDefEq checks are the root causes of the failure:
217- ❌️ Int.ofNat 0 =?= Zo'.zo
218- -/
219- #guard_msgs in
220- #defeq_abuse in
221- theorem test_zo_cmd_abuse (a : Int) : Num'.fromNat 0 = a ↔ a = Gr'.add a a := by
222- rw [zo_eq_iff]
223-
224- -- Verify: abuse is detected even when the outer scope has `respectTransparency false`.
225- -- This simulates the Mathlib lakefile setting.
226- -- (Must appear BEFORE the unif_hint below, which fixes the underlying issue.)
227- section
228- set_option backward.isDefEq.respectTransparency false
229- /--
230- warning: #defeq_abuse: tactic fails with `backward.isDefEq.respectTransparency true` but succeeds with `false`.
231- The following isDefEq checks are the root causes of the failure:
232- ❌️ Int.ofNat 0 =?= Zo'.zo
233- -/
234- #guard_msgs in
235- example (a : Int) : Num'.fromNat 0 = a ↔ a = Gr'.add a a := by
236- #defeq_abuse in rw [zo_eq_iff]
237- end
238-
239- -- A potential fix: a unif_hint telling Lean that two different `Num'` instances applied to
240- -- the same type at `0` should unify. This bridges the gap between `Int.ofNat 0`
241- -- (from the specific `Num' Int n` instance) and `Zo'.zo` (from the generic
242- -- `Num' α 0` instance via `Zo'`).
243- unif_hint (α : Type _) (inst₁ : Num' α 0 ) (inst₂ : Num' α 0 ) where ⊢
244- @Num'.fromNat α 0 inst₁ ≟ @Num'.fromNat α 0 inst₂
245-
246- /-- info: #defeq_abuse: tactic succeeds with `backward.isDefEq.respectTransparency true`. No abuse detected. -/
247- #guard_msgs in
248- example (a : Int) : Num'.fromNat 0 = a ↔ a = Gr'.add a a := by
249- #defeq_abuse in rw [zo_eq_iff]
250-
251- end ZeroInstanceAbuse
0 commit comments