mathlib3 documentation

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
```