;;; 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 the-little-prover)
  #:export (the-little-prover)
  #:use-module (vikalpa))

(define (size x)
  (if (pair? x)
      (+ (size (car x))
         (size (cdr x)))
      0))

(define-system the-little-prover ()
  (define-function atom? (x)
    (not (pair? x)))
  (define-builtin-function size (x))
  (define-builtin-function + (x y))
  (define-builtin-function natural? (x))
  (define-builtin-function < (x y))
  (define-totality-claim natural? natural? <)
  
  ;; Axioms of Equal
  (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)
    (if (equal? x y) (equal? x y) #t))

  ;; Axioms of Cons
  (define-axiom atom/cons (x y)
    (equal? (atom? (cons x y)) #f))
  (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 (atom? x)
        #t
        (equal? (cons (car x) (cdr x)) x)))

  ;; Axioms of If
  (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-nest-A (x y z)
    (if x (equal? (if x y z) y) #t))
  (define-axiom if-nest-E (x y z)
    (if x #t (equal? (if x y z) z)))

  ;; Axioms of Size
  (define-axiom natural?/size (x)
    (equal? (natural? (size x)) #t))
  (define-axiom size/car (x)
    (if (atom? x)
        #t
        (equal? (< (size (car x)) (size x)) #t)))
  (define-axiom size/cdr (x)
    (if (atom? x)
        #t
        (equal? (< (size (cdr x)) (size x)) #t)))

  ;; Axioms of `+` and `<`
  (define-axiom identity-+ (x)
    (if (natural? x)
        (equal? (+ (+ x y) z))
        #t))
  (define-axiom commute-+ (x y)
    (equal? (+ x y) (+ y x)))
  (define-axiom associate-+ (x y z)
    (equal? (+ (+ x y) z) (+ x (+ y z))))
  (define-axiom positive-+ (x y)
    (if (< '0 x)
        (if (< '0 y)
            (equal? (< '0 (+ x y)) #t)
            #t)
        #t))
  (define-axiom natural?/+ (x y)
    (if (natural? x)
        (if (natural? y)
            (equal? (natural? (+ x y)) #t)
            #t)
        #t))
  (define-axiom common-addends-< (x y z)
    (equal? (< (+ x z) (+ y z) (< x y))))

  ;; Axioms for Vikalpa
  (define-axiom natural?/0 ()
    (equal? (natural? '0) #t))
  (define-axiom natural?/succ (x)
    (if (natural? x)
        (equal? (natural? (succ x)) #t)
        #t))

  ;; Prelude
  (define-function list-induction (x)
    (if (atom? x)
        x
        (cons (car x)
              (list-induction (cdr x)))))

  (define-proof list-induction
    (natural? (size x))
    (((2 3) size/cdr)
     ((2) if-same)
     (() if-same)))
  
  (define-function star-induction (x)
    (if (atom? x)
        x
        (cons (star-induction (car x))
              (star-induction (cdr x)))))

  (define-proof star-induction
    (natural? (size x))
    (((2 3 1) size/car)
     ((2 3 2) size/cdr)
     ((2 3) if-true)
     ((2) if-same)
     (() if-same))))