(*|
=============
Week 1: Intro
=============

Author
  Nate Foster.
License
  No redistribution allowed.

.. contents::

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)`:
|*)

Theorem T1 : forall (A: Prop), A -> A.
Proof. (* .unfold *)

(*|
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.
|*)

  intros. (* .unfold *)

(*|
Notice that the newly created hypothesis was given a name automatically (:mquote:`.s(intros).h{A}.name`).

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:
|*)

Theorem T2 : forall (A B : Prop), A /\ B -> B /\ A.
Proof.
  intros A B HAB. (* .unfold *)

(*|
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`:
|*)

  destruct HAB as [HA HB].

(*|
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`?
|*)

Check conj. (* .unfold *)
Print conj. (* .unfold *)

(*|
`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:
|*)

Print T2. (* .unfold *)

(*|
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:
|*)

Print True. (* .unfold *)
Print False. (* .unfold *)

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

Goal True -> True.
Proof.
  intros HT. (* .unfold *)
  destruct HT. (* .unfold *)
  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.
|*)

Theorem T3 : forall (A: Prop), False -> A.
Proof.
  intros A HF. (* .unfold *)
  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:
|*)

Theorem T3' : forall (A: Prop), not True -> A.
Proof.
  intros A HnotT.
  destruct HnotT. (* .unfold *)
  apply I.
Qed.

(*|
What happened?  `destruct` peeked into the definition of `not`:
|*)

Print not. (* .unfold *)

(*|
Bools and props
===============

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

.. coq:: unfold
|*)

Theorem T4 : forall (A: Prop), ~(A /\ ~A).
Proof.
  unfold not.
  intros A H.
  destruct H as [H1 H2].
  apply H2.
  apply H1.
Qed.

(*|
And here is now a suspiciously similar-looking theorem, on Booleans:
|*)

Theorem T5 (b: bool) : negb (andb b (negb b)) = true.
Proof.
  destruct b.
  reflexivity.
  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:
|*)

Check true = true. (* .unfold *)

(*|
So is `true = false`:
|*)

Definition bool_bogus : Prop := true = false.

(*|
Thankfully, while `true = true` *is* provable, `true = false` is not:
|*)

Theorem bool_bogus_proof_attempt : bool_bogus.
Proof.
  unfold bool_bogus. (* .unfold *)
  (* No way to make progress. *)
Abort.

(*|
On the other hand, the *negation* of `bool_bogus` is provable:
|*)

Theorem not_bool_bogus_proof : not (bool_bogus).
Proof.
  unfold not, bool_bogus. (* .unfold *)
  intros Heq.             (* .unfold *)
  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:

-
   `neg`:
|*)

Lemma bool_to_prop_neg (b: bool) :
  bool_to_prop (negb b) = ~(bool_to_prop b).
Proof.
  unfold bool_to_prop.
  apply prop_ext.
  split.
  - destruct b.
    discriminate.
    discriminate.
  - destruct b.
    + intros H.
      destruct H.
      reflexivity.
    + reflexivity.
Qed.

(*|
-
   `and`:
|*)

Lemma bool_to_prop_and (b1 b2: bool) :
  bool_to_prop (andb b1 b2) = (bool_to_prop b1 /\ bool_to_prop b2).
Proof.
  apply prop_ext.
  split.
  - destruct b1, b2.
    + split. reflexivity. reflexivity.
    + discriminate.
    + discriminate.
    + discriminate.
  - destruct b1, b2.
    + reflexivity.
    + intros [H1 H2]. discriminate.
    + intros [H1 H2]. discriminate.
    + intros [H1 H2]. discriminate.
Qed.

Theorem T5a (b: bool) : bool_to_prop (negb (andb b (negb b))).
Proof.
  rewrite bool_to_prop_neg. (* .unfold *)
  rewrite bool_to_prop_and. (* .unfold *)
  rewrite bool_to_prop_neg. (* .unfold *)
  apply (T4 (bool_to_prop b)).
Qed.