functional extensional for multiargument functions

Stream: general

[Bernd Losert]

I'm looking for multiple-argument generalizations of funext. Do these exists? Or do I have to resort to uncurrying?

[Yakov Pechersky]

Term mode or tactic mode? You should be able to just use the ext tactic.

[Bernd Losert]

Let me try...

[Bernd Losert]

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]

Your example is wrong. You are asking for p and q to coincide at a specific x and y.

[Reid Barton]

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]

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]

Ah, I see. You're right.

[Bernd Losert]

Thanks a lot.