mathlib3 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  :
expr → tactic name
source
meta def saturate_fun  :
name → tactic expr
source
meta def equiv_type_constr (n n' : name) :
tactic unit
source
def library_note.user attribute parameters  :
unit

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]

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 add_ext_lemma (constr lem : name) (persistent : bool) :
tactic unit

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

source
meta def extensional_attribute  :
user_attribute unit (option name)

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
source
def tactic_doc.attribute.ext  :
tactic_doc_entry

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
source
def library_note.partially-applied ext lemmas  :
unit

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.

source
theorem ulift.ext_iff {α : Type s} (x y : ulift α) :
x = y ↔ x.down = y.down
source
theorem ulift.ext {α : Type s} (x y : ulift α) (h : x.down = y.down) :
x = y
source
@[ext]
theorem plift.ext {P : Prop} (a b : plift P) :
a = b
source
theorem has_zero.ext_iff {α : Type u} (x y : has_zero α) :
x = y ↔ 0 = 0
source
theorem has_zero.ext {α : Type u} (x y : has_zero α) (h : 0 = 0) :
x = y
source
@[ext]
theorem unit.ext {x y : unit} :
x = y
source
@[ext]
theorem punit.ext {x y : punit} :
x = y
source
meta structure tactic.ext_state  :
Type

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

source
meta def tactic.try_intros (patts : 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_core (cfg : tactic.apply_cfg := {md := tactic.transparency.semireducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}) :
state_t tactic.ext_state tactic unit

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

source
meta def tactic.ext_core (cfg : tactic.apply_cfg := {md := tactic.transparency.semireducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}) :
state_t tactic.ext_state tactic unit

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

source
meta def tactic.ext1 (xs : list tactic.rcases_patt) (cfg : tactic.apply_cfg := {md := tactic.transparency.semireducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}) (trace : bool := bool.ff) :
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 (xs : list tactic.rcases_patt) (fuel : option ℕ) (cfg : tactic.apply_cfg := {md := tactic.transparency.semireducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}) (trace : bool := bool.ff) :
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 (trace : interactive.parse (optional (lean.parser.tk "?"))) (xs : interactive.parse (lean.parser.many tactic.rcases_patt_parse_hi)) :
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. 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.

source
meta def tactic.interactive.ext  :
interactive.parse (optional (lean.parser.tk "?")) → interactive.parse (lean.parser.many tactic.rintro_patt_parse_hi) → interactive.parse (optional (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.
  • 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.

source
def tactic_doc.tactic.ext1 / ext  :
tactic_doc_entry

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