;;; 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 (implies prelude)
  #:use-module (vikalpa))

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

(define-system prelude ()
  (define-primitive-function pair? (x y))
  (define-primitive-function < (x y))
  (define-primitive-function natural? (x))
  (define-totality-claim natural? natural? <)

  (define-syntax-rules list ()
    ((list) '())
    ((list x . y) (cons x (list . y))))

  (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 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 car/cons (x y)
    (equal? (car (cons x y)) x))
  (define-axiom cdr/cons (x y)
    (equal? (cdr (cons x y)) y))
  (define-axiom cons/car+cdr (x)
    (if (pair? x)
        (equal? (cons (car x) (cdr x)) x)
        '#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 axiom-less-than (x y)
    (implies (natural? x)
             (natural? y)
             (equal? (< x y)
                     (if (equal? '0 x)
                         (if (equal? '0 y)
                             #f
                             #t)
                         (if (equal? '0 y)
                             #f
                             (< (sub1 x) (sub1 y)))))))
  (define-function natural-induction (n)
    (if (natural? n)
        (if (equal? '0 n)
            '0
            (add1 (natural-induction (sub1 n))))
        'undefined))

  (define-proof natural-induction
    (natural? n)
    ())

  (define-axiom false-if (x)
    (if x #t (equal? #f x)))
  
  (define-axiom sub1/add1 (x)
    (implies (natural? x)
             (equal? (sub1 (add1 x)) x)))

  (define-axiom natural/zero ()
    (equal? (natural? '0) '#t))

  (define-axiom not/true ()
    (equal? (not #t) #f))

  (define-axiom not/false ()
    (equal? (not #f) #t))

  (define-theorem equal/zero-less-than (x)
    (implies (natural? x)
             (equal? (not (< '0 x))
                     (equal? x '0))))

  (define-proof equal/zero-less-than
    (natural-induction x)
    (((2 2) if-nest)
     ((3) if-nest)
     ((2 2 1) if-same (set x (natural? '0)))
     ((2 2 1 2 1) axiom-less-than)
     ((2 2 1 1) natural/zero)
     ((2 2 1) if-true)
     ((2 2 1 1 1) equal-same)
     ((2 2 1 1) if-true)
     ((2 2 1 1 1 2) equal-if)
     ((2 2 1 1 1) equal-same)
     ((2 2 1 1) if-true)
     ((2 2 1) not/false)
     ((2 2 2 1) equal-if)
     ((2 2 2) equal-same)
     ((2 2) equal-same)
     ((2 3 2 2) if-same (set x (natural? '0)))
     ((2 3 2 2 2 1 1) axiom-less-than)
     ((2 3 2 2 2 1 1 1) equal-same)
     ((2 3 2 2 2 1 1) if-true)
     ((2 3 2 2 2 1 1) if-nest)
     ((2 3 2 2 2 1) not/true)
     ((2 3 2 2 2 2) equal-swap)
     ((2 3 2 2 2 2) false-if)
     ((2 3 2 2 2) equal-same)
     ((2 3 2 2 1) natural/zero)
     ((2 3 2 2) if-true)
     ((2 3 2) if-same)
     ((2 3) if-same)
     ((2) if-same)
     (() if-same)))
  
  (define-axiom natural/sub1 (x)
    (implies (natural? x)
             (if (equal? '0 x)
                 '#t
                 (equal? (natural? (sub1 x)) #t))))
  
;; (define-proof natural-induction
;;     (total/natural? n)
;;     (((2) if-nest)
;;      ((2 3) </sub1)
;;      ((2) if-same)
;;      (() if-same)))

(define-theorem natural/add1 (x)
    (implies (natural? x)
             (equal? (natural? (add1 x)) #t)))

  #;
  (define-axiom natural/sub1 (x)
    (if (natural? x)
        (if (< '0 x)
            (equal? (natural? (sub1 x)) '#t)
            '#t)
        '#t))

  #;
  (define-theorem less-than/sub1 (x)
    (implies (natural? x)
             (< '0 x)
             (equal? (< (sub1 x) x) '#t)))

  #;
  (define-axiom add1/sub1 (x)
    (if (natural? x)
        (if (equal? '0 x)
            '#t
            (equal? (add1 (sub1 x)) x))
        '#t))

  #;
  (define-primitive-function + (x y)
    (if (natural? x)
        (if (equal? '0 x)
            y
            (add1 (+ (sub1 x) y)))
        'undefined))
  
  #;
  (define-axiom natural/size (x)
    (equal? (natural? (size x))
            '#t))

  #;
  (define-axiom size/car (x)
    (if (pair? x)
        (equal? (< (size (car x)) (size x))
                '#t)
        '#t))

  #;
  (define-axiom size/cdr (x)
    (if (pair? x)
        (equal? (< (size (cdr x)) (size x))
                '#t)
        '#t))
  
  #;
  (define-proof +
    (total/natural? x)
    (((2) if-nest)
     ((2 3) </sub1)
     ((2) if-same)
     (() if-same)))

  #;
  (define-theorem thm-1+1=2 ()
    (equal? (+ 1 1) 2))

  #;
  (define-function natural-induction (n)
    (if (natural? n)
        (if (equal? '0 n)
            '0
            (add1 (natural-induction (sub1 n))))
        'undefined))

  #;
  (define-proof natural-induction
    (total/natural? n)
    (((2) if-nest)
     ((2 3) </sub1)
     ((2) if-same)
     (() if-same)))

  #;
  (define-theorem equal?/add1 (n)
    (if (natural? n)
        (equal? (equal? n (add1 n)) #f)
        #t))

  #;
  (define-proof equal?/add1
    (induction (natural-induction n))
    (((2 2 2 1 1) equal-if)
     ((2 2 2 1 2 1) equal-if)
     ((2 2 2 1) equal?/01)
     ((2 2 2) equal-same)
     ((2 2) if-same)
     ((2 3 1 1) natural?/sub1)
     ((2 3 1) if-true)
     ((2 3 2 2 1 1) add1/sub1)
     ((2 3 2 2 1 2 1) add1/sub1)
     ((2 3 2 2) if-same (set x (natural? (add1 (sub1 n)))))
     ((2 3 2 2) if-same (set x (natural? (sub1 n))))
     ((2 3 2 2 2 2 1) common-add1
      ;; ルール探索のアルゴリズムにバグがある
      (set x (sub1 n))
      (set y (add1 (sub1 n))))
     ((2 3 2 2 2 2 1) equal-if)
     ((2 3 2 2 2 2) equal-same)
     ((2 3 2 2 2 1) natural?/add1)
     ((2 3 2 2 2) if-true)
     ((2 3 2 2 1) natural?/sub1)
     ((2 3 2 2) if-true)
     ((2 3 2) if-same)
     ((2 3) if-same)
     ((2) if-same)
     ((3) if-nest)
     (() if-same)))

  #;
  (define-proof thm-1+1=2
    ()
    ((() if-same (set x (natural? '0)))
     ((2 1) +)
     ((2 1 2 2 1) equal-if)
     ((2 1 2 3 1 1) sub1/add1)
     ((2 1 2 3 1) +)
     ((2 1 2 3 1 2 1) equal-same)
     ((2 1 2 3 1 2) if-true)
     ((2 1 2 3 1 1) natural?/0)
     ((2 1 2 3 1) if-true)
     ((2 1 2) if-same)
     ((2 1 1) natural?/add1)
     ((2 1) if-true)
     ((2) equal-same)
     ((1) natural?/0)
     (() if-true))))