Lean4
/-- Add `proof : type` to the congruence closure. -/
def add (type : Expr) (proof : Expr) : CCM Unit := do
if (← get).inconsistent then
return
modifyTodo fun _ => #[]
let (isNeg, p) :=
match type with
| .app (.const ``Not []) a => (true, a)
| .forallE _ a (.const ``False []) _ => (true, a)
| .app (.app (.app (.const ``Ne [u]) α) lhs) rhs => (true, .app (.app (.app (.const ``Eq [u]) α) lhs) rhs)
| e => (false, e)
match p with
| .app (.app (.app (.const ``Eq _) _) lhs) rhs =>
if isNeg then
internalizeCore p none
addEqvCore p (.const ``False []) (← mkEqFalse proof) false
else
internalizeCore lhs none
internalizeCore rhs none
addEqvCore lhs rhs proof false
| .app (.app (.app (.app (.const ``HEq _) _) lhs) _) rhs =>
if isNeg then
internalizeCore p none
addEqvCore p (.const ``False []) (← mkEqFalse proof) false
else
internalizeCore lhs none
internalizeCore rhs none
addEqvCore lhs rhs proof true
| .app (.app (.const ``Iff _) lhs) rhs =>
if isNeg then
let neqProof ← mkAppM ``neq_of_not_iff #[proof]
internalizeCore p none
addEqvCore p (.const ``False []) (← mkEqFalse neqProof) false
else
internalizeCore lhs none
internalizeCore rhs none
addEqvCore lhs rhs (mkApp3 (.const ``propext []) lhs rhs proof) false
| _ =>
if ← pure isNeg <||> isProp p then
internalizeCore p none
if isNeg then
addEqvCore p (.const ``False []) (← mkEqFalse proof) false
else
addEqvCore p (.const ``True []) (← mkEqTrue proof) false
