The first “fact” cannot be proven because it is false! Given the definition: containsS :: Shape -> Coordinate -> Bool (Rectangle s1 s2) `containsS` (x,y) = let t1 = s1 / 2 t2 = s2 / 2 in -t1

Proof from axioms is something that takes great care: it is all too easy to skip a step that “obviously follows” from the axioms without proving that step. I’m not convinced this is all correct… r ≡ r `Intersect` univ [Axiom 4] ≡ r `Intersect` (r `Union` Complement r) [Axiom 5] ≡ (r `Intersect` r) […]

Leaving aside the argument about axioms by definition not requiring proof… Axiom 3: (r1 `Intersect` (r2 `Union` r3)) `containsR` p => (r1 `containsR` p) && ((r2 `Union` r3) `containsR` p) => (r1 `containsR` p) && ((r2 `containsR` p) || (r3 `containsR` p)) => ((r1 `containsR` p) && (r2 `containsR` p)) || ((r1 `containsR` p) && […]

One way to do this is to handle each constructor for a Region (and a Shape for those cases) and reflect those in the x-axis, i.e. flipX :: Region -> Region flipX (Translate (a,b) r) = Translate (a,-b) (flipX r) flipX (Scale (a,b) r) = Scale (a,-b) (flipX r) flipX (Complement r) = Complement (flipX […]

polygon :: [Coordinate] -> Region polygon [] = Empty polygon [x] = Empty polygon (x:xs) = halfPlanes x (xs ++ [x]) where halfPlanes x1 (x2:xs) = HalfPlane x1 x2 `Intersect` halfPlanes x2 xs halfPlanes xlast [] = Complement Empty

data Region = … | HalfPlane Coordinate Coordinate … (HalfPlane p1 p2) `containsR` p = p `isLeftOf` (p1,p2)

The simplest way to allow vertices in clockwise or anticlockwise order is to define isRightOf analogously to isLeftOf, and combine them with a boolean expression. isLeftOf :: Coordinate -> Ray -> Bool (px,py) `isLeftOf` ((ax,ay), (bx,by)) = let (s,t) = (px-ax, py-ay) (u,v) = (px-bx, py-by) in s * v >= t * u isRightOf […]

r1 `difference` r2 = r1 `Intersect` (Complement r2) annulus :: Radius -> Radius -> Region annulus rinner router = Shape (circle router) `difference` Shape (circle rinner)

area (Rectangle a b) = abs(a * b) area (RtTriangle a b) = abs(a * b) / 2 area (Ellipse r1 r2) = pi * abs(r1 * r2) perimeter (Rectangle s1 s2) = 2 * (abs s1 + abs s2) perimeter (RtTriangle s1 s2) = abs s1 + abs s2 + sqrt(s1^2 + s2^2) perimeter […]

oneCircle = Shape (Ellipse 1 1) manyCircles’ = [Translate (x,y) oneCircle | x