Lean4
/-- Return true iff the given function application are congruent
`e₁` should have the form `f a` and `e₂` the form `g b`.
See paper: Congruence Closure for Intensional Type Theory. -/
partial def isCongruent (e₁ e₂ : Expr) : CCM Bool := do
let .app f a := e₁ |
failure
let .app g b := e₂ |
failure
if (← getEntry e₁).any Entry.fo then
e₁.withApp fun f₁ args₁ =>
e₂.withApp fun f₂ args₂ => do
if ha : args₁.size = args₂.size then
for hi : i in [:args₁.size]do
if (← getRoot args₁[i]) != (← getRoot (args₂[i]'(ha.symm ▸ hi.2.1))) then
return false
if f₁ == f₂ then
return true
else if (← getRoot f₁) != (← getRoot f₂) then
-- `f₁` and `f₂` are not equivalent
return false
else if ← pureIsDefEq (← inferType f₁) (← inferType f₂) then
return true
else
return false
else
return false
else
-- Given `e₁ := f a`, `e₂ := g b`
if (← getRoot a) != (← getRoot b) then
-- `a` and `b` are not equivalent
return false
else if (← getRoot f) != (← getRoot g) then
-- `f` and `g` are not equivalent
return false
else if ← pureIsDefEq (← inferType f) (← inferType g) then
/- Case 1: `f` and `g` have the same type, then we can create a congruence proof for
`f a ≍ g b` -/
return true
else if f.isApp && g.isApp then
-- Case 2: `f` and `g` are congruent
isCongruent f g
else
/-
f and g are not congruent nor they have the same type.
We can't generate a congruence proof in this case because the following lemma
`hcongr : f₁ ≍ f₂ → a₁ ≍ a₂ → f₁ a₁ ≍ f₂ a₂`
is not provable.
Remark: it is also not provable in MLTT, Coq and Agda (even if we assume UIP).
-/
return false
