# Library propositional

# 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.

# 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.

# 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.

# Negation

Negation

¬P is just a shorthand for

P→False.

# 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.

LEM stands for Law of Excluded Middle.