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