Module Shadow.

  (* Inductive definitions/notation as for predefined *)

  Notation "A -> B" := (forall (_ : A), B) : type_scope.

  Theorem impl1 : forall (A B : Prop), A -> B -> A.
  Proof.
    intros A B Ha Hb. apply Ha.
  Qed.

  Print impl1.

  Inductive and (P Q : Prop) : Prop :=
  | conj : P -> Q -> and P Q.

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

  Theorem conj1 : forall (A B : Prop), A /\ B -> A.
  Proof. intros A B H. case H. intros Ha Hb.
         apply Ha. Qed.

  Theorem conj1' : forall (A B : Prop), A /\ B -> A.
  Proof. intros A B H. destruct H as [Ha Hb].
         apply Ha. Qed.

  Theorem conj1'' : forall (A B : Prop), A /\ B -> A.
  Proof. intros A B [Ha Hb]. apply Ha. Qed.

  Theorem conj2: forall (A B : Prop), A -> B -> A /\ B.
  Proof.
    intros A B Ha Hb. apply conj.
    - apply Ha.
    - apply Hb.
  Qed.

  Theorem conj2': forall (A B : Prop), A -> B -> A /\ B.
  Proof.
    intros A B Ha Hb. split.
    - apply Ha.
    - apply Hb.
  Qed.

  Inductive or (P Q : Prop) : Prop :=
  | or_introl : P -> or P Q
  | or_intror : Q -> or P Q.

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

  Theorem disj1 : forall (A B : Prop), A -> A \/ B.
  Proof. intros A B Ha. left. apply Ha. Qed.

  Theorem disj2 : forall (A B : Prop), A \/ A -> A.
  Proof.
    intros A B [Hal | Har].
    - apply Hal.
    - apply Har.
  Qed.

  Inductive False : Prop := .

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

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

  Theorem magic_wand : forall (A : Prop), False -> A.
  Proof.
    intros A Hf. destruct Hf.
  Qed.

  Theorem contra : forall (A B : Prop), (A /\ ~ A) -> B.
  Proof.
    intros A B [Ha Hna]. apply Hna in Ha. destruct Ha.
  Qed.

  Print contra.

End Shadow.

Theorem magic_wand' : forall (A : Prop), False -> A.
Proof. intros A Hf. exfalso. apply Hf. Qed.

Theorem contra' : forall (A B : Prop), (A /\ ~ A) -> B.
Proof. intros A B [Ha Hna]. exfalso.
       apply Hna. apply Ha. Qed.

Module Extra.

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

  Notation "A <-> B" := (iff A B) : type_scope.                         

  Inductive ex {A : Type} (P : A -> Prop) : Prop :=
  | ex_intro : forall x : A, P x -> ex P.

End Extra.

  (* Notation: exists x, P means ex (fun x => P) *)

Theorem tiny : exists n, n + n = 4.
Proof. apply (ex_intro _ 2). reflexivity. Qed.
 
Theorem tiny' : exists n, n + n = 4.
Proof. exists 2. reflexivity. Qed.

Theorem small:
  forall m, (exists n, m = 4 + n) ->
            (exists p, m = 2 + p).
Proof.
  intros m [n Hn].
  exists (2 + n).
  rewrite Hn. reflexivity.
Qed.

(* Below is homework *)
(* Replace 'Admitted.' with a proper proof ending with Qed. *)

(* and_dist_over_or1 : 3 points *)

Theorem and_dist_over_or1 :
  forall (A B C : Prop),
    (A /\ (B \/ C)) -> ((A /\ B) \/ (A /\ C)).
Admitted.

(* or_contrapositive : 3 points *)

Theorem or_contrapositive :
  forall (A B C : Prop),
    (A -> (B \/ C)) -> ~ B -> ~ C -> ~A.
Admitted.

(* exists_not_forall_not : 2 points *)

Theorem exists_not_forall_not :
  forall (A : Type) (P : A -> Prop),
    (exists x, P x) -> ~ (forall x, ~ P x).
Admitted.

(* not_exists_forall_not : 2 points *)

Theorem not_exists_forall_not :
  forall (A : Type) (P : A -> Prop),
    ~ (exists x, P x) -> (forall x, ~ P x).
Admitted.

(* exists_dist_over_or : 3 points *)

Theorem exists_dist_over_or :
  forall (A : Type) (P Q : A -> Prop),
    (exists x, (P x \/ Q x)) <-> ((exists x, P x) \/ (exists x, Q x)).
Admitted.

(* forall_dist_over_and : 2 points *)

Theorem forall_dist_over_and :
  forall (A : Type) (P Q : A -> Prop), (forall x, (P x /\ Q x)) <->
    ((forall x, P x) /\ (forall x, Q x)).
Admitted.

(* Below this is optional and not for credit. *)

(* The next five statements are not provable in
   intuitionistic predicate logic. But it is possible
   to prove that they are all equivalent. Can you do this? *)

Definition excluded_middle := forall P : Prop,
  P \/ ~ P.

Definition peirce := forall P Q: Prop,
  ((P -> Q) -> P) -> P.

Definition double_negation_elimination := 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).

(* Here is an example of the kind of theorem you might prove,
   and you might find the 'unfold' tactic given here useful. 
   There are twenty implications of this kind possible among
   five propositions, but you don't have to prove all twenty;
   you just have to prove enough to be able to get from any one
   to any other by transitivity of implication. *)

Theorem bigfive1: excluded_middle -> double_negation_elimination.
Proof.
  unfold excluded_middle, double_negation_elimination.
  Admitted.