theorem-proving-examples.rkt

#lang racket

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; Syntactic Sugar
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; A proposition is a dependent contract whose range ignores the result
;; and only checks for the side-condition.
;; Termination is currently omitted.
(define-syntax-rule (∀ ([x c] ...) prop)
  (->i ([x c] ...)
       (_ {x ...} (λ (_) prop))))

;; Providing a proof to a theorem is like providing a value satisfying a contract.
;; * `define/contract` checks everywhere in SCV, as opposed to Racket's
;;   ignoring self-calls. This should eventually be renamed to something else.
;; * Quirk: We need to `provide` the theorem to expose it to `havoc`.
;;   If we forget, it will deceptively appear "proved", due to no run-time error.
(define-syntax-rule (define-theorem (name [x c] ...)
                      #:conclusion prop
                      #:proof proof)
  (begin
    (define/contract name
      (∀ ([x c] ...) prop)
      (λ (x ...) proof))
    (provide (contract-out [name (∀ ([x c] ...) prop)]))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Definitions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (length l)
  (if (null? l) 0 (+ 1 (length (cdr l)))))

(define (map f xs)
  (match xs
    ['() null]
    [(cons x xs*) (cons (f x) (map f xs*))]))

(define (append xs ys)
  (match xs
    ['() ys]
    [(cons _ xs*) (cons x (append xs* ys))]))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Claims and proofs
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-theorem (map-preserves-length [f (any/c . -> . any/c)]
                                      [xs list?])
  #:conclusion (equal? (length xs) (length (map f xs)))
  #:proof
  (match xs
    ['() 'trivial]
    [(cons _ xs*) (map-preserves-length f xs*)]))

(define-theorem (append-assoc [xs list?]
                              [ys list?]
                              [zs list?])
  #:conclusion
  (equal? (append xs (append ys zs))
          (append (append xs ys) zs))
  #:proof
  (match xs
    ['() 'trivial]
    [(cons _ xs*) (append-assoc xs* ys zs)]))

(define-theorem (map-distr-append [f (any/c . -> . any/c)]
                                  [xs list?]
                                  [ys list?])
  #:conclusion
  (equal? (map f (append xs ys))
          (append (map f xs) (map f ys)))
  #:proof
  (match xs
    ['() 'trivial]
    [(cons _ xs*) (map-distr-append f xs* ys)]))

(define-theorem (length-append [xs list?]
                               [ys list?])
  #:conclusion
  (equal? (+ (length xs) (length ys))
          (length (append xs ys)))
  #:proof
  (match xs
    ['() 'trivial]
    [(cons _ xs*) (length-append xs* ys)]))