; $Id: sqrttwo.scm,v 1.2 2005/03/07 08:26:00 schwicht Exp $

; For Freek Wiedijk's "stamp collection" of irrationality of sqrt(2)
; proof formalizations.

(load "~/minlog/init.scm")
(mload "../lib/nat.scm")

; (display-program-constants "NatPlus" "NatTimes" "NatLess" "NatLeq")
; NatPlus
;   comprules
; 	n+0	n
; 	n+Succ m	Succ(n+m)
;   rewrules
; 	0+n	n
; 	Succ n+m	Succ(n+m)
; 	n1+(n2+n3)	n1+n2+n3
; NatTimes
;   comprules
; 	n*0	0
; 	n*Succ m	n*m+n
;   rewrules
; 	0*n	0
; 	Succ n*m	n*m+m
; 	n1*(n2*n3)	n1*n2*n3
; NatLess
;   comprules
; 	n<0	False
; 	0<Succ n	True
; 	Succ n<Succ m	n<m
;   rewrules
; 	n<Succ n	True ;add n<n   False
; NatLeq
;   comprules
; 	0<=n	True
; 	Succ n<=Succ m	n<=m ;add: Succ n<=0  False as computation rule
;   rewrules
; 	n<=n	True
; 	n<=n+k	True
; 	Succ m<=m	False
; 	Succ m<=0	False ;add: n<=Succ n  True

"LeqSucc" ;add as rewrite rule to NatLeq
(set-goal (pf "all n n<=Succ n"))
(ind)
(auto)
(save "LeqSucc")

"TransLeq"
(set-goal (pf "all n,m,k.n<=m -> m<=k -> n<=k"))
(ind)
(auto)
(assume "n" "IHn")
(cases)
(assume "k")
(prop)
(assume "m")
(cases)
(prop)
(assume "k")
(use "IHn")
(save "TransLeq")

"TransLeqLess"
(set-goal (pf "all n,m,k.n<=m -> m<k -> n<k"))
(ind)
(cases)
(auto)
(assume "m")
(cases)
(prop)
(assume "k")
(ng)
(prop)
(assume "n" "IHn")
(cases)
(assume "k")
(prop)
(assume "m")
(cases)
(prop)
(assume "k")
(use "IHn")
(save "TransLeqLess")

 "TransLessLeq"
(set-goal (pf "all n,m,k.n<m -> m<=k -> n<k"))
(ind)
(cases)
(assume "k")
(prop)
(assume "m")
(cases)
(prop)
(assume "k")
(ng)
(prop)
(assume "n" "IHn")
(cases)
(assume "k")
(prop)
(assume "m")
(cases)
(prop)
(assume "k")
(use "IHn")
(save "TransLessLeq")

"LtSuccCases"
(set-goal (pf "all m,n.n<Succ m -> (n<m -> Pvar^) -> (n=m -> Pvar^) -> Pvar^"))
(ind)
(cases)
(assume "H1" "H2" "H3")
(use "H3")
(use "Truth-Axiom")
(assume "n" "H1" "H2" "H3")
(use "Efq")
(use "H1")
(assume "m" "IHm")
(cases)
(assume "H1" "H2" "H3")
(use "H2")
(use "Truth-Axiom")
(use "IHm")
(save "LtSuccCases")


; "Even" and "Odd"
(add-program-constant "Even" (py "nat=>boole") 1)
(add-program-constant "Odd" (py "nat=>boole") 1)

(add-computation-rule (pt "Even 0") (pt "True"))
(add-computation-rule (pt "Odd 0") (pt "False"))
(add-computation-rule (pt "Even(Succ n)") (pt "Odd n"))
(add-computation-rule (pt "Odd(Succ n)") (pt "Even n"))

"EvenOddPlusRev"
(set-goal (pf "all n,m.(Even(n+m+m) -> Even n)&(Odd(n+m+m) -> Odd n)"))
(assume "n")
(ind)
(auto)
(save "EvenOddPlusRev")

"EvenOddSquareRev"
(set-goal (pf "all n.(Even(n*n) -> Even n)&(Odd(n*n) -> Odd n)"))
(ind)
(prop)
(assume "n" "IHn")
(split)

