liftFromEq — Mathlib

Lean4
/-- Given a reflexive relation `R`, and a proof `H : a = b`, build a proof for `R a b` -/
def liftFromEq (R : Name) (H : Expr) : MetaM Expr := do
  if R == ``Eq then
    return H
  let HType ←
    whnf
        (← inferType H)
          -- `HType : @Eq A a _`

  let some (A, a, _) := HType.eq? |
    throwError "failed to build liftFromEq equality proof expected: {H}"
  let motive ←
    withLocalDeclD `x A fun x => do
        let hType ← mkEq a x
        withLocalDeclD `h hType fun h =>
            mkRel R a x >>=
              mkLambdaFVars
                #[x, h]
                  -- `minor : R a a := by rfl`

  let minor ←
    do
      let mt ← mkRel R a a
      let m ← mkFreshExprSyntheticOpaqueMVar mt
      m.mvarId!.applyRfl
      instantiateMVars m
  mkEqRec motive minor H
Похожие утверждения