Module Shadow_Bool.

  Inductive bool : Type :=
  | true : bool
  | false : bool.

(* bool, bool_rect, bool_ind, bool_rec *)

  Check bool_ind.

  Definition andb (b1 b2 : bool) : bool :=
    match b1 with
      | true => b2
      | false => false
    end.

  Compute (andb true false).

  Example andb_true_false : andb true false = false.
  Proof. reflexivity. Qed.

  Check andb_true_false.
  Print andb_true_false.

  Definition andb_true_false' : andb true false = false := eq_refl.

  Definition and_same (b : bool) : (andb b b = b) :=
    match b with
      | true => eq_refl
      | false => eq_refl
    end.

  Print and_same.

  Theorem and_same' : forall b, andb b b = b.
  Proof. intro b. case b. reflexivity. reflexivity. Qed.
    
  Theorem and_same'' : forall b, andb b b = b.
  Proof. 
    intros b. case b.
    - reflexivity.
    - reflexivity.
  Qed.

  Theorem and_commutative : forall b1 b2, andb b1 b2 = andb b2 b1.
  Proof.
    intros b1 b2. case b1.
    - case b2.
      + reflexivity.
      + reflexivity.
    - case b2.
      + reflexivity.
      + reflexivity.
  Qed.

  Theorem and_commutative' : forall b1 b2, andb b1 b2 = andb b2 b1.
  Proof.
    intros b1 b2; case b1; case b2; reflexivity.
  Qed.

  Definition and_same_true := (and_same true).

  Check and_same_true.

  Theorem and_same_true': andb true true = true.
  Proof.
    apply (and_same true).
  Qed.
    
  Print and_same_true'.

  Theorem and_same_true'': andb true true = true.
  Proof.
    apply and_same.
  Qed.

End Shadow_Bool.

Module Shadow_Nat.

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

(* Coq has special 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.

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



(* We'll return to Nat after looking at logic. *)

End Shadow_Nat.