PolyPolymorphism and Higher-Order Functions
Polymorphism
Polymorphic Lists
... but this would quickly become tedious, partly because we
have to make up different constructor names for each datatype, but
mostly because we would also need to define new versions of all
our list manipulating functions (length, rev, etc.) for each
new datatype definition.
To avoid all this repetition, Coq supports polymorphic
inductive type definitions. For example, here is a polymorphic
list datatype.
This is exactly like the definition of natlist from the
previous chapter, except that the nat argument to the cons
constructor has been replaced by an arbitrary type X, a binding
for X has been added to the header, and the occurrences of
natlist in the types of the constructors have been replaced by
list X. (We can re-use the constructor names nil and cons
because the earlier definition of natlist was inside of a
Module definition that is now out of scope.)
So what, exactly, is list? One good way to think about it
is that list is a function from Types to Inductive
definitions; or, to put it another way, list is a function from
Types to Types. For any particular type X, the type list
X is an Inductively defined set of lists whose elements are
things of type X.
With this definition, when we use the constructors nil and
cons to build lists, we need to specify what type of lists we
are building — that is, nil and cons are now polymorphic
constructors. Observe the types of these constructors:
Check nil.
(* ===> nil : forall X : Type, list X *)
Check cons.
(* ===> cons : forall X : Type, X -> list X -> list X *)
The "∀ X" in these types should be read as an
additional argument to the constructors that determines the
expected types of the arguments that follow. When nil and
cons are used, these arguments are supplied in the same way as
the others. For example, the list containing 2 and 1 is
written like this:
(We are writing nil and cons explicitly here because we
haven't yet defined the [] and :: notations. We'll do that
in a bit.)
We can now go back and make polymorphic (or "generic")
versions of all the list-processing functions that we wrote
before. Here is length, for example:
Fixpoint length (X:Type) (l:list X) : nat :=
match l with
| nil => 0
| cons h t => S (length X t)
end.
Note that the uses of nil and cons in match patterns
do not require any type annotations: we already know that the list
l contains elements of type X, so there's no reason to include
X in the pattern. More formally, the type X is a parameter
of the whole definition of list, not of the individual
constructors.
As with nil and cons, we can use length by applying it first
to a type and then to its list argument:
To use our length with other kinds of lists, we simply
instantiate it with an appropriate type parameter:
Let's close this subsection by re-implementing a few other
standard list functions on our new polymorphic lists:
Fixpoint app (X : Type) (l1 l2 : list X)
: (list X) :=
match l1 with
| nil => l2
| cons h t => cons X h (app X t l2)
end.
Fixpoint snoc (X:Type) (l:list X) (v:X) : (list X) :=
match l with
| nil => cons X v (nil X)
| cons h t => cons X h (snoc X t v)
end.
Fixpoint rev (X:Type) (l:list X) : list X :=
match l with
| nil => nil X
| cons h t => snoc X (rev X t) h
end.
Example test_rev1 :
rev nat (cons nat 1 (cons nat 2 (nil nat)))
= (cons nat 2 (cons nat 1 (nil nat))).
Proof. reflexivity. Qed.
Example test_rev2:
rev bool (nil bool) = nil bool.
Proof. reflexivity. Qed.
Type Inference
Fixpoint app' X l1 l2 : list X :=
match l1 with
| nil => l2
| cons h t => cons X h (app' X t l2)
end.
Indeed it will. Let's see what type Coq has assigned to app':
It has exactly the same type type as app. Coq was able to
use a procedure called type inference to deduce what the types
of X, l1, and l2 must be, based on how they are used. For
example, since X is used as an argument to cons, it must be a
Type, since cons expects a Type as its first argument;
matching l1 with nil and cons means it must be a list; and
so on.
This powerful facility means we don't always have to write
explicit type annotations everywhere, although explicit type
annotations are still quite useful as documentation and sanity
checks. You should try to strike a balance in your own code
between too many type annotations (which serve only to clutter and
distract) and too few (which force the reader to perform type
inference in their head in order to understand your code).
Whenever we use a polymorphic function, we need to pass it
one or more types in addition to its other arguments. For
example, the recursive call in the body of the length function
above must pass along the type X. But just like providing
explicit type annotations everywhere, this is heavy and verbose.
Since the second argument to length is a list of Xs, it seems
entirely obvious that the first argument can only be X — why
should we have to write it explicitly?
Fortunately, Coq permits us to avoid this kind of redundancy. In
place of any type argument we can write the "implicit argument"
_, which can be read as "Please figure out for yourself what
type belongs here." More precisely, when Coq encounters a _, it
will attempt to unify all locally available information — the
type of the function being applied, the types of the other
arguments, and the type expected by the context in which the
application appears — to determine what concrete type should
replace the _.
This may sound similar to type inference — in fact, the two
procedures rely on the same underlying mechanisms. Instead of
simply omitting the types of some arguments to a function, like
Using implicit arguments, the length function can be written
like this:
Argument Synthesis
app' X l1 l2 : list X :=
we can also replace the types with _, like
app' (X : _) (l1 l2 : _) : list X :=
which tells Coq to attempt to infer the missing information, just
as with argument synthesis.
Fixpoint length' (X:Type) (l:list X) : nat :=
match l with
| nil => 0
| cons h t => S (length' _ t)
end.
In this instance, we don't save much by writing _ instead of
X. But in many cases the difference can be significant. For
example, suppose we want to write down a list containing the
numbers 1, 2, and 3. Instead of writing this...
...we can use argument synthesis to write this:
Implicit Arguments
Implicit Arguments nil [[X]].
Implicit Arguments cons [[X]].
Implicit Arguments length [[X]].
Implicit Arguments app [[X]].
Implicit Arguments rev [[X]].
Implicit Arguments snoc [[X]].
(* note: no _ arguments required... *)
Definition list123'' := cons 1 (cons 2 (cons 3 nil)).
Check (length list123'').
We can also declare an argument to be implicit while
defining the function itself, by surrounding the argument in curly
braces. For example:
Fixpoint length'' {X:Type} (l:list X) : nat :=
match l with
| nil => 0
| cons h t => S (length'' t)
end.
(Note that we didn't even have to provide a type argument to
the recursive call to length''.) We will use this style
whenever possible, although we will continue to use use explicit
Implicit Argument declarations for Inductive constructors.
One small problem with declaring arguments Implicit is
that, occasionally, Coq does not have enough local information to
determine a type argument; in such cases, we need to tell Coq that
we want to give the argument explicitly this time, even though
we've globally declared it to be Implicit. For example, if we
write:
(* Definition mynil := nil. *)
If we uncomment this definition, Coq will give us an error,
because it doesn't know what type argument to supply to nil. We
can help it by providing an explicit type declaration (so that Coq
has more information available when it gets to the "application"
of nil):
Alternatively, we can force the implicit arguments to be explicit by
prefixing the function name with @.
Using argument synthesis and implicit arguments, we can
define convenient notation for lists, as before. Since we have
made the constructor type arguments implicit, Coq will know to
automatically infer these when we use the notations.
Notation "x :: y" := (cons x y)
(at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
(at level 60, right associativity).
Now lists can be written just the way we'd hope:
Exercises: Polymorphic Lists
Exercise: 2 stars, optional (poly_exercises)
Here are a few simple exercises, just like ones in Lists.v, for practice with polymorphism. Fill in the definitions and complete the proofs below.Fixpoint repeat (X : Type) (n : X) (count : nat) : list X :=
(* FILL IN HERE *) admit.
Example test_repeat1:
repeat bool true 2 = cons true (cons true nil).
(* FILL IN HERE *) Admitted.
Theorem nil_app : ∀ X:Type, ∀ l:list X,
app [] l = l.
Proof.
(* FILL IN HERE *) Admitted.
Theorem rev_snoc : ∀ X : Type,
∀ v : X,
∀ s : list X,
rev (snoc s v) = v :: (rev s).
Proof.
(* FILL IN HERE *) Admitted.
Theorem snoc_with_append : ∀ X : Type,
∀ l1 l2 : list X,
∀ v : X,
snoc (l1 ++ l2) v = l1 ++ (snoc l2 v).
Proof.
(* FILL IN HERE *) Admitted.
☐
Following the same pattern, the type definition we gave in
the last chapter for pairs of numbers can be generalized to
polymorphic pairs (or products):
Polymorphic Pairs
As with lists, we make the type arguments implicit and define the
familiar concrete notation.
We can also use the Notation mechanism to define the standard
notation for pair types:
(The annotation : type_scope tells Coq that this abbreviation
should be used when parsing types. This avoids a clash with the
multiplication symbol.)
A note of caution: it is easy at first to get (x,y) and
X*Y confused. Remember that (x,y) is a value consisting of a
pair of values; X*Y is a type consisting of a pair of types. If
x has type X and y has type Y, then (x,y) has type X*Y.
The first and second projection functions now look pretty
much as they would in any functional programming language.
Definition fst {X Y : Type} (p : X * Y) : X :=
match p with (x,y) => x end.
Definition snd {X Y : Type} (p : X * Y) : Y :=
match p with (x,y) => y end.
The following function takes two lists and combines them
into a list of pairs. In many functional programming languages,
it is called zip. We call it combine for consistency with
Coq's standard library. Note that the pair notation can be used both in expressions and in
patterns...
Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
: list (X*Y) :=
match (lx,ly) with
| ([],_) => []
| (_,[]) => []
| (x::tx, y::ty) => (x,y) :: (combine tx ty)
end.
Indeed, when no ambiguity results, we can even drop the enclosing
parens:
Fixpoint combine' {X Y : Type} (lx : list X) (ly : list Y)
: list (X*Y) :=
match lx,ly with
| [],_ => []
| _,[] => []
| x::tx, y::ty => (x,y) :: (combine' tx ty)
end.
Exercise: 1 star (combine_checks)
Try answering the following questions on paper and checking your answers in coq:- What is the type of combine (i.e., what does Check @combine print?)
- What does
Eval simpl in (combine [1,2] [false,false,true,true]).print? ☐
Exercise: 2 stars, recommended (split)
The function split is the right inverse of combine: it takes a list of pairs and returns a pair of lists. In many functional programing languages, this function is called unzip.(*
Fixpoint split
(* FILL IN HERE *)
(* SOON: Argh: this displays totally wrong in the HTML version!!
(The square brackets get dropped.) *)
Example test_split:
split (1,false),(2,false) = (1,2,false,false).
Proof. reflexivity. Qed.
*)
☐
One last polymorphic type for now: polymorphic options.
The type declaration generalizes the one for natoption in the
previous chapter:
Polymorphic Options
Inductive option (X:Type) : Type :=
| Some : X → option X
| None : option X.
Implicit Arguments Some [[X]].
Implicit Arguments None [[X]].
We can now rewrite the index function so that it works
with any type of lists.
Fixpoint index {X : Type} (n : nat)
(l : list X) : option X :=
match l with
| [] => None
| a :: l' => if beq_nat n O then Some a else index (pred n) l'
end.
Example test_index1 : index 0 [4,5,6,7] = Some 4.
Proof. reflexivity. Qed.
Example test_index2 : index 1 [[1],[2]] = Some [2].
Proof. reflexivity. Qed.
Example test_index3 : index 2 [true] = None.
Proof. reflexivity. Qed.
Exercise: 1 star, optional (hd_opt_poly)
Complete the definition of a polymorphic version of the hd_opt function from the last chapter. Be sure that it passes the unit tests below.
Once again, to force the implicit arguments to be explicit,
we can use @ before the name of the function.
Check @hd_opt.
Example test_hd_opt1 : hd_opt [1,2] = Some 1.
(* FILL IN HERE *) Admitted.
Example test_hd_opt2 : hd_opt [[1],[2]] = Some [1].
(* FILL IN HERE *) Admitted.
☐
Like many other modern programming languages — including,
of course, all functional languages — Coq treats functions as
first-class citizens, allowing functions to be passed as arguments
to other functions, returned as results, stored in data
structures, etc.
Functions that manipulate other functions are often called
higher-order functions. Here's a simple one:
Functions as Data
Higher-Order Functions
The argument f here is itself a function (from X to
X); the body of doit3times applies f three times to some
value n.
Check @doit3times.
(* ===> doit3times : forall X : Type, (X -> X) -> X -> X *)
Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity. Qed.
Example test_doit3times': doit3times negb true = false.
Proof. reflexivity. Qed.
Partial Application
Check plus.
The → is actually a binary operator on types; that is,
Coq primitively supports only one-argument functions. Moreover,
this operator is right-associative, so the type of plus is
really a shorthand for nat → (nat → nat) — i.e., it can be
read as saying that "plus is a one-argument function that takes
a nat and returns a one-argument function that takes another
nat and returns a nat." In the examples above, we have always
applied plus to both of its arguments at once, but if we like we
can supply just the first. This is called partial
application.
Definition plus3 := plus 3.
Check plus3.
Example test_plus3 : plus3 4 = 7.
Proof. reflexivity. Qed.
Example test_plus3' : doit3times plus3 0 = 9.
Proof. reflexivity. Qed.
Example test_plus3'' : doit3times (plus 3) 0 = 9.
Proof. reflexivity. Qed.
Digression: Currying
Exercise: 2 stars, optional (currying)
In Coq, a function f : A → B → C really has the type A → (B → C). That is, if you give f a value of type A, it will give you function f' : B → C. If you then give f' a value of type B, it will return a value of type C. This allows for partial application, as in plus3. Processing a list of arguments with functions that return functions is called currying, in honor of the logician Haskell Curry.
As an exercise, define its inverse, prod_uncurry. Then prove
the theorems below to show that the two are inverses.
(Thought exercise: before running these commands, can you
calculate the types of prod_curry and prod_uncurry?)
Check @prod_curry.
Check @prod_uncurry.
Theorem uncurry_curry : ∀ (X Y Z : Type) (f : X → Y → Z) x y,
prod_curry (prod_uncurry f) x y = f x y.
Proof.
(* FILL IN HERE *) Admitted.
Theorem curry_uncurry : ∀ (X Y Z : Type)
(f : (X * Y) → Z) (p : X * Y),
prod_uncurry (prod_curry f) p = f p.
Proof.
(* FILL IN HERE *) Admitted.
☐
Here is a useful higher-order function, which takes a list
of Xs and a predicate on X (a function from X to bool)
and "filters" the list, returning a new list containing just those
elements for which the predicate returns true.
Filter
Fixpoint filter {X:Type} (test: X→bool) (l:list X)
: (list X) :=
match l with
| [] => []
| h :: t => if test h then h :: (filter test t)
else filter test t
end.
For example, if we apply filter to the predicate evenb
and a list of numbers l, it returns a list containing just the
even members of l.
Example test_filter1: filter evenb [1,2,3,4] = [2,4].
Proof. reflexivity. Qed.
Definition length_is_1 {X : Type} (l : list X) : bool :=
beq_nat (length l) 1.
Example test_filter2:
filter length_is_1
[ [1, 2], [3], [4], [5,6,7], [], [8] ]
= [ [3], [4], [8] ].
Proof. reflexivity. Qed.
We can use filter to give a concise version of the
countoddmembers function from Lists.v.
Definition countoddmembers' (l:list nat) : nat :=
length (filter oddb l).
Example test_countoddmembers'1: countoddmembers' [1,0,3,1,4,5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers'2: countoddmembers' [0,2,4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers'3: countoddmembers' nil = 0.
Proof. reflexivity. Qed.
Anonymous Functions
Here is the motivating example from before, rewritten to use
an anonymous function.
Example test_filter2':
filter (fun l => beq_nat (length l) 1)
[ [1, 2], [3], [4], [5,6,7], [], [8] ]
= [ [3], [4], [8] ].
Proof. reflexivity. Qed.
Exercise: 2 stars, optional (filter_even_gt7)
Definition filter_even_gt7 (l : list nat) : list nat :=
(* FILL IN HERE *) admit.
Example test_filter_even_gt7_1 :
filter_even_gt7 [1,2,6,9,10,3,12,8] = [10,12,8].
(* FILL IN HERE *) Admitted.
Example test_filter_even_gt7_2 :
filter_even_gt7 [5,2,6,19,129] = [].
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, optional (partition)
Use filter to write a Coq function partition:
partition : ∀ X : Type,
(X → bool) → list X → list X * list X
Given a set X, a test function of type X → bool and a list
X, partition should return a pair of lists. The first member of
the pair is the sublist of the original list containing the
elements that satisfy the test, and the second is the sublist
containing those that fail the test. The order of elements in the
two sublists should be the same as their order in the original
list.
(X → bool) → list X → list X * list X
Definition partition {X : Type} (test : X → bool) (l : list X)
: list X * list X :=
(* FILL IN HERE *) admit.
Example test_partition1: partition oddb [1,2,3,4,5] = ([1,3,5], [2,4]).
(* FILL IN HERE *) Admitted.
Example test_partition2: partition (fun x => false) [5,9,0] = ([], [5,9,0]).
(* FILL IN HERE *) Admitted.
Fixpoint map {X Y:Type} (f:X→Y) (l:list X)
: (list Y) :=
match l with
| [] => []
| h :: t => (f h) :: (map f t)
end.
It takes a function f and a list l = [n1, n2, n3, ...]
and returns the list [f n1, f n2, f n3,...] , where f has
been applied to each element of l in turn. For example:
The element types of the input and output lists need not be
the same (map takes two type arguments, X and Y). This
version of map can thus be applied to a list of numbers and a
function from numbers to booleans to yield a list of booleans:
It can even be applied to a list of numbers and
a function from numbers to lists of booleans to
yield a list of lists of booleans:
Example test_map3:
map (fun n => [evenb n,oddb n]) [2,1,2,5]
= [[true,false],[false,true],[true,false],[false,true]].
Proof. reflexivity. Qed.
Exercise: 3 stars, optional (map_rev)
Show that map and rev commute. You may need to define an auxiliary lemma.Theorem map_rev : ∀ (X Y : Type) (f : X → Y) (l : list X),
map f (rev l) = rev (map f l).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, recommended (flat_map)
The function map maps a list X to a list Y using a function of type X → Y. We can define a similar function, flat_map, which maps a list X to a list Y using a function f of type X → list Y. Your definition should work by 'flattening' the results of f, like so:
flat_map (fun n => [n,n+1,n+2]) [1,5,10]
= [1, 2, 3, 5, 6, 7, 10, 11, 12].
= [1, 2, 3, 5, 6, 7, 10, 11, 12].
Fixpoint flat_map {X Y:Type} (f:X → list Y) (l:list X)
: (list Y) :=
(* FILL IN HERE *) admit.
Example test_flat_map1:
flat_map (fun n => [n,n,n]) [1,5,4]
= [1, 1, 1, 5, 5, 5, 4, 4, 4].
(* FILL IN HERE *) Admitted.
☐
Lists are not the only inductive type that we can write a
map function for. Here is the definition of map for the
option type:
Definition option_map {X Y : Type} (f : X → Y) (xo : option X)
: option Y :=
match xo with
| None => None
| Some x => Some (f x)
end.
Exercise: 2 stars, optional (implicit_args)
The definitions and uses of filter and map use implicit arguments in many places. Replace the curly braces around the implicit arguments with parentheses, and then fill in explicit type parameters where necessary and use Coq to check that you've done so correctly. This exercise is not to be turned in; it is probably easiest to do it on a copy of this file that you can throw away afterwards. ☐Fold
Fixpoint fold {X Y:Type} (f: X→Y→Y) (l:list X) (b:Y) : Y :=
match l with
| nil => b
| h :: t => f h (fold f t b)
end.
Intuitively, the behavior of the fold operation is to
insert a given binary operator f between every pair of elements
in a given list. For example, fold plus [1,2,3,4] intuitively
means 1+2+3+4. To make this precise, we also need a "starting
element" that serves as the initial second input to f. So, for
example,
fold plus [1,2,3,4] 0
yields
1 + (2 + (3 + (4 + 0))).
Here are some more examples:
Check (fold plus).
Eval simpl in (fold plus [1,2,3,4] 0).
Example fold_example1 : fold mult [1,2,3,4] 1 = 24.
Proof. reflexivity. Qed.
Example fold_example2 : fold andb [true,true,false,true] true = false.
Proof. reflexivity. Qed.
Example fold_example3 : fold app [[1],[],[2,3],[4]] [] = [1,2,3,4].
Proof. reflexivity. Qed.
Exercise: 1 star, optional (fold_types_different)
Observe that the type of fold is parameterized by two type variables, X and Y, and the parameter f is a binary operator that takes an X and a Y and returns a Y. Can you think of a situation where it would be useful for X and Y to be different?Functions For Constructing Functions
Definition constfun {X: Type} (x: X) : nat→X :=
fun (k:nat) => x.
Definition ftrue := constfun true.
Example constfun_example1 : ftrue 0 = true.
Proof. reflexivity. Qed.
Example constfun_example2 : (constfun 5) 99 = 5.
Proof. reflexivity. Qed.
Similarly, but a bit more interestingly, here is a function
that takes a function f from numbers to some type X, a number
k, and a value x, and constructs a function that behaves
exactly like f except that, when called with the argument k,
it returns x.
Definition override {X: Type} (f: nat→X) (k:nat) (x:X) : nat→X:=
fun (k':nat) => if beq_nat k k' then x else f k'.
For example, we can apply override twice to obtain a
function from numbers to booleans that returns false on 1 and
3 and returns true on all other arguments.
Definition fmostlytrue := override (override ftrue 1 false) 3 false.
Example override_example1 : fmostlytrue 0 = true.
Proof. reflexivity. Qed.
Example override_example2 : fmostlytrue 1 = false.
Proof. reflexivity. Qed.
Example override_example3 : fmostlytrue 2 = true.
Proof. reflexivity. Qed.
Example override_example4 : fmostlytrue 3 = false.
Proof. reflexivity. Qed.
Exercise: 1 star (override_example)
Before starting to work on the following proof, make sure you understand exactly what the theorem is saying and can paraphrase it in your own words. The proof itself is straightforward.Theorem override_example : ∀ (b:bool),
(override (constfun b) 3 true) 2 = b.
Proof.
(* FILL IN HERE *) Admitted.
☐
We'll use function overriding heavily in parts of the rest of the
course, and we will end up needing to know quite a bit about its
properties. To prove these properties, though, we need to know
about a few more of Coq's tactics; developing these is the main
topic of the rest of the chapter.
We often encounter situations where the goal to be proved is
exactly the same as some hypothesis in the context or some
previously proved lemma.
More About Coq
The apply Tactic
Theorem silly1 : ∀ (n m o p : nat),
n = m →
[n,o] = [n,p] →
[n,o] = [m,p].
Proof.
intros n m o p eq1 eq2.
rewrite ← eq1.
(* At this point, we could finish with "rewrite → eq2. reflexivity."
as we have done several times above. But we can achieve the
same effect in a single step by using the apply tactic instead: *)
apply eq2. Qed.
The apply tactic also works with conditional hypotheses
and lemmas: if the statement being applied is an implication, then
the premises of this implication will be added to the list of
subgoals needing to be proved.
Theorem silly2 : ∀ (n m o p : nat),
n = m →
(∀ (q r : nat), q = r → [q,o] = [r,p]) →
[n,o] = [m,p].
Proof.
intros n m o p eq1 eq2.
apply eq2. apply eq1. Qed.
You may find it instructive to experiment with this proof
and see if there is a way to complete it using just rewrite
instead of apply.
Typically, when we use apply H, the statement H will
begin with a ∀ binding some universal variables. When
Coq matches the current goal against the conclusion of H, it
will try to find appropriate values for these variables. For
example, when we do apply eq2 in the following proof, the
universal variable q in eq2 gets instantiated with n and r
gets instantiated with m.
Theorem silly2a : ∀ (n m : nat),
(n,n) = (m,m) →
(∀ (q r : nat), (q,q) = (r,r) → [q] = [r]) →
[n] = [m].
Proof.
intros n m eq1 eq2.
apply eq2. apply eq1. Qed.
Theorem silly_ex :
(∀ n, evenb n = true → oddb (S n) = true) →
evenb 3 = true →
oddb 4 = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
To use the apply tactic, the (conclusion of the) fact
being applied must match the goal exactly — for example, apply
will not work if the left and right sides of the equality are
swapped.
Theorem silly3_firsttry : ∀ (n : nat),
true = beq_nat n 5 →
beq_nat (S (S n)) 7 = true.
Proof.
intros n H.
simpl.
(* Here we cannot use apply directly *)
Admitted.
In this case we can use the symmetry tactic, which
switches the left and right sides of an equality in the goal.
Theorem silly3 : ∀ (n : nat),
true = beq_nat n 5 →
beq_nat (S (S n)) 7 = true.
Proof.
intros n H.
symmetry.
simpl. (* Actually, this simpl is unnecessary, since
apply will do a simpl step first. *)
apply H. Qed.
Theorem rev_exercise1 : ∀ (l l' : list nat),
l = rev l' →
l' = rev l.
Proof.
(* Hint: you can use apply with previously defined lemmas, not
just hypotheses in the context. Remember that SearchAbout is
your friend. *)
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
☐
Sometimes, a proof will get stuck because Coq doesn't
automatically expand a function call into its definition. (This
is a feature, not a bug: if Coq automatically expanded everything
possible, our proof goals would quickly become enormous — hard to
read and slow for Coq to manipulate!)
Exercise: 1 star (apply_rewrite)
Briefly explain the difference between the tactics apply and rewrite. Are there situations where both can usefully be applied?☐
The unfold Tactic
Theorem unfold_example_bad : ∀ m n,
3 + n = m →
plus3 n + 1 = m + 1.
Proof.
intros m n H.
(* At this point, we'd like to do rewrite → H, since plus3 n is
definitionally equal to 3 + n. However, Coq doesn't
automatically expand plus3 n to its definition. *)
Admitted.
The unfold tactic can be used to explicitly replace a
defined name by the right-hand side of its definition.
Theorem unfold_example : ∀ m n,
3 + n = m →
plus3 n + 1 = m + 1.
Proof.
intros m n H.
unfold plus3.
rewrite → H.
reflexivity. Qed.
Now we can prove a first property of override: If we
override a function at some argument k and then look up k, we
get back the overridden value.
Theorem override_eq : ∀ {X:Type} x k (f:nat→X),
(override f k x) k = x.
Proof.
intros X x k f.
unfold override.
rewrite ← beq_nat_refl.
reflexivity. Qed.
This proof was straightforward, but note that it requires
unfold to expand the definition of override.
Exercise: 2 stars (override_neq)
Theorem override_neq : ∀ {X:Type} x1 x2 k1 k2 (f : nat→X),
f k1 = x1 →
beq_nat k2 k1 = false →
(override f k2 x2) k1 = x1.
Proof.
(* FILL IN HERE *) Admitted.
f k1 = x1 →
beq_nat k2 k1 = false →
(override f k2 x2) k1 = x1.
Proof.
(* FILL IN HERE *) Admitted.
☐
As the inverse of unfold, Coq also provides a tactic
fold, which can be used to "unexpand" a definition. It is used
much less often.
Recall the definition of natural numbers:
Similar principles apply to all inductively defined types: all
constructors are injective, and the values built from distinct
constructors are never equal. For lists, the cons constructor is
injective and nil is different from every non-empty list. For
booleans, true and false are unequal. (Since neither true
nor false take any arguments, their injectivity is not an issue.)
Coq provides a tactic, called inversion, that allows us to
exploit these principles in making proofs.
The inversion tactic is used like this. Suppose H is a
hypothesis in the context (or a previously proven lemma) of the
form
Then inversion H instructs Coq to "invert" this equality to
extract the information it contains about these terms:
The inversion tactic is probably easier to understand by
seeing it in action than from general descriptions like the above.
Below you will find example theorems that demonstrate the use of
inversion and exercises to test your understanding.
Inversion
Inductive nat : Type :=
| O : nat
| S : nat → nat.
It is clear from this definition that every number has one of two
forms: either it is the constructor O or it is built by applying
the constructor S to another number. But there is more here than
meets the eye: implicit in the definition (and in our informal
understanding of how datatype declarations work in other
programming languages) are two other facts:
| O : nat
| S : nat → nat.
- The constructor S is injective. That is, the only way we can
have S n = S m is if n = m.
- The constructors O and S are disjoint. That is, O is not equal to S n for any n.
c a1 a2 ... an = d b1 b2 ... bm
for some constructors c and d and arguments a1 ... an and
b1 ... bm.
- If c and d are the same constructor, then we know, by the
injectivity of this constructor, that a1 = b1, a2 = b2,
etc.; inversion H adds these facts to the context, and tries
to use them to rewrite the goal.
- If c and d are different constructors, then the hypothesis H is contradictory. That is, a false assumption has crept into the context, and this means that any goal whatsoever is provable! In this case, inversion H marks the current goal as completed and pops it off the goal stack.
Theorem eq_add_S : ∀ (n m : nat),
S n = S m →
n = m.
Proof.
intros n m eq. inversion eq. reflexivity. Qed.
Theorem silly4 : ∀ (n m : nat),
[n] = [m] →
n = m.
Proof.
intros n o eq. inversion eq. reflexivity. Qed.
As a convenience, the inversion tactic can also
destruct equalities between complex values, binding
multiple variables as it goes.
Theorem silly5 : ∀ (n m o : nat),
[n,m] = [o,o] →
[n] = [m].
Proof.
intros n m o eq. inversion eq. reflexivity. Qed.
Example sillyex1 : ∀ (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j →
y :: l = x :: j →
x = y.
Proof.
(* FILL IN HERE *) Admitted.
x :: y :: l = z :: j →
y :: l = x :: j →
x = y.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem silly6 : ∀ (n : nat),
S n = O →
2 + 2 = 5.
Proof.
intros n contra. inversion contra. Qed.
Theorem silly7 : ∀ (n m : nat),
false = true →
[n] = [m].
Proof.
intros n m contra. inversion contra. Qed.
Example sillyex2 : ∀ (X : Type) (x y z : X) (l j : list X),
x :: y :: l = [] →
y :: l = z :: j →
x = z.
Proof.
(* FILL IN HERE *) Admitted.
x :: y :: l = [] →
y :: l = z :: j →
x = z.
Proof.
(* FILL IN HERE *) Admitted.
☐
While the injectivity of constructors allows us to reason
∀ (n m : nat), S n = S m → n = m, the reverse direction of
the implication, provable by standard equational reasoning, is a
useful fact to record for cases we will see several times.
Here is a more realistic use of inversion to prove a
property that is useful in many places later on...
Theorem beq_nat_eq : ∀ n m,
true = beq_nat n m → n = m.
Proof.
intros n. induction n as [| n'].
Case "n = 0".
intros m. destruct m as [| m'].
SCase "m = 0". reflexivity.
SCase "m = S m'". simpl. intros contra. inversion contra.
Case "n = S n'".
intros m. destruct m as [| m'].
SCase "m = 0". simpl. intros contra. inversion contra.
SCase "m = S m'". simpl. intros H.
apply eq_remove_S. apply IHn'. apply H. Qed.
(* FILL IN HERE *)
☐
Exercise: 3 stars (beq_nat_eq')
We can also prove beq_nat_eq by induction on m, though we have to be a little careful about which order we introduce the variables, so that we get a general enough induction hypothesis — this is done for you below. Finish the following proof. To get maximum benefit from the exercise, try first to do it without looking back at the one above.Theorem beq_nat_eq' : ∀ m n,
beq_nat n m = true → n = m.
Proof.
intros m. induction m as [| m'].
(* FILL IN HERE *) Admitted.
☐
Here's another illustration of inversion. This is a slightly
roundabout way of stating a fact that we have already proved
above. The extra equalities force us to do a little more
equational reasoning and exercise some of the tactics we've seen
recently.
Theorem length_snoc' : ∀ (X : Type) (v : X)
(l : list X) (n : nat),
length l = n →
length (snoc l v) = S n.
Proof.
intros X v l. induction l as [| v' l'].
Case "l = []". intros n eq. rewrite ← eq. reflexivity.
Case "l = v' :: l'". intros n eq. simpl. destruct n as [| n'].
SCase "n = 0". inversion eq.
SCase "n = S n'".
apply eq_remove_S. apply IHl'. inversion eq. reflexivity. Qed.
Practice Session
Exercise: 2 stars, optional (practice)
Some nontrivial but not-too-complicated proofs to work together in class, and some for you to work as exercises. Some of the exercises may involve applying lemmas from earlier lectures or homeworks.Theorem beq_nat_0_l : ∀ n,
true = beq_nat 0 n → 0 = n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem beq_nat_0_r : ∀ n,
true = beq_nat n 0 → 0 = n.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem double_injective : ∀ n m,
double n = double m →
n = m.
Proof.
intros n. induction n as [| n'].
(* WORKED IN CLASS *)
Case "n = 0". simpl. intros m eq. destruct m as [| m'].
SCase "m = 0". reflexivity.
SCase "m = S m'". inversion eq.
Case "n = S n'". intros m eq. destruct m as [| m'].
SCase "m = 0". inversion eq.
SCase "m = S m'".
apply eq_remove_S. apply IHn'. inversion eq. reflexivity. Qed.
Varying the Induction Hypothesis
Exercise: 2 stars, optional (app_ass')
Give an alternate proof of the associativity of ++ with a more general induction hypothesis. Complete the following (leaving the first line unchanged).Theorem app_ass' : ∀ l1 l2 l3 : list nat,
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
intros l1. induction l1 as [ | n l1'].
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars (apply_exercise2)
In the following proof opening, notice that we don't introduce m before performing induction. This leaves it general, so that the IH doesn't specify a particular m, but lets us pick. Finish the proof.Theorem beq_nat_sym : ∀ (n m : nat),
beq_nat n m = beq_nat m n.
Proof.
intros n. induction n as [| n'].
(* FILL IN HERE *) Admitted.
☐
Theorem: For any nats n m, beq_nat n m = beq_nat m n.
Proof:
(* FILL IN HERE *)
☐
By default, most tactics work on the goal formula and leave
the context unchanged. However, most tactics also have a variant
that performs a similar operation on a statement in the context.
For example, the tactic simpl in H performs simplification in
the hypothesis named H in the context.
Exercise: 3 stars, recommended (beq_nat_sym_informal)
Provide an informal proof of this lemma that corresponds to your formal proof above:☐
Using Tactics on Hypotheses
Theorem S_inj : ∀ (n m : nat) (b : bool),
beq_nat (S n) (S m) = b →
beq_nat n m = b.
Proof.
intros n m b H. simpl in H. apply H. Qed.
Similarly, the tactic apply L in H matches some
conditional statement L (of the form L1 → L2, say) against a
hypothesis H in the context. However, unlike ordinary
apply (which rewrites a goal matching L2 into a subgoal L1),
apply L in H matches H against L1 and, if successful,
replaces it with L2.
In other words, apply L in H gives us a form of "forward
reasoning" — from L1 → L2 and a hypothesis matching L1, it
gives us a hypothesis matching L2. By contrast, apply L is
"backward reasoning" — it says that if we know L1→L2 and we
are trying to prove L2, it suffices to prove L1.
Here is a variant of a proof from above, using forward reasoning
throughout instead of backward reasoning.
Theorem silly3' : ∀ (n : nat),
(beq_nat n 5 = true → beq_nat (S (S n)) 7 = true) →
true = beq_nat n 5 →
true = beq_nat (S (S n)) 7.
Proof.
intros n eq H.
symmetry in H. apply eq in H. symmetry in H.
apply H. Qed.
Forward reasoning starts from what is given (premises,
previously proven theorems) and iteratively draws conclusions from
them until the goal is reached. Backward reasoning starts from
the goal, and iteratively reasons about what would imply the
goal, until premises or previously proven theorems are reached.
If you've seen informal proofs before (for example, in a math or
computer science class), they probably used forward reasoning. In
general, Coq tends to favor backward reasoning, but in some
situations the forward style can be easier to use or to think
about.
Exercise: 3 stars, recommended (plus_n_n_injective)
You can practice using the "in" variants in this exercise.Theorem plus_n_n_injective : ∀ n m,
n + n = m + m →
n = m.
Proof.
intros n. induction n as [| n'].
(* Hint: use the plus_n_Sm lemma *)
(* FILL IN HERE *) Admitted.
☐
We have seen many examples where the destruct tactic is
used to perform case analysis of the value of some variable. But
sometimes we need to reason by cases on the result of some
expression. We can also do this with destruct.
Here are some examples:
Using destruct on Compound Expressions
Definition sillyfun (n : nat) : bool :=
if beq_nat n 3 then false
else if beq_nat n 5 then false
else false.
Theorem sillyfun_false : ∀ (n : nat),
sillyfun n = false.
Proof.
intros n. unfold sillyfun.
destruct (beq_nat n 3).
Case "beq_nat n 3 = true". reflexivity.
Case "beq_nat n 3 = false". destruct (beq_nat n 5).
SCase "beq_nat n 5 = true". reflexivity.
SCase "beq_nat n 5 = false". reflexivity. Qed.
After unfolding sillyfun in the above proof, we find that
we are stuck on if (beq_nat n 3) then ... else .... Well,
either n is equal to 3 or it isn't, so we use destruct
(beq_nat n 3) to let us reason about the two cases.

Proof.
(* FILL IN HERE *) Admitted.
(override (override f k1 x2) k1 x1) k2 = (override f k1 x1) k2.
Proof.
(* FILL IN HERE *) Admitted.
(*
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
Proof.
intros X Y l. induction l as | [x y] l'.
(* FILL IN HERE *) Admitted.
*)
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
Proof.
intros X Y l. induction l as | [x y] l'.
(* FILL IN HERE *) Admitted.
*)
☐
Hint: what property do you need of l1 and l2 for split
combine l1 l2 = (l1,l2) to be true?
State this theorem in Coq, and prove it. (Be sure to leave your
induction hypothesis general by not doing intros on more things
than necessary.)
Exercise: 3 stars, optional (split_combine)
Thought exercise: We have just proven that for all lists of pairs, combine is the inverse of split. How would you state the theorem showing that split is the inverse of combine?(* FILL IN HERE *)
☐
(Note: the remember tactic is not strictly needed until a
bit later, so if necessary this section can be skipped and
returned to when needed.)
We have seen how the destruct tactic can be used to
perform case analysis of the results of arbitrary computations.
If e is an expression whose type is some inductively defined
type T, then, for each constructor c of T, destruct e
generates a subgoal in which all occurrences of e (in the goal
and in the context) are replaced by c.
Sometimes, however, this substitution process loses information
that we need in order to complete the proof. For example, suppose
we define a function sillyfun1 like this:
The remember Tactic
Definition sillyfun1 (n : nat) : bool :=
if beq_nat n 3 then true
else if beq_nat n 5 then true
else false.
And suppose that we want to convince Coq of the rather
obvious observation that sillyfun1 n yields true only when n
is odd. By analogy with the proofs we did with sillyfun above,
it is natural to start the proof like this:
Theorem sillyfun1_odd_FAILED : ∀ (n : nat),
sillyfun1 n = true →
oddb n = true.
Proof.
intros n eq. unfold sillyfun1 in eq.
destruct (beq_nat n 3).
(* stuck... *)
Admitted.
We get stuck at this point because the context does not
contain enough information to prove the goal! The problem is that
the substitution peformed by destruct is too brutal — it threw
away every occurrence of beq_nat n 3, but we need to keep at
least one of these because we need to be able to reason that
since, in this branch of the case analysis, beq_nat n 3 = true,
it must be that n = 3, from which it follows that n is odd.
What we would really like is not to use destruct directly on
beq_nat n 3 and substitute away all occurrences of this
expression, but rather to use destruct on something else that is
equal to beq_nat n 3. For example, if we had a variable that
we knew was equal to beq_nat n 3, we could destruct this
variable instead.
The remember tactic allows us to introduce such a variable.
Theorem sillyfun1_odd : ∀ (n : nat),
sillyfun1 n = true →
oddb n = true.
Proof.
intros n eq. unfold sillyfun1 in eq.
remember (beq_nat n 3) as e3.
(* At this point, the context has been enriched with a new
variable e3 and an assumption that e3 = beq_nat n 3.
Now if we do destruct e3... *)
destruct e3.
(* ... the variable e3 gets substituted away (it
disappears completely) and we are left with the same
state as at the point where we got stuck above, except
that the context still contains the extra equality
assumption -- now with true substituted for e3 --
which is exactly what we need to make progress. *)
Case "e3 = true". apply beq_nat_eq in Heqe3.
rewrite → Heqe3. reflexivity.
Case "e3 = false".
(* When we come to the second equality test in the
body of the function we are reasoning about, we can
use remember again in the same way, allowing us
to finish the proof. *)
remember (beq_nat n 5) as e5. destruct e5.
SCase "e5 = true".
apply beq_nat_eq in Heqe5.
rewrite → Heqe5. reflexivity.
SCase "e5 = false". inversion eq. Qed.
Theorem override_same : ∀ {X:Type} x1 k1 k2 (f : nat→X),
f k1 = x1 →
(override f k1 x1) k2 = f k2.
Proof.

Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, optional (filter_exercise)
This one is a bit challenging. Be sure your initial intros go only up through the parameter on which you want to do induction!Theorem filter_exercise : ∀ (X : Type) (test : X → bool)
(x : X) (l lf : list X),
filter test l = x :: lf →
test x = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
The following silly example uses two rewrites in a row to
get from [a,b] to [e,f].
The apply ... with ... Tactic
Example trans_eq_example : ∀ (a b c d e f : nat),
[a,b] = [c,d] →
[c,d] = [e,f] →
[a,b] = [e,f].
Proof.
intros a b c d e f eq1 eq2.
rewrite → eq1. rewrite → eq2. reflexivity. Qed.
Since this is a common pattern, we might
abstract it out as a lemma recording once and for all
the fact that equality is transitive.
Theorem trans_eq : ∀ {X:Type} (n m o : X),
n = m → m = o → n = o.
Proof.
intros X n m o eq1 eq2. rewrite → eq1. rewrite → eq2.
reflexivity. Qed.
Now, we should be able to use trans_eq to
prove the above example. However, to do this we need
a slight refinement of the apply tactic.
Example trans_eq_example' : ∀ (a b c d e f : nat),
[a,b] = [c,d] →
[c,d] = [e,f] →
[a,b] = [e,f].
Proof.
intros a b c d e f eq1 eq2.
(* If we simply tell Coq apply trans_eq at this point,
it can tell (by matching the goal against the
conclusion of the lemma) that it should instantiate X
with [nat], n with [a,b], and o with [e,f].
However, the matching process doesn't determine an
instantiation for m: we have to supply one explicitly
by adding with (m:=[c,d]) to the invocation of
apply. *)
apply trans_eq with (m:=[c,d]). apply eq1. apply eq2. Qed.
Actually, we usually don't have to include the name m
in the with clause; Coq is often smart enough to
figure out which instantiation we're giving. We could
instead write: apply trans_eq with c,d.
Exercise: 3 stars, recommended (apply_exercises)
Example trans_eq_exercise : ∀ (n m o p : nat),
m = (minustwo o) →
(n + p) = m →
(n + p) = (minustwo o).
Proof.
(* FILL IN HERE *) Admitted.
Theorem beq_nat_trans : ∀ n m p,
true = beq_nat n m →
true = beq_nat m p →
true = beq_nat n p.
Proof.
(* FILL IN HERE *) Admitted.
Theorem override_permute : ∀ {X:Type} x1 x2 k1 k2 k3 (f : nat→X),
false = beq_nat k2 k1 →
(override (override f k2 x2) k1 x1) k3 = (override (override f k1 x1) k2 x2) k3.
Proof.
(* FILL IN HERE *) Admitted.
m = (minustwo o) →
(n + p) = m →
(n + p) = (minustwo o).
Proof.
(* FILL IN HERE *) Admitted.
Theorem beq_nat_trans : ∀ n m p,
true = beq_nat n m →
true = beq_nat m p →
true = beq_nat n p.
Proof.
(* FILL IN HERE *) Admitted.
Theorem override_permute : ∀ {X:Type} x1 x2 k1 k2 k3 (f : nat→X),
false = beq_nat k2 k1 →
(override (override f k2 x2) k1 x1) k3 = (override (override f k1 x1) k2 x2) k3.
Proof.
(* FILL IN HERE *) Admitted.
☐
We've now seen a bunch of Coq's fundamental tactics — enough to
do pretty much everything we'll want for a while. We'll introduce
one or two more as we go along through the next few lectures, and
later in the course we'll introduce some more powerful
automation tactics that make Coq do more of the low-level work
in many cases. But basically we've got what we need to get work
done.
Here are the ones we've seen:
Review
- intros:
move hypotheses/variables from goal to context
- reflexivity:
finish the proof (when the goal looks like e = e)
- apply:
prove goal using a hypothesis, lemma, or constructor
- apply... in H:
apply a hypothesis, lemma, or constructor to a hypothesis in
the context (forward reasoning)
- apply... with...:
explicitly specify values for variables that cannot be
determined by pattern matching
- simpl:
simplify computations in the goal
- simpl in H:
... or a hypothesis
- rewrite:
use an equality hypothesis (or lemma) to rewrite the goal
- rewrite ... in H:
... or a hypothesis
- unfold:
replace a defined constant by its right-hand side in the goal
- unfold... in H:
... or a hypothesis
- destruct... as...:
case analysis on values of inductively defined types
- induction... as...:
induction on values of inductively defined types
- inversion:
reason by injectivity and distinctness of constructors
- remember (e) as x:
give a name (x) to an expression (e) so that we can
destruct x without "losing" e
- assert (e) as H: introduce a "local lemma" e and call it H
Additional Exercises
Exercise: 2 stars, optional (fold_length)
Many common functions on lists can be implemented in terms of fold. For example, here is an alternate definition of length:Definition fold_length {X : Type} (l : list X) : nat :=
fold (fun _ n => S n) l 0.
Example test_fold_length1 : fold_length [4,7,0] = 3.
Proof. reflexivity. Qed.
Prove the correctness of fold_length.
Theorem fold_length_correct : ∀ X (l : list X),
fold_length l = length l.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, recommended (fold_map)
We can also define map in terms of fold. Finish fold_map below.
Write down a theorem in Coq stating that fold_map is correct,
and prove it.
(* FILL IN HERE *)
☐
Inductive mumble : Type :=
| a : mumble
| b : mumble → nat → mumble
| c : mumble.
Inductive grumble (X:Type) : Type :=
| d : mumble → grumble X
| e : X → grumble X.
Which of the following are well-typed elements of grumble X for
some type X?
☐
- d (b a 5)
- d mumble (b a 5)
- d bool (b a 5)
- e bool true
- e mumble (b c 0)
- e bool (b c 0)
- c
☐
Exercise: 2 stars, optional (baz_num_elts)
Consider the following inductive definition:
How many elements does the type baz have?
(* FILL IN HERE *)
☐
☐
Exercise: 4 stars, recommended (forall_exists_challenge)
Challenge problem: Define two recursive Fixpoints, forallb and existsb. The first checks whether every element in a list satisfies a given predicate:
forallb oddb [1,3,5,7,9] = true
forallb negb [false,false] = true
forallb evenb [0,2,4,5] = false
forallb (beq_nat 5) [] = true
The function existsb checks whether there exists an element in
the list that satisfies a given predicate:
forallb negb [false,false] = true
forallb evenb [0,2,4,5] = false
forallb (beq_nat 5) [] = true
existsb (beq_nat 5) [0,2,3,6] = false
existsb (andb true) [true,true,false] = true
existsb oddb [1,0,0,0,0,3] = true
existsb evenb [] = false
Next, create a nonrecursive Definition, existsb', using
forallb and negb.
existsb (andb true) [true,true,false] = true
existsb oddb [1,0,0,0,0,3] = true
existsb evenb [] = false
(* FILL IN HERE *)
☐
☐
Exercise: 2 stars, optional (index_informal)
Recall the definition of the index function:
Fixpoint index {X : Type} (n : nat) (l : list X) : option X :=
match l with
| [] => None
| a :: l' => if beq_nat n O then Some a else index (pred n) l'
end.
Write an informal proof of the following theorem:
match l with
| [] => None
| a :: l' => if beq_nat n O then Some a else index (pred n) l'
end.
∀ X n l, length l = n → @index X (S n) l = None.
(* FILL IN HERE *)☐


Files CCore/inc/Move.h CCore/src/Move.cpp
First of all, CCore Move is not a C++11 move. Don't mess it up. Move is designed to solve the following task: assume you have an object and you want to move it to another memory location. Once you have an appropriate block of memory, you need to create the copy of the object there and destroy the original object as the one operation. Unlike the copy operation, Move can be implemented as an efficient operation for a wide range of types. This is because we don't need to create an additional state, we just have to replace the existing one into another memory location. So before the operation we have the object and the raw memory, after we have the raw memory and the moved object.
There is a technical difficulty with the Move implementation: C++ requires a some constructor call for the object creation and the destructor call for the object life-time termination (with some minor exceptions). To make the moving derivable we have to use the Move constructor as the implementation point for it.
template <class T> T * CopyMove(T *obj,Place<void> place) noexcept(EnableNoExcept); // for efficiently copyable classes template <class T> T * SwapMove(T *obj,Place<void> place) noexcept(EnableNoExcept); // for classes with objSwap() // and efficient default template <class T> T * CtorMove(T *obj,Place<void> place) noexcept(EnableNoExcept); // for classes with Move constructor template <class T> T * Move(T *obj,Place<void> place) noexcept(EnableNoExcept); // general
Normally you should use the function Move() for Move operation. If the destined type is a class type with the method objMove(), it is called to do the job. Otherwise, if the destined type is a class type with the method objSwap(), the SwapMove() is used. In this case class must have the efficient default constructor. Finally, CopyMove() is called for remaining cases. It is assumed, that such types are efficiently copyable.
You can also specialize the struct MoveAdapters.
namespace N { class C { .... }; } // namespace N namespace CCore { template<> struct MoveAdapters<false,false,N::C> { static N::C * Move(N::C *obj,Place<void> place) { .... } }; } // namespace CCore
The most convenient way to make a class movable is to define the method objSwap() and make it both swappable and movable. But for the sake of efficiency, you may define the method objMove(). In this case the best way is to define the same time the Move constructor and derived objMove() from it. Consider the following example:
struct S { A a; // class A has Move constructor B b; // type B is efficiently copyable C c; // class C has Move constructor // swap/move objects void objSwap(S &obj) { Swap(a,obj.a); Swap(b,obj.b); Swap(c,obj.c); } explicit S(ToMoveCtor<S> obj) // the Move constructor signature : a(ObjToMove(obj->a)), // member move with its Move constructor b(obj->b), // member move by copying c(ObjToMove(obj->c)) // member move with its Move constructor { } S * objMove(Place<void> place) { return CtorMove(this,place); } };
The reason to define the Move constructor is to support the further derivation of it. The Move constructor is called in the following context: an object is being moving, the original object will be destroyed by the call of destructor right after Move constructor is finished. Here is the template for the moving of Resource Host Types.
class H : NoCopy { private: ResourceHandle h; // Small Data Type public: H() { SetNull(h); } H(A a,B b,C c) { h=New(a,b,c); } ~H() { if( NotNull(h) ) Delete(h); } // may help compiler to eliminate the following // // SetNull(h); // if( NotNull(h) ) Delete(h); // end-of-object-life-time; // // sequence of actions // move objects explicit H(ToMoveCtor<H> obj) { h=obj->h; SetNull(obj->h); } H * objMove(Place<void> place) { return CtorMove(this,place); } };
The class ToMoveCtor<T> is a simple wrapper over the pointer to the type T:
/* struct ToMoveCtor<T> */
template <class T>
struct ToMoveCtor
{
T *obj;
explicit ToMoveCtor(T &obj_) { obj=&obj_; }
T * operator -> () const { return obj; }
template <class S>
ToMoveCtor<S> cast() const { return ToMoveCtor<S>(*obj); }
};
It is solely introduced to designate Move constructors. The method cast() can be used to "touch" a base class subobject in the Move constructor's body.
CCore is not using C++11 move constructors for Moving. C++11 move constructors were introduced to solve some language problems. The one of such problems is the returning value from a function. Consider this:
class C { public: C(); C(C &&src); ~C(); }; C func() { C obj; return obj; // move object here instead of copy }
But this solution is a wrongdoing. The proper approach would be the changing of the return semantic: operator return should construct the object using any desired constructor instead of copying it.
class Class { public: Class(A a,B b,C c); ~Class(); }; Class func() { A a; B b; C c; return(a,b,c); // calls Class(a,b,c) to create the return object }
The problem with the move constructor is it is a destructive implicit operation and as such is error-prone. So in CCore C++11 move is prohibited. Instead we are using the Move constructor, which is explicit and is called only under specified condition: the destructor of the argument is called right after constructor is called, i.g. there is no other methods of the argument are called between them.


{% include 'head.html' %}
{% include 'ctf.html' %} {% include 'chat.html' %}
Fakebook
Logout
{{ name }}
Welcome to the Fakebook beta, {{ name }}!
Search
{% include 'footer.html' %}


Ashley Graham marks Thanksgiving with naked pregnant selfie
Ashley Graham is seven months pregnant, and is set to welcome a baby boy in January.
And the model has given thanks for her blossoming baby bump by posting a naked selfie of her changing body.
The 32-year-old shared a beautiful nude selfie, showing off her bump, on Thanksgiving and she’s giving Demi Moore’s infamous Vanity Fair cover a run of its money.
Ashley posted the picture to her Instagram stories, with the snap seeing her standing to the side and covering her boobs with one hand.
The model positioned a Happy Thanksgiving GIF beneath her bump to make sure the picture didn’t get too NSFW, and it’s clear that even though she’s approaching maternity leave, Ashley is still working those angles.
Ashley spent Thanksgiving with her husband Justin Ervin and their family and friends, with the star posting a series of pictures of the delicious spread that they had laid on.
Advertisement Advertisement
We’re talking turkey, ribs, sweet potatoes, sprouts, cranberry sauce… sorry, we’re salivating.
And Ash made the most of eating for two, as she shared a snap from the lift after dinner with her husband, writing: ‘Mommy & Daddy are FULL.’
Justin and Ashley celebrated their ninth wedding anniversary in August, and chose the milestone to announce they were expecting their first baby together.
On an appearance on The Ellen Show, Ashley revealed they are having a baby boy, and he is due in mid-January – just before the star’s 33rd birthday.

The body positivity campaigned wrote on Instagram: ‘Getting bigger and bigger and trying to embrace my new body everyday. It’s a journey and I’m so thankful to have such a supportive community.’
All we know is Ashley looks amazing, and that is gonna be one cute baby.
Got a showbiz story?
If you've got a celebrity story, video or pictures get in touch with the Metro.co.uk entertainment team by emailing us<EMAIL_ADDRESS>calling 020 3615 2145 or by visiting our Submit Stuff page - we'd love to hear from you.


Rafforty:
Then, allow me to continue. We have not found a way to save our guild members or Kier. For now they seem doomed to remain ice sculptures. But the information they died for is very valuable.
They discovered how to defeat Ice Queen Freya! And for that, their deaths were not in vain!
Continue listening.


@inproceedings{tanwisuth2021prototype, title={A Prototype-Oriented Framework for Unsupervised Domain Adaptation}, author={Korawat Tanwisuth and Xinjie Fan and Huangjie Zheng and Shujian Zhang and Hao Zhang and Bo Chen and Mingyuan Zhou}, booktitle = {NeurIPS 2021: Neural Information Processing Systems}, month={Dec.}, Note = {(the first three authors contributed equally)}, year = {2021} }


--- permalink: /404.html layout: null ---
We're sorry that a 404 link not found has appeared.
We do our best to avoid these and will
do our best to get you where you need to go.
Please head back to the home page if you think you
can get to what you want from there.
Please feel free to contact a member of the team here:
Digital Preservation is People::Issues


Find a way to execute arbitrary javascript on this page and win Intigriti swag.
Rules:
- This challenge runs from December 7th until December 13th, 11:59 PM CET.
- Out of all correct submissions, we will draw six winners on Monday, December 14th:
- Three randomly drawn correct submissions
- Three best write-ups
- Every winner gets a €50 swag voucher for our swag shop
- The winners will be announced on our Twitter profile.
- For every 100 likes, we'll add a tip to announcement tweet.
The solution...
By the way...
Since we've paid out €185.000 in bounties in one day, we understand that some of our hackers need help calculating their bounty earnings. We asked our intern to create this fancy Intigriti bug bounty calculator for you. Enjoy!


Elizabeth Banks shocks Graham Norton Show viewers with Prince Andrew joke
Elizabeth Banks shocked viewers watching The Graham Norton Show with a totally unexpected joke about Prince Andrew.
Appearing on the show alongside Ricky Gervais, Kylie Minogue and Lewis Hamilton, Graham attempted to embarrass the actress with a hilarious throwback photo from her teens, sporting a stylish white polo neck with matching white hoops with her hair in its naturally curly state.
‘That’s my hair,’ Elizabeth laughed, with Ricky Gervais joking: ‘Sorry, that’s a tree behind you?’
Advertisement Advertisement
‘That’s Marge Simpson hair,’ Graham added.
‘But look how proud I am,’ Elizabeth added. ‘I made that necklace myself, I was not really allowed to wear hoop earrings until I was older, those were probably some of my first hoop earrings.’
Pointing at the hand lurking in the picture, Graham said: ‘I’ve only just noticed this hand, is it someone saying, “you’ll regret this photograph.”’
‘That’s Prince Andrew’s hand,’ the 45-year-old actress shot back, prompting gasps from her fellow guest Kylie Minogue and Ricky while the audience offered her uproarious laughter.
‘Oh God, Jesus,’ Ricky said, while Graham insisted: ‘Photoshop, it’s just Photoshop.’
And it seems the viewers at home were just as impressed with Elizabeth’s edgy humour as the live audience.
‘”That’s Prince Andrew’s hand!”
Elizabeth’s comment was made all the more impressive given the show’s all-star guest list, with viewers wondering how the Charlie’s Angels director had somehow managed to make the most outrageous joke on a sofa that included Ricky Gervais.
Advertisement Advertisement
‘Even @rickygervais thinking, “Ooh I wouldn’t have gone there” about Elizabeth Banks’s Prince Andrew joke,’ one Twitter user wrote.
Elizabeth Banks: 1, everyone else: 0.
The Graham Norton returns next Friday at 10.40pm on BBC One.
Got a showbiz story?
If you've got a story, video or pictures get in touch with the Metro.co.uk Entertainment team by emailing us<EMAIL_ADDRESS>calling 020 3615 2145 or by visiting our Submit Stuff page - we'd love to hear from you.


INAC 2019: Biggest art and Craft Expo commences in Abuja
By Okorie UGURU
The much awaited International Art and Crafts Expo(INAC) holding at the FCT Exhibition Pavilion will light up Abuja on November 20th and will last till 24th.
The Director-General, National ouncil for Arts and Culture, Otunba Segun Runsewe assures on a special outing with the provision of free BMI, free eye testing/glasses, free dental services, free skill acquisition and Waste to Wealth initiative.
According to the NCAC chief who is leaving no stone unturned in ensuring a successful outing, this year’s INAC has been carefully packaged to empower Nigerians by providing free skills for small and medium startups.
Read Also INAC expo toast of exhibitors
Runsewe encourages Nigerians and indeed foreign nationals to take full advantage of the components of INAC.
He confirmed that renowned event management outfit, Innate Arts and Media(I Am) will take control of logistics just as he revealed that fast rising Urban Afro musician, Yega has also been booked to perform at the closing on the 24th of November.
Out of 30 countries from around the world that are billed to exhibit during the event, 4 have expressed commitment to take special days to thrill Guests and participants.
China will take centre stage on the 21th to showcase its oriental endowments as a unique cultural destination of sorts.
On the 22nd, India will be on hand to entertain guests with breathtaking music and dance routines, in a fantastic showing reminiscent of Bollywood.
Venezuela and Bangladesh will combine on the 23rd for a double dose of excitement in what has become a much anticipated aspect of INAC since Runsewe expanded the Expo to a fanfare of global repute in 2017.


Multipart testing
Given server, that mirrors request
Multipart request may contains one or more parts with specified content-type
For file part content-type is should be not specified
test-part
{
"test": "{{name}}"
}
{
"part1": "file",
"fileName": "test.txt",
"part1": "jsonPart",
"json": {
"test": "{{name}}"
}
}
ignored


class Slug
A Slug is a unique, human-friendly identifier for an ActiveRecord.
Public Instance Methods
current?()
click to toggle source
Whether this slug is the most recent of its owner's slugs.
# File lib/friendly_id/active_record2/slug.rb, line 57 def current? sluggable.slug == self end
is_most_recent?()
click to toggle source
@deprecated Please used #current?
# File lib/friendly_id/active_record2/slug.rb, line 66 def is_most_recent? warn("Slug#is_most_recent? is deprecated and will be removed in FriendlyId 3.0. Please use Slug#current?") current? end
outdated?()
click to toggle source
# File lib/friendly_id/active_record2/slug.rb, line 61 def outdated? !current? end
to_friendly_id()
click to toggle source
# File lib/friendly_id/active_record2/slug.rb, line 71 def to_friendly_id sequence > 1 ? friendly_id_with_sequence : name end
validate_name()
click to toggle source
Raise a FriendlyId::SlugGenerationError if the slug name is blank.
# File lib/friendly_id/active_record2/slug.rb, line 76 def validate_name if name.blank? raise FriendlyId::BlankError.new("slug.name can not be blank.") end end


Review: Tech21’s ‘Made for Google’ Pixel 4 accessories are a bit of a mixed bag
by Ben SchoonIf you picked up a Pixel 4 over the holiday sales and you’re looking for a case to go with it, products with the “Made for Google” badge are a great place to start. Tech21 is one of the biggest names in that collection, and over the past couple of weeks I’ve spent some time with the company’s Pixel 4 XL accessories.
Evo Check — great protection, better customization
First and foremost, there’s Tech21’s signature case, the Evo Check. This somewhat thick plastic case is grippy, comfortable, and most importantly very protective. The case is rated for a 12-foot drop with a thick border around the sides of the phone, full protection along the back, and a raised lip to help protect the screen. The entire case is antimicrobial, too, which means it will stay much cleaner than other cases.
In testing out the Evo Check for Pixel 4 XL, I found that it’s still a pretty sweet case. The buttons feel solid and the cutouts for the speaker and USB-C port are pretty much perfect. The camera cutout on the back is a little off, though. So far, only Google’s Fabric case has been perfect for me.
Perhaps the biggest benefit to Tech21’s Evo Check for Pixel 4 is that it comes in multiple colors and with customizable buttons. I spent my time with the bright “Could by Coral” version — although, in hindsight, “Indigo” would have looked way better with my white Pixel — and it shipped with coral, yellow, and blue buttons. I swapped out the coral for the blue. The process of removing the buttons is a pain, but it’s great that you get the option.
Evo Check costs $39.99, which isn’t cheap, but it’s a great case overall that I wouldn’t regret spending the money on.
Studio Colour — slim and made from plants
My favorite of the two cases from Tech21 was the Studio Colour. I picked up the “Let Off Steam” version of this case, which is a slightly blue shade of gray. It’s basic but unique. As a side note to Tech21, I need that “Life on Mars” color found on the iPhone’s version of the case on Pixel immediately.
The Studio Colour caught my eye primarily because it’s not made from plastic like most cases are. Instead, Tech21 uses plant-based materials to craft this Pixel 4 case. This results in buttons that are a bit stiff, but the overall case feels uncompromised from the material choice. Cutouts are mostly perfect, aside from the camera which, again, is a bit off.
The slim design of the Studio Colour also felt great. The case itself is a bit stiff, which makes the overall thin profile feel safer and less prone to any damage.
Studio Colour costs $29, and it’s well worth the money if you like the colors it offers.
 They’re almost always worse-feeling or looking than the glass on your phone, but I’d rather deal with that than shell out for a screen repair or a new phone entirely.
Tech21’s Impact Shield screen protector looks good at first glance online, but I can’t stress enough that you should not spend your money on this product.
The Impact Shield is a plastic screen protector which the company says is scratch-resistant, self-healing, and “easy to apply.” Those first two points may be true — I frankly couldn’t use the product long enough to test — but even if so, they’re overshadowed by a plethora of negatives.
Most importantly, this screen protector doesn’t actually cover the entire display. It only goes up to the top bezel, leaving a good portion of the glass completely uncovered. This is something you can’t know for sure based on the company’s listings.
The screen protector itself also seems to have absolutely no oleophobic coating, which means smudges appear almost instantly and are hard to get off.
The installation process may be the most flawed portion of this product, though. Tech21’s packaging makes the instructions a bit hard to find, and you won’t find any dust removal stickers or wet wipes to help clean off the display. The included microfiber cloth also left my display with more dust attached than before I wiped it down.
The plastic installation guide piece also leaves far too much room for error, which left me with a misaligned screen protector. Part of that alignment is definitely on my own user error, but the guide piece is far worse than similar installation methods I’ve used for similar screen protectors.
I could go on a bit more about what’s wrong with the Impact Shield, but I think I’ve made my point. You should not buy this screen protector, especially for $29. There are way better options out there for much less money.
More on Google Pixel:
- Review: Google’s Pixel 4 fabric case is still great, but a step backward
- The best cases and covers for your Google Pixel 4 and 4 XL [Video]
- Google Pixel 4 Review: A truly stellar Android experience… while it lasts
Disclosure: Tech21 provided review units of the Evo Check and Impact Shield products. The Studio Colour was purchased by the author directly.
FTC: We use income earning auto affiliate links. More.


Book List 2: Electric Boogaloo
Add a Book
View All Books
Admin
Something went wrong!
My Books
Submit
Add a New Book
Add This Book
Update a Book
Update This Book


We examine services!
- reinvent proactive portals
- whiteboard customized markets
- expedite holistic eyeballs
- architect proactive niches
- seize cross-media functionalities
- expedite wireless systems
- expedite synergistic channels
- innovate wireless e-markets
- orchestrate global infrastructures
- benchmark B2C platforms
- leverage turn-key infrastructures
- iterate bricks-and-clicks e-services
- syndicate leading-edge platforms


from typing import List
import numpy as np
from banditpylib.arms import GaussianArm
from banditpylib.data_pb2 import Context, Actions, Feedback, ArmPull, \
ArmFeedback
from banditpylib.learners import Goal, IdentifyBestArm, MaximizeTotalRewards
from .utils import Bandit
[docs]class LinearBandit(Bandit):
r"""Finite-armed linear bandit
Arms are indexed from 0 by default. Each pull of arm :math:`i` will generate
an `i.i.d.` reward from distribution :math:`\langle \theta, v_i \rangle
+ \epsilon`, where :math:`v_i` is the feature vector of arm :math:`i`,
:math:`\theta` is the unknown parameter and :math:`\epsilon` is a zero-mean
noise.
:param List[np.ndarray] features: feature vectors of the arms
:param np.ndarray theta: unknown parameter theta
:param float std: standard variance of noise
"""
def __init__(self,
features: List[np.ndarray],
theta: np.ndarray,
std: float = 1.0):
if len(features) < 2:
raise ValueError('The number of arms is expected at least 2. Got %d.' %
len(features))
for (i, feature) in enumerate(features):
if feature.shape != theta.shape:
raise ValueError('Dimension of arm %d\'s feature vector is expected '
'the same as theta\'s. Got %d.' % (i, len(feature)))
self.__features = features
self.__theta = theta
self.__arm_num = len(features)
if std < 0:
raise ValueError(
'Standard deviation of noise is expected greater than 0. Got %.2f' %
std)
self.__std = std
# Each arm in linear bandit can be seen as a Gaussian arm
self.__arms = [GaussianArm(np.dot(feature, self.__theta), self.__std) \
for feature in self.__features]
self.__best_arm_id = max([(arm_id, arm.mean)
for (arm_id, arm) in enumerate(self.__arms)],
key=lambda x: x[1])[0]
self.__best_arm = self.__arms[self.__best_arm_id]
@property
def name(self) -> str:
return 'linear_bandit'
@property
def context(self) -> Context:
return Context()
def _take_action(self, arm_pull: ArmPull) -> ArmFeedback:
"""Pull one arm
Args:
arm_pull: arm id and its pulls
Returns:
arm_feedback: arm id and its rewards
"""
arm_id = arm_pull.arm.id
pulls = arm_pull.times
if arm_id not in range(self.__arm_num):
raise ValueError('Arm id is expected in the range [0, %d). Got %d.' %
(self.__arm_num, arm_id))
arm_feedback = ArmFeedback()
# Empirical rewards when `arm_id` is pulled for `pulls` times
em_rewards = self.__arms[arm_id].pull(pulls)
self.__regret += (self.__best_arm.mean * pulls - em_rewards)
arm_feedback.arm.id = arm_id
arm_feedback.rewards.extend(list(em_rewards)) # type: ignore
return arm_feedback
[docs] def feed(self, actions: Actions) -> Feedback:
feedback = Feedback()
for arm_pull in actions.arm_pulls:
if arm_pull.times > 0:
arm_feedback = self._take_action(arm_pull=arm_pull)
feedback.arm_feedbacks.append(arm_feedback)
return feedback
[docs] def reset(self):
self.__regret = 0.0
@property
def arm_num(self) -> int:
"""Total number of arms"""
return self.__arm_num
@property
def features(self) -> List[np.ndarray]:
"""
Returns:
feature vectors
"""
return self.__features
def __best_arm_regret(self, arm_id) -> int:
"""
Args:
arm_id: best arm identified by the learner
Returns:
0 if `arm_id` is the best arm else 1
"""
return int(self.__best_arm_id != arm_id)
[docs] def regret(self, goal: Goal) -> float:
if isinstance(goal, IdentifyBestArm):
return self.__best_arm_regret(goal.best_arm)
elif isinstance(goal, MaximizeTotalRewards):
return self.__regret
raise Exception('Goal %s is not supported.' % goal.name)


Your task is to first find the largest number in each of the two boxes and then add up the two
numbers.
Submit your answer in the box below.
| Box 1 | Box 2 | |
|---|---|---|
|
|
|
Tasks attempted so far:
Tasks correct so far:


TO-DO LIST
Buy Robes
Fight Malfoy
Buy New Wand
Feed Hedwig
Send Owl to Sirius
Go To Potions Class
wash Robes
Visit Hagrid
Kill Voldemort


Great moments in PC gaming: "Don't startle the witch"
by Jody MacgregorGreat moments in PC gaming are bite-sized celebrations of some of our favorite gaming memories.
Left 4 Dead
(Image credit: Valve)
Developer: Valve
Publisher: Valve
Year: 2008
Each of the special infected in Left 4 Dead has its own musical tell. The hunter's is a tripping plink-plonk-plink, the spitter's got an eerie four notes versus the smoker's simple two, while the tank rolls up with its own miniature symphony. Play for long enough and you'll learn them all, but it's probably the witch you memorize first. Her musical sting is high-pitched and insistent, the first melody quickly joined by a second to create a sense of escalation. Even before you hear her sobbing, that tune plays and you know it's time to turn off the flashlight and step carefully.
Not startling her should be easy, but then the director plants her somewhere unavoidable, or your friend turns a corner a little too fast, or a stray bullet or pipe bomb catches her and that's it. She goes from sobbing to screaming and beelines for the survivor who startled her, fingerknives out as she knocks them down. She's not the kind of threat who'll take out a whole party, and eventually you learn to deal with her, but the terror of that shrieking attack is hard to get used to.
When you stumble across zombies in Left 4 Dead they're often just doing their own thing, leaning against walls looking sad. Until you bumble up waving your guns and one-liners around they just want to be left alone with their misery.  Left 4 Dead calls them Infected rather than zombies which rehumanizes them a little, and the witch is the most human of all, the one who seems most aware of the tragedy of her situation.
The other special infected are designed to split the party.  The witch has a uniting effect, forcing everyone to huddle together on the far side of a room trying to pass without incident in total silence.
Left 4 Dead is a chatty game, one where the characters are jokey and everyone has to communicate when they need healing or are low on ammo. The fact the witch can make everyone shush and get serious, whispering into their mics when she's around as if she can hear them over the internet, is honestly a miracle.
If you think the tank is scarier just because it has more hit points I don't even know what to say to you, man.


?6
7
8
9
10
,
ã
v
The
New
York
copyright
reserved
Botanical
Garden
NEW
YORKBOTANICAL
GARDEN
01447758.........
ANNOTATION
LABEL
Oenothera
rosea
L'Her
ex
Ait.
determined
by
p.H.
Raven
&
D.R.
Parnell
1970
PLANTS
OF
JAMAICA
COLLECTED
FOR
THE
HERBARIUM
OF
DUKE
UNIVERSITY
Oenothera
rosea
Soland.
det.
C.
D.
Adams
1963
St.
Andrew
Parish:
Grassy
hillside
just
below
Mt.
Horeb,
c.
3900
feet.
Fairly
common.
Hypanthium
and
calyx
lobes
greenish-white,
tinged
with
reddish-purple;
petals
bright
reddish-purple,
greenish
yellow
at
bases;
anthers
brown,
style
and
stigmas
white,
stigmas
tipped
with
reddish
purple;
ovary
m.
r.
crosby
green,
ribbed
with
red.
H.
A.
HESPENHEIDE
w.
R.
ANDERSON
no.
372
28
June
1963
01447758
Legend -
Level of confidence that token is an accurately-transcribed word
extremely low
very low
low
undetermined
medium
high
very high


menu
FastMed
Keyword (Required)
Provider Type
Primary Care
Specialist
Urgent Care
Emergency
Search Radius
5 miles
10 miles
15 miles
25 miles
50 miles
Search
{{result.name}}
{{result.formatted_address}}
Wait: {{result.distance}} minutes
More Information


{% load templatetag_handlebars %} {% tplhandlebars uploader_parser_options %}
You can change the parser options if your data was not properly imported.
Your parser options have been changed.


A collection of my projects for skill demo: JavaScript projects Memory Card Game Simple Scientific Calculator D3.js - Data Visualization projects Bar chart - Unemployment rate in regions of Vietnam Grouped bar-chart - Bar chart - Unemployment rate in regions of Vietnam Visualization of Vietnam's regional population (data 2015). Larger font size means bigger population.


USE Method: Linux Performance Checklist
The USE Method provides a strategy for performing a complete check of system health, identifying common bottlenecks and errors. For each system resource, metrics for utilization, saturation and errors are identified and checked. Any issues discovered are then investigated using further strategies.
This is an example USE-based metric list for Linux operating systems (eg, Ubuntu, CentOS, Fedora). This is primarily intended for system administrators of the physical systems, who are using command line tools. Some of these metrics can be found in remote monitoring tools.
Physical Resources
| component | type | metric |
|---|---|---|
| CPU | utilization | system-wide: vmstat 1, "us" + "sy" + "st"; sar -u, sum fields except "%idle" and "%iowait"; dstat -c, sum fields except "idl" and "wai"; per-cpu: mpstat -P ALL 1, sum fields except "%idle" and "%iowait"; sar -P ALL, same as mpstat; per-process: top, "%CPU"; htop, "CPU%"; ps -o pcpu; pidstat 1, "%CPU"; per-kernel-thread: top/htop ("K" to toggle), where VIRT == 0 (heuristic). [1] |
| CPU | saturation | system-wide: vmstat 1, "r" > CPU count [2]; sar -q, "runq-sz" > CPU count; dstat -p, "run" > CPU count; per-process: /proc/PID/schedstat 2nd field (sched_info.run_delay); perf sched latency (shows "Average" and "Maximum" delay per-schedule); dynamic tracing, eg, SystemTap schedtimes.stp "queued(us)" [3] |
| CPU | errors | perf (LPE) if processor specific error events (CPC) are available; eg, AMD64's "04Ah Single-bit ECC Errors Recorded by Scrubber" [4] |
| Memory capacity | utilization | system-wide: free -m, "Mem:" (main memory), "Swap:" (virtual memory); vmstat 1, "free" (main memory), "swap" (virtual memory); sar -r, "%memused"; dstat -m, "free"; slabtop -s c for kmem slab usage; per-process: top/htop, "RES" (resident main memory), "VIRT" (virtual memory), "Mem" for system-wide summary |
| Memory capacity | saturation | system-wide: vmstat 1, "si"/"so" (swapping); sar -B, "pgscank" + "pgscand" (scanning); sar -W; per-process: 10th field (min_flt) from /proc/PID/stat for minor-fault rate, or dynamic tracing [5]; OOM killer: dmesg | grep killed |
| Memory capacity | errors | dmesg for physical failures; dynamic tracing, eg, SystemTap uprobes for failed malloc()s |
| Network Interfaces | utilization | sar -n DEV 1, "rxKB/s"/max "txKB/s"/max; ip -s link, RX/TX tput / max bandwidth; /proc/net/dev, "bytes" RX/TX tput/max; nicstat "%Util" [6] |
| Network Interfaces | saturation | ifconfig, "overruns", "dropped"; netstat -s, "segments retransmited"; sar -n EDEV, *drop and *fifo metrics; /proc/net/dev, RX/TX "drop"; nicstat "Sat" [6]; dynamic tracing for other TCP/IP stack queueing [7] |
| Network Interfaces | errors | ifconfig, "errors", "dropped"; netstat -i, "RX-ERR"/"TX-ERR"; ip -s link, "errors"; sar -n EDEV, "rxerr/s" "txerr/s"; /proc/net/dev, "errs", "drop"; extra counters may be under /sys/class/net/...; dynamic tracing of driver function returns 76] |
| Storage device I/O | utilization | system-wide: iostat -xz 1, "%util"; sar -d, "%util"; per-process: iotop; pidstat -d; /proc/PID/sched "se.statistics.iowait_sum" |
| Storage device I/O | saturation | iostat -xnz 1, "avgqu-sz" > 1, or high "await"; sar -d same; LPE block probes for queue length/latency; dynamic/static tracing of I/O subsystem (incl. LPE block probes) |
| Storage device I/O | errors | /sys/devices/.../ioerr_cnt; smartctl; dynamic/static tracing of I/O subsystem response codes [8] |
| Storage capacity | utilization | swap: swapon -s; free; /proc/meminfo "SwapFree"/"SwapTotal"; file systems: "df -h" |
| Storage capacity | saturation | not sure this one makes sense - once it's full, ENOSPC |
| Storage capacity | errors | strace for ENOSPC; dynamic tracing for ENOSPC; /var/log/messages errs, depending on FS |
| Storage controller | utilization | iostat -xz 1, sum devices and compare to known IOPS/tput limits per-card |
| Storage controller | saturation | see storage device saturation, ... |
| Storage controller | errors | see storage device errors, ... |
| Network controller | utilization | infer from ip -s link (or /proc/net/dev) and known controller max tput for its interfaces |
| Network controller | saturation | see network interface saturation, ... |
| Network controller | errors | see network interface errors, ... |
| CPU interconnect | utilization | LPE (CPC) for CPU interconnect ports, tput / max |
| CPU interconnect | saturation | LPE (CPC) for stall cycles |
| CPU interconnect | errors | LPE (CPC) for whatever is available |
| Memory interconnect | utilization | LPE (CPC) for memory busses, tput / max; or CPI greater than, say, 5; CPC may also have local vs remote counters |
| Memory interconnect | saturation | LPE (CPC) for stall cycles |
| Memory interconnect | errors | LPE (CPC) for whatever is available |
| I/O interconnect | utilization | LPE (CPC) for tput / max if available; inference via known tput from iostat/ip/... |
| I/O interconnect | saturation | LPE (CPC) for stall cycles |
| I/O interconnect | errors | LPE (CPC) for whatever is available |
- [1] There can be some oddities with the %CPU from top/htop in virtualized environments; I'll update with details later when I can.
- CPU utilization: a single hot CPU can be caused by a single hot thread, or mapped hardware interrupt. Relief of the bottleneck usually involves tuning to use more CPUs in parallel.
- uptime "load average" (or /proc/loadavg) wasn't included for CPU metrics since Linux load averages include tasks in the uninterruptable state (usually I/O).
- [2] The man page for vmstat describes "r" as "The number of processes waiting for run time", which is either incorrect or misleading (on recent Linux distributions it's reporting those threads that are waiting, and threads that are running on-CPU; it's just the wait threads in other OSes).
- [3] There may be a way to measure per-process scheduling latency with perf's sched:sched_process_wait event, otherwise perf probe to dynamically trace the scheduler functions, although, the overhead under high load to gather and post-process many (100s of) thousands of events per second may make this prohibitive. SystemTap can aggregate per-thread latency in-kernel to reduce overhead, although, last I tried schedtimes.stp (on FC16) it produced thousands of "unknown transition:" warnings.
- LPE == Linux Performance Events, aka perf_events. This is a powerful observability toolkit that reads CPC and can also use static and dynamic tracing. Its interface is the perf command.
- CPC == CPU Performance Counters (aka "Performance Instrumentation Counters" (PICs) or "Performance Monitoring Events" (PMUs) or "Hardware Events"), read via programmable registers on each CPU by perf (which it was originally designed to do). These have traditionally been hard to work with due to differences between CPUs. LPE perf makes life easier by providing aliases for commonly used counters. Be aware that there are usually many more made available by the processor, accessible by providing their hex values to perf stat -e. Expect to spend some quality time (days) with the processor vendor manuals when trying to use these. (My short video about CPC may be useful, despite not being on Linux).
- [4] There aren't many error-related events in the recent Intel and AMD processor manuals; be aware that the public manuals may not show a complete list of events.
- [5] The goal is a measure of memory capacity saturation - the degree to which a process is driving the system beyond its ability (and causing paging/swapping). High fault latency works well, but there isn't a standard LPE probe or existing SystemTap example of this (roll your own using dynamic tracing). Another metric that may serve a similar goal is minor-fault rate by process, which could be watched from /proc/PID/stat. This should be available in htop as MINFLT.
- [6] Tim Cook ported nicstat to Linux; it can be found on sourceforge or his blog.
- [7] Dropped packets are included as both saturation and error indicators, since they can occur due to both types of events.
- [8] This includes tracing functions from different layers of the I/O subsystem: block device, SCSI, SATA, IDE, ... Some static probes are available (LPE "scsi" and "block" tracepoint events), else use dynamic tracing.
- CPI == Cycles Per Instruction (others use IPC == Instructions Per Cycle).
- I/O interconnect: this includes the CPU to I/O controller busses, the I/O controller(s), and device busses (eg, PCIe).
- Dynamic Tracing: Allows custom metrics to be developed, live in production. Options on Linux include: LPE's "perf probe", which has some basic functionality (function entry and variable tracing), although in a trace-n-dump style that can cost performance; SystemTap (in my experience, almost unusable on CentOS/Ubuntu, but much more stable on Fedora); DTrace-for-Linux, either the Paul Fox port (which I've tried) or the OEL port (which Adam has tried), both projects very much in beta.
Software Resources
| component | type | metric |
|---|---|---|
| Kernel mutex | utilization | With CONFIG_LOCK_STATS=y, /proc/lock_stat "holdtime-totat" / "acquisitions" (also see "holdtime-min", "holdtime-max") [8]; dynamic tracing of lock functions or instructions (maybe) |
| Kernel mutex | saturation | With CONFIG_LOCK_STATS=y, /proc/lock_stat "waittime-total" / "contentions" (also see "waittime-min", "waittime-max"); dynamic tracing of lock functions or instructions (maybe); spinning shows up with profiling (perf record -a -g -F 997 ..., oprofile, dynamic tracing) |
| Kernel mutex | errors | dynamic tracing (eg, recusive mutex enter); other errors can cause kernel lockup/panic, debug with kdump/crash |
| User mutex | utilization | valgrind --tool=drd --exclusive-threshold=... (held time); dynamic tracing of lock to unlock function time |
| User mutex | saturation | valgrind --tool=drd to infer contention from held time; dynamic tracing of synchronization functions for wait time; profiling (oprofile, PEL, ...) user stacks for spins |
| User mutex | errors | valgrind --tool=drd various errors; dynamic tracing of pthread_mutex_lock() for EAGAIN, EINVAL, EPERM, EDEADLK, ENOMEM, EOWNERDEAD, ... |
| Task capacity | utilization | top/htop, "Tasks" (current); sysctl kernel.threads-max, /proc/sys/kernel/threads-max (max) |
| Task capacity | saturation | threads blocking on memory allocation; at this point the page scanner should be running (sar -B "pgscan*"), else examine using dynamic tracing |
| Task capacity | errors | "can't fork()" errors; user-level threads: pthread_create() failures with EAGAIN, EINVAL, ...; kernel: dynamic tracing of kernel_thread() ENOMEM |
| File descriptors | utilization | system-wide: sar -v, "file-nr" vs /proc/sys/fs/file-max; dstat --fs, "files"; or just /proc/sys/fs/file-nr; per-process: ls /proc/PID/fd | wc -l vs ulimit -n |
| File descriptors | saturation | does this make sense? I don't think there is any queueing or blocking, other than on memory allocation. |
| File descriptors | errors | strace errno == EMFILE on syscalls returning fds (eg, open(), accept(), ...). |
- [8] Kernel lock analysis used to be via lockmeter, which had an interface called "lockstat".
What's Next
See the USE Method for the follow-up strategies after identifying a possible bottleneck. If you complete this checklist but still have a performance issue, move onto other strategies: drill-down analysis and latency analysis.Acknowledgements
Resources used:- dstat documentation
- 20 Linux monitoring tools every sysadmin should know
- Rosetta Stone for Unix
- SystemTap Example Scripts for schedtimes.stp
- PerfUserGuide Linux profiling with Perf (LPE)
- perf announcements on LKML by Ingo Molnar, Peter Zijlstra, ...
- Perf homepage
- lock_stat by Peter Zijlstra
- lockmeter, for historical interest (now done via lock_stat)
- oprofile by John Levon
- Valgrind DRD which has a good list (8.2.4) of detected lock errors
- Linux kernel source
- man pages
Filling this this checklist has required a lot of research, testing and experimentation. Please reference back to this post if it helps you develop related material.
It's quite possible I've missed something or included the wrong metric somewhere (sorry); I'll update the post to fix these up as they are understood.


Inspect Me
What
How
What
I made a website
How
I used these to make this site:
HTML
CSS
JS (JavaScript)


Contact Grabber Options
Destination:
Select where to deliver grabbed contact
Hot Key: Alt+Shift+PageDown
Available Destination URLs:
- One URL per line
- First URL is active selection
- Add optional label at end of each URL after ## (e.g., http://my.domain.com/path?myid=123##My Domain [123])
Active Destination URL:
Go to new tab after posting contact
Lookup:
Select site to lookup grabbed contact
Hot Key: Alt+Shift+PageUp
Available Lookup URLs:
- One URL per line
- First URL is active selection
- Supply substitution variables of the form %FIELD% (only name, email, phone, and URL fields supported)
- Add optional label at end of each URL after ## (e.g., http://my.domain.com/path?name=%NAME%##My Domain [by name])
Active Lookup URL:


{{content-for "head"}} {{content-for "head-footer"}}
JavaScript is currently disabled in your browser settings or your browser does not support JavaScript.
Croodle requires JavaScript. Therefore to use Croodle, you must first enable JavaScript.