mathlib3 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 equiv_type_constr (n n' : name) :

For performance reasons, it is inadvisable to use user_attribute.get_param. The parameter is stored as a reflected expression. When calling get_param, the stored parameter is evaluated using eval_expr, which first compiles the expression into VM bytecode. The unevaluated expression is available using user_attribute.get_param_untyped.

In particular, user_attribute.get_param MUST NEVER BE USED in the implementation of an attribute cache. This is because calling eval_expr disables the attribute cache.

There are several possible workarounds:

  1. Set a different attribute depending on the parameter.
  2. Use your own evaluation function instead of eval_expr, such as e.g. expr.to_nat.
  3. Write your own has_reflect Param instance (using a more efficient serialization format). The user_attribute code unfortunately checks whether the expression has the correct type, but you can use `(id %%e : Param) to pretend that your expression e has type Param.

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.

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.

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

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

When possible, ext lemmas are stated without a full set of arguments. As an example, for bundled homs f, g, and of, f.comp of = g.comp of → f = g is a better ext lemma than (∀ x, f (of x) = g (of x)) → f = g, as the former allows a second type-specific extensionality lemmas to be applied to f.comp of = g.comp of. If the domain of of is or and of is a ring_hom, such a lemma could then make the goal f (of 1) = g (of 1).

For bundled morphisms, there is a ext lemma that always applies of the form (∀ x, ⇑f x = ⇑g x) → f = g. When adding type-specific ext lemmas like the one above, we want these to be tried first. This happens automatically since the type-specific lemmas are inevitably defined later.

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  :

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

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 patterns in the ext_state.

Apply multiple extensionality lemmas, destructing the arguments using the given 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.

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.

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