ListsWorking with Structured Data

Require Export Induction.

Module NatList.

Pairs of Numbers

Here's an Inductive with just one constructor.

Inductive natprod : Type :=
pair : nat → nat → natprod.

We can construct an element of natprod like this:

Check (pair 3 5).

We can define functions on pairs by pattern matching.

Definition fst (p : natprod) : nat :=
  match p with
  | pair x y ⇒ x
  end.
Definition snd (p : natprod) : nat :=
  match p with
  | pair x y ⇒ y
  end.

Eval compute in (fst (pair 3 5)).
(* ===> 3 *)

A nicer notation for pairs:

Notation "( x , y )" := (pair x y).

The new notation is supported both in expressions and in pattern matches:

Eval compute in (fst (3,5)).

Definition fst' (p : natprod) : nat :=
  match p with
  | (x,y) ⇒ x
  end.
Definition snd' (p : natprod) : nat :=
  match p with
  | (x,y) ⇒ y
  end.

Definition swap_pair (p : natprod) : natprod :=
  match p with
  | (x,y) ⇒ (y,x)
  end.

Let's prove some facts about pairs...

Theorem surjective_pairing' : ∀(n m : nat),
(n,m) = (fst (n,m), snd (n,m)).
Proof.
reflexivity. Qed.

Note that reflexivity is not enough if we state the lemma in a more natural way:

Theorem surjective_pairing_stuck : ∀(p : natprod),
p = (fst p, snd p).
Proof.
simpl. (* Doesn't reduce anything! *)
Abort.

Solution: use destruct.

Theorem surjective_pairing : ∀(p : natprod),
p = (fst p, snd p).
Proof.
intros p. destruct p as [n m]. simpl. reflexivity. Qed.

Lists of Numbers

An inductive definition of lists of natural numbers:

Inductive natlist : Type :=
| nil : natlist
| cons : nat → natlist → natlist.

Definition mylist := cons 1 (cons 2 (cons 3 nil)).

Some notation for lists to make our lives easier:

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

Now these all mean exactly the same thing:

Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1;2;3].

Some useful list-manipulation functions:

Fixpoint repeat (n count : nat) : natlist :=
  match count with
  | O ⇒ nil
  | S count' ⇒ n :: (repeat n count')
  end.

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

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil ⇒ l2
  | h :: t ⇒ h :: (app t l2)
  end.

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity. Qed.
Example test_app2: nil ++ [4;5] = [4;5].
Proof. reflexivity. Qed.
Example test_app3: [1;2;3] ++ nil = [1;2;3].
Proof. reflexivity. Qed.

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil ⇒ default
  | h :: t ⇒ h
  end.

Definition tl (l:natlist) : natlist :=
  match l with
  | nil ⇒ nil
  | h :: t ⇒ t
  end.

Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tl: tl [1;2;3] = [2;3].
Proof. reflexivity. Qed.

What does the following function do?

Fixpoint foo (n:nat) : natlist :=
  match n with
  | 0 ⇒ nil
  | S n' ⇒ n :: (foo n')
  end.

(Press any key when you have the answer.)

Reasoning About Lists

As with numbers, some proofs about list functions need only simplification.

Theorem nil_app : ∀l:natlist,
[] ++ l = l.
Proof. reflexivity. Qed.

...and some need case analysis.

Theorem tl_length_pred : ∀l:natlist,
  pred (length l) = length (tl l).
Proof.
  intros l. destruct l as [| n l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons n l'".
    reflexivity. Qed.

Usually, though, interesting theorems about lists require induction for their proofs.

Induction on Lists

Coq generates an induction principle for every Inductive definition, including lists. We can use the induction tactic on lists to prove things like the associativity of list-append...

Theorem app_ass : ∀l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3. induction l1 as [| n l1'].
  Case "l1 = nil".
    reflexivity.
  Case "l1 = cons n l1'".
    simpl. rewrite → IHl1'. reflexivity. Qed.

For comparison, here is an informal proof of the same theorem.

Theorem: For all lists l1, l2, and l3, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).

Proof: By induction on l1.

First, suppose l1 = []. We must show

([] ++ l2) ++ l3 = [] ++ (l2 ++ l3),

which follows directly from the definition of ++.
Next, suppose l1 = n::l1', with

  (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)

(the induction hypothesis). We must show

  ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3).

By the definition of ++, this follows from

  n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)),

which is immediate from the induction hypothesis. ☐

Here is a similar example to be worked together in class:

Theorem app_length : ∀l1 l2 : natlist,
length (l1 ++ l2) = (length l1) + (length l2).
Proof.
(* WORK IN CLASS *) Admitted.

Next, a bigger example of induction over lists: First, we define a function snoc that inserts an element at the end of a list...

Fixpoint snoc (l:natlist) (v:nat) : natlist :=
  match l with
  | nil ⇒ [v]
  | h :: t ⇒ h :: (snoc t v)
  end.