(ng)
(assume "Odd(n*n+n+n)")
(use "IHn")
(use "EvenOddPlusRev" (pt "n"))
(use "Odd(n*n+n+n)")

(ng)
(assume "Even(n*n+n+n)")
(use "IHn")
(use "EvenOddPlusRev" (pt "n"))
(use "Even(n*n+n+n)")
(save "EvenOddSquareRev")

"Double"
(add-program-constant "D" (py "nat=>nat") 1)

(add-computation-rule (pt "D 0") (pt "0"))
(add-computation-rule (pt "D(Succ n)") (pt "Succ(Succ(D n))"))

"Half"
(add-program-constant "H" (py "nat=>nat") 1)

(add-computation-rule (pt "H 0") (pt "0"))
(add-computation-rule (pt "H 1") (pt "0"))
(add-computation-rule (pt "H(Succ(Succ n))") (pt "Succ(H n)"))

"EvenDouble"
(set-goal (pf "all n Even(D n)"))
(ind)
(auto)
(save "EvenDouble")

"EvenOddDoubleHalf"
(set-goal (pf "all n.(Even n -> D(H n)=n)&(Odd n -> D(H(Succ n))=Succ n)"))
(ind)
(auto)
(save "EvenOddDoubleHalf")

"Double"
(set-goal (pf "all n D n=n+n"))
(ind)
(auto)
(save "Double")

"DoublePlus"
(set-goal (pf "all n,m D(n+m)=D n+D m"))
(assume "n")
(ind)
(auto)
(save "DoublePlus")

"TimesDouble1"
(set-goal (pf "all n,m D(n*m)=D n*m"))
(assume "n")
(ind)
(use "Truth-Axiom")
(assume "m" "IHm")
(ng)
(simp "DoublePlus")
(simp "IHm")
(use "Truth-Axiom")
(save "TimesDouble1")

"TimesDouble2"
(set-goal (pf "all n,m D(n*m)=n*D m"))
(assume "n")
(ind)
(use "Truth-Axiom")
(assume "m" "IHm")
(ng)
(simp "DoublePlus")
(simp "IHm")
(simp (pf "n*D m+n+n=n*D m+(n+n)"))
(simp "<-" "Double")
(auto)
(save "TimesDouble2")

"DoubleInj"
(set-goal (pf "all n,m.D n=D m -> n=m"))
(ind)
(cases)
(prop)
(assume "m")
(prop)
(assume "n" "IHn")
(cases)
(prop)
(assume "m")
(use "IHn")
(save "DoubleInj")

"LeqDouble"
(set-goal (pf "all n n<=D n"))
(ind)
(prop)
(assume "n" "IHn")
(ng)
(use "TransLeq" (pt "D n"))
(use "IHn")
(use "LeqSucc")
(save "LeqDouble")

"LtDouble"
(set-goal (pf "all n.0<n -> n<D n"))
(ind)
(prop)
(assume "n" "IHn")
(assume "Trivial")
(ng)
(use "TransLeqLess" (pt "D n"))
(use "LeqDouble")
(use "Truth-Axiom")
(save "LtDouble")

"DoublePos"
(set-goal (pf "all n.0<D n -> 0<n"))
(cases)
(auto)
(save "DoublePos")

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

"CvInd"
(set-goal (pf "(all n.(all m.m<n -> Q m) -> Q n) -> all n Q n"))
(assume "Prog")
(cut (pf "all n,m.m<n -> Q m"))
(assume "QHyp")
(assume "n")
(use "QHyp" (pt "Succ n"))
(use "Truth-Axiom")

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

(assume "n" "IHn")
(assume "m" "m<Succ n")
(use "LtSuccCases" (pt "n") (pt "m"))
(use "m<Succ n")
(use "IHn")
(assume "m=n")
(simp "m=n")
(use "Prog")
(use "IHn")
(save "CVInd")

