Zulip Chat Archive

Stream: general

Topic: Simp with funext and propext


Patrick Johnson (Jan 28 2023 at 15:55):

In Lean 4, when a theorem is marked as @[simp], does the elaborator automatically apply funext and propext before adding the theorem to the simp set? For example, does the following statement:

 (P Q : Prop), ¬(P  Q)  ¬P  ¬Q

get transformed to

(λ (P Q : Prop) => ¬(P  Q)) = (λ (P Q : Prop) => ¬P  ¬Q)

and the new proof (proved implicitly) gets added to the simp set? Or does simp store the theorem as is, and apply funext and propext ad-hoc on the place of simplification?

Floris van Doorn (Jan 29 2023 at 11:13):

propext gets automatically added, so having ∀ (P Q : Prop), ¬(P ∧ Q) ↔ ¬P ∨ ¬Q as a simp lemma will/should be the same as having ∀ (P Q : Prop), ¬(P ∧ Q) = ¬P ∨ ¬Q. However, funext doesn't get automatically applied. If your simp lemma states f x = g x, then f '' s won't be simplified to g '' s. If you want that, you need to reformulate your lemma to f = g.
At least, that it my understanding of it.

Praneeth Kolichala (Jan 31 2023 at 23:14):

I believe that there is a higher_order attribute that does this automatically:

def f :    := sorry
def g :    := sorry

@[simp, higher_order] lemma f_eq_g (x : ) : f x = g x := sorry

/- Without `higher_order` on f_eq_g, this does not work -/
example : f  (+1) = g  (+1) := by simp

Eric Wieser (Feb 03 2023 at 02:26):

docs#tactic.higher_order_attr


Last updated: Dec 20 2023 at 11:08 UTC