(* Require part *)
Require Import ssreflect eqtype ssrbool.

(* some magic settings *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Checking *)

Check True.
Check False.
Check 3.
Check (3+4).
Check (3=5).
Check (3,4).
Check ((3=5)/\True).
Check nat -> Prop.
Check (3,3=5): nat * Prop.
Check (fun x:nat => x = 3).
Check (forall x:nat, x < 3 \/(exists y:nat, x = y + 3)).

Locate "_ && _".

About and.

Check (and True False).

Section simple_proofs.
(* Using only move apply  by *)

Variables P Q R S : Prop.

Lemma id_P : P -> P.

 Lemma id_PP : (P -> P) -> P -> P.

Lemma imp_trans : (P -> Q) -> (Q -> R) -> P -> R.

Lemma imp_perm : (P -> Q -> R) -> Q -> P -> R.

Lemma ignore_Q : (P -> R) -> P -> Q -> R.

Lemma delta_imp : (P -> P -> Q) -> P -> Q.

Lemma delta_impR : (P -> Q) -> P -> P -> Q.

Lemma diamond : (P -> Q) -> (P -> R) -> (Q -> R -> S) -> P -> S.

Lemma weak_peirce : ((((P -> Q) -> P) -> P) -> Q) -> Q.

Check diamond.
End simple_proofs.

Check diamond.

Section haveex.

Variables P Q R T : Prop.
Hypothesis H : P -> Q.
Hypothesis H0 : Q -> R.
Hypothesis H1 : (P -> R) -> T -> Q.
Hypothesis H2 : (P -> R) -> T.

Lemma Q0 : Q.

Lemma Q1 : Q.

 Print Q0.

 Print Q1.

End haveex.

(* Using also case rewrite *)

Section boolex.

(*                  a && b == the boolean conjunction of a and b.             *)
(*                  a || b == then boolean disjunction of a and b.            *)
(*                 a ==> b == the boolean implication of b by a.              *)
(*                    ~~ a == the boolean negation of a.                      *)
(*                 a (+) b == the boolean exclusive or (or sum) of a and b.   *)


Theorem bool_xor_not_eq :
forall b1 b2,  (b1 (+) b2) = ~~(b1 == b2).

Theorem bool_not_and :
 forall b1 b2:bool,
   ~~ (b1 && b2) = ~~ b1 || ~~ b2.

Theorem bool_not_not (b:bool): ~~ (~~ b) = b.

Theorem bool_ex_middle : forall b:bool,  b || (~~ b) = true.

Theorem bool_eq_reflect : forall b1 b2:bool, (b1 == b2) = true -> b1 = b2.

Theorem bool_eq_reflect2 : forall b1 b2:bool, b1 = b2 ->  (b1 == b2) = true.

Theorem bool_not_or :
 forall b1 b2:bool,
   ~~ ( b1 || b2) =  (~~ b1) && (~~ b2).

Theorem bool_distr :
 forall b1 b2 b3:bool,
    (b1 && b3) ||(b2 && b3) =  (b1 || b2) && b3.

End boolex.

(* Mixing Prop and bool *)
(* Set Printing Coercions. *)
Section bool_prop.

Check (forall (a b : bool), a -> b).
Notation "x 'is_true'" := (is_true x) (at level 8).
Check (forall (a b : bool), a is_true ->  b is_true).
Lemma Andb_idl (a b : bool) : (b is_true -> a is_true ) -> a && b = b.

Lemma Andb_idr (a b :bool) : (a is_true-> b is_true) -> a && b = a.

Lemma Andb_id2l (a b c : bool) : (a -> b = c) -> a && b = a && c.

End bool_prop.

Section more_prop.

Lemma and_imp_dist : forall A B C D:Prop,
                     (A -> B) /\ (C -> D) -> A /\ C -> B /\ D.

Lemma not_contrad : forall A : Prop, ~(A /\ ~A).

Lemma or_and_not : forall A B : Prop, (A \/ B) /\ ~A -> B.

Lemma or_imp_dist : forall A B C D:Prop,
                     (A -> B) \/ (C -> D) -> A /\ C -> B \/ D.

Section more_prop.