Software Foundations: Working with Structured Data

Lists.v

Require Import Arith.
Require Import List.

Theorem surjective_pairing : forall (A B : Type) (p : A * B), p = (fst p , snd p).
Proof.
  intros A B p. destruct p. reflexivity.
Qed.

Fixpoint nonzeros (l : list nat) : list nat :=
  match l with
  | nil => nil
  | cons n l => if n =? 0 then nonzeros l else n :: nonzeros l
  end.

Fixpoint interleave {A : Type} (l1 l2 : list A) : list A :=
  match l1, l2 with
  | cons a1 l1, cons a2 l2 => a1 :: a2 :: interleave l1 l2
  | l1, nil => l1
  | nil, l2 => l2
  end.

Theorem app_assoc : forall (A : Type) (l1 l2 l3 : list A),
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros A l1 l2 l3.
  induction l1.
  - reflexivity.
  - simpl. rewrite -> IHl1. reflexivity.
Qed.

Lemma app_length : forall (A : Type) (l1 l2 : list A),
  length (l1 ++ l2) = length l1 + length l2.
Proof.
  intros A l1 l2.
  induction l1.
  - reflexivity.
  - simpl. rewrite -> IHl1. reflexivity.
Qed.

Theorem rev_length : forall (A : Type) (l : list A),
  length l = length (rev l).
Proof.
  intros A l.
  induction l.
  - reflexivity.
  - simpl. rewrite -> app_length, plus_comm. rewrite -> IHl. reflexivity.
Qed.

Theorem app_nil_r : forall (A : Type) (l : list A), l ++ nil = l.
Proof.
  intros A l.
  induction l.
  - reflexivity.
  - simpl. rewrite -> IHl. reflexivity.
Qed.

Theorem rev_app_distr : forall (A : Type) (l1 l2 : list A),
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros A l1 l2.
  induction l1.
  - simpl. rewrite -> app_nil_r. reflexivity.
  - simpl. rewrite -> IHl1. rewrite -> app_assoc. reflexivity.
Qed.

Theorem rev_involutive : forall (A : Type) (l : list A),
  rev (rev l) = l.
Proof.
  intros A l.
  induction l.
  - reflexivity.
  - simpl. rewrite -> rev_app_distr. rewrite -> IHl. reflexivity.
Qed.

Theorem rev_injective : forall (A : Type) (l1 l2 : list A),
  rev l1 = rev l2 -> l1 = l2.
Proof.
  intros A l1 l2 H.
  rewrite <- rev_involutive.
  rewrite <- H.
  rewrite -> rev_involutive.
  reflexivity.
Qed.

Fixpoint shunt {A : Type} (l1 l2 : list A) : list A :=
  match l1 with
  | nil => l2
  | cons a l1 => shunt l1 (a :: l2)
  end.

Lemma rev_shunt_app : forall (A : Type) (l1 l2 : list A),
  rev l1 ++ l2 = shunt l1 l2.
Proof.
  intros A l1.
  induction l1.
  - reflexivity.
  - intros l2. simpl. rewrite app_assoc, IHl1. reflexivity.
Qed.

Theorem rev_shunt : forall (A : Type) (l : list A),
  rev l = shunt l nil.
Proof.
  intros A l.
  rewrite <- (rev_shunt_app A l nil).
  rewrite app_nil_r.
  reflexivity.
Qed.