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.

def Mathlib.Tactic.Choose.mk_sometimes (u : Lean.Level) (α : Lean.Expr) (nonemp : Lean.Expr) (p : Lean.Expr) : List Lean.Expr → Lean.Expr × Lean.Expr → Lean.MetaM (Lean.Expr × Lean.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

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Choose.mk_sometimes u α nonemp p [] (val, spec) = pure (val, spec)

inductive Mathlib.Tactic.Choose.ElimStatus : Type

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.

• success: Mathlib.Tactic.Choose.ElimStatus
• failure: List Lean.Expr → Mathlib.Tactic.Choose.ElimStatus

def Mathlib.Tactic.Choose.ElimStatus.merge : Mathlib.Tactic.Choose.ElimStatus → Mathlib.Tactic.Choose.ElimStatus → Mathlib.Tactic.Choose.ElimStatus

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

Equations

• Mathlib.Tactic.Choose.ElimStatus.success.merge x = Mathlib.Tactic.Choose.ElimStatus.success
• x.merge Mathlib.Tactic.Choose.ElimStatus.success = Mathlib.Tactic.Choose.ElimStatus.success
• (Mathlib.Tactic.Choose.ElimStatus.failure ts₁).merge (Mathlib.Tactic.Choose.ElimStatus.failure ts₂) = Mathlib.Tactic.Choose.ElimStatus.failure (ts₁ ++ ts₂)

def Mathlib.Tactic.Choose.mkFreshNameFrom (orig : Lean.Name) (base : Lean.Name) : Lean.CoreM Lean.Name

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

Equations

• Mathlib.Tactic.Choose.mkFreshNameFrom orig base = if orig = `_ then Lean.mkFreshUserName base else pure orig

def Mathlib.Tactic.Choose.choose1 (g : Lean.MVarId) (nondep : Bool) (h : Option Lean.Expr) (data : Lean.Name) : Lean.MetaM (Mathlib.Tactic.Choose.ElimStatus × Lean.Expr × Lean.MVarId)

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Choose.choose1WithInfo (g : Lean.MVarId) (nondep : Bool) (h : Option Lean.Expr) (data : Lean.TSyntax `Lean.binderIdent) : Lean.MetaM (Mathlib.Tactic.Choose.ElimStatus × Lean.MVarId)

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Choose.elabChoose (nondep : Bool) (h : Option Lean.Expr) : List (Lean.TSyntax `Lean.binderIdent) → Mathlib.Tactic.Choose.ElimStatus → Lean.MVarId → Lean.MetaM Lean.MVarId

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

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Choose.elabChoose nondep h [] x✝ x = Lean.throwError (Lean.toMessageData "expect list of variables")

def Mathlib.Tactic.Choose.choose : Lean.ParserDescr

• 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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Choose.tacticChoose!___Using_ : Lean.ParserDescr

• 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

Equations

• One or more equations did not get rendered due to their size.