Data Structures

Lists : Working with Structured Data

From now on, we will see structured data, especially lists and pairs, which can contain elements of various types. In the type definition, we will already show them with polymorphic types, but don't worry, we will talk about it in the next chapter. For now, let's just ignore the type and follow the explanation. It will make more sense as we progress in our study.

Data Structures

In an inductive type definition, each constructor can receive any number of arguments -- none like Bool, Empty, or one like Nat -- and we have the Pair that receives two arguments (which can even be other two pairs) and returns a type:

record Pair (a) (b) 

The two received arguments are transformed into the first component, fst, and the second, snd.

record Pair (a) (b) {
  fst : a
  snd : b
} 

The way to construct a pair of Nat is as follows:

Pair.new Nat Nat a b  : (Pair a b)

Here are two simple functions to extract the first and second components of a pair. The definitions also illustrate how to pattern match on two constructor arguments.

Fst (pair: Pair Nat Nat) : Nat
Fst (Pair.new Nat Nat fst snd) = fst

Example 1: (Fst Nat (List Nat) (Pair 2n [1n,2n,3n])) ->  2n

Snd (pair: Pair Nat Nat) : Nat
Snd (Pair.new Nat Nat fst snd) = snd

Example 2: (Snd Nat (List Nat) (Pair 2n [1n,2n,3n])) -> [1n,2n,3n]

Some proofs

Let's try to prove some simple facts about pairs. If we declare things in a particular (and slightly peculiar) way, we can complete proofs with just reflexivity:

Surjective_pairing (p: Pair Nat Nat) : Equal (Pair Nat Nat) p (Pair.new (Fst p) (Snd p))
Surjective_pairing (Pair.new Nat Nat fst snd) = Equal.refl

But Equal.refl is not enough if the statement is:

Surjective_pairing (Pair.new Nat Nat fst snd) = Equal.refl

Since Kind expects

Equal (Pair Nat Nat) p (Pair.new (Fst p) (Snd p))

And received

Equal p p

We must "expose" the internal structure of the pair so that the Type Checker can verify whether p is really equal to Pair.new (Fst p) (Snd p).

Snd_fst_is_swap

Snd_fst_is_swap (p: Pair Nat Nat ) : Equal (Pair Nat Nat) (Pair.swap Nat Nat (Pair.swap Nat Nat p) p)
Snd_fst_is_swap (Pair.new Nat Nat fst snd) = ? 

Fst_swap_is_snd

Fst_swap_is_inverse (p: Pair Nat Nat) (a: Nat) (b: Nat) : Equal (Pair Nat Nat) (Pair.swap Nat Nat (Pair.new a b) (Pair.new b a))
Fst_swap_is_inverse p a b = ?