mathlib documentation

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

meta def equiv_type_constr  :

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]

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

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.

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

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) * 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.

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