# Library nahas_tutorial

Mike Nahas's Coq Tutorial
Started 2012-Nov-06
Version 1.2, 2019-Jan-22
Tested with Coq version 8.10+alpha

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 to write a proof and know about formal
logic. I tried to make this tutorial easy to read, so if you don't
know those things, keep reading and you
I also assume you understand a programming language. It doesn't
matter which programming language.
If you feel unprepared, the "further reading" section at the end has
useful links.
The easiest thing is to install "CoqIDE", the graphical version of
Coq. Windows and MacOS installers and the latest source code are
available at http://coq.inria.fr/download If you're running Linux,
your package manager probably has a recent-ish version.
(Debian/Ubuntu/Mint: "sudo apt install coqide", Fedora/CentOS might be
'su -c "yum install coq-coqide"'. Arch might be "sudo pacman -S
coqide")
If you like the Emacs text editor, the alternative is to run "coqtop",
the command-line version of Coq. It is also available at
http://coq.inria.fr/download The Linux package is usually called
"coq". To use it in Emacs, you have to also download and install the
"Proof General" Emacs mode. Is is available at
https://proofgeneral.github.io/ Linux package managers include some
version of it. (Debian/Ubuntu/Mint calls it "proofgeneral".
Fedora/CentOS might call it "emacs-common-proofgeneral". Arch might
call it "proofgeneral".)
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. If you can't find it, the
author hosts a recent version at
https://mdnahas.github.io/doc/nahas_tutorial.v)
Once you've made sure the file's name ends in ".v", start CoqIDE or
Emacs and load the file.
You need to know that this file was designed to work in a specific
version of Coq. Coq is a research tool and the developers
occasionally make small changes to its file format, so it is possible
that this file is for a different version of Coq. As you progress
through the tutorial, you may find a proof that your version of Coq
doesn't like. You can probably make it work, but if you can't, you
can try installing the latest version of CoqIDE and downloading the
latest version of the tutorial from the author's website.
(https://mdnahas.github.io/doc/nahas_tutorial.v)
)
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

*might*be able to pick them up.## Installing Coq

## 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. In my proofs, I 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 top-level interactions. Each of its commands starts with a capital letter: "Theorem", "Proof", and "Qed".
- The "tactics" language is used to write proofs. Its commands start with a lower-case letter: "intros" and "exact".
- The unnamed language of Coq terms is used to express what you want to prove. Its expressions use lots of operators and parentheses: "(forall A : Prop, A -> A)". (Technically, this language is a subset of the vernacular language, but it is useful to think of it as its own thing.)

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.

Look at the tactics used in this proof. (The tactics are the commands
between "Proof." and "Qed.") You should be familiar with "intros" and
"exact". The new one is "pose". We're going to use "pose" in a
forward proof. A "forward proof" creates larger and more complex
hypotheses in the context until one matches the goal. Later, we'll
see a "backward proof", which breaks the goal into smaller and simpler
subgoals until they're trivial.
In our current proof, the state right before the "pose" command is:
The subgoal is "B", so we're trying to construct a proof of B.
In the context we have "A_implies_B : A->B". "A->B", if you recall,
is equivalent to "(forall proof_of_A : A, B)", that is, for every
proof of A, we have a proof of B.
It happens that we have a proof of A in our context and it's called
(unoriginally) "proof_of_A". The expression "A_implies_B
proof_of_A" computes the proof of B that is associated with that
particular proof of A.
The command "pose" assigns the result of "A_implies_B proof_of_A" to
the new hypothesis "proof_of_B". (Note the annoying extra set of
parentheses that are necessary around the arguments to the "pose"
command.)
The proof ends with the "exact" command. We could have ended with
"exact (A_implies_B proof_of_A)", but I think it is easier to read
when it ends with with "exact proof_of_B."
This was a forward proof. Let's see a backward one.

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. For
example, "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.

This is the same theorem as before, except it has a forward proof
instead of a backward one.
In this proof, we can see the programming language underneath the
proof. "A_implies_B" is a function with type "A->B", so when it is
call with argument "proof_of_A", it generates a proof of B. The
"pose" command assigns the resulting value to the (unimaginative) name
"proof_of_B".
Likewise, "A_imp_B_imp_C" is a function with type "A->B->C". Called
with "proof_of_A" and "proof_of_B", it produces a proof of C which
becomes the hypothesis "proof_of_C".
There is a new vernacular command at the end: "Show Proof". If you
put your cursor right after it and press "control-option-right_arrow"
(in CoqIDE) or "C-C C-Enter" (in Proof General), you'll see the actual
code for the proof. It looks like this:
I formatted this version so that the correspondence to the proof is
clearer. The "intros" commands declare the parameters for the
function. "pose" declares constant values in the function. Lastly,
the "exact" command is used to return the result of the function. As
we go, you'll see the tight relationship in Coq between proofs and
code.
At this point, I want to emphasize that Coq proofs are not normally
this tedious or verbose. The proofs I've shown and the proofs I will
show are demonstrating the mechanics of how Coq works. I'm using
simple familiar types to make the mechanics' operations clear to you.
Coq's tactic language contains commands for automatic theorem proving
and for defining macros. Almost all the proofs in this tutorial are
simple enough to dispatch with a single Coq tactic. But when you
prove more complicated statements, you'll need all the commands I'm
teaching in this tutorial.
This helps explain why most Coq proofs are backwards. Once a
goal has been transformed into simple enough subgoals, those
subgoals can each be proved by automation.
So far, we've only worked with proofs, propositions, and Prop. Let's
add some more types!
The vernacular command "Inductive" lets you create a new type. I
wanted to introduce the boolean type, which has two values: "true" and
"false". The problem is that in addition to "true" and "false", Coq
has two other entities named "True" and "False", where the first
letter is capitalized. To keep the differences straight in your mind,
I'm going to introduce them to you all at once.
I find these names confusing. Recall that "Prop"s are things that may
have a proof. So I think capital-T "True" and capital-F "False" should
have been named "Provable" and "Unprovable" (or "AlwaysProvable"
and "NeverProvable"). The lower-case ones act like what you're
accustomed to.
Since we've been playing with Props, let's do some proofs with (the
badly named) "True" and "False" and we'll come back to the lower-case
"true" and "false" later.

(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

Theorem True_can_be_proven : True.

exact I.

Qed.

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.

The only new tactic here is "unfold". We said "Definition" says two
expressions are interchangeable. Well, "unfold" and "fold" will
interchange them. After the "unfold", we have
The "unfold" exposes that "~" is really an "->". And we're very
familiar with using the tactic "intros" to remove "->" at the front of
the subgoal. The command "intros proof_of_False" does just that.
After that, it goes as usual. "intros"s at the start and "exact" at
the end. It feels weird to have an hypothesis labeled
"proof_of_False" doesn't it? It's weird because we know False has no
proofs, so that hypothesis can never exist. Wouldn't it be better if
we could say that directly?...

============================ 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

Theorem thm_true_imp_true : True -> True.

Proof.

intros proof_of_True.

exact I.

"exact proof_of_True." also works.

Qed.

Theorem thm_false_imp_true : False -> True.

Proof.

intros proof_of_False.

exact I.

Theorem thm_false_imp_true : False -> True.

Proof.

intros proof_of_False.

exact I.

"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.

All of the above proofs should be obvious to you by now.
Below is another staple of logic: reduction to absurdity. If a
proposition has a proof and you prove that it cannot have a proof, then
you can conclude anything.

### 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 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

Theorem true_is_True: Is_true true.

Proof.

simpl.

exact I.

Qed.

*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

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

Proof.

intros a.

case a.

suppose a is true

simpl.

exact I.

exact I.

suppose a is false

simpl.

exact I.

Qed.

exact I.

Qed.

Take a look at the state after "case a.". There's two subgoals! I
said before that "case" creates subgoals for every possible
construction of its argument. So far, we've only used "case" with
hypotheses of type "False". False has no constructors, so it
generates no subgoals and ends our proofs.
Hypotheses of type "bool" have two possible constructors "true" and
"false". Thus, "case a" creates two new subgoals - one where "a" has
been replaced by "true" and a second where "a" has been replaced by
"false".
NOTE: The replacement of "a" by "true" (or "false") only happens
inside the subgoal. It does NOT happen in the hypotheses. It is
sometimes important to control where "a" is before calling "case"!
I believe it is good style to label the two different cases. I do
that with the comment "suppose <hyp> is <constructor>". Since the
definition of "bool" listed "true" before "false", the subgoal where
"a" is "true" becomes the current subgoal. Once we prove it, the case
where "a" is "false" will become the current subgoal.
Let's do one more example.

*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

simpl.

intros proof_of_True.

exact I.

intros proof_of_True.

exact I.

suppose a is false

simpl.

intros proof_of_False.

case proof_of_False.

Qed.

intros proof_of_False.

case proof_of_False.

Qed.

In this example, I had to control the location of "a" when using the
tactic "case".
Usually, we would do "intros a" followed by another "intros" to move
everything before the "->" into a hypothesis. If we did this, one
usage of "a" would move from the subgoal into a hypothesis and "case
a" would NOT replace it with "true" or "false". (The "case" tactic
only changes the subgoal.) And we'd be unable to prove the theorem.
Instead, I left "a" in the subgoal and delayed the second "intros"
until after the "case" command. (In fact, after the "simpl" too.) As
a result, all usages of "a" were replaced by "true" or "false" and the
theorem was provable.
One of the most amazing things about Coq is its fundamental rules are
so simple that even things like "and" and "or" can be defined in terms
of them. I'll start with "or" because it shows some special features.
Before showing you the definition for "or", I want you to see some
examples so that the definition will make sense. In the examples
below, imagine you have a hypothesis with a natural number "x".
I said the result of "or" is a proposition - something that might have
a proof. So how do we create a proof of "or"? For that, we need to
see the definition...
This vernacular command does four things.
One way to think of this is to say "(or A B)" creates a type and
"(or_introl proof_of_A)" and "(or_intror proof_of_B)" are instances of
that type. In fact, the ONLY way to create things of type "or" is by
using the constructors "or_introl" and "or_intror".
It is important to note that constructors, like "or_introl" and
"or_intror", are functions that can be called, but do not have any
definitions. They are not made of calls to other functions. They
cannot be executed and the result looked at. The tactic "simpl" will
not remove them. They are opaque constants.
The vernacular command "Inductive" creates new types. It's called
"Inductive" since it lets you create inductive types, although none of
our types so far has been inductive. (That will change!) It is the
same command we saw earlier to declare other new types with their
constants.
Right now, we want to play with "or", so let's get proving!

# 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.

This proof should have gone pretty much as you expected. The only
complication is that the "pose" command could not infer the type of B
from "or_introl proof_of_A", so the type had to be given explicitly by
putting ": A \/ B" at the end. "or_introl proof_of_A" by itself is a
proof of "A \/ anything".
The proof is shorter without the "pose", since Coq knows the type from
the subgoal we're trying to prove. You can see this in a similar proof
using "or_intror" below.

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)

