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) (α nonemp 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.

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 : ElimStatus
• failure (ts : List Lean.Expr) : ElimStatus

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

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

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

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

structure Mathlib.Tactic.Choose.ChooseArg : Type

Parsed information from a choose argument, which may include a type annotation.

• ref : Lean.Syntax

  The syntax reference for the identifier (for hover info)

• name : Lean.Name

  The name to use for the introduced variable

• expectedType? : Option Lean.Term

  Optional expected type annotation

instance Mathlib.Tactic.Choose.instInhabitedChooseArg : Inhabited ChooseArg

def Mathlib.Tactic.Choose.instInhabitedChooseArg.default : ChooseArg

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

A choose argument is either a bare identifier or a parenthesized extended binder

def Mathlib.Tactic.Choose.parseChooseArg (stx : Lean.TSyntax `Mathlib.Tactic.Choose.chooseBinder) : Lean.MetaM ChooseArg

Parse a choose argument from chooseBinder syntax. Accepts:

• x - plain identifier
• _ - anonymous
• (x : T) - identifier with type annotation
• (_ : T) - anonymous with type annotation

def Mathlib.Tactic.Choose.choose1 (g : Lean.MVarId) (nondep : Bool) (h : Option Lean.Expr) (data : Lean.Name) : Lean.MetaM (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.

def Mathlib.Tactic.Choose.choose1WithInfo (g : Lean.MVarId) (nondep : Bool) (h : Option Lean.Expr) (arg : ChooseArg) : Lean.Elab.TermElabM (ElimStatus × Lean.MVarId)

A wrapper around choose1 that parses identifiers, adds variable info to new variables, and optionally checks the type annotation.

def Mathlib.Tactic.Choose.elabChoose (nondep : Bool) (h : Option Lean.Expr) : List ChooseArg → ElimStatus → Lean.MVarId → Lean.Elab.TermElabM Lean.MVarId

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

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.

Like intro, the choose tactic supports type annotations to specify the expected type of the introduced variables. This is useful for documentation and for catching mistakes early:

example (h : ∃ n : ℕ, n > 0) : True := by
  choose (n : ℕ) (hn : n > 0) using h
  trivial

If the provided type does not match the actual type, an error is raised.

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

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.

Like intro, the choose tactic supports type annotations to specify the expected type of the introduced variables. This is useful for documentation and for catching mistakes early:

example (h : ∃ n : ℕ, n > 0) : True := by
  choose (n : ℕ) (hn : n > 0) using h
  trivial

If the provided type does not match the actual type, an error is raised.

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