(** Exercise session 1 - Part 2 — Inductive types

  Similar to last time, when you see REPLACE_ME, replace it with the relevant
  value. Again try to solve the exercises without looking at the live coding
  file. Even if it seems easy when you see us doing it, it might not be so easy
  to do on your own, so try to do it!

  Exercises all start with "EXERCISE".
  When it is written before a lemma, just prove it. :)

**)

Axiom REPLACE_ME : forall {A : Type}, A.

Module define_nat.

  (* Inductive types can be defined using the Inductive keyword *)
  Inductive nat :=
  | O : nat
  | S : nat -> nat.

  (** EXERCISE

    Define addition.

  **)
  Fixpoint add (n m : nat) {struct n} : nat :=
    REPLACE_ME.

  (** EXERCISE

    Define subtraction on natural numbers, truncating at 0.
    In other words, when n < m then sub n m = 0.

  **)
  Fixpoint sub (n m : nat) : nat :=
    REPLACE_ME.

  (** EXERCISE

    Prove the following lemma.
    You will replace Admitted with Qed once it is done.
    What Admitted does should be obvious: it admits a lemma without proof or
    with a partial proof, it can be used in subsequent proofs as if it were
    proven.

  **)
  Lemma add_0 :
    forall n,
      add n O = n.
  Proof.
  Admitted.

  (** EXERCISE **)
  Lemma add_S :
    forall n m,
      add n (S m) = S (add n m).
  Proof.
  Admitted.

  (** With the following commands we declare notations for add and sub. **)
  Infix "+" := add.
  Infix "-" := sub.

  (** EXERCISE **)
  Lemma add_sub :
    forall n m,
      (n + m) - m = n.
  Proof.
  Admitted.

End define_nat.

(** EXERCISE

  Define a boolean predicate deciding equality of natural numbers.

**)
Fixpoint eq_nat (x y : nat) : bool :=
  REPLACE_ME.

(** EXERCISE **)
Lemma eq_nat_spec :
  forall n m,
    eq_nat n m = true <-> n = m.
Proof.
Admitted.

(** EXERCISE **)
Definition cur {X Y Z} (f : X * Y -> Z) : X -> Y -> Z :=
  REPLACE_ME.

(** EXERCISE **)
Definition car {X Y Z} (f : X -> Y -> Z) : X * Y -> Z :=
  REPLACE_ME.

(** EXERCISE **)
Lemma car_cur :
  forall {X Y Z} (f : X * Y -> Z) p,
    car (cur f) p = f p.
Proof.
Admitted.

(** EXERCISE **)
Lemma cur_car :
  forall {X Y Z} (f : X -> Y -> Z) x y,
    cur (car f) x y = f x y.
Proof.
Admitted.

(** EXERCISE **)
Definition swap {X Y} (p : X * Y) : Y * X :=
  REPLACE_ME.

(** EXERCISE **)
Lemma swap_invol :
  forall {X Y} (p : X * Y),
    swap (swap p) = p.
Proof.
Admitted.

(** EXERCISE

  Prove true <> false without the tactics inversion or discriminate.

  Note: a <> b is a notation for a ≠ b, meaning a = b -> False.

**)
Lemma true_false :
  true <> false.
Proof.
Admitted.