New files.

1 files changed, 168 insertions, 0 deletions

diff --git a/phox/root2.phx b/phox/root2.phx
new file mode 100644
index 00000000..19259993
--- /dev/null
+++ b/phox/root2.phx
@@ -0,0 +1,168 @@
+(* 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.
+