Require Import ssreflect.
Require Import ssrbool.
Require Import ssrfun.
Require Import ssrnat.

Lemma trivial_qoc : forall A : Prop, A -> A.
Proof.
intros A x.
exact x.
Qed.
Print trivial_qoc.

Lemma trivial_ssr : forall A : Prop, A -> A.
Proof.
by move=> A x.
Qed.

Lemma trivial_ssr_auto : forall A : Prop, A -> A.
Proof.
by done.
Qed.

Lemma trivial_have : forall A : Prop, A -> A.
Proof.
have y: forall B : Prop, B -> B by trivial.
have z: forall C : Prop, C -> C by move=> A x; exact x.
by exact y.
Qed.

Lemma move_around : forall A B C : Prop, A -> B -> (A -> B -> C) -> C.
move=> A B C x y.
move: y x.
move: A B C => D E F.
move=> k l m.
move: l k.
exact m.
Qed.

Lemma intro_pattern : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
move=> A B C [x | [_ y]] z //.
by move: x.
Qed.

Lemma annom : forall A B : Prop, B -> (A -> A) -> (B -> B) -> A -> B.
move=> A B x *.
by exact x.
Qed.

Lemma two : forall A B C D : Prop, False -> A /\ B /\ C /\ (A -> B -> C -> D) -> D /\ A.
Proof.
move=> A B C D _ [x [y [z i]]].
(* split=> //. *)
split; last by apply x.
apply i. 
Focus 2.
by exact y.
by exact x.
by apply z.
Qed.

Lemma bool_prop : forall b1 b2 : bool, (b1 && b2) ==> (b2 && b1).
move=> b1 b2.
apply/implyP.
case/andP.
move=> x y.
apply/andP.
split. 
- by exact y.
- by exact x.
Qed.

Lemma bool_classic : forall b : bool, b || ~~b = true.
by case.
Qed.

Lemma excluded_middle_unprovable : forall P : Prop, P \/ ~P.
move=> p.
Admitted.

Lemma double_negation : forall P : Prop, ~ ~P -> P.
move=> P x.
by elim (excluded_middle_unprovable P).
Qed.

Lemma by_fails : forall P : Prop, P.
by move=> p.