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 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.
(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 might be able to pick them
up.
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
Prerequisites
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
- 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
A : Prop ============================ A -> A
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)
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.)
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".
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
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".
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.
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
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.
RULE: If your subgoal is "True",
Then use tactic "exact I.".
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
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".
RULE: If your subgoal is "~<type>" or "~(<term>)" or "(not <term>)",
Then use tactic "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!
RULE: If any hypothesis is "<name> : False",
Then use tactic "case <name>.".
We can use True and False to see that Coq's "->" operator really does
act like "implication" from logic.
-> 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.
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.
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.
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>.".
Let's do one more example.
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.
RULE: If the subgoal's top-most term is a created type,
Then use "refine (<name_of_constructor> _ ...).".
Let's prove something a little more complicated...
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.
We just saw that "and" and "or" work with Props and are inductive
types. In this section, I'll introduce "andb" and "orb" for working
with "bool"s. Rather than inductive types, "andb" and "orb" are
functions.
To be clear, "and" and "or" are "inductive types" - that is, types we
defined where instances can only be produced by calling opaque
functions called constructors. Those constructors are things like
"or_introl", "or_intror", and "conj".
In fact, the type "bool" is also inductive type. It has two
constructors: "true" and "false". These constructors take no
arguments, so they are closer to constants than "opaque functions".
To manipulate "bool"s, we could use an inductive type, but it's much
easier just to define a function. We've already seen one function on
bools: "eqb", which did equality. Some other functions that Coq defines are:
These are "and", "or", and "not" (but called "negation" for some reason).
Like with "eqb", the names all ended in "b" to indicate they work with
"bool"s. Two of these functions also come with operators:
We'll get some good practice proving that these functions on bools are
equivalent to our inductive types on Props. As part of this, we'll
need a form of equality for propositions that is called "if and only
if" or "double implication".
You should know everything you see in the proofs below. Remember,
"simpl" is used to execute a function and "case" and "destruct" are
used on inductive types.
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.
RULE If a hypothesis "<name>" contain a function call with all its arguments,
Then use the tactic "simpl in <name>.".
Let's try it with "andb" and "/\".
- combining "refine" and "exact" and skipping right over "simpl".
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."
RULE: If you have a subgoal that you want to ignore for a while,
Then use the tactic "admit.".
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.
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 _)"
We often use "exists" and "forall" at the same time. Thus, we end up
with proofs like the following.
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.
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>.".
Let's try something that explicitly relies on convertibility. Recall,
"andb" is and for "bools" and that it is represented by the operator
"&&".
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.
RULE: If you have a hypothesis
"<name> : (<constructor1> ...) = (<constructor2> ...)
OR "<name> : <constant1> = <constant2>
Then use the tactic "discriminate <name>.".
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".
WARNING: The "O" here is the capital-letter O, not the number zero.
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".
 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.
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.
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 could
- define a function "P n" that represents "O + n = n"
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
- 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>.".
Just as the "case" tactic has a similar "destruct" tactic, the "elim"
tactic has a similar "induction" tactic. Let's look at the previous
proof, but using this new tactic.
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 verical 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 a 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 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.
"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!
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 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 crashes. 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 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.
Thus, we can do:
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<EMAIL_ADDRESS>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
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>.".
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.


