(* exercise nandb *)

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

Example test_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. simpl. reflexivity. Qed.

(* exercise andb3 *)

Definition andb3 (b1: bool) (b2: bool) (b3: bool) : bool :=
  match (b1, b2, b3) with
  | (true, true, true) => true
  | _ => false
  end.

Example test_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.

(* exercise factorial *)

Fixpoint factorial (n: nat) : nat :=
  match n with
  | 0 => 1
  | S n => S n * factorial n
  end.

Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.

Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.

(* exercise blt_nat *)

Definition blt_nat (n m : nat) : bool :=
  match m - n with
  | 0 => false
  | S _ => true
  end.

Example test_blt_nat1: (blt_nat 2 2) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat2: (blt_nat 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat3: (blt_nat 4 2) = false.
Proof. simpl. reflexivity. Qed.

(* exercise plus_id_exercise *)

Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  intros n m o.
  intros H1 H2.
  rewrite -> H1.
  rewrite -> H2.
  reflexivity.
Qed.

(* exercise mult_S_1 *)

Theorem plus_1_l : forall n : nat, 1 + n = S n.
Proof. intros n. simpl. reflexivity. Qed.

Theorem mult_S_1 : forall n m : nat,
    m = S n ->
    m * (1 + n) = m * m.
Proof.
  intros n m H.
  rewrite plus_1_l.
  rewrite H.
  reflexivity.
Qed.

(* exercise andb_true_elim2 *)

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

Theorem andb_true_elim2 : forall b c : bool,
    andb b c = true -> c = true.
Proof.
  intros [] [].
  - reflexivity.
  - simpl. intros H. rewrite -> H. reflexivity.
  - reflexivity.
  - simpl. intros H. rewrite -> H. reflexivity.
Qed.

(* exercise zero_nbeq_plus_1 *)

Fixpoint beq_nat (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => beq_nat n' m'
            end
  end.

Theorem zero_nbeq_plus_1 : forall n : nat,
  beq_nat 0 (n + 1) = false.
Proof.
  intros [|n].
  reflexivity.
  reflexivity.
Qed.

(* exercise boolean functions *)

Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
    (forall (x: bool), f x = x) ->
    forall (b : bool), f (f b) = b.
Proof.
  intros id id_idem b.
  rewrite id_idem. rewrite id_idem. reflexivity.
Qed.

(* exercise and_eq_orb *)

Lemma andb_comm : forall b c : bool, andb b c = andb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

Lemma andb_l_false : forall b : bool, andb false b = false.
Proof.
  intros [].
  - reflexivity.
  - reflexivity.
Qed.

Lemma orb_comm : forall b c : bool, orb b c = orb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

Lemma orb_l_true : forall b : bool, orb true b = true.
Proof.
  intros [].
  - reflexivity.
  - reflexivity.
Qed.

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  intros []  [].
  - reflexivity.
  - rewrite -> andb_comm. rewrite -> andb_l_false.
    rewrite -> orb_l_true.
    intros H. rewrite -> H. reflexivity.
  - rewrite -> andb_l_false.
    rewrite -> orb_comm. rewrite -> orb_l_true.
    intros H. rewrite -> H. reflexivity.
  - reflexivity.
Qed.

(* exercise binary *)

Inductive bin : Type :=
| Z : bin
| DB : bin -> bin
| DI : bin -> bin.

Fixpoint incr (b : bin) : bin :=
  match b with
  | Z => DI Z
  | DB x => DI x
  | DI x => DB (incr x)
  end.

Fixpoint bin_to_nat (b : bin) : nat :=
  match b with
  | Z => 0
  | DB x => 2 * bin_to_nat x
  | DI x => 1 + (2 * bin_to_nat x)
  end.

Example text_bin_incr1: bin_to_nat (incr Z) = S (bin_to_nat Z).
reflexivity. Qed.
Example text_bin_incr2: bin_to_nat (incr (DI Z)) = S (bin_to_nat (DI Z)).
reflexivity. Qed.
Example text_bin_incr3: bin_to_nat (incr (DB Z)) = S (bin_to_nat (DB Z)).
reflexivity. Qed.
Example text_bin_incr4: bin_to_nat (incr (DI (DI Z))) = S (bin_to_nat (DI (DI Z))).
reflexivity. Qed.
Example text_bin_incr5: bin_to_nat (incr (DB (DI Z))) = S (bin_to_nat (DB (DI Z))).
reflexivity. Qed.