Require Import natbool.
Require Import poly.
Require Import logic.
Require Import util.

(** * Tactics

Recall that in Coq, a proof is represented by a term of its internal
programming language. A proposition is represented by a type, and the
correctness of a proof is verified by checking that a term has the
declared type.

Ultimately, then, proving in Coq is just a matter of programming: in
principle, we could do all our proofs by just writing out a proposition
as a type, and then writing a term with that type.

However, this tends to be impractical in the real world. Firstly, in
order to be able to express complex propositions, Coq's type system is
very complicated. This makes writing larger terms with it is very
difficult. Second, many of proofs (or parts of proofs) are conceptually
trivial, but still require lots of tedious code.

To make proof development more feasible, Coq provides a way to construct
proofs interactively using _tactics_, which are semi-automatic
directions for filling out parts of a proof. A _proof script_ is a
list of tactics, which Coq executes to create a complete proof term.

The standard style of proof scripts in Coq resembles the transcript of
commands issued in a text adventure game. Every command makes sense in
the context it is given in, and once you have solved the game, you can
replay the script to solve the game again quickly. However, when read by
itself, the list of commands makes no sense.

We are not interested only in creating formal proofs by any means
available. We are also interested in understanding general proof
techniques and the relationship between informal and formal proofs. Thus
we would like our proof scripts to read more like stories, with enough
context to help the reader make sense of the structure of the proof.
Ideally our proofs or proof scripts will look just like informal proofs,
only formulated precisely enough that even a mechanical proof checker
can verify their correctness.

With this goal in mind, we shall diverge a little from Coq's standard
tactics, and use some custom tactics that make the proof script more
legible, although it also makes them a bit more verbose.


** Proving equality by definition: [reflexivity]

The primitive notion of equality in Coq is _convertibility_: roughly,
two terms are convertible if they evaluate to the same term. This
technical notion captures the idea of equality _by definition_.

Verifying the convertibility of terms is an essential part of type
checking: if Coq thinks that a term [t] has type [T1], but type [T2] is
expected, then type checking succeeds only if [T1] and [T2] are
convertible.

The equality relation in Coq captures the notion of convertibility.
Consider the only constructor of the [eq] type, [refl_equal]: *)

Check refl_equal.

(** Note that the type of the resulting equality proof is always [a =
a], for some [a]. So if [a] and [b] are convertible, [a = b] can be
proven with [refl_equal]. The idiomatic way to do this in a proof script
is to use the [reflexivity] tactic. *)

Lemma two_plus_two_equals_four : 2 + 2 = 4.
Proof.
  reflexivity.
Qed.

(** This is our first example of a proof script. Firstly, we use the
[Lemma] command to declare the name of the proof and its type, i.e. the
proposition want to prove. This is for the most part similar to a
[Definition], except that we don't give a body of the definition, but
instead develop the proof with a script, which is delimited with [Proof]
and [Qed]. Coq accepts [Qed] only after it announces that the proof has
been completed.

While in the middle of interpreting a proof script, Coq shows us the
current _goal_, i.e. the proposition that we currently need to solve.
In the example, the proof script consists only of a single use of the
[reflexivity] tactic, which solves the goal, since [2 + 2] is
convertible with [4].

We can use [reflexivity] to prove many other trivial equalities that are
true by definition: *)

Lemma six_perfect : 1 + 2 + 3 = 1 * 2 * 3.
Proof.
  reflexivity.
Qed.

Lemma evenb_three_is_false : evenb 3 = false.
Proof.
  reflexivity.
Qed.

(** Reflexivity proofs on concrete terms like these are mostly useful
for checking that the functions that we have defined behave as we would
expect. But to get more interesting results, we need to be able to
generalize.


** Proving implications and universals: [assume] (and [intros])

Recall that a term of type [A -> B] is a function, and such functions
can be constructed with terms of the form [fun a : A => b], where [a] is
a parameter of type [A] and [b] is a term of type [B], which may be
constructed with the use of [a]. This corresponds to the standard
introduction rule of implication, which says that [A -> B] can be proven
if [B] can be proven from a hypothesis [A].

Recall also that [forall a : A, B] is exactly the same as [A -> B],
except that [a] may appear inside [B].

In a tactic script, we often prove implications and universal
quantifications by introducing the parameter as a hypothesis, and then
proving the conclusion. We do this with the custom [assume] tactic:
*)

Lemma plus_0_l : forall n : nat, 0 + n = n.
Proof.
  assume n : nat.
  reflexivity.
