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.

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

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

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

Equations

• Mathlib.Tactic.Choose.instInhabitedChooseArg = { default := Mathlib.Tactic.Choose.instInhabitedChooseArg.default }

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

Equations

• Mathlib.Tactic.Choose.instInhabitedChooseArg.default = { ref := default, name := default, expectedType? := default }

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

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

Equations

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

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

Equations

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

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.

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

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 ChooseArg → ElimStatus → Lean.MVarId → Lean.Elab.TermElabM 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.

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

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.

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

Equations

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