Variables A B C D: Prop.
(* negation (logical not) is written with "~"
~A is an abbreviation for A->False,
use "unfold not" to unfold it *)
Goal A -> ~(~A).
Proof.
unfold not.
(* TODO: proof with just intro(s) and apply *)
Admitted.
Goal ~(~A /\ A).
Admitted. (* TODO *)
Goal ~A /\ ~B <-> ~(A \/ B).
Admitted. (* TODO *)
Goal ~A \/ ~B -> ~(A /\ B).
Admitted. (* TODO *)
Goal False -> A.
(* HINT: the tactic [destruct] makes it possible to exploit
conjunctions, disjunctions, but also false assumptions *)
Admitted.
Goal (forall P, P\/~P) <-> (forall P, ~~P -> P).
Proof.
split; intros H P.
Admitted. (* TODO, difficult !!! *)
Axiom nn: forall P, ~~P -> P.
Goal ~(A /\ B) -> ~A \/ ~B.
Admitted. (* TODO, difficult, use [apply nn] at some point *)
Goal ((A -> B) -> A) -> A.
Admitted. (* TODO, idem *)