Lean4
/-- `compactRelation bs as_ps`: Produce a relation of the form:
```lean
R := fun as ↦ ∃ bs, ⋀_i a_i = p_i[bs]
```
This relation is user-visible, so we compact it by removing each `b_j` where a `p_i = b_j`, and
hence `a_i = b_j`. We need to take care when there are `p_i` and `p_j` with `p_i = p_j = b_k`.
-/
partial def compactRelation : List Expr → List (Expr × Expr) → List (Option Expr) × List (Expr × Expr) × (Expr → Expr)
| [], as_ps => ([], as_ps, id)
| b :: bs, as_ps =>
match as_ps.span (fun ⟨_, p⟩ ↦ p != b) with
| (_, []) => -- found nothing in ps equal to b
let (bs, as_ps', subst) := compactRelation bs as_ps
(b :: bs, as_ps', subst)
| (ps₁, (a, _) :: ps₂) => -- found one that matches b. Remove it.
let i := fun e ↦ e.replaceFVar b a
let (bs, as_ps', subst) := compactRelation (bs.map i) ((ps₁ ++ ps₂).map (fun ⟨a, p⟩ ↦ (a, i p)))
(none :: bs, as_ps', i ∘ subst)
