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 *)