Library Logic

(* Logic in Coq
   Version of 4/28/2009
*)

Require Export Ind.

(* ----------------------------------------------------- *)
(* Conjunction *)

Inductive and (A B : Prop) : Prop :=
  conj : A -> B -> (and A B).

(* Intuition: To construct evidence for and A B, we must
   provide evidence for A and evidence for B. *)

(* More familiar syntax: *)
Notation "A /\ B" := (and A B) : type_scope.

Exercise: 1 star (and_ind_principle)

(* See if you can predict the induction principle for
   conjunction. *)
(* Check and_ind. *)

Theorem and_example :
  (ev 0) /\ (ev 4).
Proof.
  apply conj.
    Case "left". apply ev_0.
    Case "right". apply ev_SS. apply ev_SS. apply ev_0. Qed.

(* split is a convenient shorthand for apply conj. *)
Theorem and_example' :
  (ev 0) /\ (ev 4).
Proof.
  split.
    Case "left". apply ev_0.
    Case "right". apply ev_SS. apply ev_SS. apply ev_0. Qed.

(* Conversely, the inversion tactic can be used to investigate
   a conjunction hypothesis in the context and calculate what
   evidence must have been used to build it. *)
Theorem and_1 : forall A B : Prop,
  A /\ B -> A.
Proof.
  intros A B H.
  inversion H as [HA HB].
  apply HA. Qed.

Exercise: 1 star

Theorem and_2 : forall A B : Prop,
  A /\ B -> B.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem and_commut : forall A B : Prop,
  A /\ B -> B /\ A.
Proof.
  intros A B H.
  split.
    Case "left". apply and_2 with (A:=A). apply H.
    Case "right". apply and_1 with (B:=B). apply H. Qed.

Exercise: 2 stars

Theorem and_assoc : forall A B C : Prop,
  A /\ (B /\ C) -> (A /\ B) /\ C.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 2 stars

(* Now we can prove the other direction of the equivalence of
   even and ev.  Notice that the left-hand conjunct here is
   the statement we are actually interested in; the right-hand
   conjunct is needed in order to make the induction hypothesis
   strong enough that we can carry out the reasoning in the
   inductive step.  (To see why this is needed, try proving the
   left conjunct by itself and observe where things get
   stuck.) *)
Theorem even_ev : forall n : nat,
  (even n -> ev n) /\ (even (S n) -> ev (S n)).
Proof.
  (* Hint: Use induction on n. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------ *)
(* Iff *)

Definition iff (A B : Prop) := (A -> B) /\ (B -> A).

Notation "A <-> B" := (iff A B) (at level 95, no associativity) : type_scope.

Theorem iff_implies : forall A B : Prop,
  (A <-> B) -> A -> B.
Proof.
  intros A B H.
  inversion H as [HAB HBA]. apply HAB. Qed.

Theorem iff_sym : forall A B : Prop,
  (A <-> B) -> (B <-> A).
Proof.
  intros A B H.
  inversion H as [HAB HBA].
  split. (* Note that split is just a bit smarter than apply conj,
            which would have required an unfold iff first. *)
    Case "->". apply HBA.
    Case "<-". apply HAB. Qed.

Exercise: 1 star (iff_properties)

(* Prove these properties of iff. *)

Theorem iff_refl : forall A : Prop,
  A <-> A.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem iff_trans : forall A B C : Prop,
  (A <-> B) -> (B <-> C) -> (A <-> C).
