;; 2014-04-28.  numbersintro.scm.  Preparation for work in
;; constructive analysis.  Assumes knowledge of the tutorial.

;; Seminar: Konstruktive Analysis

;; Es sollen die Grundlagen der konstruktiven Analysis sowie der
;; Extraktion von Programmen aus Beweisen erarbeitet werden.
;; Vorausgesetzt werden Kenntnisse in Mathematischer Logik (eine
;; einfuehrende Vorlesung) Ferner wird vorausgesetzt, dass die
;; Teilnehmer das Tutorium des Beweisassistenten Minlog
;; durchgearbeitet haben.  Der parallele Besuch der Vorlesung Logik II
;; wird empfohlen.

;; Vortraege:

;; 1.  Einfuehrung (auch: Minlog, numbers)
;;     Helmut Schwichtenberg, 14. April

;; [.  Irrationalitaet der Wurzel von 2.  Skript 1.1.
;;     examplesarithquotrem.scm mit neterm.  examplesarithsqrttwo.scm
;;     (-> Bachelorthema: Formalisierung des Newton-Verfahrens fuer sqrt a)]

;; 2.  Rationale und reelle Zahlen.  numbers.  RealEqChar in 
;;     examples/analysis/real.scm.  Bis RealBound in real.scm.
;;     PosNotLeToLt via Einbettung PosToNat.
;;     H.S. 28. April

;; 3.  Nicht-negative und positive reelle Zahlen.  Skript 1.4.  RealPosChar
;;     in real.scm
;;     5. Mai, Tillman Ritschl
;;     tillman.ritschl@hotmail.de

;; 4.  Arithmetische Funktionen.  Skript 1.5.
;;     Definitionen, Moduln, Eigenschaften.
;;     12. Mai, Andreas Franz
;;     franz_andreas@gmx.de

;; 5.  Vergleich reeller Zahlen.  Skript 1.6.
;;     RealApprox (in real.scm). ApproxSplit (in cont.scm)
;;     19. Mai, Franziskus Wiesnet
;;     Franziskus.Wiesnet@gmx.de

;; 6.  Vollstaendigkeit.  Skript 2.1.
;;     RatCauchyConvMod.  (kaum etwas implementiert; Liste am Ende von cont.scm)
;;     26. Mai, Stephan Kulla
;;     stephan.kulla@campus.lmu.de

;; 7.  Suprema und Infima.  Skript 4.1.
;;     examplesanalysislub.scm.  Bachelorarbeit Lucas Hoffmann.
;;     2. Juni.  Felix Monninger
;;     felix.monninger@gmail.com

;; [   Stetige Funktionen.  Skript 4.2.
;;     cont.scm.  ApproxSplitBoole.
;;     23. Juni]

;; [   Zwischenwertsatz.  Skript 4.7.
;;     cont.scm
;;     30. Juni]


;; Data types nat pos int rat rea

;; Proofs with induction

;; NatToPos and PosToNat.  Example: PosLtLeCases.  Another example:
;; PosNotLeToLt and PosNotLtToLe should be best proved using the
;; isomorphic embedding PosToNat of pos into nat.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 1.  Logic
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

(add-pvar-name "A" "B" "C" (make-arity))

;; ExOne
(set-goal "(A -> B -> C) -> (A -> B) -> A -> C")
(assume "u" "v" "w")
(use-with "u" "?" "?")
(use "w")
(use-with "v" "w")
;; Proof finished
(save "ExOne")

(define proof (rename-avars "ExOne"))
(cdp proof)
(proof-to-expr-with-formulas proof)

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

;; n, m, k are variables of type nat.

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

;; ExTwo
(set-goal "all n(P n -> Q n) -> all n P n -> all n Q n")
(assume "u" "v" "n")
(use "u")
(use "v")
;; Proof finished
(save "ExTwo")

(define proof (rename-avars "ExTwo"))
(cdp proof)
(proof-to-expr-with-formulas proof)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Quotient and remainder
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; See quotrem.scm

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The square root of 2 is irrational
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; See sqrttwo.scm

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Numbers
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

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

(display-alg "nat" "pos" "int" "rat" "rea")

(default-var-name (py "nat"))
(default-var-name (py "pos"))
(default-var-name (py "int"))
(default-var-name (py "rat"))
(default-var-name (py "rea"))

(display-pconst "NatPlus" "PosPlus")

;; Many case distinctions are necessary to prove properties of pos.
;; Cure: use isomorphic embedding PosToNat of pos into nat.

(display-pconst "PosToNat" "NatToPos")
(display-pconst "NatToPosStep")

(pp "PosToNatToPosId")
(pp "NatToPosToNatId")

;; One can prove that PosToNat is an isomorphism w.r.t. +

(pp "PosToNatPlus")
(pp "NatToPosPlus")

;; Using this isomorphism one can transfer properties of nat to pos.

(pp "PosPlusComm")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Reals, equality of reals
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

See realeqbound.scm