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  :
expr → tactic name
source
meta def saturate_fun  :
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 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
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 := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := 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 := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := 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 := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) (trace : 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 := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) (trace : 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 (lean.parser.tk "?")?) (xs : interactive.parse 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 (lean.parser.tk "?")? → interactive.parse tactic.rintro_patt_parse_hi* → 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.
  • 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.