Qed.

(** Here the [assume] begins the proof of a universally quantified
sentence "for all natural numbers [n]" by giving a name to the arbitrary
natural number (here [n]) and verifying that it has the type we expect.
After this, [n] is in our current _context_ and can be used like any
other variable.

We can then prove [0 + n = n] again by reflexivity. Note that even
though we cannot compute the _value_ of [n], [0 + n] and [n] are
still convertible, because [plus O n] always evaluates to [n], i.e. [0 +
n] is _by definition_ [n]. On the other hand, what [plus n O]
evaluates to depends on [n], so proving it is somewhat more complicated.

Coq's standard tactic for introductions is called [intros], which is
similar, but doesn't allow us to give the type of the introduced
variable explicitly. We use a custom [assume] tactic which allows this
in order to make the scripts more readable.


** Finishing proofs: [prove]

We now introduce a little bit of extra syntax for structuring the
proofs. Later on we shall have proof scripts with a number of subgoals,
each of which gets proven separately by a proof script fragment. To
better keep track of where the proof of a goal is finished, we adopt the
convention that we use [prove] to indicate a _terminating_ tactic.
The general syntax is [prove goal using tactic] where [goal] is an
optional annotation to let us write down the current goal to make the
script more legible, and [tactic] is the tactic which we expect to
prove the goal.

Here is another simple proof using the new convention: *)

Lemma mult_0_l : forall n : nat, 0 * n = 0.
Proof.
  assume n : nat.
  prove (0 * n = 0) using reflexivity.
Qed.

(** ** Rewriting terms: [rewrite]

Recall that one way of viewing an equality [a = b] is to say that in any
context, [a] can be substituted by [b]. At the level of proof scripts,
this principle can be used with the [rewrite] tactic. If we have a
hypothesis [H] of the form [a = b], then we can use it to replace [a]
with [b] in the goal or in some other hypothesis. The syntax for this is
[rewrite -> H] or [rewrite <- H] depending on whether we wish to replace
[a] with [b] or the other way around.

Here is an example of rewriting in use. *)

Lemma pred_S_example : forall n m : nat, n = S m -> pred n = m.
  assume n m : nat.
  assume H : (n = S m).
  rewrite -> H.
  prove (pred (S m) = m) using reflexivity.
Qed.

(** ** Case analysis: [per cases]

So far all of our proofs have been uniform in the sense that the
structure of the proof is not dependent on exact form of an introduced
variable: [0 + n = n] by definition, regardless of whether [n] is [0] or
some other number.

However, often it happens that we can prove some property [P x] for any
[x], but the way it is proven depends on [x]. In this case, we need to
do _case analysis_ on x, and give a different proof for each case.
Remember that proof scripts ultimately generate proof terms, which are
just programs. At that level, case analysis corresponds to simple
pattern matching on [x], with a different proof term et each branch of
the match expression.

A common situation where case analysis on [x] is needed is when we are
interested in [f x], where [f] is some function that performs pattern
matching on [x]. In this situation, if we want to know anything about
the result of [f x], we must know enough about the structure of [x] to
know which branch the pattern matching in [f] will take.

As the simplest example, let's consider the proposition [forall b :
bool, negb (negb b) = b]. We know that [b] must be one of [true] and
[false]. If it is [true], then, by definition, [negb (negb b)] evaluates
to [negb false] and ultimately [true]. Similarly, if it is [false],
[negb (negb b)] evaluates to [negb true] and [false]. The following
proof script formalizes the above reasoning. *)

Lemma negb_involutive : forall b : bool, negb (negb b) = b.
Proof.
  assume b : bool.
  per cases on b.
    suppose it is true.
      prove (negb (negb true) = true) using reflexivity.
    suppose it is false.
      prove (negb (negb false) = false) using reflexivity.
Qed.

(** _NOTE: THIS TACTIC DOESN'T WORK WITH MORE COMPLICATED
INDUCTIVE DEFINITIONS. USE THE STANDARD [destruct] TACTIC INSTEAD._

Coq's standard tactics make it hard to see which case we are
handling at which time, so we use a custom tactic [per cases], which
attempts to simulate the pattern matching syntax and hopefully makes the
structure of the proof clearer.

The [per cases on b] generates two _subgoals_, one for each
constructor of [bool]. In each subgoal, [b] has been replaced by a
concrete value of type [bool]. The goals must be proven in the order
that the constructors were declared in the definition of the inductive
type. In this case, first [true], then [false].

The custom tactic does some mystical things to the context and the goal
for its internal bookkeeping purposes. The only legal thing to do after
a [per cases] tactic is to use [suppose it is] to begin handling a new
case. The [suppose] tactic checks that we truly are handling the
declared case. Once the subgoal has been proven, handling the next case
must again be started with a [suppose] declaration.

The [bool] type is extraordinarily simple in that none of its
constructors take arguments. More commonly, a constructor takes
arguments, and by pattern matching we only get to know that e.g. some
number [n] is actually the successor [S m] of _some_ other number
[m]. The [suppose] syntax supports a primitive form of pattern matching
and allows us to bind a variable to the number than [n] is a successor
of.

Here is a simple example: *)

