Section Raisonnement_par_cas.
Variable A B C : Prop.
(*
Comme la conjonction, la disjonction \/ est associée à deux règles :
- une pour démontrer les formules de la forme A\/B
    il y a deux façons de le faire :
     |- A                     |- B
    -----(v-i-gauche)     -------(v-i-droite)
     |-  A\/B                  |- A\/B

  En Coq, ces règles s’appellent simplent 'left' et 'right'.
*)
Theorem ouGauche : A -> A\/B.
Proof.
intro Ha. (* je dois maintenant prouver A\/B sous hypothèses A.*)
left. (*j’ai indiqué que j’allais prouver ma disjonction en prouvant
      la formule de gauche. Si vous remplacez left par right, vous
      ne pourrez jamais terminer la preuve ! Car il faudrait prouver
      B sous hypothèse A ! *)
assumption. (*j’ai A en hypothèse, donc je peux conclure *)
Qed.

(* Exercice : énoncez un théorème pour la formule suivante, et démontrez-le :
    B-> (A\/A\/A\/A\/A\/B)
*)

(*

- une pour utiliser une hypothèse de la forme A\/B
En Coq, elle peut être expliquée comme suit :
  ' si je veux prouver C à partir de A\/B, comme
    je ne sais pas lequel de A ou de B est vrai (je sais qu’au moins un des deux
    est vrai, c’est tout), il faut que dans je puisse montrer C
    à partir de n’importe lequel des deux'. C’est le raisonnement par cas.

En déduction naturelle, cela s’écrit :

|- A\/B      A|-C     B|- C
-----------------------------(or-elim)
           |- C

En Coq, la logique est la même, mais la présentation est un peu différente~:
c’est la règle 'case'. La différence est qu’on ne prouve pas A\/B, mais qu’on le
laisse dans les hypothèses.


 |- A -> C     |- B -> C
------------------- (case)
  A\/B |- C

*)

Theorem analyse_par_cas : (A/\B) \/ (A/\C) -> A.
Proof.
intro.
(* maintenant je dois être capable de montrer A à partir 
  de A/\B et de A/\C. La tactique 'case' appliquée à mon hypothèse
  (qui doit être ma disjonction, va me générer deux objectifs :
    - (A/\B) -> A 
    - (A/\C) -> A  *) 
case H.

(* et maintenant, c’est facile, on l’a déjà fait au tuto précédent*)
- intro. destruct H0. assumption.
- intro. destruct H0. assumption.
Qed.

(*Exercices : démontrez la commutativité et l’associativité de la disjonction *)


End Raisonnement_par_cas.