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.

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

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

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.

def Mathlib.Tactic.subsingletonStx : Lean.ParserDescr

The subsingleton tactic tries to prove a goal of the form x = y or HEq x y using the fact that the types involved are subsingletons (a type with exactly zero or one terms). To a first approximation, it does apply Subsingleton.elim. As a nicety, subsingleton first runs the intros tactic.

• If the goal is an equality, it either closes the goal or fails.
• 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.

Techniques the subsingleton tactic can apply:

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

Properties

The tactic is careful not to accidentally specialize Sort _ to Prop, avoiding the following surprising behavior of apply Subsingleton.elim:

example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim

The reason this example goes through is that it applies the ∀ (p : Prop), Subsingleton p instance, specializing the universe level metavariable in Sort _ to 0.

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.

def Mathlib.Tactic.elabSubsingletonInsts.go (instTerms : List Lean.Term) (insts : Array (Lean.Term × Lean.Meta.AbstractMVarsResult)) : Lean.Elab.TermElabM (Array (Lean.Term × Lean.Meta.AbstractMVarsResult))

Main loop for addSubsingletonInsts.