Proof.
  (* Hint: If you have an iff hypothesis in the context, you
     can use inversion to break it into two separate
     implications.  (Think about why this works.) *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 2 stars

(* Finish the following proof by filling in an
   explicit proof object *)
Definition MyProp_iff_ev : forall n, MyProp n <-> ev n :=
  (* FILL IN HERE *)

(* ------------------------------------------------------------ *)
(* Disjunction *)

Inductive or (A B : Prop) : Prop :=
  | or_introl : A -> or A B
  | or_intror : B -> or A B.

Notation "A \/ B" := (or A B) : type_scope.

(* Intuition: There are two ways of giving evidence for A \/ B:
      - give evidence for A (and say that it is A you are
        giving evidence for! -- this is the function of the
        or_introl constructor)
      - give evidence for B, tagged with the or_intror
        constructor. *)

Exercise: 1 star (or_ind_principle)

(* See if you can predict the induction principle for disjunction. *)
(* Check or_ind. *)

(* Since A \/ B has two constructors, doing inversion on a
   hypothesis of type A \/ B yields two subgoals. *)
Theorem or_commut : forall A B : Prop,
  A \/ B -> B \/ A.
Proof.
  intros A B H.
  inversion H as [HA | HB].
    Case "left". apply or_intror. apply HA.
    Case "right". apply or_introl. apply HB. Qed.

(* From here on, we'll use the handy tactics left and right
   in place of apply or_introl and apply or_intror. *)
Theorem or_commut' : forall A B : Prop,
  A \/ B -> B \/ A.
Proof.
  intros A B H.
  inversion H as [HA | HB].
    Case "left". right. apply HA.
    Case "right". left. apply HB. Qed.
Theorem or_distributes_over_and_1 : forall A B C : Prop,
  A \/ (B /\ C) -> (A \/ B) /\ (A \/ C).
Proof.
  intros A B C. intros H. inversion H as [HA | [HB HC]].
    Case "left". split.
      SCase "left". left. apply HA.
      SCase "right". left. apply HA.
    Case "right". split.
      SCase "left". right. apply HB.
      SCase "right". right. apply HC. Qed.

Exercise: 2 stars

Theorem or_distributes_over_and_2 : forall A B C : Prop,
  (A \/ B) /\ (A \/ C) -> A \/ (B /\ C).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 1 star

Theorem or_distributes_over_and : forall A B C : Prop,
  A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* --------------------------------------------------- *)
(* Relating /\ and \/ with andb and orb *)

(* Let's record a few useful facts about the relation between the
   boolean operations andb and orb and their propositional
   counterparts, which we'll need later. *)

Theorem andb_true : forall b c,
  andb b c = true -> b = true /\ c = true.
Proof.
  intros b c H.
  destruct b.
    destruct c.
      apply conj. reflexivity. reflexivity.
      inversion H.
    inversion H. Qed.

Exercise: 1 star (bool_prop)

(* Prove these properties relating operations on booleans and
logical connectives in Prop. *)

Theorem andb_false : forall b c,
  andb b c = false -> b = false \/ c = false.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem orb_true : forall b c,
  orb b c = true -> b = true \/ c = true.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem orb_false : forall b c,
  orb b c = false -> b = false /\ c = false.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* --------------------------------------------------- *)
(* Falsehood *)

Inductive False : Prop := .

(* Intuition: False is a proposition for which there is no way
   to give evidence. *)

Exercise: 1 star (False_ind_principle)

(* Can you predict the induction principle for falsehood? *)
(* Check False_ind. *)

Theorem False_implies_nonsense :
  False -> plus 2 2 = 5.
Proof.
  intros contra.
  inversion contra. Qed.

Theorem nonsense_implies_False :
  plus 2 2 = 5 -> False.
Proof.
  intros contra.
  inversion contra. Qed.

Theorem ex_falso_quodlibet : forall (P:Prop),
  False -> P.
Proof.
  intros P contra.
  inversion contra. Qed.

(* ---------------------------------------------------- *)
(* Truth *)

Exercise: 2 stars

(* True is another inductively defined proposition.  Define it!
   Hint: the intution is that True should be a proposition for
   which it is trivial to give evidence. *)
(* FILL IN HERE *)

(* What induction principle will Coq generate for True? *)

(* ---------------------------------------------------- *)
(* Negation *)

Definition not (A:Prop) := A -> False.

(* Intuition: If we could prove A, then we could prove
   False (and hence we could prove anything at all). *)

Notation "~ x" := (not x) : type_scope.

Theorem not_False :
  ~ False.
Proof.
  unfold not. intros H. inversion H. Qed.

Theorem contradiction_implies_anything : forall A B : Prop,
  (A /\ ~A) -> B.
Proof.
  intros A B H. inversion H as [HA HNA]. unfold not in HNA.
  apply HNA in HA. inversion HA. Qed.

Theorem double_neg : forall A : Prop,
  A -> ~~A.
Proof.
  intros A H. unfold not. intros G. apply G. apply H. Qed.

Exercise: 2 stars (double_neg_inf)

(* As an exercise, write an informal proof of double_neg:

   Theorem: For any prop A, A -> ~~A

   Proof:
   (* FILL IN HERE *)

 *)

