(* Logic in Coq
   Version of 2/9/2009

   NOTE: This is a preliminary version of Logic.v. Do not submit it.
   A full, revised version will be released on Wednesday the 4th.

   You'll need to compile the previous files in order to use this one.
*)

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, optional (and_ind_principle) *)
(* See if you can predict the induction principle for
   conjunction. *)
Check and_ind.

Lemma 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]. *)
Lemma 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. *)
Lemma and_1 : forall A B : Prop, 
  A /\ B -> A.
Proof.
  intros A B H. 
  inversion H. 
  apply H0.  Qed.

(* Exercise: 1 star, optional *)
Lemma and_2 : forall A B : Prop, 
  A /\ B -> B.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.
Lemma 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 *)
Lemma 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.) *)
Lemma 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.

Lemma iff_implies : forall A B : Prop, 
  (A <-> B) -> A -> B.
Proof.  
  intros A B H. 
  inversion H. apply H0.  Qed.

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

(* Exercise: 1 star, optional *)
Lemma iff_refl : forall A : Prop, 
  A <-> A.
Proof. 
  (* OPTIONAL EXERCISE *) Admitted.

(* Exercise: 1 star, optional *)
Lemma 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.) *)
  (* OPTIONAL EXERCISE *) 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, optional (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. *)
Lemma or_commut : forall A B : Prop,
  A \/ B  -> B \/ A.
Proof.
  intros A B H.
  inversion H.
    Case "left". apply or_intror. apply H0.
    Case "right". apply or_introl. apply H0.  Qed.

(* From here on, we'll use the handy tactics [left] and
   [right] in place of [apply or_introl] and [apply
   or_intror]. *)
Lemma or_commut' : forall A B : Prop,
  A \/ B  -> B \/ A.
Proof.
  intros A B H.
  inversion H.
    Case "left". right. apply H0.
    Case "right". left. apply H0.  Qed.

Lemma 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. 
    Case "left". split.
      SCase "left". left. apply H0.
      SCase "right". left. apply H0.
    Case "right". split.
      SCase "left". right. inversion H0. apply H1.
      SCase "right". right. inversion H0. apply H2.  Qed.

(* Exercise: 2 stars *)
Lemma 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, optional *)
Lemma or_distributes_over_and : forall A B C : Prop,
  A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C).
Proof.
  (* OPTIONAL EXERCISE *) 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. *)

Lemma 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, optional *)
Lemma andb_false : forall b c,
  andb b c = false -> b = false \/ c = false.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* Exercise: 1 star, optional *)
Lemma orb_true : forall b c,
  orb b c = true -> b = true \/ c = true.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* Exercise: 1 star, optional *)
Lemma orb_false : forall b c,
  orb b c = false -> b = false /\ c = false.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

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

Inductive False : Prop := . 

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

(* Exercise: 1 star, optional (False_ind_principle) *)
(* Can you predict the induction principle for falsehood? *)
Check False_ind.

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

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

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

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

Lemma contradiction_implies_anything : forall A B : Prop,
  (A /\ ~A) -> B.
Proof.
  intros A B H. inversion H. unfold not in H1. 
  apply H1 in H0. inversion H0.  Qed.

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

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

(* Exercise: 1 star, optional *)
Lemma not_both_true_and_false : forall A : Prop,
  ~ (A /\ ~A).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Lemma five_not_even :  
  ~ ev 5.
Proof.
  unfold not. intros H. inversion H. inversion H1. inversion H3.  Qed.

(* Exercise: 1 star, optional *)
Lemma ev_not_ev_S : forall n,
  ev n -> ~ ev (S n).
Proof.
  unfold not. intros n H. induction H. (* not n! *)
  (* OPTIONAL EXERCISE *) Admitted.

(* Exercise: 3 stars, optional *)
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). 

(* ---------------------------------------------------------- *)
(* 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. *)
Lemma 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 *)
Lemma beq_nat_n_n' : forall n n' : nat,
     n <> n'
  -> beq_nat n n' = false.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Exercise: 4 stars, optional *)
Lemma beq_false_not_eq : forall n m,
  false = beq_nat n m -> n <> m.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* FIX: This is just a symmetric version of the one above.
   We should really delete one of them and just use the
   other consistently... *)
Lemma not_eq_false_beq : forall n n' : nat,
     n <> n'
  -> false = beq_nat n n'.
Proof.
  intros n n' H. apply beq_nat_n_n' in H. 
  rewrite -> H. reflexivity. Qed.

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

(* Here is an inductive definition of one more very
   important connective: 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:t, 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 : t , p" := (ex _ (fun x:t => p))
  (at level 200, x ident, right associativity) : type_scope.

(* We can use the same tactics as always for manipulate
   existentials.  For example, if to prove an existential,
   we [apply] the constructor [ex_intro].  Since the
   premise of [ex_intro] involves a variable ([witness])
   that does not appear in its conclusion, we need to
   explicitly give its value when we use [apply]. *)
Example exists_example_1 : exists n, plus n (mult n n)
   = 6.
Proof.
  apply ex_intro with (witness:=2). 
  reflexivity.  Qed.

(* 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 [inversion]. *)
Lemma exists_example_2 : forall n,
     (exists m, n = plus 4 m)
  -> (exists o, n = plus 2 o).
Proof.
  intros n H.
  inversion H. 
  exists (plus 2 witness).  
  apply H0.  Qed.

(* Exercise: 2 stars *)
Lemma 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.

(* Exercise: 1 star, optional *)
Lemma dist_not_exists : forall (X:Set) (P : X -> Prop),
  (forall x, P x) -> ~ (exists x, ~ P x).
Proof.
  (* OPTIONAL EXERCISE *) Admitted.