ListsWorking with Structured Data

Pairs of Numbers

An Inductive definition of pairs of numbers. It has just one constructor, taking two arguments:
Inductive natprod : Type :=
  | pair (n1 n2 : nat).
Check (pair 3 5) : natprod.

Functions for extracting the first and second components of a pair can then be defined 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.
Compute (fst (pair 3 5)).
(* ===> 3 *)

A nicer notation for pairs:
Notation "( x , y )" := (pair x y).
The new notation can be used both in expressions and in pattern matches.
Compute (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.

If we state properties of pairs in a slightly peculiar way, we can sometimes complete their proofs with just reflexivity and its built-in simplification:
Theorem surjective_pairing' : ∀ (n m : nat),
  (n,m) = (fst (n,m), snd (n,m)).
Proof.
  reflexivity. Qed.

But just 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 numbers:
Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : 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...

Repeat

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

Length

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

Append

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.

Head and Tail

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.

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'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons n l' *)
    reflexivity. Qed.
Usually, though, interesting theorems about lists require induction for their proofs. We'll see how to do this next.

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_assoc : ∀ l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* 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. ☐

Generalizing Statements

Sometimes statements need to be generalized to proof them by induction:
Theorem repeat_double_firsttry : ∀ c n: nat,
  repeat n c ++ repeat n c = repeat n (c + c).
Proof.
  intros c. induction c as [| c' IHc'].
  - (* c = 0 *)
    intros n. simpl. reflexivity.
  - (* c = S c' *)
    intros n. simpl.
    (*  Now we seem to be stuck.  The IH cannot be used to 
        rewrite repeat n (c' + S c'): it only works
        for repeat n (c' + c'). If the IH were more liberal here
        (e.g., if it worked for an arbitrary second summand),
        the proof would go through. *)
Abort.
A generalization of the statement that gives a stronger inductive hypothesis:
Theorem repeat_plus: ∀ c1 c2 n: nat,
    repeat n c1 ++ repeat n c2 = repeat n (c1 + c2).
Proof.
  intros c1 c2 n.
  induction c1 as [| c1' IHc1'].
  - simpl. reflexivity.
  - simpl.
    rewrite <- IHc1'.
    reflexivity.
  Qed.

Reversing a List

A more interesting example of induction over lists:
Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil ⇒ nil
  | h :: t ⇒ 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' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = n :: l' *)
    simpl.
    rewrite <- IHl'.
Abort.
A first attempt:
Theorem app_rev_length_S_firsttry: ∀ l n,
  length (rev l ++ [n]) = S (length (rev l)).
Proof.
  intros l. induction l as [| m l' IHl'].
  - (* l =  *)
    intros n. simpl. reflexivity.
  - (* l = m:: l' *)
    intros n. simpl.
    (* IHl' not applicable. *)
Abort.
A slightly strenghtened statement:
Theorem app_length_S: ∀ l n,
  length (l ++ [n]) = S (length l).
Proof.
  intros l n. induction l as [| m l' IHl'].
  - (* l =  *)
    simpl. reflexivity.
  - (* l = m:: l' *)
    simpl.
    rewrite IHl'.
    reflexivity.
Qed.
We can prove a lemma to bridge the gap.

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

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' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. rewrite → app_length.
    simpl. rewrite → IHl'. rewrite add_comm.
    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,
        length (repeat n m) = m. Which tactics do we need besides intros, simpl, rewrite, and reflexivity? (1) none, (2) destruct, (3) induction on n, (4) induction on m, or (5) can't be done with the tactics we've seen.

Options

Suppose we'd like a function to retrieve the nth element of a list. What to do if the list is too short?
Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
  match l with
  | nil ⇒ 42
  | a :: l' ⇒ match n with
               | 0 ⇒ a
               | S n' ⇒ nth_bad l' n'
               end
  end.

The solution: natoption.
Inductive natoption : Type :=
  | Some (n : nat)
  | None.
Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
  match l with
  | nil ⇒ None
  | a :: l' ⇒ match n with
               | O ⇒ Some a
               | S n' ⇒ nth_error l' n'
               end
  end.
Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.
Proof. reflexivity. Qed.

End NatList.

Partial Maps

As a final illustration of how data structures can be defined in Coq, here is a simple partial map data type, analogous to the map or dictionary data structures found in most programming languages.
First, we define a new inductive datatype id to serve as the "keys" of our partial maps.
Inductive id : Type :=
  | Id (n : nat).
Internally, an id is just a number. Introducing a separate type by wrapping each nat with the tag Id makes definitions more readable and gives us flexibility to change representations later if we want to.

We'll also need an equality test for ids:
Definition eqb_id (x1 x2 : id) :=
  match x1, x2 with
  | Id n1, Id n2 ⇒ n1 =? n2
  end.

Now we define the type of partial maps:
Inductive partial_map : Type :=
  | empty
  | record (i : id) (v : nat) (m : partial_map).

The update function overrides the entry for a given key in a partial map by shadowing it with a new one (or simply adds a new entry if the given key is not already present).
Definition update (d : partial_map)
                  (x : id) (value : nat)
                  : partial_map :=
  record x value d.

We can define functions on partial_maps by pattern matching.
Fixpoint find (x : id) (d : partial_map) : natoption :=
  match d with
  | empty ⇒ None
  | record y v d' ⇒ if eqb_id x y
                     then Some v
                     else find x d'
  end.
Is the following claim true or false?
Theorem quiz1 : ∀ (d : partial_map)
                       (x : id) (v: nat),
  find x (update d x v) = Some v.
(1) True
(2) False
(3) Not sure
Is the following claim true or false?
Theorem quiz2 : ∀ (d : partial_map)
                       (x y : id) (o: nat),
  eqb_id x y = false →
  find x (update d y o) = find x d.
(1) True
(2) False
(3) Not sure