intros proof_of_A.

refine (or_intror _).

exact proof_of_A.

refine (or_intror _).

exact proof_of_A.

suppose A_or_B is (or_intror proof_of_B)

intros proof_of_B.

refine (or_introl _).

exact proof_of_B.

Qed.

refine (or_introl _).

exact proof_of_B.

Qed.

This proof uses the tactic "case" to consider the two different ways
we might have constructed the hypothesis "A \/ B". One possibility
was using "(or_introl proof_of_A)", which would have meant there was a
proof of "A". For that case, the tactic puts "A ->" at the front of the
subgoal and we use "intros proof_of_A." to move the proof into the context.
Notice that "case" changed the subgoal and not the context. "case"
never changes the context - that's a useful property to know (and look
out for) when working with it.
The other possibility for creating the hypothesis "A \/ B" was that
the constructor "or_intror" was used. For it to be used, there had to
exist a proof of "B". So, for the second case created by "case", the
subgoal has "B ->" at the front and we use "intros proof_of_B." to move
it into the context.
Once the "proof_of_A" or "proof_of_B" is in the context, the proofs of
each subgoal follow the pattern we've seen before.
Now that we've seen how "or" works, let's take a look at "and".
I think we can go straight to the definition.
As you could expect, "and" is a function that takes two Props and
returns a Prop. That's the exact same as we saw with "or". However,
while "or" had two constructors that each took one argument, "and" has
a single constructor that takes two arguments. So, the one and only
way to create something of type "(and A B)" is to use "(conj
proof_of_A proof_of_B)".
Let's go straight to a proof!

