(* 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.                               *)
Hypothesis mult_non_0_simpl :
    forall n m p :nat,  n>0 -> n*m=n*p -> m=p.


(* 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.
Qed.

Theorem not_odd_and_even: forall n:nat,  ~(odd n /\ even n).
Proof.
Qed.

Theorem odd_square: forall n:nat, odd n -> odd (n*n).
Proof.
Qed.

Theorem odd_or_even: forall n:nat, odd n \/ even n.
Proof.
Qed.

Theorem square_even: forall n:nat, even (n*n) ->  even n.
Proof.
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.
Qed.

Theorem mult_2_non_zero_increase: forall n:nat, n>0 -> n<2*n.
Proof.
Qed.


Theorem square_root_2_not_rational_range: forall r q :nat,
  q<r -> q>0 -> forall p:nat, p*p<>2*q*q.
Proof.
Qed.

Theorem square_root_2_not_rational: forall q:nat,
 q>0 -> forall p:nat, p*p<>2*q*q.
Proof.
Qed.