blob: ecba1a7f203325926e1f5aa4e977760eabcb7a42 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(******************************************************************************
* *
* Proof that sqrt 2 is irrational *
* *
* Laurent.Thery@sophia.inria.fr *
* February 2002 *
* (Revised April 2004 for coq 8.0) *
******************************************************************************)
Require Import ArithRing.
Require Import Wf_nat.
Require Import Peano_dec.
Require Import Div2.
Require Import Even.
(******************************************************************************
* *
* Properties of div2 and double (these theorems should be in Div2.v) *
* *
******************************************************************************)
Theorem double_div2: forall (n : nat), div2 (double n) = n.
simple induction n; auto with arith.
intros n0 H.
rewrite double_S; pattern n0 at 2; rewrite <- H; simpl; auto.
Qed.
Theorem double_inv: forall (n m : nat), double n = double m -> n = m.
intros n m H; rewrite <- (double_div2 n); rewrite <- (double_div2 m); rewrite H;
auto.
Qed.
Theorem double_mult_l: forall (n m : nat), double (n * m) = double n * m.
unfold double; auto with arith.
Qed.
Theorem double_mult_r: forall (n m : nat), double (n * m) = n * double m.
unfold double; intros; ring.
Qed.
(******************************************************************************
* *
* If the power to the 2 of a number is even, then this number is even *
* *
******************************************************************************)
Theorem even_is_even_times_even: forall (n : nat), even (n * n) -> even n.
intros n H; (try case (even_or_odd n)); auto.
intros; apply even_mult_inv_r with (1 := H); auto.
Qed.
(******************************************************************************
* *
* Useful fact 4*(n/2)*(n/2) = n*n if n is even *
* *
******************************************************************************)
Theorem main_thm_aux:
forall (n : nat), even n -> double (double (div2 n * div2 n)) = n * n.
intros; rewrite double_mult_l; rewrite double_mult_r;
(repeat rewrite <- even_double); auto.
Qed.
(******************************************************************************
* Main theorem *
* We do the proof of the theorem by well founded induction: *
* Suppose that we have n*n = 2*p*p *
* if n=0 then p = O *
* if n<>0 then *
* - n is even (n=2n') and p is even (p=2p') *
* - we have n'*n'=2*p'*p' and n' < n *
* - by the induction hypothesis we have p'=O *
* - so p=O *
******************************************************************************)
Theorem main_thm: forall (n p : nat), n * n = double (p * p) -> p = 0.
intros n; pattern n; apply lt_wf_ind; clear n.
intros n H p H0.
case (eq_nat_dec n 0); intros H1.
generalize H0; rewrite H1; case p; auto; intros; discriminate.
assert (H2: even n).
apply even_is_even_times_even.
apply double_even; rewrite H0; rewrite double_div2; auto.
assert (H3: even p).
apply even_is_even_times_even.
rewrite <- (double_inv (double (div2 n * div2 n)) (p * p)).
apply double_even; rewrite double_div2; auto.
rewrite main_thm_aux; auto.
assert (H4: div2 p = 0).
apply (H (div2 n)).
apply lt_div2; apply neq_O_lt; auto.
apply double_inv; apply double_inv; (repeat rewrite main_thm_aux); auto.
rewrite (even_double p); auto; rewrite H4; auto.
Qed.
(******************************************************************************
* *
* Coercions from nat and Z to R *
* *
******************************************************************************)
Require Import Reals.
Require Import Field.
Coercion INR : nat >-> R.
Coercion IZR : Z >-> R.
(******************************************************************************
* *
* Definition of irrational *
* *
******************************************************************************)
Definition irrational (x : R) : Prop :=
forall (p : Z) (q : nat), q <> 0 -> x <> (p / q)%R.
(******************************************************************************
* *
* Final theorem *
* *
******************************************************************************)
Theorem irrational_sqrt_2: irrational (sqrt 2%nat).
intros p q H H0; case H.
apply (main_thm (Zabs_nat p)).
replace (Div2.double (q * q)) with (2 * (q * q));
[idtac | unfold Div2.double; ring].
case (eq_nat_dec (Zabs_nat p * Zabs_nat p) (2 * (q * q))); auto; intros H1.
case (not_nm_INR _ _ H1); (repeat rewrite mult_INR).
rewrite <- (sqrt_def (INR 2)); auto with real.
rewrite H0; auto with real.
assert (q <> 0%R :> R); auto with real.
field; auto with real; case p; simpl; intros; ring.
Qed.
|
