ListsWorking with Structured Data

From LF Require Export Induction.
Module NatList.

Pairs of Numbers

An Inductive definition of pairs of numbers. Note that 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.

Now let's try to prove a few simple facts about pairs.
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 the most 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. ☐

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.
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.

Exercise: 1 star, standard (eqb_id_refl)

Theorem eqb_id_refl : ∀ x, eqb_id x x = true.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Now we define the type of partial maps:

Module PartialMap.
Export NatList. (* make the definitions from NatList available here *)

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.
Proof.
(* FILL IN HERE *) Admitted.
(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.
Proof.
(* FILL IN HERE *) Admitted.
(1) True
(2) False
(3) Not sure

End PartialMap.