All natural deduction rules for propositional logic have been covered by now in the lectures. Let’s put them into practice.

Note

Code snippets can be copied by hovering over the snippet and clicking the button which appears on the top right.

Some snippets are declared as files—those can be downloaded directly by clicking the button next to the filename.

A quick word on sequents

In natural deduction, we have two broad kinds of proof rules for each propositional connective: introduction rules and elimination rules. Introduction rules explain how to build a connective from components. The introduction rules for ‘and’ and ‘or’ are:

\[\begin{aligned} \frac{A \quad B}{A \wedge B}{{\wedge}_{\mathcal{I}}} \qquad \frac{A}{A \vee B}{{\vee}_{\mathcal{I}_1}} \quad \frac{B}{A \vee B}{{\vee}_{\mathcal{I}_2}} \end{aligned}\]

Elimination rules, on the other hand, explain how to use the connective. The elimination rules for ‘and’ and ‘or’ are:

\[\begin{aligned} \frac{A \wedge B}{A}{\wedge_{\mathcal{E}_1}} \quad \frac{A \wedge B}{B}{\wedge_{\mathcal{E}_2}} \end{aligned}\]
\[\begin{aligned} \frac{A \vee B \quad \fbox{Suppose $A$ … $C$} \quad \fbox{Suppose $B$ … $C$}}{C}{{\vee}_{\mathcal{E}}} \end{aligned}\]

You will recall these from your first-year course on discrete structures.

It is better to think of Coq tactics as not necessarily ‘introducing’ or ‘eliminating’ a connective, but as manipulating the proof state according to where the connective appears. A proof state in Coq is always represented by a sequent \(\Gamma \vdash \phi\), where \(\Gamma\) is a list of hypotheses (everything above the line in Coq), and \(\phi\) is the current goal (below the line).

The proof rules that manipulate sequents are very similar to natural deduction rules, but instead of being classified into ‘introduction’ and ‘elimination’ rules, they are classified into left and right rules. Left-rules apply when the connective appears as a hypothesis—that is, on the left-hand side of a sequent. Right-rules apply when the connective appears in the conclusion—that is, on the right-hand side of a sequent.

Proofs Involving ‘And’ and ‘Or’

As discussed in the previous section, the left-rules for ‘and’ and ‘or’ should explain what happens when they appear as a hypothesis.

If we have a hypothesis of the form \(A \wedge B\), the left-rule for ‘and’ says the following:

\[\begin{aligned} \frac{\Gamma, A \wedge B \vdash C}{\Gamma, A, B \vdash C} \end{aligned}\]

In plain English: if we know \(A \wedge B\), then we know \(A\), and we also know \(B\). It breaks apart the original hypothesis so that we can use \(A\) and \(B\) separately. Not very interesting.

More interesting are hypotheses of the form \(A \vee B\). The left-rule for ‘or’ is as follows:

\[\begin{aligned} \frac{\Gamma, A \vee B \vdash C}{\Gamma, A \vdash C \qquad \Gamma, B \vdash C} \end{aligned}\]

In plain English: if we can prove \(C\) using \(A \vee B\), then we should be able to prove \(C\) from \(A\) only, and we should be able to prove \(C\) from \(B\) only. The point is that if we claim that either \(A\) or \(B\) is sufficient to prove \(C\), then either one alone should be enough to prove \(C\).

The right-rules explain what happens when ‘and’ or ‘or’ appear in the goal, rather than in our hypotheses. The right-rule for conjunction is:

\[\begin{aligned} \frac{\Gamma \vdash A \wedge B}{\Gamma \vdash A \qquad \Gamma \vdash B} \end{aligned}\]

This says that, if we want to prove \(A \wedge B\), then we must prove \(A\) only, and then we must prove \(B\) only.

The right-rules for disjunction are:

\[\begin{aligned} \frac{\Gamma \vdash A \vee B}{\Gamma \vdash A} \qquad \frac{\Gamma \vdash A \vee B}{\Gamma \vdash B} \end{aligned}\]

This gives us two ways to prove \(A \vee B\): either we prove \(A\), or we prove \(B\). Either is fine.

How do we instruct Coq to apply these rules?

Proofs Involving Negation

Recall that \(\neg A\) in constructive propositional logic is really just a shorthand for \(A \to \bot\), which means that \(A\) implies a contradiction. In Coq, the false-by-definition proposition \(\bot\) is called False.

Since negation is shorthand for a special case of implication, you can use all the tactics from the first lab.

If you see a goal of the form ~A, you can reduce it to its definition A -> False with the tactic red—short for ‘reduce’—after which you can use intros. Alternatively, if you want to unfold all instances of negation, including in hypotheses, you can use unfold "~" in *. This can help you spot valid applications of the apply tactic.

Alternatively, note that intro will apply hnf to the goal until intro can actually be applied. Hence if the goal is ~A, intro will reduce it to A -> False and then pull A up as a hypothesis. Note that intros will not do this without red first.

Classical Logic

Coq’s logic is constructive. This means that the law of excluded middle is not an axiom and cannot be proved (or disproved) in Coq’s logic. If you want to reason classically, you must add LEMlaw of excluded middle as an axiom or hypothesis explicitly.

1
2
3
(* Pick only one of these options *)
Axiom LEM : forall P : Prop, P \/ ~P.
Hypothesis LEM : forall P : Prop, P \/ ~P.

When you know LEMlaw of excluded middle, you can always reason by case analysis. For example, if you write destruct (LEM A), the proof will split into two cases: one in which you know \(A\), and one in which you know \(\neg A\).

You will need LEMlaw of excluded middle for one of the final four questions on the De Morgan laws—but we’re not telling you which one. That’s something for you to figure out yourself.

Questions

Prove the following propositions in Coq. When you have completed the proof, replace Admitted with Qed. You can download the file by clicking the button next to the filename.

CoqLab02.v
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
Section CoqLab02.

Context (A B C : Prop).

(***************************************************)
(* And / Or *)

Lemma q1 : (A /\ B) /\ C -> A /\ (B /\ C).
Proof.
  (* todo *)
Admitted.

Lemma q2 : ((A /\ B) -> C) -> (A -> (B -> C)).
Proof.
  (* todo *)
Admitted.

Lemma q3 : (A \/ B) \/ C -> A \/ (B \/ C).
Proof.
  (* todo *)
Admitted.

Lemma q4 : ((A \/ B) -> C) -> (A -> (B -> C)).
Proof.
  (* todo *)
Admitted.

(***************************************************)
(* Negation *)

Lemma q5 : (~A \/ B) -> (A -> B).
Proof.
  (* todo *)
Admitted.

Lemma q6 : (A -> B) -> (~B -> ~A).
Proof.
  (* todo *)
Admitted.

Lemma q7 : ~(A /\ ~A).
Proof.
  (* todo *)
Admitted.

(***************************************************)
(* De Morgan’s Laws *)

Hypothesis LEM : forall P : Prop, P \/ ~P.

Lemma q8 : ~(A \/ B) -> ~A /\ ~B.
Proof.
  (* todo *)
Admitted.

Lemma q9 : ~A /\ ~B -> ~(A \/ B).
Proof.
  (* todo *)
Admitted.

Lemma q10 : ~A \/ ~B -> ~(A /\ B).
Proof.
  (* todo *)
Admitted.

Lemma q11 : ~(A /\ B) -> ~ A \/ ~ B.
Proof.
  (* todo *)
Admitted.

End CoqLab02.