;;; Vikalpa --- Proof Assistant
;;; Copyright © 2020 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/macros ()
  (define-syntax-rules and ()
    ((and) '#t)
    ((and x) x)
    ((and x . xs) (if x (and . xs) #f)))
  (define-syntax-rules or ()
    ((or) '#f)
    ((or x) x)
    ((or x . xs) (if x x (or . xs))))
  (define-syntax-rules cond (else)
    ((cond (else e)) e)
    ((cond (test then) . rest)
     (if test then (cond . rest))))
  (define-syntax-rules implies ()
    ((implies x y) (if x y #t))
    ((implies x y z . rest)
     (if x (implies y z . rest) #t))))

(define-system prelude/equal (prelude/macros)
  (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/if (prelude/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/integer (prelude/if)
  (define-core-function integer? (x) exact-integer?)
  (define-core-function positive-integer? (x) exact-positive-integer?)
  (define-function zero? (x)
    (equal? x 0))
  (define-function natural? (x)
    (if (zero? x)
        #t
        (positive-integer? x)))
  (define-core-function + (x y)
    (lambda (x y)
      (if (number? x)
          (if (number? y)
              (+ x y)
              x)
          (if (number? y)
              y
              0))))
  (define-axiom succ/pred (x)
    (implies (integer? x)
             (equal? (succ (pred x)) x)))
  
  (define-trivial-total-function < (x y)
    (if (positive-integer? x)
        (if (positive-integer? y)
            (< (pred x) (pred y))
            #f)
        (if (positive-integer? y)
            #t
            (if (negative-integer? x)
                (if (negative-integer? y)
                    (< (succ x) (succ y))
                    #t)
                #f))))
  (set-measure-predicate natural?)
  (set-measure-less-than <)
  (define-axiom integer?/true (x)
    (implies (integer? x)
             (equal? (integer? x) #t)))
  (define-axiom integer/pred (x)
    (implies (integer? x)
             (equal? (integer? (pred x)) #t)))
  (define-axiom integer/succ (x)
    (implies (integer? x)
             (equal? (integer? (pred x)) #t)))
  (define-axiom positive-integer?-is-predicate (x)
    (implies (positive-integer? x)
             (equal? (positive-integer? x) #t)))
  (define-axiom negative-integer?-is-predicate (x)
    (implies (negative-integer? x)
             (equal? (negative-integer? x) #t)))
  (define-axiom natural/pred (x)
    (implies (positive-integer? x)
             (equal? (natural? (pred x)) #t)))
  (define-axiom positive-integer/pred (x)
    (implies (natural? x)
             (equal? (positive-integer? (pred x)) #t)))
  (define-axiom positive-integer-is-integer (x)
    (implies (positive-integer? x)
             (equal? (integer? x) #t)))
  (define-axiom negative-integer-is-integer (x)
    (implies (negative-integer? x)
             (equal? (integer? x) #t)))
  (define-axiom axiom-zero (x)
    (if (integer? x)
        (if (positive-integer? x)
            (equal? (zero? x) #f)
            (if (negative-integer? x)
                (equal? (zero? x) #f)
                (equal? (zero? x) #t)))
        (equal? (zero? x) #f)))
  (define-axiom axiom-positive-integer (x)
    (if (integer? x)
        (if (negative-integer? x)
            (equal? (positive-integer? x) #f)
            (if (zero? x)
                (equal? (positive-integer? x) #f)
                (equal? (positive-integer? x) #t)))
        (equal? (positive-integer? x) #f)))
  (define-axiom axiom-negative-integer (x)
    (if (integer? x)
        (if (positive-integer? x)
            (equal? (negative-integer? x) #f)
            (if (zero? x)
                (equal? (negative-integer? x) #f)
                (equal? (negative-integer? x) #t)))
        (equal? (negative-integer? x) #f)))
  (define-axiom integer/negate (x)
    (implies (integer? x)
             (equal? (integer? (negate x)) #t)))
  (define-axiom positive-integer/negate (x)
    (if (negative-integer? x)
        (equal? (positive-integer? (negate x)) #t)
        (implies (integer? x)
                 (equal? (positive-integer? (negate x)) #f))))
  (define-axiom negative-integer/negate (x)
    (if (positive-integer? x)
        (equal? (negative-integer? (negate x)) #t)
        (implies (integer? x)
                 (equal? (negative-integer? (negate x)) #f))))
  (define-axiom zero/negate (x)
    (implies (zero? x)
             (equal? (zero? (negate x)) #t)))
  (define-function abs (x)
    (if (integer? x)
        (if (negative-integer? x)
            (negate x)
            x)
        0))
  (define-theorem natural-is-integer (x)
    (implies (natural? x) (equal? (integer? x) #t)))
  (define-theorem natural/abs (x)
    (equal? (natural? (abs x)) #t))
  (define-theorem zero-is-0 (x)
    (implies (zero? x)
             (equal? x 0)))
  (define-theorem not-natural-implies-not-positive-integer (x)
    (implies (not (natural? x))
             (equal? (positive-integer? x) #f)))
  (define-theorem natural-and-not-zero-implies-positive-integer (x)
    (implies (natural? x)
             (not (zero? x))
             (equal? (positive-integer? x) #t)))
  (define-theorem %%abs/pred--zero/pred (x)
    (implies (integer? x)
             (not (positive-integer? x))
             (natural? x)
             (equal? (zero? x) #t)))
  (define-theorem %%abs/pred--x-is-1 (x)
    (implies (positive-integer? x)
             (not (positive-integer? (pred x)))
             (equal? x 1)))
  (define-theorem %%abs/pred-1 (x)
    (implies (positive-integer? x)
             (positive-integer? (pred x))
             (equal? (< (pred x) x) #t)))
  (define-theorem abs/pred (x)
    (if (positive-integer? x)
        (equal? (< (abs (pred x)) (abs x)) #t)
        #t))
  (define-theorem abs/succ (x)
    (if (negative-integer? x)
        (equal? (< (abs (succ x)) (abs x)) #t)
        #t))
  (define-function natural-induction (x)
    (if (natural? x)
        (if (zero? x)
            0
            (succ (natural-induction (pred x))))
        0))
  (define-function integer-induction (x)
    (if (positive-integer? x)
        (succ (integer-induction (pred x)))
        (if (negative-integer? x)
            (pred (integer-induction (succ x)))
            0)))
  (define-function + (x y)
    (if (positive-integer? x)
        (succ (+ (pred x) y))
        (if (negative-integer? x)
            (pred (+ (succ x) y))
            y))))

(define-system prelude/pair (prelude/integer)
  (define-core-function pair? (x) pair?)
  (define-core-function cons (x y) cons)
  (define-core-function car (x)
    (lambda (x) (if (pair? x) (car x) '())))
  (define-core-function cdr (x)
    (lambda (x) (if (pair? x) (cdr x) '()))))

(define-system prelude/tree (prelude/pair)
  (define-trivial-total-function size (x)
    (if (pair? x)
        (+ 1
           (+ (size (car x))
              (size (cdr x))))
        0))
  (define-axiom natural/size (x)
    (equal? (natural? (size x)) #t))
  (define-axiom size/car (x)
    (equal? (< (size (car x)) (size x)) #t))
  (define-axiom size/cdr (x)
    (equal? (< (size (cdr x)) (size x)) #t))
  (define-function tree-induction (x)
    (if (not (pair? x))
        x
        (cons (tree-induction (car x))
              (tree-induction (cdr x))))))

(define-system prelude/proofs (prelude/tree)
  (define-proof natural/abs
    (((1) natural?)
     ((1 1 1) abs)
     ((1 1) if-same (set x (integer? x)))
     ((1 1 3 1) if-nest)
     ((1 1 3) integer?)
     ((1 1 2 1) if-nest)
     ((1 1 2) if-same (set x (negative-integer? x)))
     ((1 1 2 2 1) if-nest)
     ((1 1 2 2) integer/negate)
     ((1 1 2 3 1) if-nest)
     ((1) if-same (set x (integer? x)))
     ((1 3 1) if-nest)
     ((1 3) if-true)
     ((1 3 1 1) abs)
     ((1 3 1 1) if-nest)
     ((1 3 1) negative-integer?)
     ((1 3) not)
     ((1 2 1) if-nest)
     ((1 2 1 3) integer?-is-predicate)
     ((1 2 1) if-same)
     ((1 2) if-true)
     ((1 2 1 1) abs)
     ((1 2 1 1) if-nest)
     ((1 2) if-same (set x (negative-integer? x)))
     ((1 2 2 1 1) if-nest)
     ((1 2 3 1 1) if-nest)
     ((1 2 3 1) equal-if-false)
     ((1 2 3) not)
     ((1 2 2) if-same (set x (positive-integer? x)))
     ((1 2 2 2 1) negative-integer/negate)
     ((1 2 2 2) not)
     ((1 2 2 3 1) negative-integer/negate)
     ((1 2 2 3) not)
     ((1 2 2 1) axiom-positive-integer)
     ((1 2 2) if-false)
     ((1 2) if-same)
     ((1) if-same)
     (() equal?)))

  (define-proof abs/pred
    (((2 1 1) abs)
     ((2 1) if-same (set x (positive-integer? (pred x))))
     ((2 1 2 1 2 1) axiom-negative-integer)
     ((2 1 2 1 2) if-false)
     ((2 1 2 1 1) positive-integer-is-integer)
     ((2 1 2 1) if-true)
     ((2 1 2 2) abs)
     ((2 1 2 2 1) positive-integer-is-integer)
     ((2 1 2 2) if-true)
     ((2 1 2 2) if-same (set x (integer? x)))
     ((2 1 2 2 2 1) axiom-negative-integer)
     ((2 1 2 2 2) if-false)
     ((2 1 2 2 3 1) axiom-negative-integer)
     ((2 1 2 2 3) if-false)
     ((2 1 2 2) if-same)
     ((2 1 2) %%abs/pred-1)
     ((2 1 3) if-same (set x (integer? (pred x))))
     ((2 1 3 2 1) if-nest)
     ((2 1 3 3 1) if-nest)
     ((2 1 3 2) if-same (set x (negative-integer? (pred x))))
     ((2 1 3 2 2 1) if-nest)
     ((2 1 3 2 3 1) if-nest)
     ((2 1 3 1 1 1) %%abs/pred--x-is-1)
     ((2 1 3 2 1 1 1) %%abs/pred--x-is-1)
     ((2 1 3 2 2 1 1 1) %%abs/pred--x-is-1)
     ((2 1 3 2 2 2 1) %%abs/pred--x-is-1)
     ((2 1 3 2 3 1 1) %%abs/pred--x-is-1)
     ((2 1 3 2 3 2 1) %%abs/pred--x-is-1)
     ((2 1 3 3 2 1) %%abs/pred--x-is-1)
     ((2 1 3) (eval))
     ((2 1) if-same)
     ((2) equal-same)
     (() if-same)))

  (define-proof %%abs/pred-1
    (natural-induction x)
    (((2 2 1 1) zero-is-0)
     ((2 2 1) positive-integer?)
     ((2 2) if-false)
     ((2 3) if-same (set x (positive-integer? (pred x))))
     ((2 3 2 1) if-nest)
     ((2 3 3 1) if-nest)
     ((2 3 3) if-true)
     ((2 3 2 2 2) if-nest)
     ((2 3 2 2 1) natural-and-not-zero-implies-positive-integer)
     ((2 3 2 2) if-true)
     ((2 3 2) if-same (set x (positive-integer? (pred (pred x)))))
     ((2 3 2 2 1) if-nest)
     ((2 3 2 3 1) if-nest)
     ((2 3 2 3) if-true)
     ((2 3 2 2 2 1) <)
     ((2 3 2 2 2 1) if-nest)
     ((2 3 2 2 2 1 1) natural-and-not-zero-implies-positive-integer)
     ((2 3 2 2 2 1) if-true)
     ((2 3 2 2 2 1) equal-if)
     ((2 3 2 2 2) equal?)
     ((2 3 2 2) if-same)
     ((2 3 2 3 1) <)
     ((2 3 2 3 1) if-nest)
     ((2 3 2 3 1 1) natural-and-not-zero-implies-positive-integer)
     ((2 3 2 3 1) if-true)
     ((2 3 2 3 1 1 1) %%abs/pred--x-is-1)
     ((2 3 2 3 1 2) %%abs/pred--x-is-1)
     ((2 3 2 3) (eval))
     ((2 3 2) if-same)
     ((2 3 3 2) if-nest)
     ((2 3 3) if-same)
     ((2 3) if-same)
     ((2) if-same)
     ((3 1) not-natural-implies-not-positive-integer)
     ((3) if-false)
     (() if-same)))

  (define-proof %%abs/pred--x-is-1
    (((2 2) if-same (set x (zero? (pred x))))
     ((2 2 2) if-same (set x (integer? x)))
     ((2 2 2 2 1) succ/pred)
     ((2 2 2 2 1 1) zero-is-0)
     ((2 2 2 2) (eval))
     ((2 2 2 1) positive-integer-is-integer)
     ((2 2 2) if-true)
     ((2 2) if-same (set x (natural? (pred x))))
     ((2 2 2) if-same (set x (integer? (pred x))))
     ((2 2 2 2 1) %%abs/pred--zero/pred)
     ((2 2 2 2) if-true)
     ((2 2 2 1) natural-is-integer)
     ((2 2 2) if-true)
     ((2 2 1) natural/pred)
     ((2 2) if-true)
     ((2) if-same)
     (() if-same)))

  (define-proof %%abs/pred--zero/pred
    (((2 2 1) natural?)
     ((2 2 1) if-nest)
     ((2 2 2) if-same (set x (zero? x)))
     ((2 2 2 2 1 1) zero-is-0)
     ((2 2 2 2) (eval))
     ((2 2 2 1) axiom-zero)
     ((2 2 2) if-true)
     ((2 2) if-same)
     ((2) if-same)
     (() if-same)))

  (define-proof natural-is-integer
    (((1) natural?)
     (() if-same (set x (integer? x)))
     ((2 2 1) integer?-is-predicate)
     ((2 2) equal-same)
     ((2) if-same)
     ((3 1) if-nest)
     ((3) if-false)
     (() if-same)))

  (define-proof zero-is-0
    (((1) zero?)
     ((2 1) equal-if)
     ((2) equal?)
     (() if-same)))
  
  (define-proof not-natural-implies-not-positive-integer
    (((1 1) natural?)
     (() if-same (set x (integer? x)))
     ((2 1 1) if-nest)
     ((2) if-not)
     ((2) if-not)
     ((2 2) if-same (set x (positive-integer? x)))
     ((2 2 3 1) equal-if-false)
     ((2 2 3) equal?)
     ((2 2 1) axiom-positive-integer)
     ((2 2) if-false)
     ((2) if-same)
     ((3 1 1) if-nest)
     ((3 1) not)
     ((3) if-true)
     ((3 1) axiom-positive-integer)
     ((3) equal?)
     (() if-same)))

  (define-proof natural-and-not-zero-implies-positive-integer
    (((1) natural?)
     (() if-same (set x (integer? x)))
     ((2 1) if-nest)
     ((2 2 2 1) axiom-positive-integer)
     ((2 2 2) equal?)
     ((2 2) if-same)
     ((2) if-same)
     ((3 1) if-nest)
     ((3) if-false)
     (() if-same)))
  
  (define-proof natural-induction
    (abs x)
    (((1) natural/abs)
     (() if-true)
     ((2 3) if-same (set x (positive-integer? x)))
     ((2 3 2) abs/pred)
     ((2 3 1) natural-and-not-zero-implies-positive-integer)
     ((2 3) if-true)
     ((2) if-same)
     (() if-same)))

  (define-proof integer-induction
    (abs x)
    (((1) natural/abs)
     (() if-true)
     ((2) abs/pred)
     ((3 2) abs/succ)
     ((3) if-same)
     (() if-same)))
  
  (define-proof +
    (abs x)
    (((1) natural/abs)
     (() if-true)
     ((2) abs/pred)
     ((3 2) abs/succ)
     ((3) if-same)
     (() if-same)))
  
  (define-proof tree-induction
    (size x)
    (((2 3 1) size/car)
     ((2 3 2) size/cdr)
     ((2 3) if-true)
     ((2) if-same)
     ((1) natural/size)
     (() if-true))))


(define-system prelude (prelude/proofs))