Systems and
Formalisms Lab

Week 1: Intro

Author

Nate Foster.

License

No redistribution allowed.

Propositional logic

Let's explore more proofs. This one states a tautology: “if A, then A”. We encode if as an implication, written ->, and we quantify over all possible propositions A by writing forall (A: Prop):

forall A : Prop, A -> A


forall A : Prop, A -> A

Goals in Coq have two parts: the context (or hypotheses) and the conclusion. A horizontal bar separates them; on paper, we would use a turnstile (⊢) instead.

The intros tactic changes ⊢ A -> A to A ⊢ A, which visually means moving A above the bar.

  
A: Prop
H: A
A

Notice that the newly created hypothesis was given a name automatically (H).

The apply tactic is the modus ponens rule: it takes a term or a hypothesis of the form A -> B, and changes the conclusion from B to A. In the simplest case, where the hypothesis is simply A, and the conclusion is A as well, apply solves the goal entirely:

  apply H.
Qed.

Proofs that rely on automatically generated names can be brittle. Thankfully, the intros tactic can name the hypotheses it creates. For example:

forall A B : Prop, A /\ B -> B /\ A


forall A B : Prop, A /\ B -> B /\ A

  
A, B: Prop
HAB: A /\ B
B /\ A

The destruct tactic performs case analysis on its argument, and gives names to each part. Here, we use it to name each side of HAB:

  
A, B: Prop
HA: A
HB: B
B /\ A

This proof can be completed by explicitly construction a proof of B /\ A from the two terms HB and HA:

  apply (conj HB HA).
Qed.

But what is conj?

conj
     : forall A B : Prop, A -> B -> A /\ B


Inductive and (A B : Prop) : Prop :=
    conj : A -> B -> A /\ B.

Arguments and (A B)%type_scope
Arguments conj [A B]%type_scope _ _

conj is the name of the single constructor of the type and! So our proof is really just unpacking a conj (that's the first destruct), then repacking it (the apply). Print shows us as much:

T2 =
fun (A B : Prop) (HAB : A /\ B) =>
match HAB with
| conj x x0 =>
    (fun (HA : A) (HB : B) => conj HB HA) x x0
end
     : forall A B : Prop, A /\ B -> B /\ A

Arguments T2 (A B)%type_scope _

If /\ is in fact a type, then are True and False also types? Indeed yes! True has a single constructor, called I, and False, thankfully, has none:

Inductive True : Prop :=  I : True.


Inductive False : Prop :=  .

What happens if we call destruct on a term of type True? No much, since it carries no information and no subterms:

True -> True


True -> True

  
HT: True
True

  
True

  apply I.
Qed.

What about False? Having a term of type False is impossible, since False has no constructors. Consequently, a case analysis yields… 0 cases, and a proof.

forall A : Prop, False -> A


forall A : Prop, False -> A

  
A: Prop
HF: False
A

  destruct HF.
Qed.

Some Coq tactics are rather smart. For example, destruct, when applied to a term of type X -> Y, first creates a new goal for X, then performs destruct on the specialization of the original term. Here is this behavior in action:

forall A : Prop, ~ True -> A


forall A : Prop, ~ True -> A

  
A: Prop
HnotT: ~ True
A

  
A: Prop
True

  apply I.
Qed.

What happened? destruct peeked into the definition of not:

not = fun A : Prop => A -> False
     : Prop -> Prop

Arguments not A%type_scope

Bools and props

Here is a theorem, and its proof, on propositions:

forall A : Prop, ~ (A /\ ~ A)


forall A : Prop, ~ (A /\ ~ A)

  
forall A : Prop, A /\ (A -> False) -> False

  
A: Prop
H: A /\ (A -> False)
False

  
A: Prop
H1: A
H2: A -> False
False

  
A: Prop
H1: A
H2: A -> False
A

  apply H1.
Qed.

And here is now a suspiciously similar-looking theorem, on Booleans:

b: bool
negb (b && negb b) = true


b: bool
negb (b && negb b) = true

  
negb (true && negb true) = true
negb (false && negb false) = true

  
negb (false && negb false) = true

  reflexivity.
Qed.

Booleans are not the same, in Coq, as propositions: booleans are a simple two-valued type, whereas Prop is a kind (a type of types). One way to relate the two is to use equality: true = true, for example, is a proposition:

true = true
     : Prop

So is true = false:

Definition bool_bogus : Prop := true = false.

Thankfully, while true = true is provable, true = false is not:

bool_bogus


bool_bogus

  
true = false

  (* No way to make progress. *)
Abort.

On the other hand, the negation of bool_bogus is provable:

~ bool_bogus


~ bool_bogus

  
true = false -> False

  
Heq: true = false
False

  discriminate Heq.
Qed.

Let's explore this bool/Prop connection further. Theorems T4 and T5 were very similar. Shouldn't we be able to reuse T4 to prove T5?

While it's not strictly necessary, the following axiom will help:

Axiom prop_ext : forall (P Q : Prop), (P <-> Q) -> P = Q.

We start with an injection from bool to Prop: bool_to_prop b is provable when b is equal to true.

Definition bool_to_prop (b: bool) : Prop := b = true.

We can use bool_to_prop to relate Prop and bool operators: