;;; 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-system prelude ()
  (define-core-function natural? (x) (lambda (x)
                                       (and (integer? x)
                                            (< 0 x))))
  (define-core-function < (x y) (natural? x) (natural? y) <)
  (define-core-function pair? (x) pair?)
  (define-core-function cons (x y) cons)
  (define-core-function car (x) (pair? x)
    (lambda (x) (if (pair? x) (car x) '())))
  (define-core-function cdr (x) (pair? x)
    (lambda (x) (if (pair? x) (cdr x) '())))
  (define-core-function + (x y)
    (lambda (x y)
      (if (number? x)
          (if (number? y)
              (+ x y)
              x)
          (if (number? y)
              y
              0))))
  (set-measure-predicate natural?)
  (set-measure-less-than <)
  (define-trivial-total-function list-induction (x)
    (if (not (pair? x))
        x
        (cons (car x)
              (list-induction (cdr x)))))
  (define-trivial-total-function size (x)
    (if (not (pair? x))
        0
        (+ 1
           (+ (size (car x))
              (size (cdr x))))))

  (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-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-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 pair/cons (x y)
    (equal? (pair? (cons x y)) '#t))

  (define-axiom cons/car+cdr (x)
    (implies (pair? x)
             (equal? (cons (car x) (cdr x)) x)))

  (define-axiom car/cons (x y)
    (equal? (car (cons x y)) x))

  (define-axiom cdr/cons (x y)
    (equal? (cdr (cons x y)) y))

  (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-axiom equal-car (x1 y1 x2 y2)
    (implies (equal? (cons x1 y1) (cons x2 y2))
             (equal? x1 x2)))

  (define-theorem caar-cons2 (x y z)
    (equal? (car (car (cons (cons x y) z))) x))
  
  (define-function app (x y)
    (if (not (pair? x))
        y
        (cons (car x)
              (app (cdr x) y))))
  
  (define-theorem assoc-app (x y z)
    (equal? (app x (app y z))
            (app (app x y) z)))

  (define-proof caar-cons2
    (((1 1)  car/cons)
     ((1) car/cons)
     (() equal-same)))

  (define-proof app
    (size x)
    (((2 3) size/cdr)
     ((2) if-same)
     ((1) natural/size)
     (() if-true)))

  (define-proof assoc-app
    (list-induction x)
    ()))