Across: 7. Coins peculiar expression for the Guardian (5) 8. Without proper leadership, most race discrimination leads to this (9) 10. Early applause for popular breakfast food (3) 11. Not affected by former parliamentarian in French conjunction (6) 12. Bank reported tax (4) 14,13 dn. 16 down said it's a sin (2,4,1,11) 15. 10 returns 100 with a party food (7) 16. Valour - it can regularly be found close to the heart (5) 17. Has-been turned 5 down (3) 18. Food used by fake babies (5) 20. During commotion, encountered returning nuisance (7) 22. Solo tip pass (4,3) 24. Unfriendly at a hundred years of age (4) 25. Friction following revolutionary angel (6) 26. Half-meal racket (3) 28. Rocking reggae set to cause division (9) 29. Hernia with decapitation? An exaggeration perhaps! (5) Down: 1. Absurdly rich, Jake dictates his own destination (8) 2. Regularly found among the pages of Dante - relive such chaos! (11) 3,17. Head off and adjust a timepiece before fellow second from 22,27 (2,3,1,8) 4. Idealists lost loony leader from erratic pulsation (8) 5. Cut back 17 across (3) 6. Came in dancing as a form of entertainment (6) 7. One who seeks the talented young 23 ... (5) 9. ... might search this town (7) 13. see 14 ac 16,23. Novel lawyer worked cat suit with bird (7,5) 17. see 3 dn 19. Banged head on street as a form of entertainment (8) 21. Abuse in glam rock (6) 22,27. Repeal her "one novel writing"! (6,3) 23. see 16 dn 27. see 22 dn


Gerudo
The all female race of Hyrule. The cut-throat,
don't-get-in-my-way, headstrong women that rule the desert.  Their
city is heavily guarded and watched to ensure no men are allowed
entry.  Until this time comes, a
female is the chief of the tribe and the role of leader is passed
from mother to daughter as she comes of age. While the tribe
consists of only women, many adventurers have made fools of
themselves in attempts to steal Gerudo treasure or to sneak into
the town; most of the time these adventurers end up running with
tails between their legs and stories of what seem to be
nightmares. The Gerudo will acknowledge formidable warriors and
will often even allow trade amongst them, but only outside of the
city walls. The weapons of choice for the Gerudo consist of long
swords, specifically scimitars, and pole arms, specifically
halberds. These women are known to be in your face at the start of
combat and their movements almost look like those of a dance. Some
Gerudo are capable of magic, and when this arises, the magic is
normally of the lightning persuasion. While most Gerudo do stay
within the confines of their town and the desert, some go off in
search of a life mate. If these Gerudo do find a mate, they
usually end up leaving the Gerudo town, but will end up returning
in order to trade or visit some of their old friends.


ID Card Generator
Enter Student Details
Enter Name:
College Name:
Enter Location:
Upload an image
Generate Card
Generated ID Card
Name:
Mehul
College Name:
Dev College
Location:
India


"Hello! Writers"
The 2021 International Writers' Conference is here!
The International Writers' Conference is the largest gathering of writers and aspiring writers all over the world. It provides one-of-a-kind event for successful writers to engage readers, aspiring writers, and opportunity for book lovers to meet their favourite writers. The 2021 edition will take place in Athens.
2021.07.09(FRI) ~ 11(SUN)
@ Zappeion Conference & Exhibition Center, Athens, Greece
Main Program
-
- Lecture
- Lecture on what it is like to be a writer. The difficulties, benefits and tips on how to hone your craft to become a better writer
-
- Book Launch
- A Book Launch event for book lovers. An opportunity to be among the first reader of highly anticipated books
-
- Forum
- Literary conversation and celebration. Audience get an opportunity to have a chat with their favourite writer
-
- Workshop
- Workshop to give writers and upcoming writers the tips and tools they need for writing and publishing success
-
- Network
- Meet bestselling authors, agents,editors, and marketing professionals. Get insider details on the business of writing


Today's schedule
Without drag handle (entire item is draggable - including with the keyboard!)
- ReorderStand-up
- ReorderSprint planning
- ReorderRetrospective
- ReorderBacklog grooming
- ReorderEnd of sprint demo
Without drag handle (entire item is draggable - including with the keyboard!)