Lemma plus_1_neq_0 : forall n, beq_nat (n + 1) 0 = false.
Proof.
assume n : nat.
per cases on n.
  suppose it is O.
    prove (beq_nat (0 + 1) 0 = false) using reflexivity.
  suppose it is (S m).
    prove (beq_nat (S m + 1) 0 = false) using reflexivity.
Qed.

(** Why do we need separate cases here, although we are just using
reflexivity in each case? The reason is that in order for us to show
that [beq_nat (n + 1) 0] evaluates to [false], we must first show that
[n + 1] evaluates to [S n'], for some [n']. It does so, but the reason
it does so depends on the value of [n]. If [n] is [0], then [n + 1]
evaluates to [1], i.e. [S O], the latter argument. If [n] is [S m], then
[n + 1] evaluates to [S (m + 1)]. So we must consider each case
separately to verify this.


** Conversions: [change]

Sometimes we need to explicitly change the goal or some hypothesis
into a convertible but syntactically different form. We may want to do
this simply because we think the new form is clearer or more relevant
to the proof, or in order to expose a subterm which can then be
substituted by another with [rewrite].

The [change] tactic performs this. The goal is converted with [change
goal] where [goal] should be convertible with the current goal. A
hypothesis can be converted with [change term in hyp] where
[hyp] is some current hypothesis whose type is convertible with
[term].

Here is an example of its use: *)

Lemma foo : forall m n, m * m = n -> (1 + m) * m = m + n.
  assume m n : nat.
  assume H : (m * m = n).
  change (S m * m = m + n).
  change (m + (m * m) = m + n).
  rewrite -> H.
  prove (m + n = m + n) using reflexivity.
Qed.

(** Here the first [change] is included only for illustration and
could be left out. However, the second [change] is crucial: it
converts the goal into a form where [m * m] appears, and only then can
we use [rewrite] to substitute it with [n].

There are also tactics for performing conversion steps without
specifying beforehand the desired result form. These include [red],
[simpl] and [unfold]. Such tactics are good for investigating what a
goal or hypothesis is convertible to, but in a final proof script
these tactics are uninformative to the reader, so [change], which is
accompanied with the desired result, should often be preferred.


** Induction

Induction is the logical counterpart of the kind of recursion that Coq
supports. Recall that in Coq, a recursive function [f] on natural
numbers practically must be designed so that:

 - we specify directly what [f O] returns
 - we specify what [f (S m)] returns from the value that [f m] returns

When we think of the function [f] as a proof that for each [n] some
property [P n] holds, the above principle gets the following
interpretation:

 - we prove directly that [P O] holds
 - we prove that [P (S m)] holds from the assumption that [P m] holds

This is the induction principle for natural numbers.

Proving by induction in Coq is very much like proving by cases, except
that in an inductive case (for natural numbers, the [S m]-case) we
also get and _inductive hypothesis_ stating that the proposition we
are trying to prove for [S m] already holds for [m].

_NOTE: THIS TACTIC DOESN'T WORK WITH MORE COMPLICATED INDUCTIVE
DEFINITIONS. USE THE STANDARD [induction] TACTIC INSTEAD._

We use a custom tactic similar to [per cases], but it is now called
[per induction]. The inductive hypothesis can be introduced with the
[assume] tactic.

Here is a proof that [0] is the right identity of [plus]. Note that we
also make use of a conversion with [change] in order to be able to use
the inductive hypothesis in rewriting. *)

Lemma plus_0_r : forall n, n + 0 = n.
Proof.
  assume n : nat.
  per induction on n.
    suppose it is O.
      prove (0 + 0 = 0) using reflexivity.
    suppose it is (S m).
      assume H : (m + 0 = m).
      change (S (m + 0) = S m).
      rewrite -> H.
      prove (S m = S m) using reflexivity.
Qed.

(** **)