; $Id: realsqrttwo.scm,v 1.4 2008/01/25 13:30:27 logik Exp $

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

; (load "~/minlog/init.scm")
(libload "numbers.scm")

; (display-program-constants "S" "PosPlus" "PosTimes" "PosLess" "PosLeq")

(set-goal (pf "all p,q.SZero(q*q)=p*p -> F"))
(ind)
(auto)
(assume "p" "IHp")
(cases)
(auto)
(save "LemmaOne")

(set-goal (pf "all p,q.2==(p#q)*(p#q) -> F"))
(use "LemmaOne")
(save "LemmaOneRat")

(add-global-assumption "RatRealEq" (pf "all a,b.a===b -> a==b"))
(add-global-assumption "RealEqTrans" (pf "all x,y,z.x===y -> y===z -> x===z"))
(add-global-assumption
 "RealRatTimesComp"
 (pf "all x1,x2,a1,a2.x1===a1 -> x2===a2 -> x1*x2===a1*a2"))

(set-goal (pf "all x,p,q.2===x*x -> x===p#q -> F"))
(strip)
(use "LemmaOneRat" (pt "p") (pt "q"))
(use "RatRealEq")
(use "RealEqTrans" (pt "x*x"))
(prop)
(use "RealRatTimesComp")
(auto)
(save "Corollary")