Library CSEnotes_propositional

Back to Coq Main Page

Proving Propositional Tautologies

Date: 2020-01-02. Tested with Coq version 8.8.1.
The following examples are based on the Class Notes from SUNY Buffalo CSE 191 "Discrete Structures", Pages 12-20. This document adds different comments to these Coq examples.

Introduction

Definition: Boolean expressions that always take value True regardless of the truth values of their variables are called tautologies. Tautologies in logic are much like identities in algebra (formulas for (a+b)2=a2+2ab+b2 and many others). They can be used to substitute all kinds of subexpressions in order to get results that are always true.
Naive Algorithm: Check, if a Boolean Expression is a tautology by computing its truth table. If the truth table always shows value "true", then it is a tautology.

Using this algorithm can be inefficient. If there are n variables in a Boolean expression, the truth table has 2n rows. Once we start proving statements about infinite sets (such as natural or integer numbers), truth tables are impossible to use, since there are infinitely many values that one can substitute in the formulas.

Therefore logic usually uses other methods of proof, based on symbolic manipulation of languages.

Proving tautologies in Coq


Variables P Q R S : Prop.

Lemma id_P : P->P.
Proof.
  intros pTrue.   exact pTrue.
Qed.

Universal Quantifier

Declaring constant propositions (with "Variables" as we just did) is unnecessary, since we handle universal logical truths that should not depend on specific variable notation. In algebra
Can we write a Boolean formula (tautology or any other) without using specific variable symbols? In the high-school algebra the formula for (a+b)2 is identical to the formula for (x+y)2 or even (a+17)2.
For this reason we want to "bind" the variables in the formula using "universal quantifier". We tell that the variable notation does not matter; the tautology would still hold, if you replace p,q,r with different letters of subexpressions.

Lemma id_P_same: forall p:Prop, p -> p.
Proof.
  intros p.
  intros pTrue.
  exact pTrue.
Qed.

Lemma imp_trans: forall p q r: Prop, (p->q)->(q->r)->p->r.
Proof.
  intros p q r.
  intros pIMPLq.
  intros qIMPLr.
  intros pTrue.
  apply qIMPLr.
  apply pIMPLq.
  exact pTrue.
Qed.

For conjunctions there are other tactics used to handle hypotheses and goals. If you have a conjunction in a hypothesis, you can use tactic destruct to break the hypothesis into two hypotheses. If you have a conjunction in the goal, you can use tactic split to get two subgoals (need to prove both).

Lemma and_comm: forall p q: Prop, (p /\ q) -> (q /\ p).
Proof.
  intros p q.
  intros H.
  destruct H as [pTrue qTrue].
  split.
  exact qTrue.
  exact pTrue.
Qed.

This command prints the most recent proof:

Show Script.

For disjunctions in hypothesis you can destruct it into two subcases. Unlike conjunctions, you need to use either one of the parts or the other. If you have disjunction in the goal, you can use tactics left and right - to pick, which part of the disjunction you want to prove.

Lemma or_comm: forall p q: Prop, (p \/ q) -> (q \/ p).
Proof.
  intros p q.
  intros H.
  destruct H as [pTrue | qTrue].
  right; exact pTrue.
  left; exact qTrue.
Qed.

The tactic "destruct" can be expressed in more detail as explained in Coq documentation.

Lemma or_commutative : forall a b: Prop, a \/ b -> b \/ a.
Proof.
  intros A B H.
  elim H.
  intro HA.
  clear H.
  right.
  exact HA.
  intro HB.
  left.
  exact HB.
Qed.

This is small and trivial example shows that you can combine conjunctions and disjunctions. It tells that whenever "p AND q" are both true, then "p OR r" is also true, since we can use hypothesis pTrue stating that p is true regardless of what is r. In order to do that we first destruct the original hypothesis (into two hypotheses pTrue and qTrue) and then take just the left part of p \/ r.

Lemma prob3a : forall p q r: Prop, (p /\ q) -> (p \/ r).
Proof.
  intros p q r.
  intros H.
  destruct H as [pTrue qTrue].
  left; exact pTrue.
Qed.

Lemma prob3b : forall p r: Prop, p->(r->p).
Proof.
  intros p r.
  intros H1 H2.
  exact H1.
Qed.