text:
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">

<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>Poly: Polymorphism and Higher-Order Functions</title>

PolyPolymorphism and Higher-Order Functions

(* $Date: 2012-09-08 20:51:57 -0400 (Sat, 08 Sep 2012) $ *)

Require Export Lists.

Polymorphism

Polymorphic Lists

 Up to this point, we've been working with lists of numbers.
    Of course, interesting programs also need to be able to manipulate
    lists whose elements are drawn from other types — lists of
    strings, lists of booleans, lists of lists, etc.  We could just
    define a new inductive datatype for each of these, for
    example...

Inductive boollist : Type :=

  | bool_nil : boollist

  | bool_cons : bool → boollist → boollist.

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

Inductive list (X:Type) : Type :=

  | nil : list X

  | cons : X → list X → list X.

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

 What sort of thing is list itself?  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 tell Coq the type of the
    elements in the 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 *)

(Side note on notation: In .v files, the "forall" quantifier is
    spelled out in letters.  In the generated HTML files, ∀ is
    usually typeset as the usual mathematical "upside down A," but
    you'll see the spelled-out "forall" in a few places.  This is just
    a quirk of typesetting: there is no difference in meaning.

 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:

Check (cons nat 2 (cons nat 1 (nil nat))).

(We've gone back to writing nil and cons explicitly here
    because we haven't yet defined the  []  and :: notations for
    the new version of lists.  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.  We'll come back to this point later.)

    As with nil and cons, we can use length by applying it first
    to a type and then to its list argument:

Example test_length1 :

    length nat (cons nat 1 (cons nat 2 (nil nat))) = 2.

Proof. reflexivity. Qed.

To use our length with other kinds of lists, we simply
    instantiate it with an appropriate type parameter:

Example test_length2 :

    length bool (cons bool true (nil bool)) = 1.

Proof. reflexivity. Qed.

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 Annotation Inference

 Let's write the definition of app again, but this time we won't
    specify the types of any of the arguments. Will Coq still accept
    it?

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':

Check app'.

Check app.

It has exactly the same type type as app.  Coq was able to
    use a process 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 find a balance in your own code between
    too many type annotations (so many that they clutter and distract)
    and too few (which forces readers to perform type inference in
    their heads in order to understand your code).

Type Argument Synthesis

 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 annotation inference — and,
    indeed, the two procedures rely on the same underlying mechanisms.
    Instead of simply omitting the types of some arguments to a
    function, like

      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.

    Using implicit arguments, the length function can be written
    like this:

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

Definition list123 :=

  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

...we can use argument synthesis to write this:

Definition list123' := cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

Implicit Arguments

 If fact, we can go further.  To avoid having to sprinkle _'s
    throughout our programs, we can tell Coq always to infer the
    type argument(s) of a given function.

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'').

Alternatively, we can 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):

Definition mynil : list nat := nil.

Alternatively, we can force the implicit arguments to be explicit by
   prefixing the function name with @.

Check @nil.

Definition mynil' := @nil nat.

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:

Definition list123''' := [1, 2, 3].

Exercises: Polymorphic Lists

Exercise: 2 stars, optional (poly_exercises)

 Here are a few simple exercises, just like ones in the Lists
    chapter, 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 rev_involutive : ∀X : Type, ∀l : list X,

  rev (rev l) = l.

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.

☐

Polymorphic Pairs

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

Inductive prod (X Y : Type) : Type :=

  pair : X → Y → prod X Y.

Implicit Arguments pair [[X] [Y]].

As with lists, we make the type arguments implicit and define the
    familiar concrete notation.

Notation "( x , y )" := (pair x y).

We can also use the Notation mechanism to define the standard
    notation for pair types:

Notation "X * Y" := (prod X Y) : type_scope.

(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 built from two
    other values; X*Y is a type built from two other 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, optional (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.

    Uncomment the material below and fill in the definition of
    split.  Make sure it passes the given unit tests.

(*

Fixpoint split

  (* FILL IN HERE *)

Example test_split:

  split (1,false),(2,false) = (1,2,false,false).

Proof. reflexivity.  Qed.

*)

(If you're reading the HTML version of this file, note that
    there's an unresolved typesetting problem in the example: several
    square brackets are missing.  Refer to the .v file for the correct
    version.  ☐

Polymorphic Options

 One last polymorphic type for now: polymorphic options.
    The type declaration generalizes the one for natoption in the
    previous chapter:

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.

Definition hd_opt {X : Type} (l : list X)  : option X :=

  (* FILL IN HERE *) admit.

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.

☐

Functions as Data

Higher-Order Functions

 Like many other modern programming languages — including
    all functional languages (ML, Haskell, Scheme, etc.) — 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:

Definition doit3times {X:Type} (f:X→X) (n:X) : X :=

  f (f (f n)).

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

 In fact, the multiple-argument functions we have already
    seen are also examples of passing functions as data.  To see why,
    recall the type of plus.

Check plus.

(* ==> nat -> nat -> nat *)

Each → in this expression is actually a binary operator
    on types.  (This is the same as saying that Coq primitively
    supports only one-argument functions — do you see why?)  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.

    Conversely, we can reinterpret the type A → B → C as (A *
    B) → C.  This is called uncurrying.  With an uncurried binary
    function, both arguments must be given at once as a pair; there is
    no partial application.

 We can define currying as follows:

Definition prod_curry {X Y Z : Type}

  (f : X * Y → Z) (x : X) (y : Y) : Z := f (x, y).

As an exercise, define its inverse, prod_uncurry.  Then prove
    the theorems below to show that the two are inverses.

Definition prod_uncurry {X Y Z : Type}

  (f : X → Y → Z) (p : X * Y) : Z :=

  (* FILL IN HERE *) admit.

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

☐

Filter

 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.

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 the Lists chapter.

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

 It is a little annoying to be forced to define the function
    length_is_1 and give it a name just to be able to pass it as an
    argument to filter, since we will probably never use it again.
    Moreover, this is not an isolated example.  When using
    higher-order functions, we often want to pass as arguments
    "one-off" functions that we will never use again; having to give
    each of these functions a name would be tedious.

    Fortunately, there is a better way. It is also possible to
    construct a function "on the fly" without declaring it at the top
    level or giving it a name; this is analogous to the notation we've
    been using for writing down constant lists, natural numbers, and
    so on.

Example test_anon_fun':

  doit3times (fun n => n * n) 2 = 256.

Proof. reflexivity. Qed.

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 (filter_even_gt7)

 Use filter (instead of Fixpoint) to write a Coq function
    filter_even_gt7 which takes a list of natural numbers as input
    and keeps only those numbers which are even and greater than 7.

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

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.

☐

Map

 Another handy higher-order function is called map.

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:

Example test_map1: map (plus 3) [2,0,2] = [5,3,5].

Proof. reflexivity. Qed.

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:

Example test_map2: map oddb [2,1,2,5] = [false,true,false,true].

Proof. reflexivity. Qed.

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

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

 An even more powerful higher-order function is called
    fold.  This function is the inspiration for the "reduce"
    operation that lies at the heart of Google's map/reduce
    distributed programming framework.

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

 Most of the higher-order functions we have talked about so
    far take functions as arguments.  Now let's look at some
    examples involving returning functions as the results of other
    functions.

    To begin, here is a function that takes a value x (drawn from
    some type X) and returns a function from nat to X that
    yields x whenever it is called, ignoring its nat argument.

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.

Optional Material

Non-Uniform Inductive Families (GADTs)

 This section needs more text!

 Recall the definition of lists of booleans:

Inductive boollist : Type :=

  boolnil  : boollist

| boolcons : bool → boollist → boollist.

 We saw how it could be generalized to "polymorphic lists" with
    elements of an arbitrary type X.  Here's another way of
    generalizing it: an inductive family of "length-indexed" lists of
    booleans:

Inductive boolllist : nat → Type :=

  boollnil  : boolllist O

| boollcons : ∀n, bool → boolllist n → boolllist (S n).

Implicit Arguments boollcons [[n]].

Check (boollcons true (boollcons false (boollcons true boollnil))).

Fixpoint blapp {n1} (l1: boolllist n1)

               {n2} (l2: boolllist n2)

             : boolllist (n1 + n2) :=

  match l1 with

  | boollnil        => l2

  | boollcons _ h t => boollcons h (blapp t l2)

  end.

Of course, these generalizions can be combined.  Here's the
    length-indexed polymorphic version:

Inductive llist (X:Type) : nat → Type :=

  lnil  : llist X O

| lcons : ∀n, X → llist X n → llist X (S n).

Implicit Arguments lnil [[X]].

Implicit Arguments lcons [[X] [n]].

Check (lcons true (lcons false (lcons true lnil))).

Fixpoint lapp (X:Type)

              {n1} (l1: llist X n1)

              {n2} (l2: llist X n2)

            : llist X (n1 + n2) :=

  match l1 with

  | lnil        => l2

  | lcons _ h t => lcons h (lapp X t l2)

  end.

More About Coq

The apply Tactic

 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.

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.

Exercise: 2 stars, optional (silly_ex)

 Complete the following proof without using simpl.

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.

Exercise: 3 stars, recommended (apply_exercise1)

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.

☐

Exercise: 1 star (apply_rewrite)

 Briefly explain the difference between the tactics apply and
    rewrite.  Are there situations where both can usefully be
    applied?

  (* FILL IN HERE *)

 ☐

The unfold Tactic

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

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.

☐

 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.

Inversion

 Recall the definition of natural numbers:

     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:

 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.

 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

      c a1 a2 ... an = d b1 b2 ... bm

    for some constructors c and d and arguments a1 ... an and
    b1 ... bm.  Then inversion H instructs Coq to "invert" this
    equality to extract the information it contains about these terms:

 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.

 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.

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.

Exercise: 1 star (sillyex1)

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.

☐

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.

Exercise: 1 star (sillyex2)

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.

☐

 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.

Lemma eq_remove_S : ∀n m,

  n = m → S n = S m.

Proof. intros n m eq. rewrite → eq. reflexivity. Qed.

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.

Varying the Induction Hypothesis

 Here is a more realistic use of inversion to prove a
    property that is useful in many places later on...

Theorem beq_nat_eq_FAILED : ∀n m,

  true = beq_nat n m → n = m.

Proof.

  intros n m H. induction n as [| n'].

  Case "n = 0".

    destruct m as [| m'].

    SCase "m = 0". reflexivity.

    SCase "m = S m'". simpl in H. inversion H.

  Case "n = S n'".

    destruct m as [| m'].

    SCase "m = 0". simpl in H. inversion H.

    SCase "m = S m'".

      apply eq_remove_S.

      (* stuck here because the induction hypothesis

         talks about an extremely specific m *)

      Admitted.

The inductive proof above fails because we've set up things so
    that the induction hypothesis (in the second subgoal generated by
    the induction tactic) is

        true = beq_nat n' m → n' = m .

     This hypothesis makes a statement about n' together with the
     particular natural number m — that is, the number m, which
     was introduced into the context by the intros at the top of the
     proof, is "held constant" in the induction hypothesis.  This
     induction hypothesis is not strong enough to make the induction
     step of the proof go through.

     If we set up the proof slightly differently by introducing just
     n into the context at the top, then we get an induction
     hypothesis that makes a stronger claim:

       ∀ m : nat, true = beq_nat n' m → n' = m

     Setting up the induction hypothesis this way makes the proof of
     beq_nat_eq go through:

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.

Similar issues will come up in many of the proofs below.  If you
    ever find yourself in a situation where the induction hypothesis
    is insufficient to establish the goal, consider going back and
    doing fewer intros to make the IH stronger.

Exercise: 2 stars (beq_nat_eq_informal)

 Give an informal proof of beq_nat_eq.

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

☐

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 0 n → 0 = n.

Proof.

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

☐

Exercise: 3 stars (beq_nat_sym_informal)

 Provide an informal proof of this lemma that corresponds
    to your formal proof above:

   Theorem: For any nats n m, beq_nat n m = beq_nat m n.

   Proof:
   (* FILL IN HERE *)

☐

Using Tactics on Hypotheses

 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.

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.

☐

Using destruct on Compound Expressions

 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:

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.

Exercise: 1 star (override_shadow)

Theorem override_shadow : ∀{X:Type} x1 x2 k1 k2 (f : nat→X),

  (override (override f k1 x2) k1 x1) k2 = (override f k1 x1) k2.

Proof.

  (* FILL IN HERE *) Admitted.

☐

Exercise: 3 stars, recommended (combine_split)

(*

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.

*)

☐

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?

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

(* FILL IN HERE *)

☐

The remember Tactic

 (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:

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.

Exercise: 2 stars (override_same)

Theorem override_same : ∀{X:Type} x1 k1 k2 (f : nat→X),

  f k1 = x1 →

  (override f k1 x1) k2 = f k2.

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 apply ... with ... Tactic

 The following silly example uses two rewrites in a row to
    get from [a,b] to [e,f].

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.

☐

Review

 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:

 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

 symmetry:
        changes a goal of the form t=u into u=t

 symmetry in H:
        changes a hypothesis of the form t=u into u=t

 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.

Definition fold_map {X Y:Type} (f : X → Y) (l : list X) : list Y :=

(* FILL IN HERE *) admit.

Write down a theorem in Coq stating that fold_map is correct,
    and prove it.

(* FILL IN HERE *)

☐

Module MumbleBaz.

Exercise: 2 stars, optional (mumble_grumble)

 Consider the following two inductively defined types.

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

(* FILL IN HERE *)

☐

Exercise: 2 stars, optional (baz_num_elts)

 Consider the following inductive definition:

Inductive baz : Type :=

   | x : baz → baz

   | y : baz → bool → baz.

How many elements does the type baz have?
(* FILL IN HERE *)

☐

End MumbleBaz.

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:

      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.

    Prove that existsb' and existsb have the same behavior.

(* 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:

   ∀ X n l, length l = n → @index X (S n) l = None.

(* FILL IN HERE *)

 ☐

Index
This page has been generated by coqdoc

redpajama_set_name: RedPajamaGithub


tree trunks painting environment tree trunk landscape paintings painting tree trunks with lime.
tree trunks painting tree trunk sculpture painting fruit tree trunks white.
tree trunks painting print eucalyptus painting tree trunks with lime.
tree trunks painting view painting fruit tree trunks with lime.
tree trunks painting watercolor tree trunks painting nature background painting tree trunks in watercolor.
tree trunks painting tree painting tree trunks blue.
tree trunks painting purpose of painting tree trunks white.
tree trunks painting tree trunk art painting x tree trunks paintings.
tree trunks painting view painting tree trunks in watercolour.
tree trunks painting painting tree trunks acrylic.
tree trunks painting how to paint snow in oil painting tree trunks white.
tree trunks painting study of the trunk of oil painting john constable painting fruit tree trunks white.
tree trunks painting tree trunk drawing painting fruit tree trunks with lime.
tree trunks painting view tree trunks painting tree trunks white.
tree trunks painting solar tree trunks oil painting painting fruit tree trunks white.
tree trunks painting environment tree trunk landscape paintings tree trunks paintings.
tree trunks painting painting tree trunks with lime.
tree trunks painting banyan tree trunks painting fruit tree trunks with lime.
tree trunks painting tree trunks with painting tree trunks in watercolor.
tree trunks painting unique tree painting campaign saves thousands of trees in state painting citrus tree trunks white.
tree trunks painting fruit tree painting trunks.
tree trunks painting environment tree trunk landscape paintings painting tree trunks in watercolor.
tree trunks painting sunlight on live oak tree trunks painting tree trunks with lime.
tree trunks painting whitewashed tree trunks the unvarnished story painting fruit tree trunks with lime.
tree trunks painting content painting tree trunks with lime.
tree trunks painting why paint tree trunks white painting tree trunks in oil.
tree trunks painting how to paint autumn trees in oil painting tree trunks in oil.
tree trunks painting tree trunks painting tree trunks in oil.
tree trunks painting invisible tree wrapped trunk camouflaged to float on air what does painting tree trunks white do.
tree trunks painting sunlit tree trunk tree trunks paintings.
tree trunks painting van tree roots and tree tree trunks paintings.
tree trunks painting yellow fall foliage on maple trees and ivy entwined tree trunks painting tree trunks white.
tree trunks painting tree trunks painting tree trunks acrylic.


It's never too early to encourage a great vocabulary! Specially made for the very young, this colourful book stimulates excitement about language and confidence with words. It focuses on frequently-used words, introducing each one on a dedicated page with cheerful illustrations. Each word has a simple definition, a range of alternative synonyms, and several short sample phrases to explain usage. Altogether there are over 1000 synonyms, with rainbow-bright artwork and plenty of guidance on how to choose the best words for each context. A lovely resource which every Key Stage 1 classroom should contain.


Stop by our gallery located at the corner of 89A and 40 Soldiers Pass Road, Suites 1 & 2, in Sedona, Arizona.
We are open from 10-5 Monday thru Saturday.
Wayne B Light is the home of the "Cross Maker" We are well known for our inspired cross jewelry collection.
Take a look at our newest custom jewelry designs. Things are always changing and we are always creating.
Contact us or come and see us. We are open from 10am to 5pm Monday through Saturday.
"The Cross Maker", Wayne is famous for his "Inspired Cross Collection".
Come visit us, you are always welcome to come enjoy the store.


At Alofany, our aim is to make shopping convenient for our customers, which is why we offer a range of payment options.
We accept MasterCard, VISA, American Express cards.
We support net banking with almost all Indian banks.
We have taken several steps to ensure that payments made on Alofany are safe and secure. At no point will anyone from Alofany ask you to share your Credit Card, Bank Account or Alofany My Account details via email or call. We request that you do not share these details with anyone under any circumstances.
An order may be cancelled if information provided by a customer is found incomplete. The customer will be notified within 24-72 hours in such an event. It will be the customer's responsibility to furnish correct information and re-place the order within 48 hours.
You can also email us directly at info@alofany.com to immediately get the best possible solutions and information.


text:
Authors: Promote Your Book
Free UK eBooks
Free eBook Filters
Do not show erotica
Show erotica
Literature & Fiction+
Anthologies & Literature Collections
Essays & Correspondence
Mythology & Folk Tales
Religious & Inspirational Fiction
Genre Fiction+
Movie Tie-Ins
Mystery, Thriller & Suspense+
Romance+
Multicultural & Interracial
New Adult & College
Science Fiction & Fantasy+
Nonfiction+
Children's eBooks+
Science Fiction, Fantasy & Scary Stories
Arts & Photography+
Comics & Graphic Novels+
Single Issue Comics
Computers & Technology+
Cookbooks, Food & Wine+
Crafts, Hobbies & Home+
Health, Fitness & Dieting+
Humor & Entertainment+
Parenting & Relationships+
Professional & Technical+
Professional Science
Religion & Spirituality+
Self-Help+
Memory Improvement
Teen & Young Adult+
Amazon Only
Amazon and Smashwords
Smashwords Only
Include Books
New Since My Last Visit
Free Today for the First Time
(in the last 30 days)
Newest, then by Ranking
By Ranking
By Stars
Books Per Page
30 Books Per Page
120 Books Per Page
Length / Type
Free eBooks of Paperback books
Save These Filter Settings
All of the filters are bookmarkable too, so you can also bookmark any page and the filter settings will be kept when you return to the bookmark
Click To Filter
Free Kindle eBooks | Biographies | from Amazon and Smashwords
Showing Free eBook 1-30 of 86
See YOUR eBook promoted here. Click here for details
The Monster That Lived Under My Bed: (Childrens Books, Picture Books, Preschool Books, Books Ages 3-5, Baby Books, Kids Books, Kindergarten books)
by Chloe Sanders
The Monster That Lived Under My BedBen has a funny pet monster that lives under boy's bed. Monster makes him laugh, does gross and funny things. But when it's time to get ready for bed, boy gets in trouble because of the monster. When the boy tries to get a bath, monster turns the lights off, and boy can't find the soap. The boy attempts to get a nighttime outfit, but monster stole his PJ and socks. Tom wanted to eat cookies and drink warm milk before bed, but monster finished all that before he could even touch it. Tom is not mad. He tries to teach the monster some manners and proper bedtime routine."Ben showed his pet Monster how to get clean,They had fun in the bath with Ben's toy submarine.They quickly got washed so they wouldn't be late."You were right, Ben," said Monster, "Bedt...
Genre: Children's eBooks, History, Literature & Fiction, Biographies, Humor, Nonfiction, Children's Nonfiction, Activities, Crafts & Games, Growing Up & Facts of Life
Size: 23 pages
Free eBook download for Kindle from 29 January 2020 onward PDT/PST
American Schoolgirl Explores Mexico: A Memoir
by Ellen Ward Lopez
Genre: Children's eBooks, Geography & Cultures, Biographies, Nonfiction, Children's Nonfiction
Size: 210 pages
Maiden Mermaid - The Tale of Sirena
by Sheri Wall
Would you make a deal with a talking catfish by the light of a full moon?Sirena, a free-spirited Native American maiden, did just that in order to win Brave, her heart's desire. And just as Catfish promisedBrave fell in love so trueIn front of their small villageBrave and Sirena said, I doShe didn't really believe she might be transformed into a mermaid forever.With engaging watercolor illustrations and captivating, rhythmic verse, Maiden Mermaid - The Tale of Sirena will be an enchanting read for both children and adults. Timeless lessons of being patient, trusting carefully, and making wise choices flow just below the surface. This Texas family legend also inspired a bronze mermaid sculpture that can be visited creekside in Salado, Texas.Get your copy now and request downloadable a...
Genre: Children's eBooks, Arts, Music & Photography, History, Biographies, Literature & Fiction, Poetry, American
Reese's Peanut Butter Cups: It's What's Inside that Counts: Invention Project Second Grade Mini-Report
by Addison Oberbrunner
In this mini-report you will discover interesting facts like: H.B. Reese's relationship with Milton Hersey, why Reese named 2 of his candies after 2 of his 16 kids, how he became a master marketer, and why he was inducted into the Candy Hall of Fame. I chose this invention for my second grade mini-report for two reasons. Number one, I like Reese's. Number two, I like chocolate. Therefore, studying H.B. Reese, the inventor of the Reese's Peanut Butter Cups was the perfect choice. I know you'll like it too....
Genre: Children's eBooks, Biographies, Science, Nature & How It Works
Size: 6 pages
The Adventures of Quint the Bookmobile: The Big Move to Roneyville
by Kathleen Quinton
Genre: Children's eBooks, Animals, Literature & Fiction, Action & Adventure, Geography & Cultures, Biographies, Science, Nature & How It Works, Nonfiction, Children's Nonfiction
by J. S. Cooper
**STANDALONE BOOK with no cliffhanger**
New Sexy Standalone from New York Times Bestselling Authors Helen Cooper and JS Cooper
It was only supposed to be one night!
We met at a wedding. He was hot. And I'd been in a year's drought.
He smiled. We got drunk.We flirted. We hooked up. I left early the next morning without saying goodbye. It was only meant to be a one night stand. I didn't want the awkward morning after moment. Not at all.
Then I went home for the weekend. And he was there. Sitting on the couch chatting to my dad. Turns out he was more than just a stranger. Turns out that my one night stand was about to cause a whole heap of trouble. Turns out that it never just stops with one night.
Readers sh...
Genre: Arts & Photography, Individual Artists, Fashion, Biographies & Memoirs, Historical, Memoirs, Professionals & Academics, Business & Investing, Industries & Professions, Personal Finance, Children's eBooks, Arts, Music & Photography, Computers & Technology, Literature & Fiction, Mysteries & Detectives, Biographies, Holidays & Celebrations, Sports & Outdoors, Comics & Graphic Novels, Manga, Databases, Microsoft, Software, Cookbooks, Food & Wine, Culinary Arts & Techniques, Drinks & Beverages, Meals, Quick & Easy, Special Occasions, Humor
Show Me Quickly: The Struggle is Real
by Elliott Reed
My name is Elliott Reed. You can call me Elliott, if you are grown or Mr. Reed, if you are not. Certain people call me "Coach" or "Mr. Elliott" too. I am writing this story just for you. I am writing it using what I call the "Ruby Standard" that I named for my then-8-year-old daughter. If I cannot explain a concept, an idea, a notion without meandering into more than a third-grader's capacity to reason then I need to reconsider it. Not the premises of it, mind you, but the delivery. I am not dumbing anything down. I am not sugar-coating anything for you. I am giving you the truth about my life because I have a very specific goal -- I want the next generation to beat the current one on everything. I want to have a competition and I want to give you an idea of what I have done right, w...
Genre: Children's eBooks, Biographies, Nonfiction, Children's Nonfiction, Growing Up & Facts of Life
Texting with Black History: Martin Luther King Jr., Sojourner Truth, and Aretha Franklin Biography Books for Kids (Texting with History Bundle Box Set Book 1)
by Bobby Basil
On sale for a limited time! The price will increase to $3.99 on January 22nd.What if you could text with important figures from Black History?Alex, a curious child, gets to do just that! In this box set, Alex texts with Martin Luther King, Jr., Sojourner Truth, and Aretha Franklin. Through each texting conversation, Alex learns about strong people who stand up for what they believe and fight for what is right. It's a biography box set for kids that uses modern day texting bubbles children understand and enjoy!***Read for free with Kindle Unlimited!***A kid friendly box set for Black History Month!This book includes:The biography of Martin Luther King, Jr.The biography of Sojourner TruthThe biography of Aretha FranklinA discussion of slavery and the civil rights movement in a way children...
Baby Zeke: The diary of a chicken jockey (an unofficial Minecraft autobiography) (Baby Zeke: The Diary of a Jockey Book 1)
by Dr. Block
Zeke was spawned as a baby zombie, and everyone made fun of him.
He had no idea why he was so little when all of the other zombies he met were so big. It did not seem fair to him.
But after meeting his mentor, Zeb, he learns that he has special powers that will help him survive in the crazy, amazing world of Minecraft.
When he later meets a chicken named Harold, his life seems to have taken a turn for the positive.
But, a nighttime raid on a village begins the process that will turn his world upside down....
Baby Zeke: The diary of a chicken jockeyBaby Zeke the Chicken Jockey series and is a must read for gaming fans everywhere!...
Genre: Children's eBooks, Computers & Technology, Literature & Fiction, Science Fiction, Fantasy & Scary Stories, Biographies, Nonfiction, Children's Nonfiction
Counting Numbers: Spanish to English Counting Numeros en Ingles (Pedro & Pete Spanish Kids Book 1)
Genre: Arts & Photography, Art, Biographies & Memoirs, Arts & Literature, Historical, Professionals & Academics, Specific Groups, Children's eBooks, Arts, Music & Photography, History, Geography & Cultures, Biographies, Education & Reference, Nonfiction, Schools & Teaching, Foreign Language Study & Reference, Children's Nonfiction
If I Didn't Know Better (Callaway Cousins)
by Barbara Freethy
The New York Times bestselling family series The Callaways continues with IF I DIDN'T KNOW BETTER, another heartwarming and page-turning romance by #1 NYT Bestselling Author Barbara Freethy.
Mia Callaway thought she had the perfect guy and the perfect job...until she didn't. After a run of bad luck, Mia is looking for an escape, so she agrees to go to Angel's Bay to clean out her aunt's house. She has no idea that the wounded soldier next door and his adorable, but also wounded, daughter are about to change her definition of perfect. Add in stolen art, a family secret, and a town where miracles can happen, and Mia's escape turns out to be the greatest adventure of her life.
Praise for the Callaways!
I love the Callaways! Heartwarming romance, intrigu...
Genre: Biographies & Memoirs, Arts & Literature, Ethnic & National, Historical, Leaders & Notable People, Memoirs, Professionals & Academics, Reference & Collections, Regional U.S., Specific Groups, Travel, Children's eBooks, Arts, Music & Photography, Computers & Technology, History, Literature & Fiction, Comics & Graphic Novels, Mysteries & Detectives, Geography & Cultures, Biographies, Holidays & Celebrations, Sports & Outdoors, Databases, Microsoft, Software, Cookbooks, Food & Wine, Baking, Canning & Preserving, Cooking by Ingredient, Cul
Texting with Andy Warhol: An Art Biography Book for Kids (Texting with History 1)
Genre: Arts & Photography, Art, Biographies & Memoirs, Arts & Literature, Historical, Professionals & Academics, Specific Groups, Children's eBooks, Arts, Music & Photography, History, Geography & Cultures, Biographies, Education & Reference, Nonfiction, Children's Nonfiction
Are you a princess? Royalty quiz book for girls (Ages 6-8 / Age 9-12): Discover which princess you are with this lovely quiz book for girls & kids (Best Quiz For Girls 1)
by Mary White
Readers will learn more about themselves and have fun while exploring hidden aspects of their personality with the "Best Quiz For Girls" series, an engaging set of quiz books. Written with a low level of complexity and filled with nice pictures. "Best Quiz For Girls" series fun questions to share with friends as well as trivia throughout the books with also curiosities about princesses included in this book! Don't be afraid that your kids will not read this book because they will absolutely love it. :)...
Genre: Children's eBooks, Biographies, Nonfiction, Children's Nonfiction, Activities, Crafts & Games
Size: Unknown
HOW TO MERIT THE CROWN?: Abram's Choice
by Haya Evelyne Berkowitz
Genre: Children's eBooks, Biographies
Sins of the Mothers (Texas Romance Series Book 4)
by Caryl McAdoo
Persistent faith brings redemption and reconciliation.
Propelled by blind love, Mary Rachel Buckmeyer defies her father to elope with Caleb Wheeler. The newlyweds run off to California then partner with his cousin in his dry goods business.
Unbeknownst to the young bride, her new husband sends his kissing cousin ahead. He wants his love and his new wife's money, too. Betrayal and murder drive Mary, soon a young mother, to the depths of despair. But she hates the man who loves her enough to cover her sins and deliver her out of the horrible pit she's dug for herself in. Or does she?
Mary Rachel travels from frontier Texas to the raw bone boomtown of 1850's San Francisco gold rush days, then all the way to genteel New York to find redemption for the sins of her mother...
Genre: Arts & Photography, Individual Artists, Fashion, Biographies & Memoirs, Memoirs, Professionals & Academics, Business & Investing, Industries & Professions, Children's eBooks, Arts, Music & Photography, History, Literature & Fiction, Comics & Graphic Novels, Geography & Cultures, Biographies, Holidays & Celebrations, Manga, Computers & Technology, Databases, Software, Cookbooks, Food & Wine, Cooking by Ingredient, Culinary Arts & Techniques, Drinks & Beverages, Meals, Professional Cooking, Special Occasions, Humor & Entertainment, Pop
JACOB'S STRENGTH: HAYA EVELYNE BERKOWITZ
by JACOB'S STRENGTH
Genre: Children's eBooks, Fairy Tales, Folk Tales & Myths, Biographies
THE BOO CLUB BOOK 1: THE HAUNTED MANSION
by Dr. Mc
There are a lot of benefits that your children can get when you as a parent read them bedtime stories. You will be able to spend quality time together with your child, and by spending time with you, you and your child get to do something new together — cheer for the good guys and boo the bad ones in the books you read. You also get a peek into how your child sees the world through the comments she makes on the plot, the characters, and the setting.
A group of four young children known as the Boo Club set out for an adventure on Halloween night. Milly, Spider, Jan, and Sam live in the town of Hauntsville, an unordinary town filled with many mysteries. Dressed as matching ghosts, they take off on their bicycles into the night. The Boo Club comes across a spooky old house while...
Genre: Children's eBooks, Arts, Music & Photography, Action & Adventure, Science Fiction, Fantasy & Scary Stories, Biographies, Holidays & Celebrations, Nonfiction, Children's Nonfiction, Activities, Crafts & Games
DAVID THE CONQUEROR: Gateway to Glory
Genre: Children's eBooks, Biographies, Literature & Fiction, World Literature, Jewish, Nonfiction, Children's Nonfiction, Teen & Young Adult, Biography
Meal Prep: Beginer's Guide 35 Days Low carbohydrate weight loss recipes
by Darius A. Shelley
Meal Prep Beginer's Guide (Low carb weight loss recipes)35 Days Meal Plan...
Genre: Arts & Photography, Art, Children's eBooks, Biographies, Cookbooks, Food & Wine, Meals, Health, Fitness & Dieting, Diets & Weight Loss, Nonfiction, Children's Nonfiction
Justice for Mackenzie (Badge of Honor: Texas Heroes Book 1)
by Susan Stoker
A member of the famed Texas Rangers, Daxton Chambers has dealt with more than his share of depravity. But the Lone Star Reaper takes evil to a whole new level, kidnapping and burying women alive. It's Dax's job to help keep San Antonio safe, but even with help from friends in various law enforcement agencies, the killer remains two steps ahead. It's hardly the ideal time for a relationship, but Mackenzie Morgan is too luscious to resist. Dax wants her--which makes her an instant target for his newfound enemy.
When the Reaper gets personal, it will take every ounce of Daxton's considerable skill and training to keep Mack alive.
**Justice for Mackenzie is the 1st book in the Badge of Honor: Texas Heroes Series. Each book is a stand-alone, with no cliffhanger ending...
Genre: Arts & Photography, Individual Artists, Fashion, Biographies & Memoirs, Memoirs, Professionals & Academics, Business & Investing, Industries & Professions, Personal Finance, Children's eBooks, Arts, Music & Photography, Computers & Technology, History, Literature & Fiction, Comics & Graphic Novels, Mysteries & Detectives, Geography & Cultures, Biographies, Holidays & Celebrations, Sports & Outdoors, Manga, Databases, Microsoft, Software, Cookbooks, Food & Wine, Cooking by Ingredient, Culinary Arts & Techniques, Drinks & Beverages, Mea
A Kiss For Grandma
by Michael Gordon
Children made Nanny light up! Simple rhymes, cute characters in adorable settings, and sweet, comforting addition to your child's bedtime routine. Here's what readers are already saying about this amazing, inspiring story: "Grandmothers are the best!My kids loved this amazing story." -- Angela "Wonderful for little ones!The story is sweet, simple and perfect for bedtime" -- Holly "t's just short enough to keep kids attention, but they want it read to them over and over. " -- Kris Kids get ready to spend some special time with the grandma! They have a lot of fun. They bake cookies and eat them together, watch cartoons, play Treasure Hunt. She's more than happy to dig out old photo albums and tell funny stories. Warning: Cuteness Overload!This book contains illustrations of ...
Genre: Children's eBooks, Biographies, Education & Reference, Nonfiction, Children's Nonfiction, Growing Up & Facts of Life
Ben Simmons: The Inspiring Story of One of Basketball's Rising All-Stars (Basketball Biography Books)
by Clayton Geoffreys
Learn the Inspiring Story of the Philadelphia 76ers' Rising All-Star, Ben Simmons!Read on your PC, Mac, smartphone, tablet or Kindle device.Limited time offer: If you buy the print edition, you can keep the Kindle edition for yourself!In Ben Simmons: The Inspiring Story of One of Basketball's Rising All-Stars, you will learn the incredible story of one of basketball's most exciting guards to watch, Ben Simmons. Since being drafted first overall in the 2016 NBA Draft, Ben Simmons has quickly emerged as one of the league's top young stars to watch.Just twenty-two years old at the time of this writing, Simmons' career is in many ways just getting started. It'll be exciting to see how he continues to grow in the years ahead. Pick up this unauthorized biography today to learn the inspiring st...
Genre: Biographies & Memoirs, Children's eBooks, Biographies, Sports & Outdoors, Nonfiction, Children's Nonfiction
n n n n ">
TRANSFORMING ANGEL - True Story of an Inner City Child - A Bridge to Something Better: Juvenile Nonfiction Short Story Inspirational (Remarkable Child Memoir Series)
by Clair Hellen
Encouraging words and meaningful spiritual quotes, everyone needs them. Discover their power and personal benefit in your life at: www.KingdomCompanions.com
Transforming Angel - In this captivating true short story, become informed of the daily drama at an inner city middle school. Learn about a teacher's heart-felt conviction to go beyond the "usual" supportive environment within her classroom. And as a result of her efforts, discover if one of her students, Brayton, can rise up like a phoenix, out of the ashes that framed his former life.
Transforming Angel is the true story of an inner city child - a bridge to something better - short read.
A juvenile nonfiction short story inspirational from the Remarkable Child Memoir Series.
Genre: Children's eBooks, Biographies, Nonfiction, Children's Nonfiction
Diary of Herobrine: Origins (an unofficial Minecraft book) (The Herobrine Story Book 1)
Learn the truth about Herobrine's origins from his own diary.
This amazing diary was recently discovered in a cave deep within a valley of the Overworld. Now, you can learn how Herobrine came to be and, more importantly, why he came to be.
WARNING: This diary is not for the faint of heart. Do NOT read this book late at night…
All illustrations in the diary (except those in the introduction) were drawn by Herobrine himself!...
Genre: Children's eBooks, Computers & Technology, Literature & Fiction, Science Fiction, Fantasy & Scary Stories, Biographies, Nonfiction, Children's Nonfiction, Activities, Crafts & Games
Roo, The Little Red Tuk Tuk: Picture Book about a Spunky Vehicle for Children age 2 - 6
by Nadishka Aloysius
There are hundreds of books about cars, trains, trucks and various construction vehicles in the market. But have you ever read one about a Tuk Tuk? Fans of Thomas the Tank Engine and Tayo the Bus will discover a new friend in this book, in a setting both exotic and exciting. Roo is a little Tuk Tuk. Join Roo as he recalls the many ups and downs of his life on the roads of Colombo (the commercial capital of Sri Lanka). From road races, to Polo tournaments, to animal rescues, this little vehicle has lived life to its fullest. Experience the joys and perils of Tuk Tuks on the streets, and learn many life lessons along the way with this courageous Tuk Tuk who is always ready to lend a helping hand and spread some cheer. You are never too little to make a difference...Also known as tri-shaws or...
Genre: Children's eBooks, Literature & Fiction, Geography & Cultures, Biographies, Nonfiction, Children's Nonfiction
Father's Words
by Smart Family
Genre: Biographies & Memoirs, Leaders & Notable People, Specific Groups, Children's eBooks, Biographies, Education & Reference, History, Americas, United States, Historical Study, Nonfiction, Schools & Teaching, Children's Nonfiction
Donald Trump: 200 Rare Photos Of Donald Trump: 200 Rare And Interesting Photos From President Donald Trump's Fascinating Life
by James Daniels
Genre: Arts & Photography, Photography, Children's eBooks, Biographies, Nonfiction, Children's Nonfiction
Silly Milly the Dane
Genre: Children's eBooks, Animals, Literature & Fiction, Biographies, Humor, Humor & Entertainment, Poetry, Nonfiction, Children's Nonfiction
It's a Hip Hop Hip Hop World For Every B-Boy and B-Girl: History For Kids (Culture For Kids Book 1)
by A.D. Largie
The Breakdancing is so spectacular!The Graffiti Spray Painting is so amazing!The Rap Rhyming is so inspiring!The Human Beat Box sound is so profound!The Street Style is so wild!Hip Hop B-Boy and his sister Hip Hop B-Girl have a problem, they are broke and it's not a joke. They know they can do so much more even though they are poor, they believe in themselves even if the world says no.The needed to express themselves so they dug deep into their soul to reveal a culture that the world would forever know. The name of this culture is called Hip Hop. Now Hip Hop B-boy and B-girl is on a mission to overcome poverty and change the world by harnessing the power of their art and culture.BOOK FEATURES:Beautiful illustrationsSwagHip Hop HairBreakdancingRhymingBOOK BENEFITS:How to overcome adversityT...
Genre: Children's eBooks, Arts, Music & Photography, Geography & Cultures, Biographies, Nonfiction, Children's Nonfiction
Mullá Ḥusayn: The Story of the Declaration of the Báb for Young Children
by Alhan Rahimi
Genre: Children's eBooks, History, Biographies, Holidays & Celebrations, Religions, Religion & Spirituality, Other Practices, Nonfiction, Children's Nonfiction
Privacy Policy | Terms & Conditions | Contact Us
DailyFreeBooks.com is not affiliated or related to Amazon.com in any way.
DailyFreeBooks is a participant in the Amazon Services LLC Associates Program, an affiliate advertising program designed to provide a means for sites to earn advertising fees by advertising and linking to Amazon.com. KINDLE is a registered trademark of Amazon.com, Inc. Amazon and the Amazon logo are trademarks of Amazon.com, Inc. or its affiliates.

redpajama_set_name: RedPajamaCommonCrawl


text:
Stamp series on Buddha marks Gurupurnima
The Rising Nepal, July 21, 2005
KATHMANDU, Nepal -- Minister for Information and Communications, Tanka Dhakal put cancellation marks on a postage stamp series on Lord Buddha issued by Nepal Philatelic Bureau from today on the occasion of Gurpurnima.
On the day of Gurupurnima (full-moon), Lord Buddha is said to have held the first sermon Dharmachakra after having attained enlightenment.
The four stamp series of Buddha depict the four episodes of Buddha?s life namely, his birth in Lumbini, enlightenment in Bodhagaya, first sermon in Sarnath and Mahaparinirvana in Kushinagar.
The small stone pillar related to Buddha was seized at the Tribhuvan International Airport when it was about to be smuggled to other countries via flight in 2057 B.S.
The stamp series printed in four mixed colours was designed by artist of the Bureau Mohan Narasingh Rana. About 2,50,000 copies of stamps have been published.
The first sermon preached by Lord Buddha on this day is known as Dharmachakra all over the world. According to him, only those who can renounce greed, illusion, affection can attain enlightenment which means to know oneself.
Speaking at the function, Minister Dhakal said only those can be genuine followers of Buddha who follow the path of non-violence and peace shown by him.
He called on the people to extend their support to historic move made by His Majesty the King which was aimed at ending terrorism in order to restore peace in the country.
Minister Dhakal, meanwhile, expressed his conviction that the string of stamps will help spread the message of peace in every corner of the world.
Speaking on the occasion, Director General of the Nepal Philatelic Bureau, Shreedhar Gautam expressed hope that the Buddha stamp series will help spread Buddha?s message of Panchsheel as well as help researchers.
The Bureau has issued 30 types of stamp series of Buddha so far. On the occasion, Chairman of the Nepal Philatelic Society, Kedar Pradhan informed that additional stamp series of Buddha will be released in the near future.
At the function presided over by patron of society and vice chairman of the Lumbini Development Trust, Omkar Gauchan, assistant director general of the Department of Archeology, Chandraprakash Tripathi and others also expressed their views.


We are a full Septic Service company - meaning we do much more than just pump out septic tanks. Here are more of our Septic Services.
If you are not sure where your tank is located, we will help you find it.
the most competitive rates in Berks County and free estimates.
K and W Septic Service is a proud member of the PSMA - the Pennsylvania Septage Management Association, and we take great pride in the environment we live in here in Berks County Pa. We believe that Conservation, and Management is extremely important in the septic business so we take great care to ensure our environment is protected.


New Delhi : Accusations are piling up against the recruitment process in government hospitals at the capital, with many senior doctors alleging instances of manipulation and favoritism taking place.
A recent report by the DNA points out to a case where allegedly a doctor was appointed for a senior resident post in the blood bank department of the Lok Nayak Jai Prakash Hospital without, apparently being present for the interview process.
The interview for the post was held on the 10th of October, 2016, where 8 candidates were supposed to be interviewed. However, only two candidates turned up and went through the said process. Ironically, when the results of the interviews were announced, it seemed that the department had selected a candidate who did not even turn up for the interview.
"This is a major goof up on the part of the administration. How can she get a job when she did not appear for the interview?" said a senior doctor from the hospital on the condition of anonymity.
Not only this, the official procedure that is followed for the appointment, first requires the candidate to submit their documents which then undergo a process of being verified by the Delhi Medical Council ( DMC). Only then can the candidate go through the final round of being interviewed by the doctors. However, according to the records , the candidates documents have been verified only on October 13, three days after the interviews took place.
"There is no possibility that any candidate can submit the documents later. This is a gross violation of the rules," said another senior doctor from the hospital.
This is true.Even if the interviews happen they happen only for formality. Some years back l wanted to do SR-ship in a govt.hospital in delhi. I appeared in many interviews at various places but could not get selected. Then I appeared in the interview for SR post in this prestigious govt medical college at Delhi. There I met the HOD in the interviewing team. I thanked her for their practical course that they had conducted one year back for MD/DNB final year students. It had genuinely helped me in clearing my DNB practical exam in first attempt. She very lovingly told me that this time she won\'t be able to help me as they have already decided the candidates and interview was just a formality. I am not revealing the name of medical college and HOD as I am indebted to them for their practical course. Since then I lost faith in govt system and never applied for any govt. job. I am doing well in private.May be that was a blessing in disguise for me.


text:
Sucioperro (; ) are a Scottish rock band from Ayr, South Ayrshire, formed in 2002.

History

Random Acts of Intimacy
The band's debut album, Random Acts of Intimacy, was released in June 2006 on the Captains of Industry record label. It features the download only single "Wolf Carnival" as well as the singles "Dialog on the 2", "The Drop" and download only "Grace And Out of Me" which includes the video for the song directed by Jamie Lenman of Reuben.

Pain Agency
The band's second album is called Pain Agency, which was released on 4 May 2009, through Maybe Records. It was produced by the band and recorded in their own studio in Ayr, South Ayrshire and was mixed by Chris Sheldon.

Mums' Bad Punk Music was released as a single on 17 November 2008 through Maybe Records. It features three non-album tracks and was released on limited edition CD and digital download.

The second single from the album was "Don't Change (What You Can't Understand)" and was released in mid-April 2009 as a digital download via Maybe Records. The package included a brace of newly recorded b-sides.

In October 2009, the band released the third single from Pain Agency in the form of "The Dissident Code". This is the last material to be released from the album.

The Heart String & How to Pull It
Sucioperro's third record, The Heart String & How to Pull It, was released on 7 March 2011 through Xtra Mile Recordings. It has spawned two singles so far 'Threads' and 'Reflexes of the Dead' both of which were trialled throughout previous UK shows prior to the release of the album.

Fused
Sucioperro recorded a fourth album in early 2012, Fused, which released in the late summer. Pre-orders were made available on their Bandcamp page, and a video released to accompany the first song previewing the album, A River of Blood. This was the first music video to be taken from the album. It was after the album's release that the other music videos were published. "To Nothing" released on 29 August 2012. "Rabbits..." was the third, published on 17 October 2012, which was then followed by "... Boxes" on the 18th. A combination of the two songs made the fifth track of the album, Rabbits in Boxes.

Band members

Current members
 JP Reid – vocals, guitar
 Fergus Munro – drums, vocals
 Stewart Chown – bass, vocals

Past members
 Michael Logg – bass (2002–2008)
 David Aird – guitar (2004–2007)
 Brendan Reilly – drums (2002–2004)
 Dave Martin – guitar (2002–2003)

Additional live members
 Gordon Love (2011–?)
 Hooligan Sadikson (2011–?)

Discography

Albums
 Random Acts of Intimacy (10 June 2006, Captains of Industry)
 Pain Agency (4 May 2009, Maybe Records)
 The Heart String & How to Pull It (7 March 2011, Xtra Mile Recordings)
 Fused (8 August 2012)

EPs
 Why Bliss Destroy (August 2002, self released)
 The Hidden Perils Of Dancing (11 November 2004, Adorno Records)
 Tour EP #1 (April 2005, self released)
 Mums' Bad Punk Music (17 November 2008, Maybe Records)
 The Dissident Code (19 October 2009, Maybe Records)
 Chemicals EP (7 March 2011, self-released, Pledgemusic download)

Singles
 "Wolf Carnival" (10 April 2006, Captains of Industry, download only)
 "Dialog on the 2" (15 May 2006, Captains of Industry)
 "The Drop" (10 October 2006, Captains of Industry)
 "Don't Change (What You Can't Understand)" (27 April 2009, Maybe Records, download only)
 "I'm Not in Charge" (14 December 2009, King Tuts Recordings)
 "Threads" (6 December 2010, self-released, download only)
 "Reflexes of the Dead" (28 February 2011, Xtra Mile Recordings, download only)

References

External links
 The official Sucioperro website
 Sucioperro myspace

Scottish rock music groups
Musical groups from Kilmarnock

redpajama_set_name: RedPajamaWikipedia


Did you mean Astronomy, there is no real career opportunities for Astrologers and I would be amazed if any University would ever teach such hokum as Astrology.
It is the abandonment of all science and common sense to assume that vast stars at incredible distances moving through the sky can have any, just any effect on anything at all.
I studied astronomy at Cambridge, take my word for it, if nothing else that this is just nonsense, vague answers that cover a vast range of experiences and the human mind makes a leap to include the experience with the vague prediction.
Experiment: Get someone to read to you the wrong horoscope some mornings and see at the end of the day if the wrong horoscope also fits your life.
There are 12 signs that means that an entire 12th of the world's population are having the same day as you, preposterous!
There are so many e-books available on the internet, of-courser paid. You can get one or two of them to start. But as such I didn't ever find any online courser providing study or training on Astrology stuff.
Check google and good luck.