Lean4
/-- Make a `CongrResult` from a LHS, a RHS, and a proof of an Iff, Eq, or HEq.
The proof is allowed to have a metavariable for its type.
Validates the inputs and throws errors in the `pf?` function.
The `pf?` function is responsible for finally unifying the type of `pf` with `lhs` and `rhs`. -/
def mk' (lhs rhs : Expr) (pf : Expr) : CongrResult where
lhs := lhs
rhs := rhs
pf? :=
if (isRefl? pf).isSome then none
else
some fun
| .eq => do
ensureSidesDefeq (← toEqPf)
| .heq => do
ensureSidesDefeq (← toHEqPf)
where
/-- Given a `pf` of an `Iff`, `Eq`, or `HEq`, return a proof of `Eq`.
If `pf` is not obviously any of these, weakly try inserting `propext` to make an `Iff`
and otherwise unify the type with `Eq`. -/
toEqPf : MetaM Expr := do
let ty ← whnf (← inferType pf)
if let some .. := ty.iff? then
mkPropExt pf
else if let some .. := ty.eq? then
return pf
else if let some (lhsTy, _, rhsTy, _) := ty.heq? then
unless ← isDefEq lhsTy rhsTy do
throwError "Cannot turn HEq proof into an equality proof. Has type{indentD ty}"
mkAppM ``eq_of_heq #[pf]
else if ← Meta.isProp lhs then
mkPropExt (← ensureIff pf)
else
discard <| mkEqForExpectedType (← inferType pf)
return pf
/-- Given a `pf` of an `Iff`, `Eq`, or `HEq`, return a proof of `HEq`.
If `pf` is not obviously any of these, weakly try making it be an `Eq` or an `Iff`,
and otherwise make it be a `HEq`. -/
toHEqPf : MetaM Expr := do
let ty ← whnf (← inferType pf)
if let some .. := ty.iff? then
mkAppM ``heq_of_eq #[← mkPropExt pf]
else if let some .. := ty.eq? then
mkAppM ``heq_of_eq #[pf]
else if let some .. := ty.heq? then
return pf
else if ← withNewMCtxDepth <| isDefEq (← inferType lhs) (← inferType rhs) then
mkAppM ``heq_of_eq #[← toEqPf]
else
discard <| mkHEqForExpectedType (← inferType pf)
return pf
/-- Get the sides of the type of `pf` and unify them with the respective `lhs` and `rhs`. -/
ensureSidesDefeq (pf : Expr) : MetaM Expr := do
let pfTy ← inferType pf
let some (_, lhs', _, rhs') := (← whnf pfTy).sides? |
panic! "Unexpectedly did not generate an eq or heq"
unless ← isDefEq lhs lhs' do
throwError "Congruence hole has type{(indentD pfTy)}\n\
but its left-hand side is not definitionally equal to the expected value{indentD lhs}"
unless ← isDefEq rhs rhs' do
throwError "Congruence hole has type{(indentD pfTy)}\n\
but its right-hand side is not definitionally equal to the expected value{indentD rhs}"
return pf
