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.