# mathlibdocumentation

tactic.ext

meta def derive_struct_ext_lemma (n : name) :

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 (n n' : 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

theorem ulift.ext_iff {α : Type s} (x y : ulift α) :
x = y x.down = y.down

theorem ulift.ext {α : Type s} (x y : ulift α) (h : x.down = y.down) :
x = y

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

theorem has_zero.ext_iff {α : Type u} (x y : has_zero α) :
x = y 0 = 0

theorem has_zero.ext {α : Type u} (x y : has_zero α) (h : 0 = 0) :
x = y

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

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

meta structure tactic.ext_state  :
Type
• patts :
• trace_msg :
• fuel :

Helper structure for ext and ext1. lemmas keeps track of extensionality lemmas applied so far.

meta def tactic.try_intros (patts : list tactic.rcases_patt) :

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_core (cfg : tactic.apply_cfg := ) :

Apply one extensionality lemma, and destruct the arguments using the patterns in the ext_state.

meta def tactic.ext_core (cfg : tactic.apply_cfg := ) :

Apply multiple extensionality lemmas, destructing the arguments using the given patterns.

meta def tactic.ext1 (xs : list tactic.rcases_patt) (cfg : tactic.apply_cfg := ) (trace : bool := ff) :

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

meta def tactic.ext (xs : list tactic.rcases_patt) (fuel : option ) (cfg : tactic.apply_cfg := ) (trace : bool := ff) :

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.

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. Placing a ? after ext1 (e.g. ext1? i ⟨a,b⟩ : 3) will display a sequence of tactic applications that can replace the call to ext1.

• 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.
• Placing a ? after ext (e.g. ext? i ⟨a,b⟩ : 3) will display a sequence of tactic applications that can replace the call to ext.

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.

In the previous example, applying ext? ⟨a,b⟩ will produce the trace message:

Try this: apply funext, rintro ⟨a, b⟩


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