# Library nahas_tutorial

Mike Nahas's Coq Tutorial
Started 2012-Nov-06
Version 1.0, 2014-Oct-10

Dedicated to Kernighan and Ritchie, who wrote a magnificent introduction to a programming language.
Coq is a proof assistant. Coq helps you write formal proofs.
A "formal proof" is a mathematical proof that is written in a language
similar to a programming language. (Actually, Coq's language
(NOTE: Yes, a human error could exist in the verifying program, the
operating system, the computer, etc.. The risk in the verifying
program is kept small by keeping the program very simple and small.
As for the other parts, checking a proof on multiple systems make it
much more likely that any errors are in the proofs rather than in the
verification of the proof.)
This tutorial will teach you the basics of using Coq to write formal
proofs. My aim is to teach you a powerful subset of Coq's commands by
showing you lots of actual proofs. This tutorial will not teach you
all of the Coq commands, but you will learn enough to get started
using Coq.
This tutorial will teach you how to use Coq to write formal proofs. I
assume you already know how how write a proof and about the formal
logic on which proofs are based on. If this tutorial teaches you
about proofs or formal proofs, that is a happy accident. I also
assume you understand a programming language. It doesn't matter which
programming language.
For learning about proofs, I recommend the Pulitzer Prize winning book
"Godel, Escher, Bach", Chapters 7 and 8. (Pages 181 to 230 in my
copy.)
For learning about some of the ideas used in formal proofs, it might
be good to read about Intuitionistic logic, the Curry-Howard
correspondence, and the BHK-Interpretation.
http://en.wikipedia.org/wiki/Intuitionistic_logic
http://en.wikipedia.org/wiki/Curry-Howard_correspondence
http://en.wikipedia.org/wiki/BHK_interpretation
If you have more interest in logic, I highly recommend Gentzen's
"Investigations into Logical Deductions". It's not necessary at all,
but it is a beautiful paper.
If you need to learn a programming language, OCaML is the one that
would help you with Coq the most. Coq is written in OCaML and it
borrows a lot of OCaML's syntax and style.
http://caml.inria.fr/
To get started, you need to install Coq.
The simple way is:
If you like the Emacs text editor, the alternative is
This file (yes, the one you're reading right now) is a Coq file. Coq
file's names usually end in ".v". If this file's name currently ends
in ".txt", you'll want to change it to ".v" before loading it into
CoqIDE or Emacs. (If this file's name ends in ".html" or ".pdf",
someone used Coq to generate this document, in which case you need to
find the original ".v" file they used.)
Once you've made sure the file's name ends in ".v", start CoqIDE or
Emacs and load the file.
Coq will ignore everything that starts with a '(' followed by a '*'
and end with a '*' followed by a ')'. These are called comments.

Dedicated to Kernighan and Ritchie, who wrote a magnificent introduction to a programming language.

# Introduction

*is*a programming language, but we'll get to that later.) Formal proofs are harder for a human to read, but easier for a program to read. The advantage is that a formal proof can be verified by a program, eliminating human error.## Prerequisites

## Installing Coq

- Get "CoqIDE", the graphical version of Coq. It is available at http://coq.inria.fr/download (If you're running Linux, your package manager may have it.)

- Get "coqtop", the command-line version of Coq. It is available at http://coq.inria.fr/download (If you're running Linux, your package manager may have it.)
- Get "Proof General" Emacs mode. Is is available at http://proofgeneral.inf.ed.ac.uk/
- Install Proof General for Emacs. This is not difficult. Or, at least, it is easier than learning Emacs. The Proof General documentation will tell you how to install it.

## Loading this file

# Comments

# Your First Proof!

"for all things you could prove, if you have a proof of it, then you have a proof of it."

Theorem my_first_proof : (forall A : Prop, A -> A).

Proof.

intros A.

intros proof_of_A.

exact proof_of_A.

Qed.

## Dissection of your first proof

*SAME*thing. I think it is good style to only use "Theorem". Instead of "Qed", you may also see proofs that end with "Admitted" or "Defined", but these mean

*DIFFERENT*things. Use "Qed" for now.)

- The "vernacular" language manages definitions, and each of its commands starts with a capital letter: "Theorem", "Proof", and "Qed".
- The "tactics" language is used to write proofs, and its commands start with a lower-case letter: "intros" and "exact".
- The "Gallina" language is used to express what you want to prove, and its expressions use lots of operators and parentheses: "(forall A : Prop, A -> A)".

Theorem my_first_proof__again : (forall A : Prop, A -> A).

Proof.

intros A.

intros proof_of_A.

exact proof_of_A.

Qed.

## Seeing where you are in a proof

A : Prop proof_of_A : A ============================ A

Theorem my_first_proof__again__again : (forall A : Prop, A -> A).

Proof.

intros A.

intros proof_of_A.

exact proof_of_A.

Qed.

## Your first Tactic!

============================ forall A : Prop, A -> A

*RULE*: If the subgoal starts with "(forall <name> : <type>, ..." Then use tactic "intros <name>."

A : Prop ============================ A -> A

*RULE*: If the subgoal starts with "<type> -> ..." Then use tactic "intros <name>."

A : Prop proof_of_A : A ============================ A

- (forall x : nat, (x < 5) -> (x < 6))
- (forall x y : nat, x + y = y + x)
- (forall A : Prop, A -> A)

*RULE*: If the subgoal matches an hypothesis, Then use tactic "exact <hyp_name>."

# Proofs with ->

## Proof going forward

Theorem forward_small : (forall A B : Prop, A -> (A->B) -> B).

Proof.

intros A.

intros B.

intros proof_of_A.

intros A_implies_B.

pose (proof_of_B := A_implies_B proof_of_A).

exact proof_of_B.

Qed.

A : Prop B : Prop proof_of_A : A A_implies_B : A -> B ============================ B

*RULE*: If you have an hypothesis "<hyp_name>: <type1> -> <type2> -> ... -> <result_type>" OR an hypothesis "<hyp_name>: (forall <obj1>:<type1>, (forall <obj2>:<type2>, ... <result_type> ...))" OR any combination of "->" and "forall", AND you have hypotheses of type "type1", "type2"..., Then use tactic "pose" to create something of type "result_type".

## Proof going backward

Theorem backward_small : (forall A B : Prop, A -> (A->B)->B).

Proof.

intros A B.

intros proof_of_A A_implies_B.

refine (A_implies_B _).

exact proof_of_A.

Qed.

Notice that we're trying to prove the exact same theorem as before.
However, I'm going to show a "backward proof" that breaks the goal
into smaller and simpler subgoals. We will start this proof trying to
find a proof of B, but then change that to find the simpler proof of
A.
First, notice that the 4 "intros" commands from our last proof have
changed to just 2. The "intros" command can take any number of
arguments, each argument stripping a forall (or ->) off the front of
the current subgoal. (WARNING: Don't use "intros" with no arguments
at all - it doesn't do what you'd expect!) We could have combined all
the "intros" into a single command, but I think it is cleaner to
introduce the Props and the derived values separately.
The state right before the "refine" command is:
The subgoal is the Prop "B", so we're trying to construct a proof of
B.
We know that "A_implies_B" can create a proof of B, given a proof of
A. We saw the syntax for it was "A_implies_B something_of_type_A".
The command "refine (A_implies_B _)." let's us create the proof of B
without specifying the argument of type A. (The parentheses are
necessary for it to parse correctly.) This solves our current subgoal
of type B and the unspecified argument - represented by the underscore
("_") - become a new "child" subgoal.
In this case, the child subgoal has us trying to find a proof of A.
Since it's a child subgoal, we indent the tactics used to solve it.
And the tactic to solve it is our well worn "exact".
The important thing to take away from this proof is that we changed
the subgoal. That's what happens in a backward proof. You keep
changing the subgoal to make it smaller and simpler. "A" doesn't seem
much smaller or simpler than "B", but it was.
Now, let's rev this up...

A : Prop B : Prop proof_of_A : A A_implies_B : A -> B ============================ B

A : Prop B : Prop proof_of_A : A A_implies_B : A -> B ============================ A

*RULE*: If you have subgoal "<goal_type>" AND have hypothesis "<hyp_name>: <type1> -> <type2> -> ... -> <typeN> -> <goal_type>", Then use tactic "refine (<hyp_name> _ ...)." with N underscores.## Proof going backward (large)

Theorem backward_large : (forall A B C : Prop, A -> (A->B) -> (B->C) -> C).

Proof.

intros A B C.

intros proof_of_A A_implies_B B_implies_C.

refine (B_implies_C _).

refine (A_implies_B _).

exact proof_of_A.

Qed.

Look at the sequence of tactics. It starts with a pair of "intros"s.
That's followed by the new kid on the block "refine". We finish with
"exact". That pattern will start to look familiar very soon.
The state before the first "refine" is:
Our current subgoal is "C" and "C" is at the end of "B -> C", so we
can do "refine (B_implies_C _)". That command creates a new child
subgoal "B".
Then, our subgoal is "B" and "B" is at the end of "A -> B", so "refine
(A_implies_B _)" creates a new child subgoal of "A".
Then we finish with "exact proof_of_A.". Easy as pie.
Let's do a really big example!

A : Prop B : Prop C : Prop proof_of_A : A A_implies_B : A -> B B_implies_C : B -> C ============================ C

## Proof going backward (huge)

Theorem backward_huge : (forall A B C : Prop, A -> (A->B) -> (A->B->C) -> C).

Proof.

intros A B C.

intros proof_of_A A_implies_B A_imp_B_imp_C.

refine (A_imp_B_imp_C _ _).

exact proof_of_A.

refine (A_implies_B _).

exact proof_of_A.

Qed.

Yes, something is different here! We have our starting "intros"s. We
have a "refine". But then the commands are indented and we have two
"exact"s!
The state before the first refine is:
Now, we have a subgoal "C" and "C" is at the end of "A->B->C", so we
can do "refine (A_imp_B_imp_C _ )". Notice that "A_imp_B_imp_C" has
two implication arrows (the "->"s), so refine requires two underscores
and creates two subgoals - one for something of type A and another for
something of type B.
I hinted that a formal proof is actually written in a programming
language. We see that very clearly here. "A_imp_B_imp_C" is a
function that takes two arguments, one of type A and one of type B,
and returns a value of type C. The type of the function is "A->B->C"
and a call to it looks like "A_imp_B_imp_C something_of_type_A
something_of_type_B". Notice that there are no parentheses needed -
you just put the arguments next to the name of the function.
E.g. "function arg1 arg2" This is a style common in functional
programming languages. For those familiar with imperative languages,
like C, C++, and Java, it will feel odd not to have parentheses and
commas to denote the arguments.
The first "refine" created two subgoals. CoqIDE and Proof General
will tell you that two subgoals exist, but they will only show you the
context for the current subgoal.
In the text of the proof, we represent that "refine" created multiple
subgoals by formatting them like an "if-then-else" or "switch/match"
statement in a programming language. The proofs for each subgoal get
indented and we use a blank line to separate them.
The proof of the first subgoal is trivial. We need an "A" and we have
"proof_of_A : A". "exact proof_of_A" completes the subgoal. We now
put the blank line in the proof to show we're moving on to the next
subgoal.
The rest of the proof we've seen before. The proof for it is indented
to show it's the result of a "branch" in the proof created by "refine
(A_imp_B_impC _ )".
Having seen this complex theorem proved with a backward proof, let's
see what it would look like with a forward one.

A : Prop B : Prop C : Prop proof_of_A : A A_implies_B : A -> B A_imp_B_imp_C : A -> B -> C ============================ C

## Proof going forward (huge)

Theorem forward_huge : (forall A B C : Prop, A -> (A->B) -> (A->B->C) -> C).

Proof.

intros A B C.

intros proof_of_A A_implies_B A_imp_B_imp_C.

pose (proof_of_B := A_implies_B proof_of_A).

pose (proof_of_C := A_imp_B_imp_C proof_of_A proof_of_B).

exact proof_of_C.

Show Proof.

Qed.

(fun (A B C : Prop) (proof_of_A : A) (A_implies_B : A -> B) (A_imp_B_imp_C : A -> B -> C) => let proof_of_B := A_implies_B proof_of_A in let proof_of_C := A_imp_B_imp_C proof_of_A proof_of_B in proof_of_C)

# true and false vs. True and False

Inductive False : Prop := . Inductive True : Prop := | I : True. Inductive bool : Set := | true : bool | false : bool.

- Capital-F "False" is a Prop with no proofs.
- Capital-T "True" is a Prop that has a single proof called "I". (That's a capital-I, not a number 1.)
- Lastly, "bool" is a Set and "bool" has two elements: lower-case-t "true" and lower-case-f "false".

## Capital-T True and Capital-F False

### True is provable

If we look at the state before the first (and only) line of the proof,
we see:
There are no hypotheses; the context is empty. We are trying to find
a proof of True. By its definition, True has a single proof called
"I". So, "exact I." solves this proof.
Now, we turn to False.
I wrote earlier that a proposition either has a proof or it does not
(yet) have a proof. In some cases, we can prove that a proposition
can never have a proof. We do that by showing that for every possible
proof of a proposition, we could generate a proof of False. Because
False has no proofs (by its definition), we know that the proposition
has no proofs.
So, to show that "A : Prop" has no proofs, we need to show
We do this so often that there is an operator "~" to represent it.
"Definition" is a vernacular command that says two things are
interchangeable. So, "(not A)" and "A -> False" are interchangeable.
"Notation" is a vernacular command that creates an operator, in this
case "~", and defines it as an alternate notation for an expression,
in this case "(not _)". Since "not" takes a Prop, "~" can only be
applied to a Prop.
(NOTE: The Notation command is how the operator "->" was created
for "(forall ...)".)
Let's try to prove some things are unprovable!

============================ True

*RULE*: If your subgoal is "True", Then use tactic "exact I".### Unprovability

- (forall proof_of_A: A, False)

- A -> False

Definition not (A:Prop) := A -> False. Notation "~ x" := (not x) : type_scope.

### False is unprovable

Theorem False_cannot_be_proven : ~False.

Proof.

unfold not.

intros proof_of_False.

exact proof_of_False.

Qed.

============================ False -> False

Theorem False_cannot_be_proven__again : ~False.

Proof.

intros proof_of_False.

case proof_of_False.

Qed.

This is the same theorem as before, but two things have changed in
this proof.
First, it doesn't have "unfold not.". Since we know "~" is shorthand
for "->", we can skip over the unfold tactic and go straight to using
"intros".
The second change is that we found a new way to finish a proof!
Instead of "exact", we use the "case" tactic. "case" is
powerful: it creates subgoals for every possible construction of its
argument. Since there is no way to construct a False, "case"
creates no subgoals! Without a subgoal, we're done!
We can use True and False to see that Coq's "->" operator really does
act like "implication" from logic.

*RULE*: If your subgoal is "~<type>" or "~(<term>)" or "(not <term>)", Then use tactic "intros".*RULE*: If any hypothesis is "<name> : False", Then use tactic "case <name>."### -> Examples

"exact proof_of_True." also works.

"case proof_of_False." also works.

Qed.

Theorem thm_false_imp_false : False -> False.

Proof.

intros proof_of_False.

case proof_of_False.

Theorem thm_false_imp_false : False -> False.

Proof.

intros proof_of_False.

case proof_of_False.

"exact proof_of_False." works, but is not recommended.

Qed.

True->False can never be proven. We demonstrate that by
proving ~(True->False).

Theorem thm_true_imp_false : ~(True -> False).

Proof.

intros T_implies_F.

refine (T_implies_F _).

exact I.

Qed.

Proof.

intros T_implies_F.

refine (T_implies_F _).

exact I.

Qed.

### Reducto ad absurdium

Theorem absurd2 : forall A C : Prop, A -> ~ A -> C.

Proof.

intros A C.

intros proof_of_A proof_that_A_cannot_be_proven.

unfold not in proof_that_A_cannot_be_proven.

pose (proof_of_False := proof_that_A_cannot_be_proven proof_of_A).

case proof_of_False.

Qed.

## The return of lower-case true and lower-case false

Inductive bool : Set := | true : bool | false : bool.

"Require Import" is a vernacular command that loads definitions from a
library. In this case, the library is named "Bool" and there is a
file named "Bool.v" that contains its definitions, proofs, etc..
Two of the functions are:
The first function "eqb" returns true if the two arguments match.
("eqb" is short for "equal for type bool".)
The second function "Is_true" converts a bool into a Prop. In the
future, you can use "(<name> = true)", but we haven't described "="
yet. The operator "=" is REALLY cool, but you have to understand more
basic types, like bool, first.
Let's do some proofs with these functions.

Definition eqb (b1 b2:bool) : bool := match b1, b2 with | true, true => true | true, false => false | false, true => false | false, false => true end. Definition Is_true (b:bool) := match b with | true => True | false => False end.

### Is_true true is True

*RULE*: If the current subgoal contains a function call with all its arguments, Then use the tactic "simpl".

### Is_true called with a complex constant.

Theorem not_eqb_true_false: ~(Is_true (eqb true false)).

Proof.

simpl.

exact False_cannot_be_proven.

Qed.

*OR*we could just say the proof already exists! We gave the proof of "~False" the name "False_cannot_be_proven", so the tactic "exact False_cannot_be_proven" finishes the proof immediately! Sweet, isn't it?

### case with bools

suppose a is true

suppose a is false

*RULE*: If there is a hypothesis "<name>" of a created type AND that hypothesis is used in the subgoal, Then you can try the tactic "case <name>"

Theorem thm_eqb_a_t: (forall a:bool, (Is_true (eqb a true)) -> (Is_true a)).

Proof.

intros a.

case a.

suppose a is true

suppose a is false

simpl.

intros proof_of_False.

case proof_of_False.

Qed.

intros proof_of_False.

case proof_of_False.

Qed.

# And, Or

## Or

- (or (x < 5) (x = 7))
- (or True False)
- (or (x = 0) (x = 1))

- or (A B:Prop) : Prop

Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B where "A \/ B" := (or A B) : type_scope.

- declares "or", a function that takes two Props and produces a Prop
- declares "or_introl", a constructor that takes a proof of "A" and returns a proof of "(or A B)"
- declares "or_intror", a constructor that takes a proof of "B" and returns a proof of "(or A B)"
- declares "\/", an operator that is interchangeable with "or"

Inductive False : Prop := . Inductive True : Prop := I : True. Inductive bool : Set := | true : bool | false : bool.

Theorem left_or : (forall A B : Prop, A -> A \/ B).

Proof.

intros A B.

intros proof_of_A.

pose (proof_of_A_or_B := or_introl proof_of_A : A \/ B).

exact proof_of_A_or_B.

Qed.

Theorem right_or : (forall A B : Prop, B -> A \/ B).

Proof.

intros A B.

intros proof_of_B.

refine (or_intror _).

exact proof_of_B.

Qed.

An even shorter proof would have just "exact (or_intror proof_of_B)".
But if you don't know all the constructor's arguments, using "refine"
is a fine approach.
Let's prove something a little more complicated...

*RULE*: If the subgoal's top-most term is a created type, Then use "refine (<name_of_constructor> _ ...)".### Or commutes

Theorem or_commutes : (forall A B, A \/ B -> B \/ A).

Proof.

intros A B.

intros A_or_B.

case A_or_B.

suppose A_or_B is (or_introl proof_of_A)

suppose A_or_B is (or_intror proof_of_B)

## And

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

Theorem both_and : (forall A B : Prop, A -> B -> A /\ B).

Proof.

intros A B.

intros proof_of_A proof_of_B.

refine (conj _ _).

exact proof_of_A.

exact proof_of_B.

Qed.

### And commutes

Theorem and_commutes : (forall A B, A /\ B -> B /\ A).

Proof.

intros A B.

intros A_and_B.

case A_and_B.

suppose A_and_B is (conj proof_of_A proof_of_B)

### destruct tactic

destruct <hyp> as [ <arg1> <arg2> ... ].

Theorem and_commutes__again : (forall A B, A /\ B -> B /\ A).

Proof.

intros A B.

intros A_and_B.

destruct A_and_B as [ proof_of_A proof_of_B].

refine (conj _ _).

exact proof_of_B.

exact proof_of_A.

Qed.

*RULE*: If a hypothesis "<name>" is a created type with only one constructor, Then use "destruct <name> as <arg1> <arg2> ... " to extract its arguments

### functions and inductive types

- andb (b1 b2:bool) : bool
- orb (b1 b2:bool) : bool
- negb (b:bool) : bool

Infix "&&" := andb : bool_scope. Infix "||" := orb : bool_scope.

Definition iff (A B:Prop) := (A -> B) /\ (B -> A). Notation "A <-> B" := (iff A B) : type_scope.

Theorem orb_is_or : (forall a b, Is_true (orb a b) <-> Is_true a \/ Is_true b).

Proof.

intros a b.

unfold iff.

refine (conj _ _).

Proof.

intros a b.

unfold iff.

refine (conj _ _).

orb -> \/

intros H.

case a, b.

case a, b.

suppose a,b is true, true

suppose a,b is true, false

suppose a,b is false, true

suppose a,b is false, false

simpl in H.

case H.

case H.

\/ -> orb

intros H.

case a, b.

case a, b.

suppose a,b is true, true

suppose a,b is true, false

suppose a,b is false, true

suppose a,b is false, false

case H.

suppose H is (or_introl A)

intros A.

simpl in A.

case A.

simpl in A.

case A.

suppose H is (or_intror B)

intros B.

simpl in B.

case B.

Qed.

simpl in B.

case B.

Qed.

- combining "refine" and "exact" and skipping right over "simpl".

*RULE*If a hypothesis "<name>" contain a function call with all its arguments, Then use the tactic "simpl in <name>"

Theorem andb_is_and : (forall a b, Is_true (andb a b) <-> Is_true a /\ Is_true b).

Proof.

intros a b.

unfold iff.

refine (conj _ _).

andb -> /\

intros H.

case a, b.

case a, b.

suppose a,b is true,true

suppose a,b is true,false

simpl in H.

case H.

case H.

suppose a,b is false,true

simpl in H.

case H.

case H.

suppose a,b is false,false

simpl in H.

case H.

case H.

/\ -> andb

intros H.

case a,b.

case a,b.

suppose a,b is true,true

suppose a,b is true,false

simpl in H.

destruct H as [ A B].

case B.

destruct H as [ A B].

case B.

suppose a,b is false,true

simpl in H.

destruct H as [ A B].

case A.

destruct H as [ A B].

case A.

suppose a,b is false,false

simpl in H.

destruct H as [ A B].

case A.

Qed.

destruct H as [ A B].

case A.

Qed.

### admit tactic

- HINT: Remember "~A" is "A -> False".
- HINT: You can make use of the proof "False_cannot_be_proven"
- HINT: When you get stuck, look at "thm_true_imp_false".

delete "admit" and put your proof here.

Qed.

*RULE*: If you have a subgoal that you want to ignore for a while, Then use the tactic "admit"

# Existence and Equality

## Existence

Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P. Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, right associativity, format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") : type_scope.

Definition basic_predicate

:=

(fun a => Is_true (andb a true))

.

Theorem thm_exists_basics : (ex basic_predicate).

Proof.

pose (witness := true).

refine (ex_intro basic_predicate witness _).

simpl.

exact I.

Qed.

- the predicate
- the witness
- a proof of the predicated called with the witness

Theorem thm_exists_basics__again : (exists a, Is_true (andb a true)).

Proof.

pose (witness := true).

refine (ex_intro _ witness _).

Proof.

pose (witness := true).

refine (ex_intro _ witness _).

Coq automatically determines the predicate! We're left to prove that the witness satisfies the function.

*RULE*: If the current subgoal starts "exists <name>, ..." Then create a witness and use "refine (ex_intro _ witness _)"

### More existence

b is true

b is false

If you look at the proof above, the witness was always equal to "b".
So, let's try simplifying the proof.

Theorem thm_forall_exists__again : (forall b, (exists a, Is_true(eqb a b))).

Proof.

intros b.

refine (ex_intro _ b _).

witness is b

We used "b" as the witness and ended up with the state:
Now, we have already proved:
I've told you that "->" is the type of a function and that "->" is
shorthand for "(forall ...)", so it's not a far leap to see that our
theorem "eqb_a_a" is a function from any bool (called "a" in the
statement) to a proof of "Is_true (eqb a a)".
In our current proof, we needed that statement to hold for our
particular hypothesis of "b". That is done by the function call
"eqb_a_a b", which substitutes the specific "b" into the place of the
generic "a" in the body of the "forall". The result is "Is_true (eqb
b b)", which solves our proof.
Here is a classic theorem of logic, showing the relationship between
"forall" and "exists". It gives us a chance to "destruct" an instance
of type "ex".

b : bool ============================ Is_true (eqb b b)

Theorem eqb_a_a : (forall a : bool, Is_true (eqb a a)).

### Exists and Forall

Theorem forall_exists : (forall P : Set->Prop, (forall x, ~(P x)) -> ~(exists x, P x)).

Proof.

intros P.

intros forall_x_not_Px.

unfold not.

intros exists_x_Px.

destruct exists_x_Px as [ witness proof_of_Pwitness].

pose (not_Pwitness := forall_x_not_Px witness).

unfold not in not_Pwitness.

pose (proof_of_False := not_Pwitness proof_of_Pwitness).

case proof_of_False.

Qed.

The proof requires some explanation.
This proof is hard to read. If you have difficulty reading a proof,
you can always use CoqIDE or Proof General to step through the proof
and look at the state after each tactic.
Another good example of "exists" is proving that the implication goes
the other way too.

- we use intros and unfold until we have everything in the context.
- we use "destruct" to extract the witness and the proof of "P witness".
- we call "(forall x, ~(P x))" with the witness, to generate "(P witness) -> False"
- we call "P witness -> False" with "P witness" to get a proof of "False".
- we use the tactic "case" on "proof_of_False"

Theorem exists_forall : (forall P : Set->Prop, ~(exists x, P x) -> (forall x, ~(P x))).

Proof.

intros P.

intros not_exists_x_Px.

intros x.

unfold not.

intros P_x.

unfold not in not_exists_x_Px.

refine (not_exists_x_Px _).

exact (ex_intro P x P_x).

Qed.

Again, this isn't a very readable proof. It goes by:
For some predicates, the witness is a single value or is easy to
generate. Other times, it isn't. In those cases, we can write a
function to calculate the witness.
Right now, we can't write very complicated functions, since we only
know a few types. When we have lists and natural numbers, you'll see
some examples.
Now we come to the big prize: equality! Equality is a derived concept
in Coq. It's an inductive type, just like "and", "or", and "ex"
("exists"). When I found that out, I was shocked and fascinated!
It's defined as:
The "Inductive" statement creates a new type "eq" which is a function
of a type A and 2 values of type A to Prop. (NOTE: One value of type
A is written (x:A) before the ":" and the other is written "A ->"
after. This is done so Coq infers the type "A" from the first
value and not the second.) Calling "eq" with all its arguments
returns a proposition (with type Prop). A proof of "eq x y" means
that "x" and "y" both have the same type and that "x" equals "y".
The only way to create a proof of type "eq" is to use the only
constructor "eq_refl". It takes a value of "x" of type "A" and
returns "@eq A x x", that is, that "x" is equal to itself. (The "@"
prevents Coq from inferring values, like the type "A".) The name
"eq_refl" comes from the reflexive property of equality.
Lastly, comes two operators. The less commonly used one is "x = y :>
A" which let's you say that "x" and "y" are equal and both have type
"A". The one you'll use most of the time, "x = y", does the same but
let's Coq infer the type "A" instead of forcing you to type it.
Now, if you we paying attention, you saw that "eq_refl" is the only
constructor. We can only create proofs of "x = x"! That doesn't seem
useful at all!
What you don't see is that Coq allows you to execute a function call
and substitute the result for the function call. For example, if we had
a function "plus" that added natural numbers (which have type "nat"),
we could use "eq_refl (plus 1 1)" to create a proof of
"eq nat (plus 1 1) (plus 1 1)". Then, if we execute the second function
call, we get "eq nat (plus 1 1) 2", that is, "1 + 1 = 2"!
The concept of substituting a function call with its result or
substituting the result with the function call is called
"convertibility". One tactic we've seen, "simpl", replaces
convertibile values. We'll see more tactics in the future.
Now that we have a concept of what "=" means in Coq, let's use it!

- we use intros and unfold until our subgoal is "False".
- we use "refine" to call a function whose type ends in "-> False"
- we create something of type "exists" by calling "ex_intro"

### Calculating witnesses

## Equality

Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : x = x :>A where "x = y :> A" := (@eq A x y) : type_scope. Notation "x = y" := (x = y :>_) : type_scope.

### Equality is symmetric

Theorem thm_eq_sym : (forall x y : Set, x = y -> y = x).

Proof.

intros x y.

intros x_y.

destruct x_y as [].

exact (eq_refl x).

Qed.

I use the "destruct" tactic on the type "eq" because it only has one
constructor. Let's look at the state before and after that call.
Before, it is:
And after:
By destructing the "eq_refl", Coq realizes that "x" and "y" are
convertible and wherever the second name is, it can be replaced by
the first. So, "y" disappears and is replaced by "x". (NOTE:
"destruct" unlike "case", does change the context, so the hypotheses
"y" and "x_y" also disappear.)
After "destruct", we're left with a subgoal of "x = x", which is
solved by calling "eq_refl".
Just to become familiar, let's prove the other big property of
equality: transitivity.

x : Set y : Set x_y : x = y ============================ y = x

x : Set ============================ x = x

### Equality is transitive

Theorem thm_eq_trans : (forall x y z: Set, x = y -> y = z -> x = z).

Proof.

intros x y z.

intros x_y y_z.

destruct x_y as [].

destruct y_z as [].

exact (eq_refl x).

Qed.

Seems pretty easy, doesn't it?
Rather than using "destruct", most proofs using equality use the
tactics "rewrite" and "rewrite <-". If "x_y" has type "x = y", then
"rewrite x_y" will replace "x" with "y" in the subgoal and "rewrite <-
x_y" will go the other way, replacing "y" with "x".
Let's see these tactics by proving transitivity again.

Theorem thm_eq_trans__again : (forall x y z: Set, x = y -> y = z -> x = z).

Proof.

intros x y z.

intros x_y y_z.

rewrite x_y.

rewrite <- y_z.

exact (eq_refl y).

Qed.

That is much cleaner.
Let's try something that explicitly relies on convertibility. Recall,
"andb" is and for "bools" and that it is represented by the operator
"&&".

*RULE*: If you have a hypothesis "<name> : <a> = <b>" AND "<a>" in your current subgoal Then use the tactic "rewrite <name>"*RULE*: If you have a hypothesis "<name> : <a> = <b>" AND "<b>" in your current subgoal Then use the tactic "rewrite <- <name>"
suppose a,b is true,true

suppose a,b is true,false

suppose a,b is false,true

suppose a,b is false,false

So, for this proof, we divided it into 4 cases and used convertibility
to show that equality held in each. Pretty simple.
I should do an example with inequality too.
Coq uses the operator "<>" for inequality, which really means
"equality is unprovable" or "equality implies False".
Let's start with a simple example. Recall that "negb" is the
"not" operation for bools.

### Inequality with discriminate

Notation "x <> y :> T" := (~ x = y :>T) : type_scope. Notation "x <> y" := (x <> y :>_) : type_scope.

Theorem neq_nega: (forall a, a <> (negb a)).

Proof.

intros a.

unfold not.

case a.

intros a_eq_neg_a.

simpl in a_eq_neg_a.

discriminate a_eq_neg_a.

intros a_eq_neg_a.

simpl in a_eq_neg_a.

discriminate a_eq_neg_a.

Qed.

Proof.

intros a.

unfold not.

case a.

intros a_eq_neg_a.

simpl in a_eq_neg_a.

discriminate a_eq_neg_a.

intros a_eq_neg_a.

simpl in a_eq_neg_a.

discriminate a_eq_neg_a.

Qed.

*RULE*: If you have a hypothesis "<name> : (<constructor1> ...) = (<constructor2> ...) OR "<name> : <constant1> = <constant2> Then use the tactic "discriminate <name>"

# Natural Numbers and Induction

## Peano Arithmetic

- 0 is a natural number.
- For every natural number n, (S n) is a natural number.

- 0 is 0
- 1 is (S 0) = (1 + 0)
- 2 is (S (S 0)) = (1+ (1 + 0))
- 3 is (S (S (S 0)) = (1 + (1 + (1 + 0)))
- ...

Inductive nat : Set := | O : nat | S : nat -> nat.

*WARNING*: The "O" here is the capital-letter O,

*not*the number zero.

Fixpoint plus (n m:nat) : nat := match n with | O => m | S p => S (p + m) end where "n + m" := (plus n m) : nat_scope.

- (plus (S (S O)) (S (S (S O))))
- (S (plus (S O) (S (S (S O)))))
- (S (S (plus O (S (S (S O))))))
- (S (S (S (S (S O))))))

Theorem plus_2_3 : (S (S O)) + (S (S (S O))) = (S (S (S (S (S O))))).

Proof.

simpl.

exact (eq_refl 5).

Qed.

## Induction

If "P" is a predicate such that (P 0) is proven, and for all n, (P n) -> (P (S n)) is proven, Then (P n) is proven for all n.

Its output should look like this:
Now, we
But that's a lot of work. Luckily, Coq defines tactics that do most
of the work for us! These tactics take a subgoal and infer the
predicate P, and then generates child subgoals for the other pieces.
One tactic, "elim" works very similarly to "case".

nat_ind : forall P : nat -> Type, P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

*could*- define a function "P n" that represents "O + n = n"
- prove that the function holds for "P O"
- prove that the function holds for "P (S n)" assuming "P n"
- and then call the function nat_ind with those 3 values.

base case

inductive case

intros n'.

intros inductive_hypothesis.

simpl.

rewrite inductive_hypothesis.

exact (eq_refl (S n')).

Qed.

intros inductive_hypothesis.

simpl.

rewrite inductive_hypothesis.

exact (eq_refl (S n')).

Qed.

It's obvious how the tactic "elim" generates the base case and
inductive case. It was important to me to show that the "n" in the
inductive case was different from the original "n" in our goal. I
chose to name it "n'" which is spoken "n prime".
I used the "rewrite" tactic with the inductive hypothesis to
substitute "n' + O" in the subgoal. If you're using the "elim"
tactic, you should always use the inductive hypothesis. If you don't,
you should use the "case" tactic instead of "elim".
Now that we know how to use induction, let's do a difficult proof.
Let's prove that "n + m = m + n".

*RULE*: If there is a hypothesis "<name>" of a created type AND that hypothesis is used in the subgoal, AND the type has a recursive definition Then you can try the tactic "elim <name>"### Addition is Symmetric

base case for n

elim m.

base case for m

inductive case for m

intros m'.

intros inductive_hyp_m.

simpl.

rewrite <- inductive_hyp_m.

simpl.

exact (eq_refl (S m')).

intros inductive_hyp_m.

simpl.

rewrite <- inductive_hyp_m.

simpl.

exact (eq_refl (S m')).

inductive case for n

intros n'.

intros inductive_hyp_n.

simpl.

rewrite inductive_hyp_n.

elim m.

intros inductive_hyp_n.

simpl.

rewrite inductive_hyp_n.

elim m.

base case for m

simpl.

exact (eq_refl (S n')).

intros m'.

intros inductive_hyp_m.

simpl.

rewrite inductive_hyp_m.

simpl.

exact (eq_refl (S (m' + S n'))).

Qed.

exact (eq_refl (S n')).

intros m'.

intros inductive_hyp_m.

simpl.

rewrite inductive_hyp_m.

simpl.

exact (eq_refl (S (m' + S n'))).

Qed.

That is a
"nat" is a commonly used type in Coq and there are a lot of operators
defined for it. Having seen how "plus" was defined, you can probably
guess the definition for "mult".
Also defined are:
Along with:
The dangerous one in this group is "minus". The natural numbers don't
go lower than 0, so "(1 - 2)" cannot return a negative number. Since
Coq must return something of type "nat", it returns "O" instead. So
you can do crazy proofs like this without intending!

*hard*proof. I've seen an expert in Coq get stuck on it for 10 minutes. It uses a lot of the features that I've demonstrated in this tutorial. I encourage you to open a new file and try to prove it yourself. If you get stuck on part of it, you should use the "admit" tactic and move onto another part. If you get really stuck, open up this file and look at how I did it in my proof. You should keep practicing on that proof until you can do it automatically.### Common nat operators

Fixpoint mult (n m:nat) : nat := match n with | O => 0 | S p => m + p * m end where "n * m" := (mult n m) : nat_scope.

- "n - m" := (minus n m)
- "n <= m" := (le n m)
- "n < m" := (lt n m)
- "n >= m" := (ge n m)
- "n > m" := (gt n m)

- "x <= y <= z" := (x <= y /\ y <= z)
- "x <= y < z" := (x <= y /\ y < z)
- "x < y < z" := (x < y /\ y < z)
- "x < y <= z" := (x < y /\ y <= z)
- "max n m"
- "min n m"

Later, with lists, I'll show you different ways to implement "minus"
without this flaw.
You've learned the basics of Coq. This section introduces some
commonly used data types, so that you get to see them and get some
more experience reading proofs.

# Data types

## Lists and Option

Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A.

Infix "::" := cons (at level 60, right associativity) : list_scope.So, the value "5 :: 4 :: nil" would be a "list nat" containing the values 5 and 4.

Definition length (A : Type) : list A -> nat := fix length l := match l with | nil => O | _ :: l' => S (length l') end.

Theorem cons_adds_one_to_length :

(forall A:Type,

(forall (x : A) (lst : list A),

length (x :: lst) = (S (length lst)))).

Proof.

intros A.

intros x lst.

simpl.

exact (eq_refl (S (length lst))).

Qed.

(forall A:Type,

(forall (x : A) (lst : list A),

length (x :: lst) = (S (length lst)))).

Proof.

intros A.

intros x lst.

simpl.

exact (eq_refl (S (length lst))).

Qed.

The proof is pretty simple, but the statement of what we want to prove
is not! First, we need "A", which is the type stored in our lists.
Then we need an instance of A and a instance of a list of A. Only
then can we state that putting an element on the front of a list
increases its length by 1.
Now, the simplest function you can imagine for a linked list is "hd",
which returns the first value in the list. But there's a problem:
what should we return if the list is empty?
In some programming languages, you might throw an exception - either
explicitly or through a memory violation. In others, you might assume
the program crashs. But if you to prove a program correct, these
aren't choices you can make. The program needs to be predictable.
There are choices you can make:
You didn't think of that last one, did you?! I'll show you each of these
approaches so that you can see what they look like.

### The three forms of hd

- have "hd" take an additional parameter, which it returns if the list is empty
- have "hd" return a new data structure that may or may not contain the value
- pass "hd" a proof that the list is not empty

#### hd with additional parameter

Definition hd (A : Type) (default : A) (l : list A)

:=

match l with

| nil => default

| x :: _ => x

end.

This is the default version of hd in Coq and it looks like you would
expect. This version is more useful than you might think thanks to
"partial evaluation".
"partial evaluation" is passing only
Thus, we can do:

*some*of the arguments to a function. In Coq, and many functional languages, the result is a new function where the supplied arguments are now treated like constants in the function and the remaining parameters are can still be passed in.
The remaining parameter - the list - can still be passed to
"my_hd_for_nat_lists", but the "Type" parameter has been bound to
"nat" and the parameter "default" has been bound to zero.
We can confirm that it works correctly by using the vernacular command
"Compute", which executes all the function calls and prints the result.

Prints "= 0 : nat".

Prints "= 5 : nat".
We can also prove it correct.

Theorem correctness_of_hd :

(forall A:Type,

(forall (default : A) (x : A) (lst : list A),

(hd A default nil) = default /\ (hd A default (x :: lst)) = x)).

Proof.

intros A.

intros default x lst.

refine (conj _ _).

simpl.

exact (eq_refl default).

simpl.

exact (eq_refl x).

Qed.

(forall A:Type,

(forall (default : A) (x : A) (lst : list A),

(hd A default nil) = default /\ (hd A default (x :: lst)) = x)).

Proof.

intros A.

intros default x lst.

refine (conj _ _).

simpl.

exact (eq_refl default).

simpl.

exact (eq_refl x).

Qed.

#### hd returns option

Inductive option (A : Type) : Type := | Some : A -> option A | None : option A.

Again, using "Compute" we can examine what it returns.

Prints "= None : option nat".

Prints "= Some 5 : option nat".
We can also prove it correct.

Theorem correctness_of_hd_error :

(forall A:Type,

(forall (x : A) (lst : list A),

(hd_error A nil) = None /\ (hd_error A (x :: lst)) = Some x)).

Proof.

intros A.

intros x lst.

refine (conj _ _).

simpl.

exact (eq_refl None).

simpl.

exact (eq_refl (Some x)).

Qed.

(forall A:Type,

(forall (x : A) (lst : list A),

(hd_error A nil) = None /\ (hd_error A (x :: lst)) = Some x)).

Proof.

intros A.

intros x lst.

refine (conj _ _).

simpl.

exact (eq_refl None).

simpl.

exact (eq_refl (Some x)).

Qed.

#### hd with a proof that the list is non-empty

Definition hd_never_fail (A : Type) (lst : list A) (safety_proof : lst <> nil)

: A

:=

(match lst as b return (lst = b -> A) with

| nil => (fun foo : lst = nil =>

match (safety_proof foo) return A with

end

)

| x :: _ => (fun foo : lst = x :: _ =>

x

)

end) eq_refl.

: A

:=

(match lst as b return (lst = b -> A) with

| nil => (fun foo : lst = nil =>

match (safety_proof foo) return A with

end

)

| x :: _ => (fun foo : lst = x :: _ =>

x

)

end) eq_refl.

I don't expect you to understand this function, let alone write
it. It took me 30 minutes to write it, mostly by copying from code
printed using "Show Proof." from the complicated proofs above.
But I do expect you to understand that it

*can*be written in Coq. And, I expect you to be able to read a prove that the function does what I said it does.
Theorem correctness_of_hd_never_fail :

(forall A:Type,

(forall (x : A) (rest : list A),

(exists safety_proof : ((x :: rest) <> nil),

(hd_never_fail A (x :: rest) safety_proof) = x))).

Proof.

intros A.

intros x rest.

assert (witness : ((x :: rest) <> nil)).

unfold not.

intros cons_eq_nil.

discriminate cons_eq_nil.

refine (ex_intro _ witness _).

simpl.

exact (eq_refl x).

Qed.

(forall A:Type,

(forall (x : A) (rest : list A),

(exists safety_proof : ((x :: rest) <> nil),

(hd_never_fail A (x :: rest) safety_proof) = x))).

Proof.

intros A.

intros x rest.

assert (witness : ((x :: rest) <> nil)).

unfold not.

intros cons_eq_nil.

discriminate cons_eq_nil.

refine (ex_intro _ witness _).

simpl.

exact (eq_refl x).

Qed.

The proof is pretty simple. We create a witness for the exists.
Since the witness involves an inequality, we end its proof with
"discriminate". Then we use "simpl" to show that the function returns
what the right value.
In this proof, I used the tactic "assert" instead of "pose". I wanted
to write:
"hd" extracts the first value in a list and its partner "tl" returns
the list after that first element. In Coq, it's definition is:

pose (witness := _ : ((x :: rest) <> nil)).But Coq does not allow that for some reason. "pose" cannot have "_" for the complete value. If you want to use "_" for the whole value of pose, you have to use the tactic "assert".

### Tail of lists

If you want to test your skills, it would be good practice to write
three different versions of "tl", just like I did for "hd", and prove
them correct.
Here's just a simple proof that the "hd" and "tl" of a non-empty list
can be used to reconstruct the list.

Definition tl_error (A : Type) (l : list A) : option list A := ... Definition tl_never_fail (A : Type) (lst : list A) (safety_proof : lst <> nil) : list A := ...

Theorem hd_tl :

(forall A:Type,

(forall (default : A) (x : A) (lst : list A),

(hd A default (x::lst)) :: (tl A (x::lst)) = (x :: lst))).

Proof.

intros A.

intros default x lst.

simpl.

exact (eq_refl (x::lst)).

Qed.

(forall A:Type,

(forall (default : A) (x : A) (lst : list A),

(hd A default (x::lst)) :: (tl A (x::lst)) = (x :: lst))).

Proof.

intros A.

intros default x lst.

simpl.

exact (eq_refl (x::lst)).

Qed.

### Appending lists

Definition app (A : Type) : list A -> list A -> list A := fix app l m := match l with | nil => m | a :: l1 => a :: app l1 m end. Infix "++" := app (right associativity, at level 60) : list_scope.

delete "admit" and put your proof here.

Proof.

Theorem app_nil_r : (forall A:Type, (forall l:list A, forall l:list A, l ++ nil = l)).

admit.

Theorem app_nil_r : (forall A:Type, (forall l:list A, forall l:list A, l ++ nil = l)).

admit.

delete "admit" and put your proof here.

delete "admit" and put your proof here.

delete "admit" and put your proof here.

delete "admit" and put your proof here.

Proof.

# Conclusion

# Vernacular commands

- "Theorem" starts a proof.
- "Qed" ends a proof.
- "Definition" declares a function.
- "Fixpoint" declares a recursive function.
- "Inductive" declares data types.
- "Notation" creates new operators.
- "Infix" also creates new operators.
- "Show Proof" prints out the current state of the proof.
- "Require Import" reads in definitions from a file.
- "Check" prints out a description of a type.
- "Compute" prints out the result of a function call.

# The tactic guide

*RULE*: If the subgoal starts with "(forall <name> : <type>, ..." Then use tactic "intros <name>."

*RULE*: If the subgoal starts with "<type> -> ..." Then use tactic "intros <name>."

*RULE*: If the subgoal matches an hypothesis, Then use tactic "exact <hyp_name>."

*RULE*: If you have an hypothesis "<hyp_name>: <type1> -> <type2> -> ... -> <result_type>" OR an hypothesis "<hyp_name>: (forall <obj1>:<type1>, (forall <obj2>:<type2>, ... <result_type> ...))" OR any combination of "->" and "forall", AND you have hypotheses of type "type1", "type2"..., Then use tactic "pose" to create something of type "result_type".

*RULE*: If you have subgoal "<goal_type>" AND have hypothesis "<hyp_name>: <type1> -> <type2> -> ... -> <typeN> -> <goal_type>", Then use tactic "refine (<hyp_name> _ ...)." with N underscores.

*RULE*: If your subgoal is "True", Then use tactic "exact I".

*RULE*: If your subgoal is "~<type>" or "~(<term>)" or "(not <term>)", Then use tactic "intros".

*RULE*: If any hypothesis is "<name> : False", Then use tactic "case <name>."

*RULE*: If the current subgoal contains a function call with all its arguments, Then use the tactic "simpl".

*RULE*: If there is a hypothesis "<name>" of a created type AND that hypothesis is used in the subgoal, Then you can try the tactic "case <name>"

*RULE*: If the subgoal's top-most term is a created type, Then use "refine (<name_of_constructor> _ ...)".

*RULE*: If a hypothesis "<name>" is a created type with only one constructor, Then use "destruct <name> as <arg1> <arg2> ... " to extract its arguments

*RULE*: If a hypothesis "<name>" contain a function call with all its arguments, Then use the tactic "simpl in <name>"

*RULE*: If you have a subgoal that you want to ignore for a while, Then use the tactic "admit"

*RULE*: If the current subgoal starts "exists <name>, ..." Then create a witness and use "refine (ex_intro _ witness _)"

*RULE*: If you have a hypothesis "<name> : <a> = <b>" AND "<a>" in your current subgoal Then use the tactic "rewrite <name>"

*RULE*: If you have a hypothesis "<name> : <a> = <b>" AND "<b>" in your current subgoal Then use the tactic "rewrite <- <name>"

*RULE*: If you have a hypothesis "<name> : (<constructor1> ...) = (<constructor2> ...) OR "<name> : <constant1> = <constant2> Then use the tactic "discriminate <name>"

*RULE*: If there is a hypothesis "<name>" of a created type AND that hypothesis is used in the subgoal, AND the type has a recursive definition Then you can try the tactic "elim <name>"