Zulip Chat Archive

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.

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 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