scv-proof-examples.rkt

#lang racket/base
(require racket/match
         racket/contract
         racket/list
         racket/function
         (only-in typed/racket/base assert))

;; Assume primitive `induct-on` that can inspect contracts
;; and produce induction principles for *some* contracts
;; deemed to specify inductive data
;; (e.g. naturals, and many ad-hoc recursive contracts
;; whose recursive references follow immutable struct fields)

;; (define nat-induct (induct-on exact-nonnegative-integer?))
(define/contract nat-induct
  (->i ([x exact-nonnegative-integer?]
        [P (exact-nonnegative-integer? . -> . contract?)]
        [on-0 {P} (->i ([x 0]) (_ {x} (P x)))]
        [on-n {P} (->i ([n exact-nonnegative-integer?] [ih {n} (P n)])
                       (_ {n} (P (+ 1 n))))])
       (_ {x P} (P x)))
  ;; Assume `induct-on` generates something like this
  (λ (n P on-0 on-n)
    (case n
      [(0)  (on-0 0)]
      [else (on-n (- n 1) (nat-induct (- n 1) P on-0 on-n))])))

;; (define list-induct (induct-on list?))
(define/contract list-induct
  (->i ([xs list?]
        [P (list? . -> . contract?)]
        [on-null {P} (->i ([x null?]) (_ {x} (P x)))]
        [on-cons {P} (->i ([x.car any/c] [x.cdr list?] [ih {x.cdr} (P x.cdr)])
                          (_ {x.car x.cdr} (P (cons x.car x.cdr))))])
       (_ {xs P} (P xs)))
  ;; Assume `induct-on` generates something like this
  (λ (l P on-null on-cons)
    (match l
      ['() (on-null '())]
      [(cons x l*) (on-cons x l* (list-induct l* P on-null on-cons))])))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; fib (nat induction)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define plus-2-2/c (λ _ (= (+ 2 2) 4)))
(define plus-comm/c (->i ([x integer?] [y integer?])
                         (_ {x y} (λ _ (= (+ x y) (+ y x))))))
(define int-up/c (->i ([n integer?]) (_ {n} (and/c integer? (λ (m) (< n m))))))

(define/contract plus-2-2 plus-2-2/c 'duh)
(define/contract plus-comm plus-comm/c (λ (x y) 'duh))
(define/contract int-up int-up/c (λ (n) (+ n 1)))

(define fib
  (match-lambda
    [0 0]
    [1 1]
    [n (+ (fib (- n 1)) (fib (- n 2)))]))

(define/contract fib-2=1 (λ _ (= (fib 2) 1))
  (assert (= (fib 2) (+ (fib 1) (fib 0)))))

(define/contract fib-3=2 (λ _ (= (fib 3) 2))
  (begin
    (assert (= (fib 3) (+ (fib 2) (fib 1))))
    ;; Somehow need to have kept around fib-2=1's flat contract
    ;; If execution never approximates, none of these is neccessary
    fib-2=1))

(define (up/c f)
  (->i ([n exact-nonnegative-integer?])
       (_ {n} (λ _ (<= (f n) (f (+ 1 n)))))))

(define/contract fib-up (up/c fib)
  (match-lambda
    [0 (assert (<  (fib 0) (fib 1)))]
    [1 (assert (<= (fib 1) (+ (fib 1) (fib 0))))
       (assert (= (fib 2) (+ (fib 1) (fib 0))))]
    [n (assert (<= (fib n) (+ (fib n) (fib (- n 1)))))
       (assert (= (fib (+ n 1)) (+ (fib n) (fib (- n 1)))))]))

(define mono/c
  (->i ([f (exact-nonnegative-integer? . -> . integer?)]
        [up-f {f} (up/c f)]
        [x exact-nonnegative-integer?]
        [y {x} (and/c exact-nonnegative-integer? (>/c x))])
       (_ {f x y} (<= (f x) (f y)))))

(define/contract f-mono mono/c
  (λ (f up x y)
    (nat-induct (- y (+ 1 x))
                (λ (d) (<= (f x) (f (+ x d))))
                (λ (d) (assert (<= (f x) (f (+ x 1)))))
                (λ (d ih)
                  (assert (<= (f x) (f (- y 1))))
                  (up (- y 1))))))

(define/contract fib-mono
  (->i ([n exact-nonnegative-integer?]
        [m {n} (>/c n)])
       (_ {n m} (λ _ (<= (fib n) (fib m)))))
  (λ (n m)
    (f-mono fib fib-up n m)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; append (list induction)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; assume definitions of `append`, `map` available in same module

(define append-nil-id/c
  (->i ([xs list?]) (_ {xs} (λ _ (equal? (append xs '()) xs)))))
(define append-assoc/c
  (->i ([xs list?] [ys list?] [zs list?])
       (_ (xs ys zs)
          (λ _ (equal? (append xs (append ys zs))
                       (append (append xs ys) zs))))))
(define map-fusion/c
  (parametric->/c
   {α β γ}
   (->i ([f (β . -> . γ)]
         [g (α . -> . β)]
         [xs (listof α)])
        (_ {f g xs} (λ _ (equal? (map (compose1 f g) xs)
                                 (map f (map g xs))))))))

(define/contract append-nil-id append-nil-id/c
  (λ (xs)
    (list-induct xs
                 (λ (l) (λ _ (equal? (append l '()) l)))
                 (λ (mt) 'duh)
                 (λ (h t ih) 'duh))))
(define/contract append-assoc append-assoc/c
  (λ (xs ys zs)
    (list-induct
     xs
     (λ (l)
       (λ _ (equal? (append l (append ys zs))
                    (append (append l ys) zs))))
     (λ (_null) ; shouldn't need any of the blow
       (assert (equal? (append '() (append ys zs)) (append ys zs)))
       (assert (equal? (append (append '() ys) zs) (append ys zs))))
     (λ (x xs* ih) ; shouldn't need any/most of the below
       (define lhs  (append (cons x xs*) (append ys zs)))
       (define lhs* (cons x (append xs* (append ys zs))))
       (define rhs  (append (append (cons x xs*) ys) zs))
       (define rhs* (append (cons x (append xs* ys)) zs))
       (assert (equal? lhs lhs*))
       (assert (equal? rhs rhs*))
       (assert (equal? lhs* rhs*))))))
(define/contract map-fusion map-fusion/c
  (λ (f g xs)
    (list-induct xs
                 (λ (l) (λ _ (equal? (map (compose1 f g) l) (map f (map g l)))))
                 (λ (mt) 'duh)
                 (λ (h t ih) 'duh))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; swap (case analysis )
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define swap
  (match-lambda
    [(list* x₁ x₂ xs) (if (> x₁ x₂) (list* x₂ x₁ xs) (list* x₁ x₂ xs))]
    [xs xs]))

(define/contract swap-idemp
  (->i ([xs list?])
       (_ (xs) (λ _ (equal? (swap (swap xs)) xs))))
  (match-lambda
    [(list* x₁ x₂ xs) (if (> x₁ x₂) 'duh 'duh)]
    [_ 'duh]))