(** * Propositions
In Coq the type of propositions is [Prop]. We declare three
arbitrary objects of this type. *)
Variable P:Prop.
Variable Q:Prop.
Variable R:Prop.
(** The [Check] query can be used to check that expressions make
sense, and see their type. The next queries show Coq notations
for disjunction, conjunction and implication. *)
Check True.
Check P \/ Q.
Check False /\ P.
Check P -> Q -> R.
(** * Commutativity of conjunction.
Here we declare an unnamed goal, and prove it.
A proof is a succession of tactics, each tactic reducing
the first subgoal to a new (possibly empty) list of subgoals.
Bullets [+] can be used to identify the branching points
in a proof. Other possible bullets are [*], [-], [**], [+++], etc.
If a bullet is used for a subgoal, the same bullet must be used
for all other subgoals of the same level. *)
Goal P/\Q -> Q/\P.
Proof.
intro.
destruct H.
split.
+ exact H0.
+ exact H.
Qed.
(** * Commutativity of disjunction. *)
Goal P\/Q -> Q\/P.
Proof.
intro.
destruct H.
+ right. exact H.
+ left. exact H.
Qed.
(** * Distributivity
Solve these exercises using the tactics shown above. *)
Goal P/\(Q\/R) -> (P/\Q)\/(P/\R).
Proof.
Admitted.
Goal (P/\Q)\/(P/\R) -> P/\(Q\/R).
Proof.
Admitted.
(** * A form of commutativity for implication.
Two things to note here:
- the associativity of implication;
- the [intros] variant of [intro]. *)
Goal (P->Q->R) -> (Q->P->R).
Proof.
intros H HQ HP.
apply H.
+ exact HP.
+ exact HQ.
Qed.
(** * Multiple hypotheses
Prove the following equivalence, keeping in mind that
[P<->Q] is a shorthand for [(P->Q)/\(Q->P)].
In Coq, one generally writes [P->Q->R] rather than [P/\Q -> R],
since the first form is easier to work with using the provided
tactics. *)
Goal (P -> Q -> R) <-> (P /\ Q -> R).
Proof.
Admitted.
(** * Negation
Negation [~P] is just a shorthand for [P->False]. *)
Goal P -> ~~P.
Proof.
intros H Hn.
apply Hn.
exact H.
Qed.
Goal (~P /\ ~Q) -> ~(P \/ Q).
Proof.
Admitted.
Goal ~(P \/ Q) -> (~P /\ ~Q).
Proof.
Admitted.
Goal (~P \/ ~Q) -> ~(P /\ Q).
Proof.
Admitted.
(** * Classical reasoning
Coq implements a constructive logic. For classical
reasoning, one needs to declare an axiom. [RAA] stands
for Reductio Ad Absurdum.
These goals are a bit more difficult. *)
Axiom RAA : forall A:Prop, ~~A -> A.
Goal ~(P /\ Q) -> (~P \/ ~Q).
Proof.
Admitted.
(** [LEM] stands for Law of Excluded Middle. *)
Lemma LEM : P \/ ~P.
Proof.
Admitted.
Goal (P->Q) \/ (Q->P).
Proof.
Admitted.