Software Foundations 04 Lists

Software Foundations

Online Textbook

Michael Clarkson's Open Online Course (on Youtube) Michael Charkson's Course (on Bilibili)

Xiong Yingfei's Course Webpage (2023 Spring)

This note is used as a brief summary and supplementofr the textbook and courses.

Lists

Pairs

We define the pair of natural numbers. (Cartesian product) 

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Inductive natprod : Type :=
  | pair (n1 n2 : nat).

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.

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

Then comes a new usage of destruct:

1
2
3
4
5
6
7
8
9
10
Theorem surjective_pairing : forall (p : natprod),
  p = (fst p, snd p).
(* Wrong proof *)
Proof.
  simpl. (* Doesn't reduce anything! *)
Abort.
(* Correct proof *)
Proof.
  intros p. destruct p as [n m]. simpl. reflexivity. 
Qed.

Lists of Natural Numbers

1
2
3
4
5
6
7
8
Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

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

The concatenation operation of natlist is then defined as follows. 

1
2
3
4
5
6
7
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).

Then comes the usage of destruct: 

1
2
3
4
5
6
7
8
9
Theorem tl_length_pred : forall 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.

And of instruction 

1
2
3
4
5
6
7
8
9
Theorem app_assoc : forall 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.

Search Command

1
2
3
4
5
6
7
8
9
10
11
12

(** Display a list of all theorems involving [rev]:  *)
Search rev.

(** Use a pattern to search for all theorems involving the equality of two additions: *)
Search (_ + _ = _ + _).

(** Search inside a particular module as a restriction: *)
Search (_ + _ = _ + _) inside Induction.

(** Make the search more precise by using variables in the search pattern instead of wildcards: *)
Search (?x + ?y = ?y + ?x).

Options

1
2
3
Inductive natoption : Type :=
  | Some (n : nat)
  | None.

Recall Haskell's Maybe, Nothing and Just.

Partial Maps

1
2
3
4
5
6
7
8
9
Inductive id : Type :=
  | Id (n : nat).

Inductive partial_map : Type :=
  | empty
  | record (i : id) (v : nat) (m : partial_map).

Definition update (d : partial_map) (x : id) (value : nat) : partial_map :=
  record x value d.