Lean4
/-- `PComp.add c1 c2 elimVar` creates the result of summing the linear comparisons `c1` and `c2`,
during the process of eliminating the variable `elimVar`.
The computation assumes, but does not enforce, that `elimVar` appears in both `c1` and `c2`
and does not appear in the sum.
Computing the sum of the two comparisons is easy; the complicated details lie in tracking the
additional fields of `PComp`.
* The historical set `pcomp.history` of `c1 + c2` is the union of the two historical sets.
* `vars` is the union of `c1.vars` and `c2.vars`.
* The effectively eliminated variables of `c1 + c2` are the union of the two effective sets,
with `elim_var` inserted.
* The implicitly eliminated variables of `c1 + c2` are those that appear in
`vars` but not `c.vars` or `effective`.
(Note that the description of the implicitly eliminated variables of `c1 + c2` in the algorithm
described in Section 6 of https://doi.org/10.1016/B978-0-444-88771-9.50019-2 seems to be wrong:
that says it should be `(c1.implicit.union c2.implicit).sdiff explicit`.
Since the implicitly eliminated sets start off empty for the assumption,
this formula would leave them always empty.)
-/
def add (c1 c2 : PComp) (elimVar : ℕ) : PComp :=
let c := c1.c.add c2.c
let src := c1.src.add c2.src
let history := c1.history.union c2.history
let vars := c1.vars.union c2.vars
let effective := (c1.effective.union c2.effective).insert elimVar
let implicit := (vars.sdiff (.ofList c.vars _)).sdiff effective
⟨c, src, history, effective, implicit, vars⟩
