mathlib documentation

tactic.ext

source
meta def derive_struct_ext_lemma (n : name) :
tactic 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
source
meta def get_ext_subject (a : expr) :
tactic name

source
def ext_param_type  :
Type

Equations
source
meta def opt_minus  :
lean.parser (option name → ext_param_type)

source
meta def ext_param  :
lean.parser ext_param_type

source
meta def saturate_fun (a : name) :
tactic expr

source
meta def equiv_type_constr (n n' : name) :
tactic unit

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

see Note [user attribute parameters]

source
meta def get_ext_lemmas  :
tactic (name_map name)

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

source
meta def get_ext_lemma_names  :
tactic (list name)

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

source
meta def extensional_attribute  :
user_attribute unit (list ext_param_type)

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
source
@[ext]
theorem plift.ext {P : Prop} (a b : plift P) :
a = b

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

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

source
meta def tactic.try_intros (a : list tactic.rcases_patt) :
tactic (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.

source
meta def tactic.ext1 (xs : list tactic.rcases_patt) (cfg : tactic.apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) :
tactic (list tactic.rcases_patt)

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

source
meta def tactic.ext (a : list tactic.rcases_patt) (a_1 : option ℕ) :
tactic (list tactic.rcases_patt)

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.

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

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.

source
meta def tactic.interactive.ext (a : interactive.parse (tactic.rcases_patt_parse tt) * ) (a_1 : interactive.parse (lean.parser.tk ":" *> lean.parser.small_nat)?) :
tactic unit
  • 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.