Module Shadow_Nat.

  Inductive nat : Set :=
  | Z : nat (* Coq uses the letter O, alas *)
  | S : nat -> nat.

(* Special Coq shorthand for predefined nats: 0, 1, 2... *)

(* definition of recursive function *)

  Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | Z => m
    | S n' => S (plus n' m)
  end.

(* telling Coq about infix notation *)

  Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                      : nat_scope.

  Fixpoint mult (n m : nat) : nat :=
  match n with
    | Z => Z
    | S n' => plus m (mult n' m)
  end.

  Notation "x * y" := (mult x y)
                       (at level 40, left associativity)
                      : nat_scope.

  Definition pred (n: nat) : nat :=
    match n with
      | Z => Z
      | (S n') => n'
    end.

  Theorem pred_removes_S : forall n, n = pred (S n).
  Proof. reflexivity. Qed.

  Theorem S_injective : forall n m, S n = S m -> n = m.
  Proof.
    intros n m H.
    rewrite pred_removes_S. rewrite <- H. reflexivity.
  Qed.

  Theorem S_injective' : forall n m, S n = S m -> n = m.
  Proof.
    intros n m H1.
    assert (H2: n = pred (S n)). { reflexivity. }
    rewrite H1 in H2. rewrite H2. reflexivity.
  Qed.

  Theorem S_injective'' : forall n m, S n = S m -> n = m.
  Proof. intros n m H. injection H. intros H1. apply H1.
  Qed.

  Definition disc_fn (n: nat) : Prop :=
    match n with
      | Z => True
      | S _ => False
    end. 
  
  Theorem disc2 : ~ (Z = S Z).
  Proof.
    intro H1. 
    assert (H2 : disc_fn Z). { apply I. }
    rewrite H1 in H2. apply H2.
  Qed.
  
  Theorem disc1 : ~ (Z = S Z).
  Proof.
    intro H. discriminate H.
  Qed.

  Theorem plus_n_0 : forall n, n + Z = n.  
  Proof.
    intros n. case n.
    - reflexivity.
    - intros n0. simpl. 
  Abort.

  Theorem plus_n_0 : forall n, n + Z = n.
  Proof.
    intros n. destruct n.
    - reflexivity.
    - simpl. 
  Abort.

  Theorem plus_n_0 : forall n, n + Z = n.
  Proof.
    intros [ | n'].
    - reflexivity.
    - simpl. 
  Abort.

  Check nat_ind.
  Check nat_rect.
  Print nat_rect.


  Theorem plus_n_0 : forall n, n + Z = n.  
  Proof.
    apply nat_ind.
    - reflexivity.
    - intros n IH. simpl. rewrite IH. reflexivity.
  Qed.

  Theorem plus_n_0' : forall n, n + Z = n.  
  Proof.
    intro n. elim n.
    - reflexivity.
    - intros n0 IH. simpl. rewrite IH. reflexivity.
  Qed.

  Theorem plus_n_0'' : forall n, n + Z = n.  
  Proof.
    induction n.
    - reflexivity.
    - simpl. rewrite IHn. reflexivity.
  Qed.

  Theorem plus_n_0''' : forall n, n + Z = n.  
  Proof.
    induction n as [| n' IHn'].
    - reflexivity.
    - simpl. rewrite IHn'. reflexivity.
  Qed.

(* evenness *)

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

Example ev_zero : ev Z.
Proof. apply ev_0. Qed.

Example ev_four : ev (S (S (S (S Z)))).
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

Theorem ev_minus2' : forall n,
  ev n -> ev (pred (pred n)).
Proof.
  intros n E.
  destruct E as [| n' E'].
  - (* E = ev_0 *) simpl. apply ev_0.
  - (* E = ev_SS n' E' *) simpl. apply E'.  Qed.

Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
Proof. intros n H. destruct H. Abort.

Theorem ev_inversion :
  forall (n : nat), ev n ->
    (n = Z) \/ (exists n', n = S (S n') /\ ev n').
Proof.
  intros n Hev.
  destruct Hev as [ | n' Hn'].
  - left. reflexivity.
  - right. exists n'. split. reflexivity. apply Hn'.
Qed.

Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
Proof. intros n H. apply ev_inversion in H. destruct H.
 - discriminate H.
 - destruct H as [n' [Hnn' Hevn']]. injection Hnn'.
   intro Heq. rewrite Heq. apply Hevn'.
Qed.

Theorem evSS_ev' : forall n, ev (S (S n)) -> ev n.
Proof. intros n H. inversion H as [| x Hn Hx]. apply Hn. Qed.

Theorem one_not_even : ~ ev (S Z).
Proof.
  intros H. apply ev_inversion in H.
  destruct H as [ | [n' [Hn' _]]].
  - discriminate H.
  - discriminate Hn'.
Qed.

Theorem one_not_even' : ~ ev (S Z).
  intros H. inversion H. Qed.


(* definition of <= as inductive proposition *)

  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.

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

  Definition lt (n m:nat) := le (S n) m.

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

  Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
  Proof. intros n m p H1 H2.
   induction H2 as [m | m p' H IH]. 
   - apply H1.
   - apply le_S. apply IH. apply H1.
  Qed.

  (* definition of the = relation as an inductive proposition *)
  
  Inductive EQ {A : Type} (x : A) : A -> Type :=
  | eq_refl': EQ x x.

  Check EQ_ind.
  Print EQ_rect.

  (* predefined has 'eq', 'eq_refl', and notation for infix = *)

(* above done in lecture *)

(* below is homework *)

  Fixpoint nateq (n m : nat) : bool :=
    match n with
      | Z => match m with
              | Z => true
              | S _ => false
            end
      | S n' => match m with
                 | Z => false
                 | S m' => nateq n' m'
                end
    end.

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

  (* eq_is_nateq : 3 points *)

  Theorem eq_is_nateq : forall n m, n = m -> nateq n m = true.
  Admitted.
  

  (* nateq_is_eq : 3 points *)

  Theorem nateq_is_eq : forall n m, nateq n m = true -> n = m.
  Admitted.


  (* Z_le_n : 1 point *)

  Theorem Z_le_n : forall n, Z <= n.
  Admitted.


  (* Sn_le_n_le : 2 points *)

  Theorem Sn_le_n_le : forall n m, S n <= m -> n <= m.
  Admitted.

  (* S_le_m_n : 2 points *)

  Theorem S_le_m_n : forall n m, (S n <= S m) -> n <= m.
  Admitted.

  (* not_Sn_le_n : 3 points *)

  Theorem not_Sn_le_n : forall n, ~ (S n <= n).
  Admitted.

  (* S_fn : 1 point *)

  Theorem S_fn : forall n m, n = m -> S n = S m.
  Admitted.

  (* both_les_eq : 4 points *)

  Theorem both_les_eq : forall n m, n <= m -> m <= n -> n = m.
  Admitted.

End Shadow_Nat.