Now we can use snoc to reverse a list:

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil ⇒ nil
  | h :: t ⇒ snoc (rev t) h
  end.

Example test_rev1: rev [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.

Let's try to prove length (rev l) = length l.

Theorem rev_length_firsttry : ∀l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l'].
  Case "l = []".
    reflexivity.
  Case "l = n :: l'".
    simpl.
    rewrite ← IHl'.
Abort.

We can prove a lemma to bridge the gap.

Theorem length_snoc : ∀n : nat, ∀l : natlist,
  length (snoc l n) = S (length l).
Proof.
  intros n l. induction l as [| n' l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons n' l'".
    simpl. rewrite → IHl'. reflexivity. Qed.

Now we can complete the original proof.

Theorem rev_length : ∀l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons".
    simpl. rewrite → length_snoc.
    rewrite → IHl'. reflexivity. Qed.

To prove the following theorem, which tactics will we need besides intros, simpl, rewrite and reflexivity? (1) none (2) destruct, (3) induction on n, (4) induction on l, or (5) can't be done with the tactics we've seen.

Theorem foo1 : ∀n :nat, ∀l: natlist,
repeat n 0 = l → length l = 0.

What about the next one?

Theorem foo2 : ∀n m:nat, ∀l: natlist,
repeat n m = l → length l = m.

Which tactics do we need besides intros, simpl, rewrite and reflexivity? (1) none (2) destruct, (3) induction on m, (4) induction on l, or (5) can't be done with the tactics we've seen.

What about the next one?

Theorem foo3 : ∀l: natlist, ∀n m:nat,
length l = m → length (snoc l n) = S m.

Which tactics do we need besides intros, simpl, rewrite and reflexivity? (1) none (2) destruct, (3) induction on m, (4) induction on l, (5) using an auxiliary lemma, or (6) can't be done with the tactics we've seen.

What about the next one?

Theorem foo4 : ∀n :nat, ∀l1 l2: natlist,
snoc l1 n = l2 → (blt_nat 0 (length l2)) = true.

Which tactics do we need besides intros, simpl, rewrite and reflexivity? (1) none (2) destruct, (3) induction on n, (4) induction on l1, (5) induction on l2, (6) can't be done with the tactics we've seen.

Options

Inductive natoption : Type :=
| Some : nat → natoption
| None : natoption.

We'd like to write a function to retrieve the nth element of a list, but what if it's too short?

Fixpoint index_bad (n:nat) (l:natlist) : nat :=
  match l with
  | nil ⇒ 42 (* arbitrary! *)
  | a :: l' ⇒ match beq_nat n O with
               | true ⇒ a
               | false ⇒ index_bad (pred n) l'
               end
  end.

The solution: natoption.

Fixpoint index (n:nat) (l:natlist) : natoption :=
  match l with
  | nil ⇒ None
  | a :: l' ⇒ match beq_nat n O with
               | true ⇒ Some a
               | false ⇒ index (pred n) l'
               end
  end.

Example test_index1 : index 0 [4;5;6;7] = Some 4.
Proof. reflexivity. Qed.
Example test_index2 : index 3 [4;5;6;7] = Some 7.
Proof. reflexivity. Qed.
Example test_index3 : index 10 [4;5;6;7] = None.
Proof. reflexivity. Qed.

We can rewrite this function using Coq's "if" expressions, which work on any inductive type with two constructors.

Fixpoint index' (n:nat) (l:natlist) : natoption :=
  match l with
  | nil ⇒ None
  | a :: l' ⇒ if beq_nat n O then Some a else index' (pred n) l'
  end.

Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n' ⇒ n'
  | None ⇒ d
  end.

Dictionaries

Last example: a dictionary data structure mapping a finite set of keys (numbers) to corresponding values (also numbers, for now).

Module Dictionary.

Inductive dictionary : Type :=
  | empty : dictionary
  | record : nat → nat → dictionary → dictionary.

Definition insert (key value : nat) (d : dictionary) : dictionary :=
  (record key value d).

We can define functions on dictionary by pattern matching, as always.

Fixpoint find (key : nat) (d : dictionary) : natoption :=
  match d with
  | empty ⇒ None
  | record k v d' ⇒ if (beq_nat key k)
                       then (Some v)
                       else (find key d')
  end.

Is the following claim true or false?

Theorem dictionary_invariant1 : ∀(d : dictionary)
(k v: nat),
(find k (insert k v d)) = Some v.

(1) True

(2) False

(3) Not sure

Is the following claim true or false?

Theorem dictionary_invariant2 : ∀(d : dictionary)
                                  (m n o: nat),
  (beq_nat m n) = false →
  (find m d) = (find m (insert n o d)).

(1) True

(2) False

(3) Not sure

End Dictionary.

End NatList.

(* $Date: 2013-07-30 12:24:33 -0400 (Tue, 30 Jul 2013) $ *)