(* Logic in Coq
   Version of 2/11/2009
*)

Require Export Indsol.

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

(* Exercise: 3 stars *)
(* Prove (again) that equality is transitive without using [rewrite]
   or [reflexivity].  (If you're stumped, try some of the tactics
   we've used with other inductively defined datatypes in the
   past.) *)
Theorem trans_eq' : forall (X : Set) (n m o : X),
  n = m -> m = o -> n = o.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

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! (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
   [X]s -- 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.
    apply Hnm.
    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.
  (* OPTIONAL EXERCISE *) Admitted.

(* Exercise: 2 stars (le_Sn_n_inf) *)
(* Provide an informal proof of the following theorem:

   Theorem: For any 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.
  (* OPTIONAL EXERCISE *) 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.