openai.rkt

#lang rosette

(require rackunit syntax/parse/define)

;; https://openai.com/blog/formal-math/

(define-simple-macro (prove e ...) (check-pred unsat? (verify (begin e ...))))

(test-case "Problem 1"
  (define-symbolic* x p real?)

  (prove
   (assume (= (abs (- x 2)) p))
   (assume (< x 2))
   (assert (= (- x p) (- 2 (* 2 p))))))

(test-case "Problem 3"
  (define-symbolic* A B x real?)
  (define-symbolic* f g (~> real? real?))

  (prove
   (assume (forall (list x) (= (f x) (+ (* A x) B))))
   (assume (forall (list x) (= (g x) (+ (* B x) A))))
   (assume (not (= A B)))
   (assume (forall (list x) (= (- (f (g x)) (g (f x))) (- B A))))
   (assert (= (+ A B) 0))))

(test-case "Problem 4"
  (define-symbolic* a b c real?)
  (prove
   (assume (and (< 0 a) (< 0 b) (< 0 c)))
   (assume (< c (+ a b)))
   (assume (< b (+ a c)))
   (assume (< a (+ b c)))
   (assert (<= (+ (* a a (- (+ b c) a))
                  (* b b (- (+ c a) b))
                  (* c c (- (+ a b) c)))
               (* 3 a b c)))))

(test-case "Problem 5"
  (define-symbolic* u (~> integer? real?))
  (define-symbolic* n integer?)

  (prove
   (assume (forall (list n) (= (u (+ n 1)) (+ (u n) 1))))
   (assume (= (for/fold ([sum 0]) ([i (in-range 98)]) (+ sum (u (+ i 1)))) 137))
   (assert (= (for/fold ([sum 0]) ([i (in-range 49)]) (+ sum (u (* (+ i 1) 2)))) 93))))

(test-case "Problem 6"
  (define-symbolic* a b c real?)

  (prove
   (assert
    (>=
     (* (+ (* a a) (* a b) (* b b))
        (+ (* b b) (* b c) (* c c))
        (+ (* c c) (* c a) (* a a)))
     (expt (+ (* a b) (* b c) (* c a)) 3)))))