Zulip Chat Archive
Stream: lean4
Topic: Possible bug with `simpa`
Artie Khovanov (Aug 19 2024 at 21:36):
The following code
theorem foo (P : Type*) [PartialOrder P] (b : P):
∀ {a : P}, a ≥ b → b ≥ a → a = b :=
by simpa using ge_antisymm
gives the error
type mismatch
h✝
has type
?m.5712 ≤ ?m.5713 → ?m.5713 ≤ ?m.5712 → ?m.5713 = ?m.5712 : Prop
but is expected to have type
b ≤ a✝ → a✝ ≤ b → a✝ = b : Prop
However, if the argument is made explicit, then the same proof works:
import Mathlib.Order.Defs
theorem foo (P : Type*) [PartialOrder P] (b : P):
∀ (a : P), a ≥ b → b ≥ a → a = b :=
fun a => by simpa using ge_antisymm
Additionally, using simp
followed by exact
also works:
import Mathlib.Order.Defs
theorem foo (P : Type*) [PartialOrder P] (b : P):
∀ {a : P}, a ≥ b → b ≥ a → a = b :=
by simp; exact ge_antisymm
Is this an issue with simpa
?
( @Yaël Dillies )
Last updated: May 02 2025 at 03:31 UTC