## Stream: general

### Topic: functional extensional for multiargument functions

#### 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 ext tactic.

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 p and q to coincide at a specific x and y.

#### 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: Dec 20 2023 at 11:08 UTC