replaced root2.phx by new square-root-2.phx

2 files changed, 368 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.
-
diff --git a/phox/square-root-2.phx b/phox/square-root-2.phx
new file mode 100644
index 00000000..92a888b3
--- /dev/null
+++ b/phox/square-root-2.phx
@@ -0,0 +1,368 @@
+tex
+  title = "Proof that square root of 2 is not rational"
+  author = "Christophe Raffalli, Paul Rozière"
+  institute = "LAMA, Universit\\'e de Savoie, PPS, Universit\\'e Paris VII"
+  documents = math
+.
+
+Import nat.
+
+flag auto_lvl 1.
+
+(* Cette preuve est à peu près celle envoyée à F. Wiedijk -- Nijmegen
+-- The Fifteen Provers of the World --
+            http://www.cs.kun.nl/~freek/comparison/index.html 
+Voir une preuve plus simple : sqrt2.phx 
+*)
+
+(*! math
+\section{The library:}
+
+The theorem used \underline{explicitely} from the library are
+
+\begin{itemize}
+\item \verb#demorganl# a set of rewrite rules for Demorgan's law.
+\item \verb#calcul.N# a set of rewrite rules for natural numbers.
+\item \verb#well_founded.N#: \[ $$well_founded.N \].
+\item \verb#odd_or_even.N#: \[ $$odd_or_even.N \].
+\item \verb#lesseq.case1.N#: \[ $$lesseq.case1.N \].
+\item \verb#neq.less_or_sup.N#: \[ $$neq.less_or_sup.N \].
+\item \verb#not.lesseq.imply.less.N#: \[ $$not.lesseq.imply.less.N \].
+\item \verb#lesseq.imply.not.greater.N#: \[ $$lesseq.imply.not.greater.N \].
+\end{itemize}
+
+Comments: The first four are natural to use explicitely.  The last two
+could probably be removed by adding some \verb#new_intro# or
+\verb#new_elim# in the library.  \verb#lesseq.case1.N# and
+\verb#neq.less_or_sup.N# are more problematic, they would require to
+extend the system with some kind of binary elimination rule (with two
+principal premices ?).
+
+\section{Some basic lemmas.}
+
+They should be included in the library ? 
+*)
+
+theorem minimal.element /\X (\/n:N X n -> \/n:N (X n & /\p:N (X p -> n <= p))).
+(*! math
+\begin{lemma}\label{minimal.element}
+Every non empty subset \[ X \] of \[ N \] admits a minimal element:
+$$ \[ $0 \] $$
+\end{lemma}
+*)
+intro 2.
+by_absurd.
+rewrite_hyp H0 demorganl.
+(*! math
+\begin{proof}
+We assume \[ $$H \] and \[ $$H0 \] ( \[ H0 \] ).
+*)
+use /\n:N ~ X n.
+(*! math
+We get a contradiction from \[ $$G \] which is proven by well founded induction:
+*)
+trivial.
+intros.
+elim well_founded.N with H1.
+intros.
+(*! math
+we assume \[ $$H3 \] and must prove \[ $0 \].
+*)
+intro.
+apply H0 with H4.
+lefts G $& $\/.
+(*! math
+Assuming \[ $$H4 \] and using ( \[ H0 \] ) we get an integer \[ x \] such that
+\[ $$H6 \] and \[ $$H7 \]. This gives a contradiction with \[ $$H3 \].
+\end{proof}
+*)
+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)).
+(*! math
+\begin{lemma}\label{not_odd_and_even.N}
+An integer can not be odd and even:
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+By induction over \[ x \].
+\end{proof}
+*)
+intro 2.
+elim H.
+trivial 6.
+intros.
+intro.
+left H4.
+elim H2 with [case].
+trivial =H0 H4 H6.
+elim H1.
+axiom H3.
+axiom H6.
+intro.
+rmh H4.
+left H5.
+rmh H5.
+rewrite_hyp H4 H7 calcul.N.
+left H4.
+axiom H4.
+save.
+
+theorem sum_square.N /\x,y:N (x + y)^N2 = x^N2 + N2*x*y + y^N2.
+(*! math
+\begin{lemma}\label{sum_square.N}
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+Easy.
+\end{proof}
+*)
+intros.
+rewrite calcul.N mul.left.distributive.N mul.right.distributive.N add.associative.N.
+intro.
+save.
+
+
+fact less.exp.N /\n,x,y:N( x <= y -> x^n <= y^n).
+(*! math
+\begin{lemma}\label{less.exp.N}
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+By induction on \[ n \].
+\end{proof}
+*)
+intros.
+elim H.
+trivial.
+rewrite calcul.N.
+trivial.
+save.
+
+fact less_r.exp.N  /\n,x,y:N( x^n < y^n -> x < y).
+(*! math
+\begin{lemma}\label{less_r.exp.N}
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+Follows from lemma \ref{less.exp.N}.
+\end{proof}
+*)
+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).
+(*! math
+\begin{lemma}\label{less.ladd.N}
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+Easy induction over \[ x \].
+\end{proof}
+*)
+intros.
+elim H.
+rewrite calcul.N.
+trivial.
+save.
+
+
+(*! math
+\section{The proof itself}
+*)
+
+theorem n.square.pair /\n:N (\/p:N n^N2=N2*p -> \/q:N n=N2*q).
+(*! math
+\begin{lemma}\label{n.square.pair}
+ If the square of \[ n \] is even then \[ n \] is even:
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+*)
+intros.
+lefts H0 $\/ $&.
+apply odd_or_even.N with H.
+lefts G $\/ $& $or.
+(*! math
+We assume \[ $$H1 \] ( \[ H1 \] ).
+We distinguish two cases. If \[ n \] is even we get what we want. 
+*)
+trivial.
+(*! math
+If  \[ n \] is odd we have \[ $$H3 \]
+*) 
+prove  n^N2 = N2*(N2*y^N2+N2*y) + N1.
+(*! math
+which implies \[ $0 \]
+*) 
+rewrite H3 sum_square.N.
+rewrite add.associative.N mul.associative.N mul.left.distributive.N.
+from N1 + N4 * y + (N2 * y) ^ N2 = N1 + N4 * y + N4 * y ^ N2.
+intro.
+(*! math
+and this gives a contradiction by lemma \ref{not_odd_and_even.N} using ( \[ H1 \] )
+\end{proof}
+*) 
+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).
+(*! math
+\begin{lemma}\label{decrease}
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+Using lemma \ref{less_r.exp.N} and lemma \ref{less.ladd.N}
+\end{proof}
+*)
+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.
+trivial.
+trivial  =H0 H2.
+save.
+
+lem sup_zero /\m,n : N (m^ N2 = N2 * n^ N2 -> N0 < m -> N0 < n).
+(*! math
+\begin{lemma}\label{sup_zero}
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+Using lemma \[ $$ neq.less_or_sup.N \] from the library.
+\end{proof}
+*)
+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).
+(*! math
+\begin{definition}
+We define \[ Q m = $$Q m \].
+\end{definition}
+*)
+
+lem dec /\m:N (Q m -> \/m':N (Q m' & m' < m)).
+(*! math
+\begin{lemma}\label{dec}
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+*)
+intros.
+lefts H0 $Q $\/ $&.
+(*! math
+We assume that \[ $$H0 \] and \[ $$H2 \] (\[ H2 \]) and we must prove \[ $0 \].
+*)
+apply sup_zero with H2 and H0.
+(*! math
+By lemma \ref{sup_zero} we get \[ $$G \]. We show that \[ n \] is the integer we are looking for.
+*)
+intro.
+instance ?1 n.
+intros.
+intros.
+trivial.
+(*! math
+We just need to prove \[ $0 \] and \[1 $0 \].
+*)
+prove \/p:N (m ^ N2 = N2 * p).
+intro.
+instance ?2  n^N2.
+trivial.
+apply n.square.pair with G0.
+lefts G1 $& $\/.
+(*! math
+Using lemma \ref{n.square.pair} we get \[ q \] such that \[  $$H4 \]
+*)
+prove n ^N2 = N2 * q ^N2.
+rewrite_hyp H2 H4.
+prove N2 * (N2 * q ^N2) = N2 * n ^ N2.
+from H2.
+left G1.
+intro.
+(*! math
+and then \[ $$G1 \].
+*)
+trivial =H3 G1.
+(*! math
+Finally \[ $0 \] follows from lemma \ref{decrease}.
+\end{proof}
+*) 
+elim decrease.
+save.
+
+lem sq2_irrat /\m:N ~Q m.
+(*! math
+\begin{lemma}\label{sq2_irrat}
+$$ \[ $0 \] $$
+\end{lemma}
+\begin{proof}
+Follows from the previous lemma by selecting the minimal element in \[ Q \] (using lemme \ref{minimal.element}) and getting a contradiction.
+\end{proof}
+*)
+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).
+(*! math
+\begin{theorem} The square-root of 2 is irrational. For this we just need to prove the following:
+$$ \[ $0 \] $$
+\end{theorem}
+\begin{proof}
+*)
+intros.
+apply sq2_irrat  with H.
+(*! math
+We assume \[ $$H1 \].
+By the previous lemma we have \[ $$G \].
+*)
+elim H with [case].
+intro.
+intro.
+(*! math
+If \[ $$H2 \] we easely get \[ $0 \].
+*)
+elim H0 with [case].
+intro.
+rewrite_hyp H1 H2 H4 calcul.N.
+left H1;; intros.
+prove Q m.
+(*! math
+If \[ m > N0 \] then we have \[ Q m \] and a contradiction.
+\end{proof}
+*)
+intros $Q $\/ $&.
+trivial.
+select 2.
+axiom H1.
+trivial.
+elim G.
+save.