## 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.

Pretty simple proof. There is only one constructor for things of type
"(and A B)", which is "conj". It takes two arguments, which after
"refine", become two subgoals. The proofs of each are trivial.
After seeing "or", "and" should be easy, so let's jump to the complex
proof.

### 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)

intros proof_of_A proof_of_B.

refine (conj _ _).

exact proof_of_B.

exact proof_of_A.

Qed.

refine (conj _ _).

exact proof_of_B.

exact proof_of_A.

Qed.

The "case" tactic looked at all the different ways to construct an
"and" in the hypothesis and found there was only one: "(conj
proof_of_A proof_of_B)". So, the tactic created one subgoal with both
of those required values at the front of the subgoal.
Similarly, when we need to build an "and" to satisfy the subgoal,
there is only one way to construct an "and": "conj" with two
arguments. Thus, after "refine" two subgoals were created, one
requiring something of type "B" and the other requiring something of
type "A".
The previous proof used "case" to create subgoals for all constructors
for something of type "A /\ B". But there was only one constructor.
So, we really didn't need to indent. Nor should we waste a line with
a comment saying "suppose". And it'd be really nice if we didn't have
to write the "intros" command.
Luckily, Coq provides a tactic called "destruct" that is a little more
versatile than "case". I recommend using it for types that have a
single constructor. The format is:
I put a comment with the name of the constructor inside the square
braces.
The result is a much shorter and cleaner proof.

