Require Export Induction.
Module NatList.

Inductive natlist : Type :=
  | nil  : natlist
  | cons : nat -> natlist -> natlist.

Notation "x :: l" := (cons x l)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil => O
  | h :: t => S (length t)
  end.

Fixpoint snoc (l:natlist) (x:nat) : natlist :=
  match l with
  | nil => x :: nil
  | h :: t => h :: (snoc t x)
  end.
                  
(* Exercise: Define the "member" function on natlists *)
Fixpoint member (l:natlist) (x:nat) : bool := admit.

(* Prove the following three theorems. Looking at them: Which do you
need to use induction on? Which require destruct (only)? Which require
only intros and reflexivity? *)

Theorem member_in_cons : forall (l : natlist) (x : nat),
  member (x :: l) x = true.
Proof. Admitted.

Theorem member_not_in_nil : forall (x : nat),
  member (nil) x = false.
Proof. Admitted.

Theorem snoc_plus_one : forall (x : nat) (l : natlist),
  length (snoc l x) = 1 + (length l).
Proof. Admitted.

(* To do: Quick visit of PartialMap from Lists.v *)