Exercise: 2 stars

Theorem contrapositive : forall A B : Prop,
  (A -> B) -> (~B -> ~A).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 1 star

Theorem not_both_true_and_false : forall A : Prop,
  ~ (A /\ ~A).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem five_not_even :
  ~ ev 5.
Proof.
  unfold not. intros Hev5. inversion Hev5 as [|n Hev3 Heqn].
  inversion Hev3 as [|n' Hev1 Heqn']. inversion Hev1. Qed.

Exercise: 1 star

Theorem ev_not_ev_S : forall n,
  ev n -> ~ ev (S n).
Proof.
  unfold not. intros n H. induction H. (* not n! *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 4 stars, optional (classical_axioms)

(* Prove that the following five propositions are equivalent. *)
Definition peirce := forall P Q: Prop,
  ((P->Q)->P)->P.
Definition classic := forall P:Prop,
  ~~P -> P.
Definition excluded_middle := forall P:Prop,
  P \/~P.
Definition de_morgan_not_and_not := forall P Q:Prop,
  ~(~P/\~Q) -> P\/Q.
Definition implies_to_or := forall P Q:Prop,
  (P->Q) -> (~P\/Q).

(* FILL IN HERE *)

(* ---------------------------------------------------------- *)
(* Inequality *)

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

(* A useful proof idiom: If you are trying to prove a goal that
   is nonsensical, apply the lemma ex_falso_quodlibet to change
   the goal to False.  This makes it easier to use assumptions
   of the form ~P that are available in the context. *)
Theorem not_false_then_true : forall b : bool,
  b <> false -> b = true.
Proof.
  intros b H. destruct b.
  Case "b = true". reflexivity.
  Case "b = false".
    unfold not in H. (* optional step *)
    apply ex_falso_quodlibet.
    apply H. reflexivity. Qed.

Exercise: 2 stars

Theorem not_eq_false_beq : forall n n' : nat,
     n <> n'
  -> false = beq_nat n n'.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 4 stars, optional

Theorem beq_false_not_eq : forall n m,
  false = beq_nat n m -> n <> m.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------------ *)
(* Existential quantification *)

Inductive ex (X : Set) (P : X -> Prop) : Prop :=
  ex_intro : forall witness:X, P witness -> ex X P.

(* The intuition is that, in order to give evidence for the
   assertion "there is some x for which P holds" we must actually
   name a WITNESS -- a specific value x for which we can give
   evidence that P holds. *)

(* Let's add some convenient notation for the ex type.
   The details of how this works are not important: the
   critical point is that it allows us to write exists x, P or exists x:X, P, just as we do with the forall
   quantifier.  *)
Notation "'exists' x , p" := (ex _ (fun x => p))
  (at level 200, x ident, right associativity) : type_scope.
Notation "'exists' x : X , p" := (ex _ (fun x:X => p))
  (at level 200, x ident, right associativity) : type_scope.

(* To prove an existential statement, use apply ex_intro. *)
Example exists_example_1 : exists n, plus n (mult n n)
   = 6.
Proof.
  apply ex_intro with (witness:=2).
  reflexivity. Qed.
(* Note that we have to explicitly give the witness. *)

(* Or, instead of writing apply ex_intro with e, we can
   write the convenient shorthand exists e. *)
Example exists_example_1' : exists n,
     plus n (mult n n)
   = 6.
Proof.
  exists 2.
  reflexivity. Qed.
(* Conversely, if we have an existential hypothesis in the
   context, we can eliminate it with destruct.  Note the use of
   the as... pattern to name the variable that Coq introduces
   to name the witness value.  (If we don't explicitly choose
   one, Coq will just call it @witness@, which makes proofs
   confusing.) *)
Theorem exists_example_2 : forall n,
     (exists m, n = plus 4 m)
  -> (exists o, n = plus 2 o).
Proof.
  intros n H.
  inversion H as [m Hm].
  exists (plus 2 m).
  apply Hm. Qed.

(* NOTE: In the lecture, I originally used inversion for the
   same purpose, and I didn't explicitly give the as...
   pattern.  This way looks a little nicer. *)

Exercise: 1 star

Theorem dist_not_exists : forall (X:Set) (P : X -> Prop),
  (forall x, P x) -> ~ (exists x, ~ P x).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 2 stars

