Writing Proofs
Formulating Proofs
Can use Check
to check that formal statement is well-formed:
1 2 3 4 5 |
|
Should be a well-formed term of type Prop
for proposition.
Check does not check the provability of the statement
→ use keywords such as Lemma
(or Theorem
, Remark
, Corollary
, etc.) to express the start of a statement is going to be proved.
Use keyword Proof
to start proof text and end it with either Qed
or Admitted
.
1 2 |
|
Type annotation is not necessary if it can be inferred from the statement.
Use ->
for implication:
1 2 |
|
Proof by Simplification
- strategy for proving identities
- use
simpl
to simplify both sides of the equation - use
reflexivity
to check that both sides contain identical values - use
Theorem
which works the same as (@see:Example
) - note use of \(\forall\) i.e.
forall
to include all natural numbers intros
movesn
from goal to context of current assumptions- tactics - commands used between
Theorem
andQed
to guide the process of checking claim we are making e.g.intros
,simpl
,reflexivity
→ (@see: tactics)
Simple example
1 2 3 |
|
None: this example can be written without simpl
because reflexivity
performs
simplification automatically. Adding simpl
allows seeing intermediate state
→ use simpl
when interested in the new goal it creates.
More examples
1 2 3 4 5 6 7 8 9 |
|
Proof by Rewriting
Tactic called rewrite
replaces expression in the goal state
1 2 3 4 5 6 7 8 9 10 |
|
- writing
->
says: replace left side of the equality hypothesis H with the right side <-
used to replace in the opposite direction
1 2 3 4 5 6 7 8 |
|
Can use Check
to examine previously declared lemmas and theorems.
These are from and proven in the standard library:
1 2 3 4 5 |
|
- Can use
rewrite
with a previously proven theorem instead of hypothesis from context - if theorem involves quantified variables, Coq tries to instantiate them by matching with the current goal
1 2 3 4 5 6 7 |
|
Proof by Case Analysis
- sometimes must consider possible forms separately → simplification or rewrite is not an option
destruct
tactic says to consider cases separately
Simple examples
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
|
Introduction Pattern and Bullets
-
as [| n']
is an introduction pattern- tells Coq what variable names to use
- between square brackets: list of lists of names, separated by
|
- in example:
- first component is empty since the
O
constructor is nullary - second component gives a single name,
n'
, sinceS
is unary constructor
- first component is empty since the
-
In each subgoal, Coq remembers the assumption about n that is relevant for this subgoal → either
n = 0
orn = S n'
for somen'
. -
eqn:E
tells destruct to give the nameE
to this equation (optional)
Example: negation is its own inverse
1 2 3 4 5 6 7 8 |
|
-
signs before reflexivity are called bullets
- after a bullet is the entire proof for the corresponding subgoal
- in example: each of the subgoals is easily proved by reflexivity
- using bullets is optional but more readable if used
- can use other symbols (*
, +
, --
, ***
, etc.) or curly braces
Nested Destruct
Can invoke destruct
inside subgoal → use different bullets at different levels
1 2 3 4 5 6 7 8 9 10 |
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 |
|
Destruct Shorthand
Destructing after intros has a shorthand:
1 2 3 4 5 6 |
|
If there are no constructor arguments that need names, can just write []
to get the case analysis.
1 2 3 4 5 6 7 8 9 |
|
Proof by Induction
Goal - show that \(P(0)\) holds - show that, for any \(n'\), if \(P(n')\) holds, then so does \(P(S n')\); - conclude that \(P(n)\) holds for all n
Steps 1. begin with the goal of proving \(P(n)\) for all \(n\) 2. break it down by applying the induction tactic into two separate subgoals - one where we must show \(P(O)\) - one where we must show \(P(n') → P(S n')\)
Example
1 2 3 4 5 |
|
Note: use of the intros here is redundant. When applied to a goal that contains quantified variables, the induction tactic will automatically move them into the context.
Use as
to specify the names of the variables to be introduced in the subgoals.
Since there are two subgoals the as
clause has two parts separated by |
:
- in first subgoal
n
is replaced by0
(first part is empty)- goal becomes \(0 = 0 + 0\)
- in second subgoal
n
is replaced byS n'
(specified in second part)- assumption \(n' + 0 = n'\) is added to the context with name
IHn'
- goal becomes \(S n' = (S n') + 0\) which simplifies to \(S n' = S (n' + 0)\) which follows from
IHn'
.
- assumption \(n' + 0 = n'\) is added to the context with name
Another simple example
1 2 3 4 5 6 7 |
|
Using Assert
Sometimes need to break large proofs into sequence of theorems, with later proofs referring to earlier theorems.
Some proofs include parts that are too trivial for top-level name → use assert
to state and prove a needed sub-theorem at point of use.
Example
1 2 3 4 5 6 7 |
|
assert
tactic introduces two sub-goals:
1. assertion itself, which we name H
→ alternative syntax using as
: assert (0 + n = n) as H
2. second goal is the same as the one at the point where assert is invoked, except now we have assumption H
that 0 + n = n
Prove the first goal and use the second to make progress.