// // // A proof of the irrationality of the square root of 2 in ATS/LF // // author: Hongwei Xi (Nov 1, 2007) // // // // Aaron Stump mentioned the problem during his visit at BU on Nov 1, 2007. // This solution is self-contained. // // // March 6th, 2008 // The code is ported to ATS/Anairiats by Hongwei Xi. This example involves // an interesting use of manual splitting on an integer variable. See below. // (* ****** ****** *) dataprop MUL1 (int, int, int) = | {n:int} MUL1bas (0, n, 0) | {m,n,p:int | m >= 0} MUL1ind (m+1, n, p+n) of MUL1 (m, n, p) | {m,n,p:int | m > 0} MUL1neg (~m, n, ~p) of MUL1 (m, n, p) // m * 0 = x implies x = 0 prfun lemma00 {m:nat} {x:int} .. (pf: MUL1 (m, 0, x)): [x == 0] void = sif m > 0 then begin let prval MUL1ind pf1 = pf in lemma00 pf1 end end else begin let prval MUL1bas () = pf in () end end // m * n = x implies m * (n-1) = x - m prfun lemma01 {m,n:nat} {x:int} .. (pf: MUL1 (m, n, x)) : MUL1 (m, n-1, x-m) = sif m > 0 then begin let prval MUL1ind pf1 = pf in MUL1ind (lemma01 pf1) end end else begin let prval MUL1bas () = pf in MUL1bas () end end // commutativity of multiplication // m * n = x implies n * m = x prfun lemma_commute {m,n:nat} {x:int} .. (pf: MUL1 (m, n, x)) : MUL1 (n, m, x) = sif n > 0 then begin let prval pf1 = lemma01 (pf) in MUL1ind (lemma_commute {m,n-1} (pf1)) end end else begin let prval () = lemma00 (pf) in MUL1bas () end end // (p + p) * (p + p) = x implies x = 4 * x4 for some x4 prfun lemma1 {p:nat} {x:int} .

. (pf: MUL1 (p+p, p+p, x)): [x4:int | x == 4*x4] MUL1 (p, p, x4) = sif p > 0 then let prval MUL1ind pf1 = pf prval MUL1ind pf2 = pf1 prval pf2' = lemma_commute {p+p-2,p+p} (pf2) prval MUL1ind pf21' = pf2' prval MUL1ind pf22' = pf21' prval [x41:int] pf_1 = lemma1 {p-1} {x-8*p+4} (pf22') // prval () = verify_constraint {x-8*p+4==4*x41} () prval pf_2 = MUL1ind (pf_1) prval pf_3 = lemma_commute (pf_2) prval pf_4 = MUL1ind (pf_3) in #[x41+2*p-1 | pf_4] end else let prval MUL1bas () = pf in #[0 | pf] end // end of [sif] // end of [lemma1] // [x <= 0 || x >= 1] is an example of manual splitting! // p * p = x + x implies p = 2 * p2 for some p2 prfun lemma2 {p:nat} {x:int} .

. (pf: MUL1 (p, p, x+x)): [p2:int | p == 2*p2] void = sif p >= 2 then let prval MUL1ind pf1 = pf prval MUL1ind pf2 = pf1 prval pf2' = lemma_commute {p-2,p} (pf2) prval MUL1ind pf21' = pf2' prval MUL1ind pf22' = pf21' prval [p21:int] () = lemma2 {p-2}{x-2*p+2} (pf22') in #[p21+1 | ()] end else sif p == 1 then let (* prval () = (): [x <= 0 || x >= 1] void // an example of manual splitting! *) prval MUL1ind pf1 = pf prval MUL1bas () = pf1 in #[0 | ()] // impossible end else let prval MUL1bas () = pf in #[0 | ()] end // end of [sif] (* (q/p) * (q/p) = 2 => contradiction if p * p = x and q * q = 2x, then x = 0 *) // (p * p = x and q * q = x + x) implies x = 0 prfun lemma_main {p,q:nat} {x:int} .

. (pf1: MUL1 (p, p, x), pf2: MUL1 (q, q, x+x)): [x == 0] void = sif p > 0 then let prval [q2:int] () = lemma2 {q} {x} (pf2) // q = 2*q2 prval [x2:int] pf2' = lemma1 {q2} {x+x} (pf2) // x+x = 4*x2 prval [p2:int] () = lemma2 {p} {x2} (pf1) // p = 2*p2 prval [x4:int] pf1' = lemma1 {p2} {x2+x2} (pf1) // x2+x2 = 4*x4 in lemma_main {p2,q2} {x4} (pf1', pf2') end else begin let prval MUL1bas () = pf1 in () end end (* ****** ****** *) (* end of [irrationality_of_sqrt2.dats] *)