flip f x y = f y x flip (flip f) x y = flip f y x = f x y ∴ flip (flip f) = f

(Polygon pts) `containsS` p = let leftOfList = map isLeftOfp (zip pts (tail pts ++ [head pts])) isLeftOfp = isLeftOf p in and leftOfList

First, the new definitions: data Region = UnitCircle | Polygon [Coordinate] | AffineTransform Matrix3x3 Region | Empty deriving Show type Vector3 = (Float, Float, Float) type Matrix3x3 = (Vector3, Vector3, Vector3) type Matrix2x2 = ((Float, Float), (Float, Float)) And some old ones that will suffice unchanged: type Coordinate = (Float, Float) type Ray = (Coordinate, […]

There are a couple of ways to do this (the basic problem being how to deal with concave polygons). One way is to convert the polygon to a convex hull and a list of triangles representing subtractions from the convex hull, then check containment within the hull and non-containment within the triangles. However, I present […]

See Exercises 2.4 and 5.1. Then: area” :: Shape -> Float area” (Polygon (v1:vs)) = if convex (Polygon (v1:vs)) then let areas = map ((v2, v3) -> triArea v1 v2 v3) (zip vs (tail vs)) in foldl (+) 0 areas else error “Non-convex polygon”

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) && […]