(* Durant ce TD nous allons démontrer l'irrationalité de sqrt(2). *) (* Plus précisément, nous allons montrer qu'il n'existe pas de couple (p,q) *) (* d'entiers avec q<>0 tel que p^2 = 2*q^2. *) (* Nous suivons la preuve classique par descente infinie : *) (* - si p^2 est pair, p l'est aussi ; *) (* - si p est pair, 4 divise p^2 donc 2 divise q^2 ; *) (* - par suite, il existe (p',q') plus petits, satisfaisant la même *) (* propriété. *) (* - On conclue par l'absurde en supposant (p,q) minimal. *) (* Pour charger les théorèmes relatifs aux entiers *) Require Export Arith. (* Pour utiliser la tactique ring *) Require Import ArithRing. (* la tactique ring permet de résoudre n'importe quel but de la forme *) (* expr1 = expr2 où expr1 et expr2 sont des expressions arithmétiques *) (* c'est-à-dire des composées d'additions et de multiplications de *) (* variables et de constantes. ring ne va pas regarder les hypothèses *) (* donc expr1 et expr2 doivent être égales sans qu'une information *) (* supplémentaire soit nécessaire. *) (* ring ne connait pas le constructeur S des entiers. Vous devez donc *) (* changer les (S n) en (n+1) pour que ring s'y retrouve. Si ring échoue *) (* il laisse le but inchangé. *) (* Nous admettons ce résultat dans un premier temps. Question bonus, si *) (* vous finissez en avance : démontrez-le. *) Theorem mult_non_0_simpl : forall n m p :nat, n>0 -> n*m=n*p -> m=p. Proof. Admitted. (* On attaque la preuve *) Definition odd : nat -> Prop := fun n:nat => exists n':nat, n = 2*n'+1. Definition even : nat -> Prop := fun n:nat => exists n':nat, n = 2*n'. Theorem even_succ_odd: forall n:nat, even (S n) -> odd n. Proof. intros n H. elim H. clear H. intros x H. induction x. discriminate. exists x. apply eq_add_S. rewrite H. rewrite S_to_plus_one with x. rewrite S_to_plus_one with (2*x+1). ring. Qed. Theorem odd_succ_even : forall n:nat, odd (S n) -> even n. Proof. intros n H. elim H. clear H. intros x H. exists x. apply eq_add_S. rewrite H. rewrite S_to_plus_one with (2*x). ring. Qed. Theorem not_odd_and_even: forall n:nat, ~(odd n /\ even n). Proof. induction n. intro H. elim H. clear H. intros Hodd Heven. elim Hodd. intros x Habs. rewrite plus_comm in Habs. discriminate. intro H. elim H. clear H. intros Hodd Heven. apply IHn. split; [apply even_succ_odd | apply odd_succ_even]; assumption. Qed. Theorem odd_square: forall n:nat, odd n -> odd (n*n). Proof. intros n Hodd. elim Hodd. clear Hodd. intros x Hodd. exists (2*x*x+2*x). rewrite Hodd. ring. Qed. Theorem odd_or_even: forall n:nat, odd n \/ even n. Proof. induction n. right. exists 0. compute. reflexivity. elim IHn ; intro H ; elim H ; clear H ; intros x H ; [right | left]; [exists (x+1) | exists x]; rewrite H; rewrite S_to_plus_one; ring. Qed. Theorem square_even: forall n:nat, even (n*n) -> even n. Proof. intros n H. elim (odd_or_even n); intro H'. elim (not_odd_and_even (n*n)). split; try (apply odd_square); assumption. assumption. Qed. Theorem square_root_2_rat_decrease: forall q p :nat, p*p=2*q*q -> exists q':nat, q=2*q' /\ exists p':nat, p'*p'=2*q'*q'. Proof. intros q p H. elim (square_even p). intros p' Evenp. elim (square_even q). intros q' Evenq. exists q'. split. assumption. exists p'. rewrite Evenp in H. rewrite Evenq in H. apply mult_non_0_simpl with (n:=4). apply gt_Sn_O. assert (TrivialEquality : 4*(p'*p') = 2*p'*(2*p')). ring. rewrite TrivialEquality. rewrite H. ring. rewrite Evenp in H. exists (p'*p'). apply mult_non_0_simpl with (n:=2). apply gt_Sn_O. pattern (2*q*q) in H. rewrite<- mult_assoc in H. rewrite<- H. ring. exists (q*q). rewrite H. ring. Qed. Theorem mult_2_non_zero_increase: forall n:nat, n>0 -> n<2*n. Proof. intro n. case n ; clear n. trivial. intros n H. simpl. apply lt_n_S. rewrite plus_0_r. rewrite<- plus_Snm_nSm. apply lt_plus_trans. exact (lt_n_Sn n). Qed. Lemma useful_lemma : forall n:nat, 2*n>0 -> n>0. Proof. intro n. case n; clear n. trivial. intros n _. apply gt_Sn_O. Qed. Theorem square_root_2_not_rational_range: forall r q :nat, q q>0 -> forall p:nat, p*p<>2*q*q. Proof. induction r. intros q Habs _. inversion Habs. intros q H1 H2 p Habs. elim (square_root_2_rat_decrease q p Habs). intros x H. elim H. clear H. intros Eq1 H. elim H. clear H. intros y Eq2. apply IHr with (q:=x) (p:=y). apply lt_le_trans with (m := q). rewrite Eq1. apply mult_2_non_zero_increase. apply useful_lemma. rewrite<- Eq1. exact H2. apply le_S_n. exact H1. apply useful_lemma. rewrite<- Eq1. assumption. assumption. Qed. Theorem square_root_2_not_rational: forall q:nat, q>0 -> forall p:nat, p*p<>2*q*q. Proof. intros q H. apply square_root_2_not_rational_range with (r:=q+1). rewrite plus_comm. rewrite<- S_to_plus_one. compute. apply le_n. assumption. Qed. (* Bonus : démonstration du lemme précédemment admis *) Lemma greater_than_0_succ : forall n, n>0 -> exists p, n = S p. Proof. intro n. case n; clear n. intro Habs. inversion Habs. intros n _. exists n. reflexivity. Qed. Lemma le_eq_ge : forall n m, (n=m) \/ ((nm)). Proof. intros n m. elim (le_or_lt n m); [intro H | intro Hnm]. elim (le_lt_or_eq n m H); clear H ; intro Hnm. right. left. assumption. left. assumption. right. right. assumption. Qed. Theorem mult_non_0_simpl_ : forall n m p :nat, n>0 -> n*m=n*p -> m=p. Proof. intros n m p Hn. elim (greater_than_0_succ n Hn). intros n' Hnn'. rewrite Hnn'. clear Hn n Hnn'. elim (le_eq_ge m p); intros Hmp H. trivial. elim Hmp; clear Hmp; intro Hmp ; [absurd (S n' * m < S n' *p) | absurd (S n' * p < S n' * m)]; (rewrite H ; apply lt_irrefl) || (apply mult_S_lt_compat_l ; assumption). Qed.