(*****************************************************************************)
(*                                                                           *)
(*                 Tactiques pour la logique de base                         *)
(*                                                                           *)
(*****************************************************************************)

(* Introduction des variables et des hypothèses (intro) *)

Theorem trivial: forall (A : Prop), A -> A.
Proof.
Qed.

(* Conjonction: décomposition (split) et utilisation (case)*)

Theorem and_commutative: forall (A  B : Prop), A /\ B -> B /\ A.
Proof.
Qed.

(* Disjonction: décomposition (right & left) et utilisation (case) *)

Theorem or_commutative: forall (A  B:Prop), A \/ B -> B \/ A.
Proof.
Qed.

(* Implication décomposition (intro) et utilisation (apply) *)

Theorem mp: forall (A B : Prop), A -> (A -> B) -> B.
Proof.
Qed.

(* Implication un peu plus dur *)

Theorem S: forall (A B C : Prop), (A -> B -> C) -> (A -> B) -> A -> C.
Proof.
Qed.

(* Implication et conjonction *)

Theorem Praeclarum: 
  forall (A B C D : Prop), (A -> B) /\ (C -> D) -> A /\ C -> B /\ D.
Proof.
Qed.

(* Implication et quantification *)

Theorem resolution:
  forall (p q : Type -> Prop) (a : Type),
     (p a) -> (forall (x : Type), (p x) -> (q x)) -> (q a).
Proof.
Qed.

(* Existentiel: décomposition (exists) utilisation (case) *)

Theorem Simple:
  forall (A : Set) (R : A -> A -> Prop),
  (forall (x y z : A), (R x y) /\ (R y z) -> (R x z)) ->
  (forall (x y : A), (R x y) -> (R y x)) ->
  forall (x : A), (exists (y:A), (R x y)) -> (R x x).
Proof.
Qed.

(* Négation: décomposition (intro) et utilisation (case) *)

Theorem not_not: forall (A : Prop), A -> ~ (~ A).
Proof.
Qed.

(* Négation et disjonction *)

Theorem mini_cases: forall (A B : Prop), (A \/ ~ B) /\ B -> A.
Proof.
Qed.

(* Difficile !! *)

Theorem not_quite_classic: forall (A : Prop), ~ (~ (A \/ ~ A)).
Proof.
Qed.

(* Ajout du tiers exclu*)

Require Import Classical.
Check classic.

Theorem not_not_converse: forall (A : Prop), ~ (~ A) -> A.
Proof.
Qed.