### 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

simpl.

refine (or_introl _).

exact I.

refine (or_introl _).

exact I.

suppose a,b is true, false

simpl.

exact (or_introl I).

exact (or_introl I).

suppose a,b is false, true

exact (or_intror I).

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

simpl.

exact I.

exact I.

suppose a,b is true, false

exact I.

suppose a,b is false, true

exact I.

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.

Wow! We're not in Kansas any more!
First, I used "case" to split the "\/" hidden inside the "<->".
Second, inside each of those branches, I did "case a,b", which created
4 subgoals, for every possible combination of the two constructors. I
thought the proof was clearer that way, even though doing "case a"
followed by "case b" might have been shorter.
The proofs for when "a" or "b" were true were easy. They were all the
same proof. You can see that I make the proof shorter as I went along
When both "a" and "b" were false, I decided it was best to do "case"
on an instance of False. For "orb", that was pretty easy. I did
"simpl in H", which executed functions calls inside a hypothesis.
That gave me an hypothesis of type False, and "case H" ended the
subgoal.
However, for the inductive type "or", it was more complicated. I used
"case H" to consider the different ways of constructing the "or".
Both constructors - "or_introl" and "or_intror" - lead to a False
hypothesis.
That was a real proof. Welcome to the big leagues.
Let's try it with "andb" and "/\".

- 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

