diff options
Diffstat (limited to 'phox/square-root-2.phx')
-rw-r--r-- | phox/square-root-2.phx | 368 |
1 files changed, 0 insertions, 368 deletions
diff --git a/phox/square-root-2.phx b/phox/square-root-2.phx deleted file mode 100644 index 92a888b3..00000000 --- a/phox/square-root-2.phx +++ /dev/null @@ -1,368 +0,0 @@ -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. |