Theorem dist_exists_or : forall (X:Set) (P Q : X -> Prop),
  (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------ *)
(* Equality. *)

(* We enclose this definition in a module to avoid confusion with
   the standard library equality (which we have used extensively
   already). *)
Module MyEquality.

Inductive eq (A:Set) : A -> A -> Prop :=
  refl_equal : forall x, eq A x x.

Notation "x = y" := (eq _ x y) (at level 70, no associativity) : type_scope.

(* An alternate definition *)
Inductive eq' (A:Set) (x:A) : A -> Prop :=
    refl_equal' : eq' A x x.

Notation "x =' y" := (eq' _ x y) (at level 70, no associativity) : type_scope.

Exercise: 3 stars, optional

(* Verify that the two definitions of equality are equivalent. *)
Theorem two_defs_of_eq_coincide : forall (A:Set) x y,
  eq A x y <-> eq' A x y.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* The induction principle for eq' says that it represents
   so-called "Leibniz equality:" if two things are equal and some
   predicate holds on one of them, then it holds on the other
   too.*)
(* Check eq'_ind. *)

End MyEquality.

(* ------------------------------------------------------- *)
(* Inversion, again *)

(* We've seen inversion used with both equality hypotheses and
   hypotheses asserting inductively defined propositions.  Now
   that we've seen that these are actually the same thing, let's
   take a closer look at how inversion behaves...

   In general, the inversion tactic 

      - takes a hypothesis H whose type is some inductively
        defined proposition P

      - for each constructor C in P's definition

          - generates a new subgoal in which we assume H was
            built with C

          - adds the arguments (premises) of C to the context of
            the subgoal as extra hypotheses

          - matches the conclusion (result type) of C against the
            current goal and calculates a set of equalities that
            must hold in order for C to be applicable
            
          - adds these equalities to the context of the subgoal

          - if the equalities are not satisfiable (e.g., they
            involve things like S n = O, immediately solves the
            subgoal.

   EXAMPLE: If we invert a hypothesis built with or, there are
   two constructors, so two subgoals get generated.  The
   conclusion (result type) of the constructor -- A \/ B --
   doesn't place any restrictions on the form of A or B, so
   we don't get any extra equalities in the context of the
   subgoal.

   EXAMPLE: If we invert a hypothesis built with and, there is
   only one constructor, so only one subgoal gets generated.
   Again, the conclusion (result type) of the constructor -- A /\ B -- doesn't place any restrictions on the form of A or
   B, so we don't get any extra equalities in the context of
   the subgoal.  The constructor does have two arguments, though,
   and these can be seen in the context in the subgoal.

   EXAMPLE: If we invert a hypothesis built with eq, there is
   again only one constructor, so only one subgoal gets
   generated.  Now, though, the form of the refl_equal
   constructor does give us some extra information: it tells us
   that the two arguments to eq must be equal!  The inversion
   tactic adds this to the context.
*)

(* ----------------------------------------------------- *)
(* Induction principles in Prop *)

(* Last week, we looked in detail at the induction principles
   that Coq generates for inductively defined SETS.  Inductively
   defined PROPOSITIONS are handled slightly differently.  For
   example, from what we've said so far, you might expect the
   inductive definition of ev

     Inductive ev : nat -> Prop :=
       | ev_0 : ev O
       | ev_SS : forall n:nat, ev n -> ev (S (S n)).

   to give rise to an induction principle that looks like this...

     ev_ind_max :
       forall P : (forall n : nat, ev n -> Prop),
            P O ev_0
         -> (forall (n : nat) (e : ev n), 
              P n e -> P (S (S n)) (ev_SS n e))
         -> forall (n : nat) (e : ev n), P n e

   ... because:

     - Since ev is indexed by a number n (every ev object
       e is a piece of evidence that some particular number n
       is even), the proposition P is parameterized by both n
       and e -- that is, the induction principle can be used to
       prove assertions involving both an even number and the
       evidence that it is even.

     - Since there are two ways of giving evidence of
       evenness (ev has two constructors), applying the
       induction principle generates two subgoals:

         - We must prove that P holds for O and ev_0.

         - We must prove that, whenever n is an even number and
           e is evidence of its evenness, if P holds of n
           and e, then it also holds of S (S n) and ev_SS n e.

     - If these subgoals can be proved, then the induction
       principle tells us that P is true for ALL even numbers
       n and evidence e of their evenness.

   But this is a little more flexibility than we actually need or
   want: it is giving us a way to prove logical assertions
   involving EVIDENCE of evenness, while all we really care about
   is proving properties of NUMBERS that are even -- we are
   interested in assertions about numbers, not about evidence.
   It would therefore be more convenient to have an induction
   principle for proving propositions P that are parameterized
   just by n and whose conclusion establishes P for all even
   numbers n:

       forall P : nat -> Prop,
          ...
          -> forall n : nat, ev n -> P n

   For this reason, Coq actually generates the following
   simplified induction principle for ev:

     ev_ind :
       forall P : nat -> Prop,
            P O
         -> (forall n : nat, ev n -> P n -> P (S (S n)))
         -> forall n : nat, ev n -> P n

   Similarly, from the inductive definition of the proposition
   and A B

     Inductive and (A B : Prop) : Prop :=
       conj : A -> B -> (and A B).

   we might expect Coq to generate this induction principle

     and_ind_max :
       forall (A B : Prop) (P : A /\ B -> Prop),
            (forall (a : A) (b : B), P (conj A B a b))
         -> forall a : A /\ B, P a

   but actually it generates this simpler and more useful one:

     and_ind :
       forall A B P : Prop,
            (A -> B -> P)
         -> A /\ B -> P

   In the same way, when given the inductive definition of or A B

     Inductive or (A B : Prop) : Prop :=
       | or_introl : A -> or A B
       | or_intror : B -> or A B.

   instead of the "maximal induction principle"

     or_ind_max :
       forall (A B : Prop) (P : A \/ B -> Prop),
            (forall a : A, P (or_introl A B a))
         -> (forall b : B, P (or_intror A B b))
         -> forall o : A \/ B, P o

   what Coq actually generates is this:

     or_ind :
       forall A B P : Prop,
            (A -> P)
         -> (B -> P)
         -> A \/ B -> P
*)

Module P.

Exercise: 3 stars (p_provability)

(* Consider the following inductively defined proposition: *)

    Inductive p : (tree nat) -> nat -> Prop :=
      | c1 : forall n, p (leaf _ n) 1
      | c2 : forall t1 t2 n1 n2,
                p t1 n1 -> p t2 n2 -> p (node _ t1 t2) (plus n1 n2)
      | c3 : forall t n, p t n -> p t (S n).

(* Describe, in English, the conditions under which the
   proposition p t n is provable. 

   (* FILL IN HERE *)

*)

End P.

(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* Relations as propositions *)

(* A proposition parameterized over a number (like ev) can be
   thought of as a PREDICATE -- i.e., the subset of nat for
   which the proposition is provable.

   A two-argument proposition can be thought of as a RELATION --
   i.e., the set of pairs for which the proposition is
   provable. *)

Module FirstLe.
(* A first try at the "less than or equal" relation on numbers... *)

Inductive le : nat -> nat -> Prop :=
  | le_n : forall n, le n n
  | le_S : forall n m, (le n m) -> (le n (S m)).

(* Check le_ind. *)

End FirstLe.

(* Note that the left-hand argument n to le is the same
   everywhere in the definition, so we can actually make it a
   "general parameter" to the whole definition, rather than an
   argument to each constructor.  *)
Inductive le (n:nat) : nat -> Prop :=
  | le_n : le n n
  | le_S : forall m, (le n m) -> (le n (S m)).
(* HIDE: That's exactly the same as Coq's. *)

Notation "m <= n" := (le m n).

(* Why is the second one better?  Because it gives us a simpler
   induction principle. *)
(* Check le_ind. *)

(* Some sanity checks on the definition.  (Notice that, although
   these are the same kind of simple "unit tests" as we gave for
   the testing functions we wrote in the first few lectures, we
   must construct their proofs explicitly -- simpl and
   reflexivity don't do the job, because the proofs aren't just
   a matter of simplifying computations. *)
Theorem test_le1 :
  3 <= 3.
Proof.
  (* WORK IN CLASS *) Admitted.

Theorem test_le2 :
  3 <= 6.
Proof.
  (* WORK IN CLASS *) Admitted.

Theorem test_le3 :
  ~ (2 <= 1).
Proof.
  (* WORK IN CLASS *) Admitted.

(* The "strictly less than" relation n < m can now be
   defined in terms of le. *)
Definition lt (n m:nat) := le (S n) m.

Notation "m < n" := (lt m n).

(* A few more simple relations on numbers *)

Inductive square_of : nat -> nat -> Prop :=
  sq : forall n:nat, square_of n (mult n n).

Inductive next_nat (n:nat) : nat -> Prop :=
  | nn : next_nat n (S n).

Inductive next_even (n:nat) : nat -> Prop :=
  | ne_1 : ev (S n) -> next_even n (S n)
  | ne_2 : ev (S (S n)) -> next_even n (S (S n)).

Exercise: 2 stars

(* Define an inductive relation total_relation that
   holds between every pair of natural numbers. *)
(* FILL IN HERE *)

Exercise: 2 stars

(* Define an inductive relation empty_relation (on
   numbers) that never holds. *)
(* FILL IN HERE *)

Exercise: 3 stars (R_provability)

Module R.
(* Suppose we give Coq the following definition: *)

Inductive R : nat -> nat -> nat -> Prop :=
   | c1 : R 0 0 0
   | c2 : forall m n o, R m n o -> R (S m) n (S o)
   | c3 : forall m n o, R m n o -> R m (S n) (S o)
   | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
   | c5 : forall m n o, R m n o -> R n m o.

(* Which of the following propositions are provable?
     (a) R 1 1 2
     (b) R 2 2 6

    If we dropped constructor c5 from the definition of R, would
    the set of provable propositions change?  Briefly (1
    sentence) explain your answer.

    If we dropped constructor c4 from the definition of R, would
    the set of provable propositions change?  Briefly (1
    sentence) explain your answer.

(* FILL IN HERE *)

*)

End R.

Exercise: 4 stars, challenge problem (filter_challenge)

(* One of the main purposes of Coq is to prove that programs
   match their specifications.  To this end, let's prove that our
   definition of filter matches a specification.  Here is the
   specification, written out informally in English.

     Suppose we have a set X, a function test: X->bool, and a
     list l of type list X.  Suppose further that l is an
     in-order merge of two lists, l1 and l2, such that every
     item in l1 satisfies test and no item in l2 satisfies
     test.  Then filter test l = l1.

   Your job is to translate this specification into a Coq theorem
   and prove it.  (Hint: You'll need to begin by defining what it
   means for one list to be a merge of two others.  Do this with
   an inductive relation, not a Fixpoint.)
 *)

(* FILL IN HERE *)

(* --------------------------------------------------------- *)
(* Relations, in General *)

(* We've now defined a few particular relations.  As you probably
   remember from your undergraduate discrete math course, there
   are a lot of ways of discussing and describing relations IN
   GENERAL -- ways of classifying relations (are they reflexive,
   transitive, etc.), theorems that can be proved generically
   about classes of relations, constructions that build one
   relation from another, etc.  Let us pause here to review a few
   of these that will be useful in what follows. *)

(* A RELATION on a set X is a proposition parameterized by two
   Xs -- i.e., it is a logical assertion involving two values
   from the set X.  (This definition is just giving a name to
   the idea that we've been using for the past few minutes.) *)
Definition relation (X: Set) := X->X->Prop.

(* A relation R on a set X is a PARTIAL FUNCTION if, for
   every x, there is at most one y such that R x y -- or,
   to put it differently, if R x y1 and R x y2 together imply
   y1 = y2. *)
Definition partial_function (X: Set) (R: relation X) :=
  forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.

Implicit Arguments partial_function [X].

Theorem next_nat_partial_function :
   partial_function next_nat.
Proof.
  unfold partial_function.
  intros x y1 y2 P Q.
  inversion P. inversion Q.
  reflexivity. Qed.

Theorem le_not_a_partial_function :
  ~ (partial_function le).
Proof.
  (* WORK IN CLASS *) Admitted.

Exercise: 2 stars

(* Show that the total_relation you defined above is not
   a partial function, but that empty_relation is. *)
(* FILL IN HERE *)

Definition reflexive (X: Set) (R: relation X) :=
  forall a : X, R a a.

Implicit Arguments reflexive [X].

Theorem le_reflexive :
  reflexive le.
Proof.
  unfold reflexive. intros n. apply le_n. Qed.

Definition transitive (X: Set) (R: relation X) :=
  forall a b c : X, (R a b) -> (R b c) -> (R a c).

Implicit Arguments transitive [X].
Theorem le_trans :
  transitive le.
Proof.
  intros n m o Hnm Hmo.
  induction Hmo.
  Case "le_n". apply Hnm.
  Case "le_S". apply le_S. apply IHHmo. Qed.

Theorem lt_trans:
  transitive lt.
Proof.
  unfold lt. unfold transitive.
  intros n m o Hnm Hmo.
  destruct o as [| o'].
  Case "o = 0".
    inversion Hmo.
  Case "o = S o'".
    apply le_S in Hnm.
    apply le_trans with (a := (S n)) (b := (S m)) (c := (S o')).
    apply Hnm. apply Hmo. Qed.

Exercise: 2 stars

(* We can also prove lt_trans more laboriously by induction, 
   without using le_trans.  Do this.*)
Theorem lt_trans' :
  transitive lt.
Proof.
  (* Prove this by induction on evidence that m is 
     less than o *)
  unfold lt. unfold transitive.
  intros n m o Hnm Hmo.
  induction Hmo as [| m' Hm'o].
    (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 2 stars

(* Prove the same thing again by induction on o *)
Theorem lt_trans'' :
  transitive lt.
Proof.
  unfold lt. unfold transitive.
  intros n m o Hnm Hmo.
  induction o as [| o'].
    (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* The transitivity of le, in turn, can be used to prove some
   facts that will be useful later (e.g., for the proof of
   antisymmetry in the next section)... *)
Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
Proof.
  intros n m H. apply le_trans with (S n).
    apply le_S. apply le_n.
    apply H. Qed.

Exercise: 1 star

Theorem le_S_n : forall n m,
  (S n <= S m) -> (n <= m).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Exercise: 2 stars (le_Sn_n_inf)

(* Provide an informal proof of the following theorem:

   Theorem: For every n, ~(S n <= n)

   A formal proof of this is an optional exercise below, but try
   the informal proof without doing the formal proof first

   Proof:
   (* FILL IN HERE *)
 *)

Exercise: 1 star

Theorem le_Sn_n : forall n,
  ~ (S n <= n).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Definition symmetric (X: Set) (R: relation X) :=
  forall a b : X, (R a b) -> (R b a).

Implicit Arguments symmetric [X].

Exercise: 2 stars

Theorem le_not_symmetric :
  ~ (symmetric le).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Definition antisymmetric (X: Set) (R: relation X) :=
  forall a b : X, (R a b) -> (R b a) -> a = b.

Implicit Arguments antisymmetric [X].

Exercise: 2 stars

Theorem le_antisymmetric :
  antisymmetric le.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Definition equivalence (X:Set) (R: relation X) :=
  (reflexive R) /\ (symmetric R) /\ (transitive R).

Implicit Arguments equivalence [X].

Definition partial_order (X:Set) (R: relation X) :=
  (reflexive R) /\ (antisymmetric R) /\ (transitive R).
Implicit Arguments partial_order [X].

Definition preorder (X:Set) (R: relation X) :=
  (reflexive R) /\ (transitive R).
Implicit Arguments preorder [X].

Theorem le_partial_order :
  partial_order le.
Proof.
  unfold partial_order. split.
    Case "refl". apply le_reflexive.
    split.
      Case "antisym". apply le_antisymmetric.
      Case "transitive.". apply le_trans. Qed.

(* --------------------------------------------------------- *)
(* More facts about <= and < *)

(* Let's pause briefly to record several facts about the <= and
   < relations that we are going to need later in the course.
   The proofs make good practice exercises. *)

Exercise: 2 stars, optional (le_exercises)


Theorem O_le_n : forall n,
  0 <= n.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem le_plus : forall a b,
  a <= a + b.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem plus_lt : forall n1 n2 m,
  plus n1 n2 < m ->
  n1 < m /\ n2 < m.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem lt_S : forall n m,
  n < m ->
  n < S m.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem le_step : forall n m p,
  n < m ->
  m <= S p ->
  n <= p.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem ble_nat_true : forall n m,
  ble_nat n m = true -> n <= m.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem ble_nat_n_Sn_false : forall n m,
  ble_nat n (S m) = false ->
  ble_nat n m = false.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem ble_nat_false : forall n m,
  ble_nat n m = false -> ~(n <= m).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.