airflow.executors.local_executor
¶
LocalExecutor runs tasks by spawning processes in a controlled fashion in different modes. Given that BaseExecutor has the option to receive a parallelism parameter to limit the number of process spawned, when this parameter is 0 the number of processes that LocalExecutor can spawn is unlimited.
The following strategies are implemented: 1. Unlimited Parallelism (self.parallelism == 0): In this strategy, LocalExecutor will spawn a process every time execute_async is called, that is, every task submitted to the LocalExecutor will be executed in its own process. Once the task is executed and the result stored in the result_queue, the process terminates. There is no need for a task_queue in this approach, since as soon as a task is received a new process will be allocated to the task. Processes used in this strategy are of class LocalWorker.
2. Limited Parallelism (self.parallelism > 0): In this strategy, the LocalExecutor spawns the number of processes equal to the value of self.parallelism at start time, using a task_queue to coordinate the ingestion of tasks and the work distribution among the workers, which will take a task as soon as they are ready. During the lifecycle of the LocalExecutor, the worker processes are running waiting for tasks, once the LocalExecutor receives the call to shutdown the executor a poison token is sent to the workers to terminate them. Processes used in this strategy are of class QueuedLocalWorker.
Arguably, SequentialExecutor could be thought as a LocalExecutor with limited parallelism of just 1 worker, i.e. self.parallelism = 1. This option could lead to the unification of the executor implementations, running locally, into just one LocalExecutor with multiple modes.
Module Contents¶
-
class
airflow.executors.local_executor.
LocalWorker
(result_queue)[source]¶ Bases:
multiprocessing.Process
,airflow.utils.log.logging_mixin.LoggingMixin
LocalWorker Process implementation to run airflow commands. Executes the given command and puts the result into a result queue when done, terminating execution.
-
class
airflow.executors.local_executor.
QueuedLocalWorker
(task_queue, result_queue)[source]¶ Bases:
airflow.executors.local_executor.LocalWorker
LocalWorker implementation that is waiting for tasks from a queue and will continue executing commands as they become available in the queue. It will terminate execution once the poison token is found.
-
class
airflow.executors.local_executor.
LocalExecutor
[source]¶ Bases:
airflow.executors.base_executor.BaseExecutor
LocalExecutor executes tasks locally in parallel. It uses the multiprocessing Python library and queues to parallelize the execution of tasks.
-
class
_UnlimitedParallelism
(executor)[source]¶ Bases:
object
Implements LocalExecutor with unlimited parallelism, starting one process per each command to execute.
-
class


