Bernd Losert (Dec 12 2021 at 19:58):
I'm looking for multiple-argument generalizations of funext. Do these exists? Or do I have to resort to uncurrying?
Yakov Pechersky (Dec 12 2021 at 20:04):
Term mode or tactic mode? You should be able to just use the
Bernd Losert (Dec 12 2021 at 20:05):
Let me try...
Bernd Losert (Dec 12 2021 at 20:18):
Hmm... I'm not sure how to apply this tactic. How would it work with this code:
import logic.basic variable a : Type* theorem foo : forall (p q : a -> a -> Prop) (x y : a), (p x y -> q x y) -> (q x y -> p x y) -> p = q := begin assume p q x y h h', let h'' := iff.intro h h', apply iff_iff_eq.mp h'', end
Yaël Dillies (Dec 12 2021 at 20:21):
Your example is wrong. You are asking for
q to coincide at a specific
Reid Barton (Dec 12 2021 at 20:21):
The pattern should be something like
apply funext, intro x, apply funext, intro y, apply propext, but also the
ext tactic should do this all in one shot
Yaël Dillies (Dec 12 2021 at 20:22):
Here's probably what you meant
import logic.basic import tactic.ext variable a : Type* theorem foo : ∀ (p q : a -> a -> Prop), (∀ x y, p x y -> q x y) → (∀ x y, q x y -> p x y) → p = q := begin intros p q hpq hqp, ext x y, exact ⟨hpq x y, hqp x y⟩, end
Bernd Losert (Dec 12 2021 at 20:24):
Ah, I see. You're right.
Bernd Losert (Dec 12 2021 at 20:25):
Thanks a lot.
Last updated: Aug 03 2023 at 10:10 UTC