(* TP2 Logique classique *)


(* -------------------------------------------------------------------------- *)

(* 1. RETOUR SUR LES LISTES *)


(* On définit les listes de nat *)
Inductive nlist : Set :=
| nnil : nlist                  
| ncons : nat -> nlist -> nlist. 

(* ... avec des notations confortables *)
Infix "::" := ncons.
Notation "[]" := nnil.


(* EXERCICE 1 *)
(* Définir la fonction "concat" qui concatène deux nlist l1 et l2 (par récursion sur l1) *)
Fixpoint concat (l1 l2 : nlist) : nlist := 
[].

(* On note ++ en notation infix pour la concatenation *)
Infix "++" := concat.


(* EXERCICE 2 *)
(* Définir la fonction "length" qui retourne la longueur d'une nlist *)


(* EXERCICE 3 *)
(* Définir la fonction "appartient" qui retourne vrai si un nat appartient à une nlist *)



(* -------------------------------------------------------------------------- *)

(* 2. MODÉLISATIONS ET PREUVES EN LOGIQUE PROPOSITIONNELLE *)

(* On introduit les variables propositionnelles avec lesquelles 
   on va travailler par la suite *)
Section logique_propositionnelle.
Context (P Q R A B D Z J F M S T: Prop).

(* EXERCICE 4 *)
(* Modéliser l'exercice de TD "Georges aime la logique", prouver que Georges aime la logique *)


(* EXERCICE 5 *)
(* Modéliser l'exercice de TD "Zoé va à Paris", prouver que Zoé va à Paris *)
(* - introduction du /\ : split
*)


(* LE NOT *)

(* - la notation not : unfold not
   - la notation not en hypothèse : unfold not in [nom de l'hypothèse avec ~]
*)

(* EXERCICE 6 *)
Theorem DeMorgan_sens1 : (~P \/ ~Q) -> ~(P /\ Q).
Admitted.


(* Si on a toto et ~toto dans les hypothèses, alors le but est résolu avec "contradiction." *)

(* EXERCICE 7 *)
Theorem exercice_7 : P -> ~P -> Q.
Admitted.


(* LE TIERS-EXCLU *)

(* On introduit la règle de tiers-exclu. *)
Context (Tiers_exclu: forall X: Prop, X \/ ~X).

(* Pour l'utiliser, c'est-à-dire pour avoir deux sous buts, un avec toto en hypothèse, l'autre avec ~toto, on invoquera :
   destruct (Tiers_exclu toto).
*)


(* EXERCICE 8 *)
Theorem exercice_8 : P \/ ~P.
Admitted.


(* EXERCICE 9 *)
Theorem exercice_9 : ((P -> Q) -> P) -> P.
Admitted.


(* EXERCICE 10 *)
(* Modéliser l'exercice de TD "Frodon est triste", prouver que Frodon est triste *)


(* EXERCICE 11 *)
(* Modéliser l'exercice de TD "Gérard est déprimé", prouver que Gérard est déprimé *)


(* EXERCICE 12 *)
(* Quid de ~~P et P ? *)
Theorem exercice_6c: (~~P -> P) /\ (P -> ~~P).
(* Pour l'un des deux sens on aura besoin du tiers-exclu et, en remarquant
   qu'on peut déduire False des hypothèses, de la simplification "exfalso". *)
Admitted.


(* -------------------------------------------------------------------------- *)


(* EXERCICE 13 *)
Theorem exercice_comp_1: (P \/ Q) -> (Q \/ P).
Admitted.


(* EXERCICE 14 *)
Theorem exercice_comp_2 : (P -> Q -> R) <-> (P /\ Q -> R).
Admitted.


(* EXERCICE 15 *)
Theorem exercice_comp_3 : (P -> Q) /\ (P -> R) <-> (P -> Q /\ R).
Admitted.

End logique_propositionnelle.

(* -------------------------------------------------------------------------- *)