Collections

Pair

• for simple cases of fixed size, can create types to hold multiple values
• Each constructor in Inductive type definition can take 0 or more arguments
  → create fixed size type to hold multiple values
• use tactics such as destruct to expose the type structure and to complete the proof.

Example: construct pair by providing 2 arguments

Inductive natprod : Type :=
| pair (n1 n2 : nat).

(* add notation for easier syntax *)
Notation "( x , y )" := (pair x y).

Definition first (n:natprod) : nat :=
    match n with
    | (x, _) => x
    end.

Definition second(n:natprod): nat :=
    match n with
    | (_, y) => y
    end.

Theorem surjective_pairing: forall (p: natprod),
    p = (first(p), second(p)).
Proof.
    intros p. destruct p as [n m].
    simpl. reflexivity. Qed.

List

List is either empty, or a pair of a number and another list.

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

(*Add notations to make it easier to use:*)
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
Notation "[ ]" := nil.

List operations

List length

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

Append

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

Reverse

Fixpoint reverse (l:natlist) : natlist :=
  match l with
  | nil => nil
  | h :: t => append (reverse t) [h]
  end.

Get head/tail

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

Definition tail (l : natlist) : natlist :=
  match l with
  | nil => nil
  | h :: t => t
  end.

Compute length([1,1,1]).     (* 3: nat *)
Compute append [2,3,5] [4].  (* [2, 3, 5, 4] *)
Compute head 0 [2,4,6].      (* 2 *)
Compute tail [7,8,9].        (* [8, 9] *)

More interesting example:

Fixpoint alternate (l1 l2 : natlist) : natlist :=
  match l1, l2 with
  | nil, l => l
  | l, nil => l
  | h1 :: t1, h2 :: t2 =>  h1 :: h2 :: (alternate t1 t2)
  end.

Proofs for lists

• some simple cases are solvable with reflexivity

Theorem tl_length_pred : forall l: natlist,
  pred (length l) = length (tail l).
Proof.
  intros l. destruct l as [| n l'].
  - reflexivity.
  - reflexivity. Qed.

• generally use induction
• list is either nil or number and list
  • these are the only possible shapes
• during induction: either nil, or cons (constructor) applied to some number and smaller list
  • show proposition \(P\) is true for empty list
  • show \(P\) is true of when l is cons n l' for some number n and smaller list l'

Theorem app_assoc : forall l1 l2 l3 : natlist,
  append (append l1 l2) l3 = append l1 (append l2 l3).
Proof.
  intros l1 l2 l3. induction l1 as [| n l1' IHl1'].
  - reflexivity.
  - simpl.
    rewrite -> IHl1'.
    reflexivity.
 Qed.

Dictionary/Map

• define id that will serve as keys to improve legibility
• create dictionary which is either
  • empty
  • combination of <K,V> and another dictionary

(* type for keys *)
Inductive id : Type :=
  | Id (n : nat).

(* key equality test *)
Definition eqb_id (x1 x2 : id) :=
  match x1, x2 with
  | Id n1, Id n2 => n1 == n2
  end.

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

Dictionary operations

Update

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

Find

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.

see natoption definition

Polymorphic lists

• create a list of polymorphic type X
• nil and cons are now polymorphic constructors
  → caller must provide first argument that is the type of the list

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

Example: list of numbers

(* empty list *)
Check (nil nat) : list nat.

(* list containing 3 *)
Check (cons nat 3 (nil nat)) : list nat.

(* list with 3 elements *)
Check list_of_3 := cons nat 1 (cons nat 2 (cons nat 3 (nil nat)))

Make a list of \(n\) elements

Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
  match count with
  | 0 => nil X
  | S count' => cons X x (repeat X x count')
end.

Alternative way:

• can define X x count and let rely on type inference
• can use wildcards: (X : _) (x : _) (count : _)

Fixpoint repeat_alt X x count : list X :=
  match count with
  | 0 => nil _
  | S count' => cons _ x (repeat_alt _ x count')
  end.

Implicit arguments

• use implicit arguments
• Arguments specifies
  • name of the function
  • list of argument names with curly braces around any implicit arguments
• Arguments without name can use wilcard _
• This way no type needs to be specified to create a list

Arguments nil {X}.
Arguments cons {X} _ _.
Arguments repeat {X} x count.

(* note: no explicit type *)
Definition list1 := cons 1 (cons 2 (cons 3 nil)).

• Arguments can also be made implicit in function declaration → avoid this style with Inductive

Fixpoint repeat_impl {X : Type} (x : X) (count : nat) : list X :=
  match count with
  | 0 => nil
  | S count' => cons x (repeat_impl x count')
  end.

Explicit type

• sometimes need to use explicit types when not enough info is available to infer type from context → use @ or specify type

Definition mynil : list nat := nil.
Definition mynil' := @nil nat.
Check @nil : forall X : Type, list X.

Polymorphic list operations

Fixpoint append {X : Type} (l1 l2 : list X) : (list X) :=
  match l1 with
  | nil => l2
  | cons h t => cons h (append t l2)
  end.

Fixpoint reverse {X:Type} (l:list X) : list X :=
  match l with
  | nil => nil
  | cons h t => append (reverse t) (cons h nil)
end.

Fixpoint length {X : Type} (l : list X) : nat :=
  match l with
  | nil => 0
  | cons _ l' => S (length l')
end.

(* notation *)
Notation "x :: y" := (cons x y)(at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (append x y)(at level 60, right associativity).

Now use polymorphic list:

Definition number_list := [1, 2, 3].
Definition boolean_list := [true, false, false].

Polymorphic Product

• This is a polymorphic version of pair

Inductive prod (X Y : Type) : Type :=
| pair (x : X) (y : Y).

(* make the type implicit *)
Arguments pair {X} {Y} _ _.

(* set easier notation *)
Notation "X * Y" := (prod X Y) : type_scope.

(* get first and second element *)
Definition first {X Y : Type} (p : X * Y) : X :=
  match p with
  | (x, y) => x
  end.

Definition second {X Y : Type} (p : X * Y) : Y :=
  match p with
  | (x, y) => y
  end.

Example: from two lists to a list of pairs

Fixpoint zip_list {X Y : Type} (lx : list X) (ly : list Y) : list (X * Y) :=
match lx, ly with
  | [], _ => []
  | _, [] => []
  | x :: tx, y :: ty => (x, y) :: (zip_list tx ty)
end.