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

source

meta structure tactic.expand_exists.parse_ctx :

Type

original_decl : declaration
decl : bool → name → expr → pexpr → tactic unit
names : list name
pis_depth : ℕ

Data known when parsing pi expressions.

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

source

meta structure tactic.expand_exists.parse_ctx_exists :

Type

to_parse_ctx : tactic.expand_exists.parse_ctx
with_args : expr → expr
spec_chain : pexpr
exists_decls : list name

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.

source

meta structure tactic.expand_exists.parse_ctx_props :

Type

to_parse_ctx_exists : tactic.expand_exists.parse_ctx_exists
project_proof : pexpr → pexpr

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

source

meta def tactic.expand_exists.instantiate_exists_decls (ctx : tactic.expand_exists.parse_ctx_exists) (p : expr) :

expr

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.

source

meta def tactic.expand_exists.parse_one_prop (ctx : tactic.expand_exists.parse_ctx_props) (p : expr) :

tactic unit

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

source

meta def tactic.expand_exists.parse_props :

tactic.expand_exists.parse_ctx_props → expr → tactic unit

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

source

meta def tactic.expand_exists.parse_exists :

tactic.expand_exists.parse_ctx_exists → expr → tactic unit

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.

source

meta def tactic.expand_exists.parse_pis :

tactic.expand_exists.parse_ctx → expr → tactic unit

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

source

meta def tactic.expand_exists_attr :

user_attribute unit (list name)

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

source

def tactic_doc.attribute.expand_exists :

tactic_doc_entry

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

expand_exists #

`expand_exists` #