;; 2013-04-18.  ind.scm

(load "~/minlog/init.scm")

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Course-of-values induction
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(add-pvar-name "P" (make-arity (py "nat")))

;; CVInd
(set-goal "all n(all m(m<n -> P m) -> P n) -> all n P n")
(assume "Prog")
(assert "all n,m(m<n -> P m)")

(ind)
(assume "m" "Absurd")
(use "Efq")
(use "Absurd")

(assume "n" "IHn" "m" "m<Succ n")
(use "NatLtSuccCases" (pt "n") (pt "m"))
(use "m<Succ n")
(use "IHn")
(assume "m=n")
(simp "m=n")
(use "Prog")
(use "IHn")

(assume "Hyp" "n")
(use "Hyp" (pt "Succ n"))
(use "Truth-Axiom")
;; Proof finished.
(save "CVInd")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Double induction  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(add-pvar-name "R" (make-arity (py "nat") (py "nat")))

;; DInd
(set-goal "R 0 0 -> 
           all n,m(R n m -> R n(Succ m)) ->
           all n(all m R n m -> R(Succ n)0) ->
           all n,m R n m")
(assume "Init" "mStep" "nStep")
(ind)
;; Base
(ind)
(use "Init")
(use "mStep")
;; Step
(assume "n" "IHn")
(ind)
(use "nStep")
(use "IHn")
(use "mStep")
;; Proof finished.
(save "DInd")