simpl.

exact (conj I I).

exact (conj I I).

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

simpl.

exact I.

exact I.

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".

Theorem negb_is_not : (forall a, Is_true (negb a) <-> (~(Is_true a))).

Proof.

admit.

delete "admit" and put your proof here.

Admitted.

when done, replace "Admitted." with "Qed."
Like "and" and "or", the concepts of "there exists" and "equality" are
not fundamental to Coq. They are concepts defined inside of it. Only
"forall" and the notion of creating a type with constructors is
fundamental to Coq.
In Coq, you cannot just declare that something exists. You must prove
it.
For example, we might want to prove that "there exists a bool 'a' such
that (Is_true (andb a true))". We cannot just state that the
"bool" exists. You need to produce a value for "a" - called the
witness - and then prove that the statement holds for the witness.
The definition and operator are:
The proposition "ex P" should be read: "P is a function returning a
Prop and there exists an argument to that function such that (P arg)
has been proven". The function "P" is known as "the predicate". The
constructor for "ex P" takes the predicate "P" , the witness (called
"x" here) and a proof of "P x" in order to return something of type
"ex P".
"exists ..., ..." is an operator to provide a friendly notation. For
"and" and "or", we did the same with "/\" and "\/". For existence,
the usually operator is a capital E written backwards, but that's
difficult to type, so Coq uses the word "exists".
Let's test this out with the easy theorem I already mentioned.

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

simpl.

exact I.

Qed.

exact I.

Qed.

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

### More existence

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

Proof.

intros b.

case b.

b is true

pose (witness := true).

refine (ex_intro _ witness _).

simpl.

exact I.

refine (ex_intro _ witness _).

simpl.

exact I.

b is false

pose (witness := false).

refine (ex_intro _ witness _).

simpl.

exact I.

Qed.

refine (ex_intro _ witness _).

simpl.

exact I.

Qed.

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

exact (eqb_a_a b).

Qed.

Qed.

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
convertible 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>.".Theorem andb_sym : (forall a b, a && b = b && a).

Proof.

intros a b.

case a, b.

suppose a,b is true,true

simpl.

exact (eq_refl true).

exact (eq_refl true).

suppose a,b is true,false

simpl.

exact (eq_refl false).

exact (eq_refl false).

suppose a,b is false,true

simpl.

exact (eq_refl false).

exact (eq_refl false).

suppose a,b is false,false

simpl.

exact (eq_refl false).

Qed.

exact (eq_refl false).

Qed.

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.

To prove this, once again I had to delay calling "intros" until after
"case". If I did not, "a" in "a_eq_neg_a" would not get replaced
"true" or "false". I also used a new tactic: "discriminate".
"discriminate" operates on a hypothesis where values of inductive type
are compared using equality. If the constructors used to generate the
type are the different, like here where we have "true = false", then
Coq knows that situation can never happen. It's like a proof of
False. In that case, "discriminate <hypname>." ends the subgoal.
When working with inductive types, you will use "discriminate" to
eliminate a lot of cases that can never happen.
To really show off equality, we'll need something more numerous than
just 2 booleans. Next up is natural numbers - an infinite set of
objects - and induction - which allows us to prove properties about
infinite sets of objects!
The natural numbers are 0, 1, 2, 3, 4, ... . They are the simplest
mathematical concept that contain an unbounded number of values.
In 1889, Peano published a simple set of axioms (fundamental rules)
that defined the natural numbers and how to prove things about them.
Peano's axioms have become the standard way in logic of talking about
and manipulating the natural numbers. More complex schemes - like the
decimal numbers we usually use - are justified by proving them
equivalent to Peano's axioms.
Peano's definition of natural numbers is:
"(S n)" is spoken as "the successor of n" but you should think about
it as "1 + n". If we were to list the first few of Peano's natural
numbers, they would be:
Peano's natural numbers are represented in Coq by the type "nat".
So, Coq's natural numbers exactly matches the definition of Peano.
If we want to do something with "nat"s, we need some functions. Here
is how Peano's definition of addition looks in Coq.
Previously, we used the vernacular command "Definition" to define a
function. The command here is "Fixpoint". "Fixpoint" must be used
any time you define a recursive function. It's hard to see that
"plus" calls itself because the recursive call is hidden by the "+" in
"p + m".
We know that (2 + 3) = 5, so let's see how that property holds in Coq.
Below, the difference between lines is one execution of a function
call to "plus".
Each execution of "plus" strips an "S" off the front of the first
number and puts it in front of the recursive call to "plus". When the
first parameter is "O", "plus" returns the second argument.
Remember that "O" and "S" are constructors - they're opaque functions
that were created when we declared "nat". There is no way to execute
them. Therefore, "(S (S (S (S (S O))))))" does not have any function
calls that can be executed and, therefore, is the canonical form of
the number 5.
The proof of "2 + 3 = 5" only need one call to "simpl" to get it to
the canonical form.

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

