# Documentation

Mathlib.Tactic.Choose

# choose tactic #

Performs Skolemization, that is, given h : ∀ a:α, ∃ b:β, p a b |- G produces f : α → β, hf: ∀ a, p a (f a) |- G.

TODO: switch to rcases syntax: choose ⟨i, j, h₁ -⟩ := expr.

Given α : Sort u, nonemp : Nonempty α, p : α → Prop, a context of free variables ctx, and a pair of an element val : α and spec : p val, mk_sometimes u α nonemp p ctx (val, spec) produces another pair val', spec' such that val' does not have any free variables from elements of ctx whose types are propositions. This is done by applying Function.sometimes to abstract over all the propositional arguments.

Equations
Instances For

Results of searching for nonempty instances, to eliminate dependencies on propositions (choose!). success means we found at least one instance; failure ts means we didn't find instances for any t ∈ ts. (failure [] means we didn't look for instances at all.)

Rationale: choose! means we are expected to succeed at least once in eliminating dependencies on propositions.

Instances For

Combine two statuses, keeping a success from either side or merging the failures.

Instances For

mkFreshNameFrom orig base returns mkFreshUserName base if orig = _ and orig otherwise.

Instances For
def Mathlib.Tactic.Choose.choose1 (g : Lean.MVarId) (nondep : Bool) (h : ) (data : Lean.Name) :

Changes (h : ∀xs, ∃a:α, p a) ⊢ g to (d : ∀xs, a) ⊢ (s : ∀xs, p (d xs)) → g and (h : ∀xs, p xs ∧ q xs) ⊢ g to (d : ∀xs, p xs) ⊢ (s : ∀xs, q xs) → g. choose1 returns a tuple of

• the error result (see ElimStatus)
• the data new free variable that was "chosen"
• the new goal (which contains the spec of the data as domain of an arrow type)

If nondep is true and α is inhabited, then it will remove the dependency of d on all propositional assumptions in xs. For example if ys are propositions then (h : ∀xs ys, ∃a:α, p a) ⊢ g becomes (d : ∀xs, a) (s : ∀xs ys, p (d xs)) ⊢ g.

Instances For
def Mathlib.Tactic.Choose.choose1WithInfo (g : Lean.MVarId) (nondep : Bool) (h : ) (data : Lean.TSyntax Lean.binderIdent) :

A wrapper around choose1 that parses identifiers and adds variable info to new variables.

Instances For
def Mathlib.Tactic.Choose.elabChoose (nondep : Bool) (h : ) :
List (Lean.TSyntax Lean.binderIdent)

A loop around choose1. The main entry point for the choose tactic.

Equations
Instances For
• choose a b h h' using hyp takes a hypothesis hyp of the form ∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b for some P Q : X → Y → A → B → Prop and outputs into context a function a : X → Y → A, b : X → Y → B and two assumptions: h : ∀ (x : X) (y : Y), P x y (a x y) (b x y) and h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y). It also works with dependent versions.

• choose! a b h h' using hyp does the same, except that it will remove dependency of the functions on propositional arguments if possible. For example if Y is a proposition and A and B are nonempty in the above example then we will instead get a : X → A, b : X → B, and the assumptions h : ∀ (x : X) (y : Y), P x y (a x) (b x) and h' : ∀ (x : X) (y : Y), Q x y (a x) (b x).

The using hyp part can be omitted, which will effectively cause choose to start with an intro hyp.

Examples:

example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := by
choose i j h using h
guard_hyp i : ℕ → ℕ → ℕ
guard_hyp j : ℕ → ℕ → ℕ
guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n
trivial

example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := by
choose! f h h' using h
guard_hyp f : ℕ → ℕ
guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i
guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i
trivial

Instances For
• choose a b h h' using hyp takes a hypothesis hyp of the form ∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b for some P Q : X → Y → A → B → Prop and outputs into context a function a : X → Y → A, b : X → Y → B and two assumptions: h : ∀ (x : X) (y : Y), P x y (a x y) (b x y) and h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y). It also works with dependent versions.

• choose! a b h h' using hyp does the same, except that it will remove dependency of the functions on propositional arguments if possible. For example if Y is a proposition and A and B are nonempty in the above example then we will instead get a : X → A, b : X → B, and the assumptions h : ∀ (x : X) (y : Y), P x y (a x) (b x) and h' : ∀ (x : X) (y : Y), Q x y (a x) (b x).

The using hyp part can be omitted, which will effectively cause choose to start with an intro hyp.

Examples:

example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := by
choose i j h using h
guard_hyp i : ℕ → ℕ → ℕ
guard_hyp j : ℕ → ℕ → ℕ
guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n
trivial

example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := by
choose! f h h' using h
guard_hyp f : ℕ → ℕ
guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i
guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i
trivial
`
Instances For