Classes
CssAbsPrimitiveLengthValue
CssAbsPrimitiveValue
CssAbsValue
CssCharsetRule
The CSSCharsetRule interface represents a @charset rule in a CSS style sheet. The value of the encoding attribute does not affect the encoding of text data in the DOM objects; this encoding is always UTF-16. After a stylesheet is loaded, the value of the encoding attribute is the value found in the @charset rule. If there was no @charset in the original document, then no CSSCharsetRule is created. The value of the encoding attribute may also be used as a hint for the encoding used on serialization of the style sheet. The value of the @charset rule (and therefore of the CSSCharsetRule) may not correspond to the encoding the document actually came in; character encoding information e.g. in an HTTP header, has priority (see CSS document representation) but this is not reflected in the CSSCharsetRule.
CssCollectedProperty
Used internally to store collected properties.
CssCollectedStyleDeclaration
Used internally for collection of styles for a specific element
CssColor
The RGB-Color interface is used to represent any RGB color value.
CssFontFaceRule
The ICssFontFaceRule interface represents a @font-face
rule in a CSS style sheet.
The @font-face
rule is used to hold a set of font descriptions.
CssImportRule
The CSSImportRule interface represents a @import rule within a CSS style sheet. The @import rule is used to import style rules from other style sheets.
CssMediaRule
The CSSMediaRule interface represents a @media rule in a CSS style sheet. A @media rule can be used to delimit style rules for specific media types.
CssNumber
CssPageRule
The CSSPageRule interface represents a @page rule within a CSS style sheet. The @page rule is used to specify the dimensions, orientation, margins, etc. of a page box for paged media.
CssPrimitiveAngleValue
CssPrimitiveColorValue
CssPrimitiveLengthValue
CssPrimitiveRgbValue
CssPrimitiveValue
This implements the ICssPrimitiveValue interface which represents a single CSS value.
CssPrimitiveVarsValue
CssPropertyProfile
CssRect
The Rect interface is used to represent any rect value. This interface reflects the values in the underlying style property. Hence, modifications made to the CSSPrimitiveValue objects modify the style property.
CssRule
CssRuleList
The CSSRuleList interface provides the abstraction of an ordered collection of CSS rules. The items in the CSSRuleList are accessible via an integral index, starting from 0.
CssStyleDeclaration
The ICssStyleDeclaration interface represents a single CSS declaration block. This interface may be used to determine the style properties currently set in a block or to set style properties explicitly within the block.
While an implementation may not recognize all CSS properties within a CSS declaration block, it is expected to provide access to all specified properties in the style sheet through the ICssStyleDeclaration interface. Furthermore, implementations that support a specific level of CSS should correctly handle CSS shorthand properties for that level. For a further discussion of shorthand properties, see the CSS2Properties interface.
This interface is also used to provide a read-only access to the computed values of an element. See also the ViewCSS interface.
Note: The CSS Object Model doesn't provide an access to the specified or actual values of the CSS cascade
CssStyleRule
The CSSStyleRule interface represents a single rule set in a CSS style sheet.
CssStyleSheet
The ICssStyleSheet interface is a concrete interface used to represent a CSS style sheet i.e., a style sheet whose content type is "text/css".
CssUnknownRule
The CSSUnknownRule interface represents an at-rule not supported by this user agent.
CssValue
This implements the ICssValue interface, which represents a simple or a complex value. A ICssValue object only occurs in a context of a CSS property.
CssXmlDocument
A XmlDocument with CSS support
CssXmlElement
CssXPathSelector
StaticSection
Creates a static section for a CssXmlDocument. Typical use: using(StaticSection.Use(doc)) { // blah blah }
Interfaces
ICssCharsetRule
The ICssCharsetRule
interface represents a @charset
rule in a CSS style sheet. The value of the
encoding attribute does not affect the encoding of text data in the DOM objects; this encoding is
always UTF-16. After a stylesheet is loaded, the value of the encoding attribute is the value found in the
@charset
rule. If there was no @charset
in the original document, then no ICssCharsetRule
is created.
The value of the encoding attribute may also be used as a hint for the
encoding used on serialization of the style sheet.
ICssColor
The RGB-Color interface is used to represent any RGB color value. This interface reflects the values in the underlying style property. Hence, modifications made to the ICssPrimitiveValue objects modify the style property.
ICssCounter
The Counter interface is used to represent any counter or counters function value. This interface reflects the values in the underlying style property.
ICssFontFaceRule
The ICssFontFaceRule
interface represents a @font-face
rule in a CSS style sheet.
The @font-face
rule is used to hold a set of font descriptions.
ICssImportRule
The ICssImportRule
interface represents a @import
rule within a CSS style sheet.
The @import
rule is used to import style rules from other style sheets.
ICssMediaRule
The ICssMediaRule
interface represents a @media
rule in a CSS style sheet.
A @media
rule can be used to delimit style rules for specific media types
ICssPageRule
The ICssPageRule
interface represents a @page
rule within a CSS style sheet.
The @page
rule is used to specify the dimensions, orientation, margins, etc. of a page box for paged media.
ICssPrimitiveValue
The ICssPrimitiveValue
interface represents a single CSS value.
ICssRect
The ICssRect
interface is used to represent any rect value. This interface reflects the values
in the underlying style property. Hence, modifications made to the ICssPrimitiveValue
objects modify the style property.
ICssRule
The ICssRule
interface is the abstract base interface for any type of CSS statement.
This includes both rule sets and at-rules. An implementation is expected to preserve all rules
specified in a CSS style sheet, even if the rule is not recognized by the parser.
Unrecognized rules are represented using the ICssUnknownRule interface.
ICssRuleList
The ICssRuleList
interface provides the abstraction of an
ordered collection of CSS rules.
ICssStyleDeclaration
The ICssStyleDeclaration
interface represents a single CSS declaration block.
ICssStyleRule
The ICssStyleRule
interface represents a single rule set in a CSS style sheet.
ICssStyleSheet
The ICssStyleSheet
interface is a concrete interface used to represent a CSS style sheet
i.e., a style sheet whose content type is text/css
.
ICssUnknownRule
The ICssUnknownRule
interface represents an at-rule not supported by this user agent.
ICssValue
The ICssValue
interface represents the current computed value of a CSS property.
ICssValueList
The ICssValueList
interface provides the abstraction of an ordered collection of CSS values.
ICssView
This interface represents a CSS view. The GetComputedStyle(XmlElement, String) method provides a read only access to the computed values of an element.
IDocumentCss
This interface represents a document with a CSS view.
IDomImplementationCss
This interface allows the DOM user to create a ICssStyleSheet outside the context of a document. There is no way to associate the new ICssStyleSheet with a document in DOM Level 2.
IElementCssInlineStyle
Inline style information attached to elements is exposed through the style attribute.
Enums
CssPrimitiveType
The CssPrimitiveType
enumeration contains the list of possible primitive value types in CSS.
This class is an extension of the CSS spec. The CSS spec has a list of constants instead of an enum class.
CssRuleType
The CssRuleType
Enum contains the possible Rule Type Values. This is an extension of the CSS specification.
The spec contains only a list of contstant in the ICssRule interface.
CssStyleSheetType
The different types of CssStyleSheets
CssValueType
The CssValueType
Enum contains the possible CSS Value Types. This is an extension to the
CSS specification. The specification has a list of constants defined within the ICssValue Interface


{% load socialaccount %} {% load account %}
{{userdata.bio}}
Level: {{level}}
Distance Traveled (mi): {{ workout.distance}} Duration of Run: {{ workout.length}} Calories Burned: {{ workout.calories}} {% if workout.notes %} Notes: {{ workout.notes }} {% endif %}
Duration of Workout: {{ workout.length}} Sets: {{ workout.sets}} Reps: {{ workout.reps}} Weight: {{ workout.weight}} Total Weight Lifted (lbs): {{ workout.total_weight_lifted}} Calories Burned: {{ workout.calories}} {% if workout.notes %} Notes: {{ workout.notes}} {% endif %}
Calories Burned: {{ workout.calories}} Duration of Workout: {{ workout.length}} Distance: {{ workout.distance}} Sets: {{ workout.sets}} Reps: {{ workout.reps}} Weight: {{ workout.weight}} Total Weight Lifted (lbs): {{ workout.total_weight_lifted}} {% if workout.notes %} Notes: {{ workout.notes}} {% endif %}
You have no workouts to display
{% else %}{{userdata.user.first_name}} has no workouts to display
{% endif %} {% endif %}{% if is_current_user %}
{% endif %} {% if following %}You are not following anyone ☹
{% else %}{{userdata.user.first_name}} is not following anyone ☹
{% endif %} {% endif %}{% if followers %}
You have no followers ☹
{% else %}{{userdata.user.first_name}} has no followers ☹
{% endif %} {% endif %}


Contents
Previous
Next
Other experiments were performed to test if single-precision data can
be considered sufficient for SCIARA simulations by comparing results
produced by the GPU version with those produced by the CPU (sequential)
version with single precision data (i.e., float
type
variables), and those produced still by the same GPU version against a
double precision CPU implementation (i.e., double
type
variables). In each case, comparison results were satisfactory,
especially for the double-precision versions, where the areal
extensions of simulations resulted the same, except for few errors of
approximation in a limited number of cells. As expected, speed-up
measurements were better for float-value implementations, even if more
approximation errors were present with respect to the corresponding
double-value version.
Achieved speedup values of experiments carried out for
evaluating the performance the GPU version of the SCIARA-fv3 MCA
lava-flow model on the GTX 480 (Fermi architecture) and the GTX 680
(Kepler architecture) graphic hardware, using the Atomic function
hybrid memory (AHM) and the LAC hybrid memory (LAC) A Intel i7-2600
based hardware was adopted for reference sequential tests. The
\(517 \times 378\) matrix refers to the 2006 Mt. Etna event.
| CA dim | AHM
(float) | LAC (float) |
|
\(517 \times 378\) | 12.3 |
14.3 |
|
\(400 \times 400 \) | 21.7 |
20.8 |
Achieved speedup values of experiments carried out for
evaluating the performance the GPU version of the SCIARA-fv3 MCA
lava-flow model on the GTX 480 (Fermi architecture) and the GTX 680
(Kepler architecture) graphic hardware, using the Atomic function
hybrid memory (AHM) and the LAC hybrid memory (LAC) A Intel i7-2600
based hardware was adopted for reference sequential tests. The
\(517 \times 378\) matrix refers to the 2006 Mt. Etna event.
| CA dim | AHM
(float) | LAC (float) |
|
\(517 \times 378\) | 19.9 |
21.5 |
|
\(400 \times 400 \) | 27.3 |
26.5 |
Contents
Previous
Next


|
ObjectifyWithGWT
Using Objectify with Google Web Toolkit
en, fr Got CRUD?This must be the most common "design pattern" when developing web applications:
However, there is often an impedance mismatch between the data tier and the presentation tier in web development tools. Because, for example, Hibernate or JDO proxies cannot be passed through GWT RPC, developers are often forced to construct Data Transfer Objects to shuffle data back and forth. Sometimes this is a good idea (say, when you have sophisticated program logic in your entities) but sometimes this is a laborious pain in the arse. No More DTOsWith a tiny amount of care, your entity objects can be passed through GWT serialization and used as-is in the presentation layer. Simply write your entity as if it is a GWT client class!
Simply add this to your module.gwt.xml: <inherits name="com.googlecode.objectify.Objectify" /> You can now manipulate your entity objects in GWT and seamlessly pass them back and forth to the server through GWT-RPC. Objectify enables you to use Key<?>, Key (the datastore version), and all the datastore basic types (Link, Email, GeoPt, etc) in your client code. TransienceA careful distinction must be made between @Transient (the javax.persistence annotation) fields and transient (the Java keyword) fields:
AnnotationsIn general GWT will ignore annotation on your classes. It is not necessary to include them in your gwt include modules. Annotations like @Entity , @LoadAlso , and the like will be ignored during GWT serialization. Client-Side AccessNone of the Objectify action objects (Objectify, ObjectifyService, ObjectifyFactory, DAO) can be used from GWT client code. Basically only entities (and their associated data (types) are allowed to cross the GWT Service boundaries). As of Objectify 3.0, constructing Key<?> objects client-side is now considerably more difficult. You can only use one constructor, the one which takes a native datastore Key . The other constructors do not exist in the Key<?> super-source. See this discussion. ExampleA very simple example can be found here. Request FactoryDavid Chandler wrote an article on Using Objectify with RequestFactory. |


*** User 2017-05-05 21:52:13.736 ***
21:52:13.736 [info] Disabling blocking sync...
*** User 2017-05-05 21:52:13.740 ***
21:52:13.740 [info] Configured peer_service_manager partisan_default_peer_service_manager on node 'node-1@MacBook-Pro-de-Anne-France'
*** User 2017-05-05 21:52:15.273 ***
21:52:15.272 [info] Enabling membership...
*** User 2017-05-05 21:52:15.274 ***
21:52:15.274 [info] Disabling blocking sync...
*** User 2017-05-05 21:52:15.279 ***
21:52:15.279 [info] Configured peer_service_manager partisan_default_peer_service_manager on node 'node-2@MacBook-Pro-de-Anne-France'
*** User 2017-05-05 21:52:16.807 ***
21:52:16.806 [info] Enabling membership...
*** User 2017-05-05 21:52:16.808 ***
21:52:16.808 [info] Disabling blocking sync...
*** User 2017-05-05 21:52:16.813 ***
21:52:16.813 [info] Configured peer_service_manager partisan_default_peer_service_manager on node 'node-3@MacBook-Pro-de-Anne-France'
*** User 2017-05-05 21:52:17.077 ***
Joining node: 'node-3@MacBook-Pro-de-Anne-France' to 'runner@MacBook-Pro-de-Anne-France' at port 51879
*** User 2017-05-05 21:52:17.078 ***
Joining issued: 'node-3@MacBook-Pro-de-Anne-France' to 'runner@MacBook-Pro-de-Anne-France' at port 51879
*** User 2017-05-05 21:52:17.078 ***
Joining node: 'node-2@MacBook-Pro-de-Anne-France' to 'runner@MacBook-Pro-de-Anne-France' at port 51862
*** User 2017-05-05 21:52:17.078 ***
Joining issued: 'node-2@MacBook-Pro-de-Anne-France' to 'runner@MacBook-Pro-de-Anne-France' at port 51862
*** User 2017-05-05 21:52:17.079 ***
Joining node: 'node-1@MacBook-Pro-de-Anne-France' to 'runner@MacBook-Pro-de-Anne-France' at port 51851
*** User 2017-05-05 21:52:17.080 ***
Joining issued: 'node-1@MacBook-Pro-de-Anne-France' to 'runner@MacBook-Pro-de-Anne-France' at port 51851
*** User 2017-05-05 21:52:17.140 ***
Waiting for join to complete with manager: partisan_default_peer_service_manager
*** User 2017-05-05 21:52:17.142 ***
Finished.
*** CT 2017-05-05 21:52:17.142 *** COVER INFO
Adding nodes to cover test: ['runner@MacBook-Pro-de-Anne-France']
*** CT 2017-05-05 21:52:17.154 *** COVER INFO
Successfully added nodes to cover test: []
*** User 2017-05-05 21:52:17.578 ***
Case finished: union_test
*** User 2017-05-05 21:52:24.621 ***
21:52:24.621 [info] Application lasp exited with reason: stopped
*** User 2017-05-05 21:52:24.621 ***
21:52:24.621 [info] Application partisan exited with reason: stopped
=== Ended at 2017-05-05 21:52:24
=== successfully completed test case
=== Returned value: ok
Test run history
| Top level test index


Module reader (2.4.0)
API documentation for bigquery_storage_v1.reader
module.
Classes
ReadRowsIterable
ReadRowsIterable(reader, read_session=None)
An iterable of rows from a read session.
| Name | Description |
| reader |
google.cloud.bigquery_storage_v1.reader.ReadRowsStream
A read rows stream. |
| read_session |
Optional[ReadSession]
DEPRECATED. This argument was used to specify the schema of the rows in the stream, but now the first message in a read stream contains this information. |
ReadRowsPage
ReadRowsPage(stream_parser, message)
An iterator of rows from a read session message.
| Name | Description |
| stream_parser |
google.cloud.bigquery_storage_v1.reader._StreamParser
A helper for parsing messages into rows. |
| message |
google.cloud.bigquery_storage_v1.types.ReadRowsResponse
A message of data from a read rows stream. |
ReadRowsStream
ReadRowsStream(client, name, offset, read_rows_kwargs, retry_delay_callback=None)
A stream of results from a read rows request.
This stream is an iterable of ReadRowsResponse. Iterate over it to fetch all row messages.
If the fastavro library is installed, use the rows() method to parse all messages into a stream of row dictionaries.
If the pandas and fastavro libraries are installed, use the
to_dataframe()
method to parse all messages into a pandas.DataFrame
.
This object should not be created directly, but is returned by other methods in this library.