As you can see by "eq_refl 5", Coq will translate decimal numbers into
terms of "nat" automatically. This means capital-letter "O" and the
digit "0" are really the same term, which prevents a lot of mistakes.
There are ways to instruct Coq to treat decimals as other types, such
as integers, rationals, etc.
We can convince ourselves that the function "plus" has all the
properties associated with addition, by proving those properties. So,
let's prove them!

Theorem plus_O_n : (forall n, O + n = n).

Proof.

intros n.

simpl.

exact (eq_refl n).

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.

Check nat_ind.

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.

Theorem plus_n_O : (forall n, n + O = n).

Proof.

intros n.

elim n.

base case

simpl.

exact (eq_refl O).

exact (eq_refl O).

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".

*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>.".### Induction tactic

Theorem plus_n_O__again : (forall n, n + O = n).

Proof.

intros n.

induction n as [|n' inductive_hypothesis].

Proof.

intros n.

induction n as [|n' inductive_hypothesis].

base case

simpl.

exact (eq_refl O).

exact (eq_refl O).

inductive case

simpl.

rewrite inductive_hypothesis.

exact (eq_refl (S n')).

Qed.

rewrite inductive_hypothesis.

exact (eq_refl (S n')).

Qed.

So, the "induction" tactic does the same thing as "elim.", except the
names of the created variables are listed in the tactic, rather than
being assigned later using "intros" in the inductive case of the proof.
The "induction" command creates 2 subgoals, one for the base case and
another for the inductive case, and after the "as" keyword, there are
2 lists of variable names, one for the base case and one for the
inductive case. Those lists are separated by vertical bars ('|')
inside the square brackets. The base case doesn't create any
variables, so its list is empty. The inductive case creates two
variables, and they are named "n'" and "inductive_hypothesis".
I said the "induction" command was similar to "destruct" and, if the
type "destruct"ed has more than one constructor, the "destruct"
command will create subgoals for each constructor and the command
needs a list of variable names for each constructor. For example, the
type "or" has two constructors. Recall that something of type "or A
B" can be created by "or_introl proof_of_A" or "or_intror proof_of_B".
If I "destruct" an "or A B", it will create two subgoals and the
"destruct" needs to have a list of variables for each. To
demonstrate this, I'll redo the proof that or commutes.

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

Proof.

intros A B.

intros A_or_B.

destruct A_or_B as [proof_of_A | proof_of_B].

suppose A_or_B is (or_introl proof_of_A)

refine (or_intror _).

exact proof_of_A.

exact proof_of_A.

suppose A_or_B is (or_intror proof_of_B)

refine (or_introl _).

exact proof_of_B.

Qed.

exact proof_of_B.

Qed.

In my proofs, I like to use "case" and "elim" and only use "destruct"
for types with a single constructor. However, some people prefer to
use "destruct" and "induction" for every proof. The writers of Coq
are talking about removing this duplication and may remove "case" and
"elim" in the future.
If you want to use "destruct" and "induction", it is helpful to use
the Vernacular command "Print", which prints out a definition and
shows you how many constructors there are and which variables you need
to name for each one.

Print or.

Print nat_ind.

Print nat_ind.

### Addition is Symmetric

Theorem plus_sym: (forall n m, n + m = m + n).

Proof.

intros n m.

elim n.

Proof.

intros n m.

elim n.

base case for n

elim m.

base case for m

exact (eq_refl (O + O)).

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"

Theorem minus_is_funny : (0 - 1) = (0 - 2).

Proof.

simpl.

exact (eq_refl 0).

Qed.

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

Require Import List.

## 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 an 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 crashes. But if you want 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.
Definition my_hd_for_nat_lists

:=

hd nat 0.

:=

hd nat 0.

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.

Compute my_hd_for_nat_lists nil.

Prints "= 0 : nat".

Compute my_hd_for_nat_lists (5 :: 4 :: nil).

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.

Definition hd_error (A : Type) (l : list A)

:=

match l with

| nil => None

| x :: _ => Some x

end.

:=

match l with

| nil => None

| x :: _ => Some x

end.

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

Compute hd_error nat nil.

Prints "= None : option nat".

Compute hd_error nat (5 :: 4 :: nil).

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 proof 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

Definition tl (A : Type) (l:list A) :=

match l with

| nil => nil

| a :: m => m

end.

match l with

| nil => nil

| a :: m => m

end.

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.

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

Proof.

admit.

delete "admit" and put your proof here.

Admitted.

when done, replace "Admitted." with "Qed."

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

Proof.

admit.

delete "admit" and put your proof here.

Admitted.

when done, replace "Admitted." with "Qed."

Theorem app_comm_cons : forall A (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y.

Proof.

admit.

delete "admit" and put your proof here.

Admitted.

when done, replace "Admitted." with "Qed."

Theorem app_assoc : forall A (l m n:list A), l ++ m ++ n = (l ++ m) ++ n.

Proof.

admit.

delete "admit" and put your proof here.

Admitted.

when done, replace "Admitted." with "Qed."

Theorem app_cons_not_nil : forall A (x y:list A) (a:A), nil <> x ++ a :: y.

Proof.

admit.

delete "admit" and put your proof here.

Admitted.

when done, replace "Admitted." with "Qed."
I designed this tutorial to give you just enough to get started in
Coq. You know enough concepts to have an idea of how things work in
Coq and how things relate. You may only know a small number of simple
tactics, but they're powerful enough that you can prove real theorems.
As you get more experience, you'll see more complex concepts and use
more tactics. You may even get to use SSReflect, which is a separate
tactics language! As you read more Coq proofs, you'll also see
different styles for writing proofs. (Any expert will tell you that
this tutorial's simple style is strikingly different from that used in
their proofs.)
I hope you've seen some of the power and possibilities of Coq. Many
expert provers consider Coq proofs a puzzle and I wish you luck in
solving your puzzles!
HTML and Coq versions of the tutorial are hosted on the author's professional website.
https://mdnahas.github.io/doc/nahas_tutorial.html
https://mdnahas.github.io/doc/nahas_tutorial.v
The author, Michael Nahas, can be reached at michael@nahas.com
Coq uses a lot of concepts that I didn't explain. Below are some good
sources on those topic.
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, you can
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 a deep 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.
https://ocaml.org
To learn more about Coq, I found the textbook "Software Foundations"
readable. It focuses on proving programs correct. You can also look
at Coq's documentation webpage.
https://softwarefoundations.cis.upenn.edu/
https://coq.inria.fr/documentation

# Conclusion

# Postscripts

## Contact

## Further Reading

## Vernacular commands

- "Theorem" starts a proof.
- "Qed" ends a proof.
- "Admitted" ends an incomplete 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>.".