Lean4
/-- Try to apply `Subsingleton.helim` if the goal is a `HEq`. Tries synthesizing a `Subsingleton`
instance for both the LHS and the RHS.
If successful, this reduces proving `@HEq α x β y` to proving `α = β`.
-/
def subsingletonHelim? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
mvarId.withContext <|
observing? do
mvarId.checkNotAssigned `subsingletonHelim
let some (α, lhs, β, rhs) := (← withReducible mvarId.getType').heq? |
failure
withSubsingletonAsFast fun elim => do
let eqmvar ←
mkFreshExprSyntheticOpaqueMVar (← mkEq α β)
(← mvarId.getTag)
-- First try synthesizing using the left-hand side for the Subsingleton instance
if let some pf← observing? (mkAppM ``FastSubsingleton.helim #[eqmvar, lhs, rhs]) then
mvarId.assign <| elim pf
return [eqmvar.mvarId!]
let eqsymm ←
mkAppM ``Eq.symm
#[eqmvar]
-- Second try synthesizing using the right-hand side for the Subsingleton instance
if let some pf← observing? (mkAppM ``FastSubsingleton.helim #[eqsymm, rhs, lhs]) then
mvarId.assign <| elim (← mkAppM ``HEq.symm #[pf])
return [eqmvar.mvarId!]
failure