"LemmaOneAux"
(set-goal (pf "all n,m.n*n=D(m*m) -> m*m=D(H n*H n)"))
(assume "n" "m" "n*n=D(m*m)")
(simp "TimesDouble1")
(use "DoubleInj")
(simp "<-" "n*n=D(m*m)")
(simp "TimesDouble2")
(simp (pf "D(H n)=n"))
(use "Truth-Axiom")
(use "EvenOddDoubleHalf")
(use "EvenOddSquareRev")
(simp "n*n=D(m*m)")
(use "EvenDouble")
(save "LemmaOneAux")

"NotPosImpZero"
(set-goal (pf "all n.(0<n -> F) -> n=0"))
(ind)
(auto)
(save "NotPosImpZero")

"ZeroSquare"
(set-goal (pf "all n.n*n=0 -> n=0"))
(ind)
(auto)
(save "ZeroSquare")

"SquarePos"
(set-goal (pf "all n.0<n -> 0<n*n"))
(cases)
(auto)
(save "SquarePos")

"LeqLess"
(set-goal (pf "all n,m.(n<=m -> F) -> m<n"))
(ind)
(cases)
(prop)
(assume "m")
(prop)
(assume "n" "IHn")
(cases)
(prop)
(use "IHn")
(save "LeqLess")

"LessLeq"
(set-goal (pf "all n,m.(n<m -> F) -> m<=n"))
(ind)
(cases)
(prop)
(assume "m")
(prop)
(assume "n" "IHn")
(cases)
(prop)
(use "IHn")
(save "LessLeq")

"LeqMonTimes1"
(set-goal (pf "all n,m,k.n<=m -> n*k<=m*k"))

"LessIrrefl" ;add as rewrite rule to NatLess
(set-goal (pf "all n.n<n -> F"))
(ind)
(auto)
(save "LessIrrefl")

"LeqMonPlus"
(set-goal (pf "all n1,n2,m1,m2.n1<=n2 -> m1<=m2 -> n1+m1<=n2+m2"))
(assume "n1" "n2")
(ind)
(ind)
(prop)
(assume "m2" "IHm2")
(assume "n1<=n2" "Trivial")
(use "TransLeq" (pt "n2+m2"))
(use "IHm2")
(use "n1<=n2")
(use "Truth-Axiom")
(use "LeqSucc")
(assume "m1" "IHm1")
(cases)
(prop)
(use "IHm1")
(save "LeqMonPlus")

"LeqSquare"
(set-goal (pf "all n,m.n<=m -> n*n<=m*m"))
(ind)
(assume "m")
(prop)
(assume "n" "IHn")
(cases)
(prop)
(assume "m")
(ng)
(assume "n<=m")
(use "LeqMonPlus")
(use "LeqMonPlus")
(auto)
(save "LeqSquare")

"LtSquareRev"
(set-goal (pf "all m,n.m*m<n*n -> m<n"))
(assume "m" "n" "m*m<n*n")
(use "LeqLess")
(assume "n<=m")
(cut (pf "m*m<m*m"))
(use "LessIrrefl")
(use "TransLessLeq" (pt "n*n"))
(use "m*m<n*n")
(use "LeqSquare")
(use "n<=m")
(save "LtSquareRev")

"LemmaOne"
(set-goal (pf "all n,m.n*n=D(m*m) -> n=0"))
(use-with "CVInd"
	  (make-cterm (pv "m") (pf "all n.m*m=D(n*n) -> m=0")) "?")
(assume "n" "IHn" "m"  "n*n=D(m*m)")
(cases (pt "0<n"))
(assume "0<n")
(use "ZeroSquare")
(simp "n*n=D(m*m)")
(cut (pf "m=0"))
(assume "m=0")
(simp "m=0")
(use "Truth-Axiom")
(use "IHn" (pt "H n"))
(use "LtSquareRev")
(simp "n*n=D(m*m)")
(use "LtDouble")
(use "DoublePos")
(simp "<-" "n*n=D(m*m)")
(use "SquarePos")
(use "0<n")

(use "LemmaOneAux")
(use "n*n=D(m*m)")
(use "NotPosImpZero")
(save "LemmaOne")

(dpe)