diff options
Diffstat (limited to 'phox/root2.phx')
-rw-r--r-- | phox/root2.phx | 168 |
1 files changed, 0 insertions, 168 deletions
diff --git a/phox/root2.phx b/phox/root2.phx deleted file mode 100644 index 19259993..00000000 --- a/phox/root2.phx +++ /dev/null @@ -1,168 +0,0 @@ -(* Example proof by Paul Roziere. See http://www.cs.kun.nl/~freek/comparison/ *) - -Import nat. - -flag auto_lvl 1. - -theorem minimal.element /\X (\/n:N X n -> \/n:N (X n & /\p:N (X p -> n <= p))). -intro 2. -by_absurd. -rewrite_hyp H0 demorganl. -use /\n:N ~ X n. -trivial. -intros. -elim well_founded.N with H1. -intros. -intro. -apply H0 with H4. -lefts G $& $\/. -elim H3 with H5. -elim not.lesseq.imply.less.N. -save. - -theorem not_odd_and_even.N /\x,y,z:N (~ (x = N2 * y & x = N1 + N2 * z)). -intro 2. -elim H. -trivial. -intros. -intro. -left H4. -elim H2 with [case]. -trivial =H0 H4 H6. -elim H1. -axiom H3. -axiom H6. -intro. -rmh H4. -left H5. -intros. -rmh H5. -left H4. -axiom H4. -intros. -save. - -theorem sum_square.N /\x,y:N (x + y)^N2 = x^N2 + N2*x*y + y^N2. -intros. -intro. -save. - -fact less.exp.N /\n,x,y:N( x <= y -> x^n <= y^n). -intros. -elim H. -trivial. -rewrite calcul.N. -trivial. -save. - -fact less_r.exp.N /\n,x,y:N( x^n < y^n -> x < y). -intros. -elim lesseq.case1.N with y and x. -apply less.exp.N with n and H3. -elim lesseq.imply.not.greater.N with y^n and x^n ;; Try intros. -save. - -fact less.ladd.N /\x,y:N (N0 < y -> x < x + y). -intros. -elim H. -rewrite calcul.N. -trivial. -save. - -theorem n.square.pair /\n:N (\/p:N n^N2=N2*p -> \/q:N n=N2*q). -intros. -lefts H0 $\/ $&. -apply odd_or_even.N with H. -lefts G $\/ $& $or. -trivial. -prove n^N2 = N1 + N2*(N2*y^N2+N2*y). -rewrite H3 sum_square.N. -from N1 + N2 * N2 * y + (N2 * y) ^ N2 = N1 + N4 * y + N2 * N2 * y ^ N2. -intro. -elim not_odd_and_even.N with N (n^N2). -intros. -select 3. -intro. -axiom H1. -axiom G. -axiom H0. -intros. -save. - -lem decrease /\m,n : N (m^ N2 = N2 * n^ N2 -> N0 < n -> n < m). -intros. -elim less_r.exp.N with N2 ;; Try intros. -prove m^N2 = n^N2 + n^N2. axiom H1. -elim less.ladd.N ;; Try intros. -trivial =H0 H2. -save. - -lem sup_zero /\m,n : N (m^ N2 = N2 * n^ N2 -> N0 < m -> N0 < n). -intros. -elim neq.less_or_sup.N with N0 and n ;; Try intros. -rewrite_hyp H1 H3 calcul.N. -trivial. -trivial. -save. - -def Q m = m > N0 & \/n:N (m^ N2 = N2 * n^ N2). - -lem dec /\m:N (Q m -> \/m':N (Q m' & m' < m)). -intros. -lefts H0 $Q $\/ $&. -apply sup_zero with H2 and H0. -intro. -instance ?1 n. -intros. -intros. -trivial. -prove \/p:N (m ^ N2 = N2 * p). -intro. -instance ?2 n^N2. -trivial. -apply n.square.pair with G0. -lefts G1 $& $\/. -prove n ^N2 = N2 * q ^N2. -rewrite_hyp H2 H4. -prove N2 * N2 * q ^N2 = N2 * n ^ N2. -from H2. -left G1. -trivial =. -intro. -intros. -intros. -intros. -trivial =H3 G1. -elim decrease. -save. - -lem sq2_irrat /\m:N ~Q m. -intros. -intro. -elim minimal.element with Q. -intros $\/ $&. -axiom H. -axiom H0. -lefts H1. -elim dec with H2. -lefts H4. -apply H3 with H5. -elim lesseq.imply.not.greater.N with n and m'. -save. - -theorem square2_irrat /\m,n : N (m^ N2 = N2 * n^ N2 -> m = N0 & n = N0). -intros. -apply sq2_irrat with H. -elim H with [case]. -intro. -intro. -elim H0 with [case]. -intro. -rewrite_hyp H1 H2 H4 calcul.N. -left H1;; intros. -prove Q m. -intros $Q $\/ $& ;; Try axiom H1. -trivial. -elim G. -save. - |