(* Question 1 *)

Une sorte est le type d'un type.
La sorte Set est celle dans laquelle on calcule, 
la sorte Prop celle dans laquelle on raisonne.
nat est l'ensemble des entiers naturels (données sur lesquels on calcule)
le est la relation d'ordre sur les entiers naturels (sur laquelle on raisonne)

(* Question 2 *)

Qed vérifie que le terme de preuve construit à bien pour type l'énoncé.
Il enregistre aussi dans le contexte la liaison entre le nom du théorème,
son énoncé et sa preuve.

(* Question 3 *)
                  ---------------------- ----------------  
                   A\/B,~B,B|- B->False   A\/B,~B,B |- B
                  ---------------------- ---------------- 
                       A\/B, ~B, B |- False
----------------- --------------------------------------- --------------------
A\/B, ~B, A |- A          A\/B, ~B, B |- A                   A\/B, ~B |- A\/B
----------------- --------------------------------------- --------------------
    A\/B, ~B |- A
--------------------
|- A \/ B -> ~B -> A

(* Question 4 *)

fun (A B:Prop) => fun (H1:A\/B) => fun (H2:~B) => 
    (or_ind A B A (fun (H3:A) => H3) (fun (H4:B) (False_ind A (H2 H4)) H1)

Proof: fun (A B : Prop) (H : A \/ B) (H0 : ~ B) =>
       or_ind (fun H1 : A => H1) (fun H4 : B => False_ind A (H0 H4)) H

(* Question 5 *)

forall A B C : Prop, (A -> B -> C) -> (A -> B) -> A -> C

(* Question 6 *)

Fixpoint puissance (x:nat) (n:nat) {struct n} : nat :=
match n with 
| O     => 1
| (S p) => x *(puissance x p)
end.

(* Question 7 *)

Lemma puissance_1 : forall x:nat, puissance x 0 = 1.
simpl;reflexivity.
Qed.

Lemma puissance_2 : forall n:nat, puissance 1 n = 1.
intros n; simpl.
elim n.
simpl;reflexivity.
simpl.
intros n'.
rewrite <- plus_n_O.
intros; assumption.
Qed.

(* Question 8 *)

Inductive pile : Set := vide : pile | empiler : nat -> pile -> pile.

Definition is_vide (p:pile) : Prop :=
match p with
| vide => True
| empiler _ _ => False
end.

(* Question 9 *)

Definition depiler (p:pile) : pile :=
match p with
| vide => vide
| empiler n p2 => p2
end.

Definition echanger (p:pile) : pile :=
match p with 
| vide => vide
| empiler n1 p1 => 
   match p1 with 
     | vide => p
     | empiler n2 p2 => empiler n2 (empiler n1 p2)
   end
end.

(* Question 10 *)

Fixpoint hauteur (p:pile) {struct p}: nat :=
match p with 
| vide => 0
| empiler n1 p1 => hauteur p1 + 1
end.

(* Question 11 *)

Fixpoint mod2 (n:nat) : nat :=
match n with
| O => O
| (S O) => 1
| (S (S p)) => mod2 p
end.


nat_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

(* Question 12 *)

Axiom nat2_ind : 
  forall P:nat->Prop, P 0 -> P 1 -> 
    (forall n:nat, P n -> P (S (S n))) -> forall n:nat, P n. 

Require Export Omega.

Lemma bornes_mod2 : forall n:nat, 0<=mod2 n <=1.
intros n; apply (nat2_ind (fun (n:nat) => 0 <= mod2 n <= 1)).
simpl; omega.
simpl; omega.
intros; simpl; assumption.
Qed.

Lemma bornes_mod2' : forall n:nat, 0<=mod2 n <=1 /\ 0<=mod2 (S n) <=1.
intros n; elim n.
simpl; omega.
intros n' HR.
elim HR.
intros H1 H2.
split.
apply H2.
simpl.
apply H1.
Qed.


Lemma trans : (forall n:nat, 0<=mod2 n <=1 /\ 0<=mod2 (S n) <=1) -> 
  (forall n:nat, 0<=mod2 n <=1).
intros.
generalize (H n); intros.
elim H0.
auto.