# mathlibdocumentation

tactic.ext

derive_struct_ext_lemma n generates two extensionality lemmas based on the equality of all non-propositional projections.

On the following:

@[ext]
structure foo (α : Type*) :=
(x y : ℕ)
(z : {z // z < x})
(k : α)
(h : x < y)


derive_struct_lemma generates:

lemma foo.ext : ∀ {α : Type u_1} (x y : foo α),
x.x = y.x → x.y = y.y → x.z == y.z → x.k = y.k → x = y
lemma foo.ext_iff : ∀ {α : Type u_1} (x y : foo α),
x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z == y.z ∧ x.k = y.k

meta def get_ext_subject  :

def ext_param_type  :
Type

Equations
meta def opt_minus  :

meta def ext_param  :

meta def saturate_fun  :

meta def equiv_type_constr  :
name

For performance reasons, the parameters of the @[ext] attribute are stored in two auxiliary attributes:

attribute [ext [thunk]] funext

-- is turned into
attribute [_ext_core (@id name @funext)] thunk
attribute [_ext_lemma_core] funext

meta def get_ext_lemmas  :

Returns the extensionality lemmas in the environment, as a map from structure name to lemma name.

meta def get_ext_lemma_names  :

Returns the extensionality lemmas in the environment, as a list of lemma names.

Tag lemmas of the form:

@[ext]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...


The attribute indexes extensionality lemma using the type of the objects (i.e. my_collection) which it gets from the statement of the lemma. In some cases, the same lemma can be used to state the extensionality of multiple types that are definitionally equivalent.

attribute [ext [(→),thunk,stream]] funext


Those parameters are cumulative. The following are equivalent:

attribute [ext [(→),thunk]] funext
attribute [ext [stream]] funext


and

attribute [ext [(→),thunk,stream]] funext


One removes type names from the list for one lemma with:

attribute [ext [-stream,-thunk]] funext


Also, the following:

@[ext]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...


is equivalent to

@[ext *]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...


This allows us specify type synonyms along with the type that is referred to in the lemma statement.

@[ext [*,my_type_synonym]]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...


The ext attribute can be applied to a structure to generate its extensionality lemmas:

@[ext]
structure foo (α : Type*) :=
(x y : ℕ)
(z : {z // z < x})
(k : α)
(h : x < y)


will generate:

@[ext] lemma foo.ext : ∀ {α : Type u_1} (x y : foo α),
x.x = y.x → x.y = y.y → x.z == y.z → x.k = y.k → x = y
lemma foo.ext_iff : ∀ {α : Type u_1} (x y : foo α),
x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z == y.z ∧ x.k = y.k

@[ext]
theorem plift.ext {P : Prop} (a b : plift P) :
a = b

@[ext]
theorem unit.ext {x y : unit} :
x = y

@[ext]
theorem punit.ext {x y : punit} :
x = y

Try to introduce as many arguments as possible, using the given patterns to destruct the introduced variables. Returns the unused patterns.

meta def tactic.ext1  :
(tactic.apply_cfg :=

Apply one extensionality lemma, and destruct the arguments using the given patterns. Returns the unused patterns.

meta def tactic.ext  :

Apply multiple extensionality lemmas, destructing the arguments using the given patterns. ext ps (some n) applies at most n extensionality lemmas. Returns the unused patterns.

meta def tactic.interactive.ext1  :
interactive.parse (tactic.rcases_patt_parse tt) *

ext1 id selects and apply one extensionality lemma (with attribute ext), using id, if provided, to name a local constant introduced by the lemma. If id is omitted, the local constant is named automatically, as per intro.

meta def tactic.interactive.ext  :
interactive.parse (tactic.rcases_patt_parse tt) *
• ext applies as many extensionality lemmas as possible;
• ext ids, with ids a list of identifiers, finds extentionality and applies them until it runs out of identifiers in ids to name the local constants.
• ext can also be given an rcases pattern in place of an identifier. This will destruct the introduced local constant.

When trying to prove:

α β : Type,
f g : α → set β
⊢ f = g


applying ext x y yields:

α β : Type,
f g : α → set β,
x : α,
y : β
⊢ y ∈ f x ↔ y ∈ f x


by applying functional extensionality and set extensionality.

When trying to prove:

α β γ : Type
f g : α × β → γ
⊢ f = g


applying ext ⟨a, b⟩ yields:

α β γ : Type,
f g : α × β → γ,
a : α,
b : β
⊢ f (a, b) = g (a, b)


by applying functional extensionality and destructing the introduced pair.

A maximum depth can be provided with ext x y z : 3.