ChainIntersectionAlgorithm.lean

/-
This is a legacy file, no longer needed for the human facing specification of
mesh intersection.
-/

import CSG.Def
import CSG.Legacy.ChainDef
import CSG.Impl.Legacy.ChainIntersectionAlgorithm
import CSG.Proof.ChainIntersectionAlgorithm

/-!
# The chain intersection algorithm and its specification
-/

namespace CSG.Legacy

/--
The **intersection of two simplicial chains**, as a computable function. The
implementation lives in `CSG.Impl.Legacy.ChainIntersectionAlgorithm`. -/
def intersect (w₁ w₂ : Chain) : Chain :=
  Impl.Legacy.ChainIntersectionAlgorithm.intersect w₁ w₂

/-- **Correctness of the intersection algorithm** (Feito & Rivero, Theorem 4).

For normal inputs, the chain produced by `intersect` is normal and its solid is
the intersection of the input solids, up to a finite union of planes.  This is
the same specification claimed existentially in
`CSG.Legacy.exists_intersection_chain`, now realized by a concrete function. -/
theorem intersect_spec (w₁ w₂ : Chain) (h₁ : Chains.Normal w₁) (h₂ : Chains.Normal w₂) :
    Chains.Normal (intersect w₁ w₂) ∧
      EqOffPlanes (Chains.solid (intersect w₁ w₂)) (Chains.solid w₁ ∩ Chains.solid w₂) :=
  Proof.ChainIntersectionAlgorithm.intersect_spec w₁ w₂ h₁ h₂

end CSG.Legacy