Extending have, let and suffices

This file extends the have, let and suffices tactics to allow the addition of hypotheses to the context without requiring their proofs to be provided immediately.

As a style choice, this should not be used in mathlib; but is provided for downstream users who preferred the old style.

def Mathlib.Tactic.optBinderIdent : Lean.Parser.Parser

A parser for optional binder identifiers

Equations

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

def Mathlib.Tactic.optBinderIdent.name (id : Lean.TSyntax `Mathlib.Tactic.optBinderIdent) : Lean.Name

Retrieves the name of the optional identifier, if provided. Returns this otherwise

Equations

• Mathlib.Tactic.optBinderIdent.name id = if id.raw[0].isIdent = true then id.raw[0].getId else Lean.TSyntax.getId (Lean.HygieneInfo.mkIdent { raw := id.raw[0] } `this)

def Mathlib.Tactic.haveIdLhs' : Lean.Parser.Parser

Uses checkColGt to prevent

have h
exact Nat

From being interpreted as

have h
  exact Nat

Equations

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

def Mathlib.Tactic.tacticHave_ : Lean.ParserDescr

The have tactic is for adding opaque definitions and hypotheses to the local context of the main goal. The definitions forget their associated value and cannot be unfolded, unlike definitions added by the let tactic.

• have h : t := e adds the hypothesis h : t if e is a term of type t.
• have h := e uses the type of e for t.
• have : t := e and have := e use this for the name of the hypothesis.
• have pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that have only one applicable constructor. For example, given h : p ∧ q ∧ r, have ⟨h₁, h₂, h₃⟩ := h produces the hypotheses h₁ : p, h₂ : q, and h₃ : r.
• The syntax have (eq := h) pat := e is equivalent to match h : e with | pat => _, which adds the equation h : e = pat to the local context.

The tactic supports all the same syntax variants and options as the have term.

Properties and relations

• It is not possible to unfold a variable introduced using have, since the definition's value is forgotten. The let tactic introduces definitions that can be unfolded.
• The have h : t := e is like doing let h : t := e; clear_value h.
• The have tactic is preferred for propositions, and let is preferred for non-propositions.
• Sometimes have is used for non-propositions to ensure that the variable is never unfolded, which may be important for performance reasons. Consider using the equivalent let +nondep to indicate the intent.

Equations

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

def Mathlib.Tactic.tacticLet_ : Lean.ParserDescr

The let tactic is for adding definitions to the local context of the main goal. The definition can be unfolded, unlike definitions introduced by have.

• let x : t := e adds the definition x : t := e if e is a term of type t.
• let x := e uses the type of e for t.
• let : t := e and let := e use this for the name of the hypothesis.
• let pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that let only one applicable constructor. For example, given p : α × β × γ, let ⟨x, y, z⟩ := p produces the local variables x : α, y : β, and z : γ.
• The syntax let (eq := h) pat := e is equivalent to match h : e with | pat => _, which adds the equation h : e = pat to the local context.

The tactic supports all the same syntax variants and options as the let term.

Properties and relations

• Unlike have, it is possible to unfold definitions introduced using let, using tactics such as simp, dsimp, unfold, and subst.
• The clear_value tactic turns a let definition into a have definition after the fact. The tactic might fail if the local context depends on the value of the variable.
• The let tactic is preferred for data (non-propositions).
• Sometimes have is used for non-propositions to ensure that the variable is never unfolded, which may be important for performance reasons.

Equations

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

def Mathlib.Tactic.tacticSuffices_ : Lean.ParserDescr

Given a main goal ctx ⊢ t, suffices h : t' from e replaces the main goal with ctx ⊢ t', e must have type t in the context ctx, h : t'.

The variant suffices h : t' by tac is a shorthand for suffices h : t' from by tac. If h : is omitted, the name this is used.

Equations

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

def Mathlib.Tactic.haveLetCore (goal : Lean.MVarId) (name : Lean.TSyntax `Mathlib.Tactic.optBinderIdent) (bis : Array (Lean.TSyntax `Lean.Parser.Term.letIdBinder)) (t : Option Lean.Term) (keepTerm : Bool) : Lean.Elab.TermElabM (Lean.MVarId × Lean.MVarId)

Adds hypotheses to the context, turning them into goals to be proved later if their proof terms aren't provided (t: Option Term := none).

If the bound term is intended to be kept in the context, pass keepTerm : Bool := true. This is useful when extending the let tactic, which is expected to show the proof term in the infoview.

Equations

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