subsingleton tactic

The subsingleton tactic closes Eq or HEq goals using an argument that the types involved are subsingletons. To first approximation, it does apply Subsingleton.elim but it also will try proof_irrel_heq, and it is careful not to accidentally specialize Sort _ to Prop.

def Lean.Meta.mkSubsingleton (ty : Expr) : MetaM Expr

Returns the expression Subsingleton ty.

Equations

• Lean.Meta.mkSubsingleton ty = do let u ← Lean.Meta.getLevel ty pure ((Lean.Expr.const `Subsingleton [u]).app ty)

def Lean.Meta.synthSubsingletonInst (ty : Expr) (insts : Array (Term × AbstractMVarsResult) := #[]) : MetaM Expr

Synthesizes a Subsingleton ty instance with the additional local instances made available.

Equations

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

def Lean.MVarId.subsingleton (g : MVarId) (insts : Array (Term × Meta.AbstractMVarsResult) := #[]) : MetaM Unit

Closes the goal g whose target is an Eq or HEq by appealing to the fact that the types are subsingletons. Fails if it cannot find a way to do this.

Has support for showing BEq instances are equal if they have LawfulBEq instances.

Equations

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

def Mathlib.Tactic.subsingletonStx : Lean.ParserDescr

subsingleton proves the main goal of the form ∀ a ... b, x = y or ∀ a ... b, x ≍ y using the fact that the type(s) of x and y are subsingletons (a type with exactly zero or one elements). If subsingleton cannot close the goal, it fails.

Techniques the subsingleton tactic can apply:

• proof irrelevance
• heterogeneous proof irrelevance (via proof_irrel_heq)
• using Subsingleton (via Subsingleton.elim)
• proving instances of the type BEq α are equal if they are both lawful (via lawful_beq_subsingleton)

• subsingleton [inst1, inst2, ...] can be used to add additional Subsingleton instances to the local context. This can be more flexible than have := inst1; have := inst2; ...; subsingleton since the tactic does not require that all placeholders be solved for.

Equations

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

def Mathlib.Tactic.elabSubsingletonInsts (instTerms? : Option (Array Lean.Term)) : Lean.Elab.TermElabM (Array (Lean.Term × Lean.Meta.AbstractMVarsResult))

Elaborates the terms like how Lean.Elab.Tactic.addSimpTheorem does, abstracting their metavariables.

Equations

• Mathlib.Tactic.elabSubsingletonInsts (some instTerms) = Mathlib.Tactic.elabSubsingletonInsts.go✝ instTerms.toList #[]
• Mathlib.Tactic.elabSubsingletonInsts instTerms? = pure #[]