;;; Vikalpa --- Proof Assistant
;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
;;;
;;; This file is part of Vikalpa.
;;;
;;; Vikalpa is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or
;;; (at your option) any later version.
;;;
;;; Vikalpa is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
;;; General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.

(define-module (vikalpa prelude)
  #:export (prelude)
  #:use-module (vikalpa))

(define (exact-positive-integer? x)
  (and (exact-integer? x)
       (positive? x)))

(define (exact-negative-integer? x)
  (and (exact-integer? x)
       (negative? x)))

(define (succ x)
  (if (number? x)
      (+ x 1)
      1))

(define (pred x)
  (if (number? x)
      (- x 1)
      -1))

(define (negate x)
  (if (exact-integer? x)
      (- x)
      0))

(define-syntax implies
  (syntax-rules ()
    ((_ x y) (if x y #t))
    ((_ x y z ...) (if x (implies y z ...) #t))))

(define-system prelude/macro ()
  (define-syntax-rules cond (else)
    ((cond (else e)) e)
    ((cond (test then) . rest)
     (if test then (cond . rest))))
  (define-syntax-rules or ()
    ((or) '#f)
    ((or x) x)
    ((or x . xs) (if x x (or . xs))))
  (define-syntax-rules implies ()
    ((implies x y) (if x y #t))
    ((implies x y z . rest)
     (if x (implies y z . rest) #t)))
  (define-syntax-rules is-a ()
    ((is-a x y) (implies x (equal? y #t)))))

(define-system prelude/axiom/equal (prelude/macro)
  (define-axiom equal-same (x)
    (equal? (equal? x x) '#t))
  (define-axiom equal-swap (x y)
    (equal? (equal? x y) (equal? y x)))
  (define-axiom equal-if (x y)
    (implies (equal? x y) (equal? x y)))
  (define-axiom equal-if-false (x y)
    (if x #t (equal? x #f))))

(define-system prelude/axiom/if (prelude/axiom/equal)
  (define-axiom if-nest (x y z)
    (if x
        (equal? (if x y z) y)
        (equal? (if x y z) z)))
  (define-axiom if-true (x y)
    (equal? (if '#t x y) x))
  (define-axiom if-false (x y)
    (equal? (if '#f x y) y))
  (define-axiom if-same (x y)
    (equal? (if x y y) y))
  (define-axiom if-not (x y z)
    (equal? (if (not x) y z)
            (if x z y))))

(define-system prelude/number (prelude/axiom/if)
  (define-core-function number? (x) number?)
  (define-axiom number-predicate (x)
    (is-a (number? x) (number? x)))

  (define-core-function real? (x) real?)
  (define-axiom real-predicate (x)
    (implies (real? x) (equal? (real? x) #t)))
  (define-axiom real-is-a-numbers (x)
    (implies (real? x) (equal? (number? x) #t)))

  (define-core-function integer? (x) integer?)
  (define-axiom integer-predicate (x)
    (implies (integer? x) (equal? (integer? x) #t)))
  (define-axiom integer-is-a-real (x)
    (implies (integer? x) (equal? (number? x) #t)))

  (define-core-function/guard exact? (x) (number? x) exact?)
  (define-axiom exact-predicate (x)
    (implies (exact? x) (equal? (exact? x) #t)))

  (define-function/guard inexact? (x)
    (number? x)
    (not (exact? x)))
  (define-theorem inexact-predicate (x)
    (implies (inexact? x) (equal? (inexact? x) #t)))

  (define-core-function exact-integer? (x) exact-integer?)
  (define-axiom exact-integer-predicate (x)
    (implies (exact-integer? x) (equal? (exact-integer? x) #t)))
  (define-axiom exact-integer-is-a-integer (x)
    (implies (exact-integer? x) (equal? (integer? x) #t)))
  (define-axiom exact-integer-is-a-exact (x)
    (implies (exact-integer? x) (equal? (exact? x) #t)))

  (define-core-function/guard < (x y) (and (real? x) (real? y)) <)
  (define-axiom less-than-predicate (x y)
    (implies (< x y) (equal? (< x y) #t)))

  (define-function/guard positive? (x)
    (real? x)
    (< 0 x))
  (define-theorem positive-predicate (x)
    (implies (positive? x) (equal? (positive? x) #t)))
  (define-function/guard negative? (x)
    (real? x)
    (< x 0))
  (define-theorem negative-predicate (x)
    (implies (negative? x) (equal? (negative? x) #t)))

  (define-function exact-positive-integer? (x)
    (and (exact-integer? x)
         (positive? x)))
  (define-theorem exact-positive-integer-predicate (x)
    (implies (exact-positive-integer? x)
             (equal? (exact-positive-integer? x) #t)))

  (define-function exact-zero? (x) (equal? x 0))
  (define-theorem exact-zero-predicate (x)
    (implies (exact-zero? x) (equal? (exact-zero? x) #t)))

  (define-function natural? (x)
    (if (exact-zero? x)
        #t
        (exact-positive-integer? x)))
  (define-theorem (predicate natural?) (x)
    (implies (natural? x) (equal? (natural? x) #t))))

(define-system prelude/measure/natural (prelude/number)
  (set-measure-predicate natural?)
  (set-measure-predicate <))

(define-system prelude (prelude/measure/natural)
  (define-proof inexact?
    ((rewrite (2) if-nest)
     (rewrite () if-same)))
  (define-proof inexact-predicate
    ((rewrite (1) inexact?)
     (rewrite () if-not)
     (rewrite (3 1) inexact?)
     (rewrite (3 1 1) equal-if-false)
     (eval (3))
     (rewrite () if-same)))
  (define-proof positive?
    ((eval (2 1 1))
     (rewrite (2 1) if-true)
     (rewrite (2) if-nest)
     (rewrite () if-same)))
  (define-proof positive-predicate
    ((rewrite (1) positive?)
     (rewrite (2 1) positive?)
     (rewrite (2 1) less-than-predicate)
     (eval (2))
     (rewrite () if-same)))
  (define-proof negative?
    ((rewrite (2 1) if-nest)
     (eval (2 1))
     (rewrite (2) if-true)
     (rewrite () if-same)))
  (define-proof negative-predicate
    ((rewrite (1) negative?)
     (rewrite (2 1) negative?)
     (rewrite (2 1) less-than-predicate)
     (eval (2))
     (rewrite () if-same))))