8 Conjectures

Say you have a language and you have defined some functions on the language:

(define-language Shapes
  (s (square x y r)
     (overlay s s))
  ((x y r) number)
  ; for the results
  (t (rectangle x y x y))
 
; determine the area of a shape
(define-metafunction Shapes
  ; we leave off the optional contract because there is no specification for the domain
  [(area (rectangle x_min x_max y_min y_max))
   ,(* (- (term x_max) (term x_min)) (- (term y_max) (term y_min)))]
  [(area (square x y r))
   ,(* (term r) (term r))]
  [(area (overlay s_top s_bot))
   ,(+ (term (area s_top)) (term (area s_bot)))])
 
; compute the bounding rectangle of a shape
(define-metafunction Shapes
  bb : s -> t
  [(bb (square x y r))
   (rectangle x ,(+ (term x) (term r)) ,(- (term y) (term r)) y)]
  [(bb (overlay s_top s_bot))
   (bb-aux (bb s_top) (bb s_bot))])
 
; auxiliary function:
(define-metafunction Shapes
  bb-aux : t t -> t
  [(bb-aux (rectangle x_min1 x_max1 y_min1 y_max1)
              (rectangle x_min2 x_max2 y_min2 y_max2))
   (rectangle ,(min (term x_min1) (term x_min2))
              ,(max (term x_max1) (term x_max2))
              ,(min (term y_min1) (term y_min2))
              ,(max (term y_max1) (term y_max2)))]))

You can experiment with these functions:
> (term (bb (overlay (square 1.1 2.7 3) (square -7.2 -2.0 3))))

'(rectangle -7.2 4.1 -5.0 2.7)

> (term (area (bb (overlay (square 1.1 2.7 3) (square -7.2 -2.0 3)))))

87.01

> (term (area (square 1.1 2.7 3)))

9

> (term (area (square -7.2 -2.0 3)))

9

From experiments such as these and/or inspiration, you may come up with conjectures such as

the area of the bounding area of some shape s is always larger than the area of the s

in English or, with Redex,

(> (area (bb s)) (area s))

It turns out that Redex comes with a random testing tool that can help you check such conjectures:
> (redex-check Shapes s (> (term (area (bb s))) (term (area s))))

redex-check: counterexample found after 1 attempt:

(square +inf.0 +inf.0 +inf.0)

The redex-check facility generates examples of s with respect to language Shapes and checks whether the conjecture—formulated as a Boolean expression— (> (term (area (bb s))) (term (area s))) produces true. If so, great. If not, it has found a counter-example, and in this case it has. A square’s bounding box is itself, and the area of the two are equal. So we revise our conjecture to use >= and not just >:
> (redex-check Shapes s (>= (term (area (bb s))) (term (area s))))

redex-check: counterexample found after 1 attempt:

(square +inf.0 +inf.0 +inf.0)

But again, redex-check finds a counter-example. This time, the counter-example consists of a combination of two squares that overlap. While the area of the bounding box is just the area of the surrounding rectangle, the area function computes the area of an overlay construction as the sum of the two.

Draw the situation on a grid to figure out why the conjecture fails.

To fix the conjecture, we need to change the area function. Specifically, we need to subtract the overlap between the two shapes:
(area (overlay s_top s_bot)) =
(- (+ (area s_top) (area s_bot)) (area (intersection s_top s_bot)))
meaning we also need to define the intersection function.

In short, before you try to prove conjectures it is often helpful to have them checked so that minor typos or real misunderstandings are eliminated before you invest effort in a full-fledged proof.