# 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 PQ QP.
Proof.
intro.
destruct H.
split.
+ exact H0.
+ exact H.
Qed.

# Commutativity of disjunction.

Goal PQ QP.
Proof.
intro.
destruct H.
+ right. exact H.
+ left. exact H.
Qed.

# Distributivity

Solve these exercises using the tactics shown above.

Goal P/\(QR) (PQ)\/(PR).
Proof.

Goal (PQ)\/(PR) P/\(QR).
Proof.

# A form of commutativity for implication.

Two things to note here:
• the associativity of implication;
• the intros variant of intro.

Goal (PQR) (QPR).
Proof.
intros H HQ HP.
apply H.
+ exact HP.
+ exact HQ.
Qed.

# Multiple hypotheses

Prove the following equivalence, keeping in mind that PQ is a shorthand for (PQ)/\(QP).
In Coq, one generally writes PQR rather than PQ R, since the first form is easier to work with using the provided tactics.

Goal (P Q R) (P Q R).
Proof.

# Negation

Negation ¬P is just a shorthand for PFalse.

Goal P ~~P.
Proof.
intros H Hn.
apply Hn.
exact H.
Qed.

Goal (~P ¬Q) ~(P Q).
Proof.

Goal ~(P Q) (~P ¬Q).
Proof.

Goal (~P ¬Q) ~(P Q).
Proof.

# 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 : A:Prop, ~~A A.

Goal ~(P Q) (~P ¬Q).
Proof.