# mathlib3documentation

tactic.expand_exists

# expand_exists#

expand_exists is an attribute which takes a proof that something exists with some property, and outputs a value using classical.some, and a proof that it has that property using classical.some_spec. For example:

@[expand_exists it it_spec]
lemma it_exists (n : ℕ) : ∃ m : ℕ, n < m := sorry


produces

def it (n : ℕ) : ℕ := classical.some (it_exists n)

lemma it_spec (n : ℕ) : n < it n := classical.some_spec (it_exists n)



Data known when parsing pi expressions.

decl's arguments are: is_theorem, name, type, value.

Data known when parsing exists expressions (after parsing pi expressions).

• with_args applies pi arguments to a term (eg id -> id #2 #1 #0).
• spec_chain takes the form of classical.some_spec^n (it_exists ...), with n the depth of ∃ parsed.
• exists_decls is a list of declarations containing the value(s) of witnesses.

Data known when parsing the proposition (after parsing exists and pi expressions).

project_proof projects a proof of the full proposition (eg A ∧ B ∧ C) to a specific proof (eg B).

Replaces free variables with their exists declaration. For example, if:

def n_value : ℕ := ... -- generated by expand_exists


then this function converts #0 in #0 = #0 from ∃ n : ℕ, n = n to n_value = n_value.

Parses a proposition and creates the associated specification proof. Does not break down the proposition further.

Parses a proposition and decides if it should be broken down (eg P ∧ Q -> P and Q) depending on how many names are left. Then creates the associated specification proof(s).

Parses an ∃ a : α, p a, and creates an associated definition with a value of α. When p α is not an exists statement, it will call parse_props.

Parses a ∀ (a : α), p a. If p is not a pi expression, it will call parse_exists

From a proof that (a) value(s) exist(s) with certain properties, constructs (an) instance(s) satisfying those properties. For instance:

@[expand_exists nat_greater nat_greater_spec]
lemma nat_greater_exists (n : ℕ) : ∃ m : ℕ, n < m := ...

#check nat_greater      -- nat_greater : ℕ → ℕ
#check nat_greater_spec -- nat_greater_spec : ∀ (n : ℕ), n < nat_greater n


It supports multiple witnesses:

@[expand_exists nat_greater_m nat_greater_l nat_greater_spec]
lemma nat_greater_exists (n : ℕ) : ∃ (m l : ℕ), n < m ∧ m < l := ...

#check nat_greater_m      -- nat_greater : ℕ → ℕ
#check nat_greater_l      -- nat_greater : ℕ → ℕ
#check nat_greater_spec-- nat_greater_spec : ∀ (n : ℕ),
n < nat_greater_m n ∧ nat_greater_m n < nat_greater_l n


It also supports logical conjunctions:

@[expand_exists nat_greater nat_greater_lt nat_greater_nonzero]
lemma nat_greater_exists (n : ℕ) : ∃ m : ℕ, n < m ∧ m ≠ 0 := ...

#check nat_greater         -- nat_greater : ℕ → ℕ
#check nat_greater_lt      -- nat_greater_lt : ∀ (n : ℕ), n < nat_greater n
#check nat_greater_nonzero -- nat_greater_nonzero : ∀ (n : ℕ), nat_greater n ≠ 0


Note that without the last argument nat_greater_nonzero, nat_greater_lt would be:

#check nat_greater_lt -- nat_greater_lt : ∀ (n : ℕ), n < nat_greater n ∧ nat_greater n ≠ 0



From a proof that (a) value(s) exist(s) with certain properties, constructs (an) instance(s) satisfying those properties. For instance:

@[expand_exists nat_greater nat_greater_spec]
lemma nat_greater_exists (n : ℕ) : ∃ m : ℕ, n < m := ...

#check nat_greater      -- nat_greater : ℕ → ℕ
#check nat_greater_spec -- nat_greater_spec : ∀ (n : ℕ), n < nat_greater n


It supports multiple witnesses:

@[expand_exists nat_greater_m nat_greater_l nat_greater_spec]
lemma nat_greater_exists (n : ℕ) : ∃ (m l : ℕ), n < m ∧ m < l := ...

#check nat_greater_m      -- nat_greater : ℕ → ℕ
#check nat_greater_l      -- nat_greater : ℕ → ℕ
#check nat_greater_spec-- nat_greater_spec : ∀ (n : ℕ),
n < nat_greater_m n ∧ nat_greater_m n < nat_greater_l n


It also supports logical conjunctions:

@[expand_exists nat_greater nat_greater_lt nat_greater_nonzero]
lemma nat_greater_exists (n : ℕ) : ∃ m : ℕ, n < m ∧ m ≠ 0 := ...

#check nat_greater         -- nat_greater : ℕ → ℕ
#check nat_greater_lt      -- nat_greater_lt : ∀ (n : ℕ), n < nat_greater n
#check nat_greater_nonzero -- nat_greater_nonzero : ∀ (n : ℕ), nat_greater n ≠ 0


Note that without the last argument nat_greater_nonzero, nat_greater_lt would be:

#check nat_greater_lt -- nat_greater_lt : ∀ (n : ℕ), n < nat_greater n ∧ nat_greater n ≠ 0

`