Section Exercice1.

Require Export Bool.

Print bool.

End Exercice1.


Section IsometriesDuTriangle.

Inductive Rot : Set :=  R0 | R1 | R2.

Definition RoR : Rot -> Rot -> Rot := fun r r' : Rot =>
match r with
  | R0 => r'
  | R1 => match r' with
            | R0 => R1
            | R1 => R2
            | R2 => R0
          end
  | R2 => match r' with
            | R0 => R2
            | R1 => R0
            | R2 => R1
          end
end.

Lemma RoRNilpotent : forall r : Rot, RoR r (RoR r r) = R0.
Proof.
intro r.
case r; compute; reflexivity.
Qed.

Lemma RoRCommut : forall r r' : Rot, RoR r r' = RoR r' r.
Proof.
intros r r'.
case r; case r'; compute; reflexivity.
Qed.

Inductive Sym : Set := Sa | Sb | Sc.

Definition SoS : Sym -> Sym -> Rot := fun s s' =>
match s' with
  | Sa => match s with
            | Sa => R0
            | Sb => R2
            | Sc => R1
          end
  | Sb => match s with
            | Sa => R1
            | Sb => R0
            | Sc => R2
          end
  | Sc => match s with
            | Sa => R2
            | Sb => R1
            | Sc => R0
          end
end.

Lemma SoSInvolutive : forall s : Sym, SoS s s = R0.
Proof.
intro s.
case s; compute; reflexivity.
Qed.

Lemma SoSnonCommut : forall s s' : Sym, s <> s' -> SoS s s' <> SoS s' s.
Proof.
intros s s'.
case s; case s'; intros H H'; compute in H';
( discriminate || elim H ; reflexivity ).
Qed.

Definition RoS : Rot -> Sym -> Sym := fun (r1 : Rot) (s2 : Sym)  =>
match r1 with
  | R0 => s2 
  | R1 => match s2 with
            | Sa => Sc
            | Sb => Sa
            | Sc => Sb
          end
  | R2 => match s2 with
            | Sa => Sb
            | Sb => Sc
            | Sc => Sa
          end
end.

Definition SoR : Sym -> Rot -> Sym := fun (s1 : Sym) (r2 : Rot)  =>
match s1 with
  | Sa => match r2 with
            | R0 => Sa
            | R1 => Sb
            | R2 => Sc
          end 
  | Sb => match r2 with
            | R0 => Sb
            | R1 => Sc
            | R2 => Sa
          end
  | Sc => match r2 with
            | R0 => Sc
            | R1 => Sa
            | R2 => Sb
          end
end.

Inductive Isom : Set :=
  | Cr : Rot -> Isom
  | Cs : Sym -> Isom.

Definition rond : Isom -> Isom -> Isom := fun i i' =>
match i with
  | Cr r => match i' with
               | Cr r' => Cr (RoR r r')
               | Cs s => Cs (RoS r s)
            end
  | Cs s => match i' with
               | Cr r => Cs (SoR s r)
               | Cs s' => Cr (SoS s s')
             end
end.

Lemma power_sixt : forall i : Isom,
 rond i (rond i (rond i (rond i (rond i i)))) = Cr R0.
Proof.
intro i.
case i ; intro rs; case rs; compute; reflexivity.
Qed.

Inductive Sommet : Set := A | B | C.

Definition app : Isom -> Sommet -> Sommet := fun i p =>
match i with
  | Cr r => match r with
               | R0 => p
               | R1 => match p with | A => B | B => C | C => A end
               | R2 => match p with | A => C | B => A | C => B end
            end
  | Cs s => match s with
               | Sa => match p with | A => A | B => C | C => B end
               | Sb => match p with | A => C | B => B | C => A end
               | Sc => match p with | A => B | B => A | C => C end
            end
end.

Lemma comp_app : forall (f g : Isom) (x : Sommet),
app f (app g x) = app (rond f g) x.
Proof.
intros f g x.
case f; intro rsf ; case rsf ;
case g; intro rsg ; case rsg ;
case x; compute ; reflexivity.
Qed.

