# 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  :
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.

meta def add_ext_lemma (constr lem : name) (persistent : bool) :

Marks lem as an extensionality lemma corresponding to type constructor constr; if persistent is true then this is a global attribute, else local.

meta def extensional_attribute  :

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, ext stream] 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 my_collection]
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, 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.
• set_option trace.ext true will trace every attempted lemma application, along with the time it takes for the application to succeed or fail. This is useful for debugging slow ext calls.

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.