End IsometriesDuTriangle.


Section Exercice3.

Theorem and_comm : forall P Q:Prop,  P /\ Q -> Q /\ P.
Proof.
intros P Q H.
elim H. clear H. intros Hp Hq.
split ; assumption.
Qed.

Theorem or_comm : forall P Q:Prop, P \/ Q -> Q \/ P.
Proof.
intros P Q H.
elim H ; intro ; [ right | left ]; assumption.
Qed.

Theorem arrow_under_and : forall P Q R S:Prop,
  (P->Q) /\ (R->S) -> P /\ R ->  Q /\ S.
Proof.
intros P Q R S H.
elim H. clear H. intros Hpq Hrs.
intro H. elim H. clear H. intros Hp Hr.
split ; [ apply Hpq | apply Hrs ] ; assumption.
Qed.

Lemma trans_sym_refl : forall E:Set, forall R:E->E->Prop,
(forall x y z, (R x y) -> (R y z) -> (R x z)) ->
(forall x y, (R x y) -> (R y x)) ->
(forall x y, (R x y) -> (R x x)).
Proof.
intros E R Trans Symetrie x y Rxy.
apply Trans with (y:=y).
assumption.
apply Symetrie. assumption.
Qed.

Theorem trans_sym_exists_refl : forall E:Set, forall R:E->E->Prop,
(forall x y z, (R x y) -> (R y z) -> (R x z)) ->
(forall x y, (R x y) -> (R y x)) ->
forall x, (exists e:E, (R x e)) -> (R x x).
Proof.
intros E R Trans Symetrie x H.
elim H. clear H. intros e H.
apply trans_sym_refl with (y:=e); assumption.
Qed.

Theorem Th2 : forall E:Set, forall P Q:E->Prop,
 (exists e:E, (P e) /\ (Q e)) -> (exists e:E, P e) /\ (exists e:E, Q e).
Proof.
intros E P Q H.
elim H. clear H. intros e H.
elim H. clear H. intros Hp Hq.
split; exists e; assumption.
Qed.

Theorem Th3 : forall P:Prop, P -> ~~P.
Proof.
intros P Hp HnotP.
apply HnotP. assumption.
Qed.

Theorem impl_with_or : forall P Q: Prop, (P \/ ~Q) /\ Q -> P.
Proof.
intros P Q H.
elim H. clear H. intros H Hq.
elim H.
trivial.
intro HnotQ. elim HnotQ. assumption.
Qed.


(* Il existe en Écosse un club très fermé qui obéit aux règles suivantes : *)
(*   tout membre non écossais porte des chaussettes rouges ;               *)
(*   tout membre porte un kilt ou ne porte pas de chaussettes rouges ;     *)
(*   les membres mariés ne sortent pas le dimanche ;                       *)
(*   un membre sort le dimanche si et seulement s'il est écossais ;        *)
(*   tout membre qui porte un kilt est écossais et marié ;                 *)
(*   tout membre écossais porte un kilt.                                   *)

Parameters Ecossais ChaussettesRouges Kilt Mariage SortLeDimanche : Prop.
Definition Club : Prop := 
  (~Ecossais -> ChaussettesRouges) /\
  (Kilt \/ ~ChaussettesRouges) /\
  (Mariage -> ~SortLeDimanche) /\
  (SortLeDimanche -> Ecossais) /\ (Ecossais -> SortLeDimanche) /\
  (Kilt -> Ecossais /\ Mariage) /\
  (Ecossais -> Kilt).

Theorem ClubIsEmpty : Club -> False.
Proof.
intro HClub.
repeat (elim HClub; clear HClub; intro; intro HClub).

assert (HnonKilt : Kilt -> False).
intro HKilt.
elim (H4 HKilt). intros HEcossais HMariage.
elim (H1 HMariage).
apply (H3 HEcossais).

elim H0.
  exact HnonKilt.

  intro HnonChaussettes.
  apply HnonChaussettes.
  apply H.
  intro HEcossais.
  apply HnonKilt.
  apply (HClub HEcossais).
Qed.