Lists

From The Twelf Project
(Redirected from Heterogeneous lists)
Jump to: navigation, search

This page describes the data structure of lists as well as a large number of operations and theorems about them.

Definition

This standard definition of lists in Twelf . We first define what the list elements are: in this example they are just an arbitrary type elem. This example is parametric in the type of the elements, so you can change this definition to anything you like.

elem: type.

a : elem.
b : elem.
c : elem -> elem.

The important defintion is the one of lists. There are two ways of constructing a Twelf object of type list. The first is the constructor for the empty list nil. The second is the constructor cons that given an object of type elem and an object of type list creates a list with elem as head and list as tail.

list : type. %name list Ls.

nil : list.
cons : elem -> list -> list.
%freeze list.

Equalities

Equality is defined as identity, which makes the symmetry and transitivity proofs entirely trivial. One congruence lemma needs to be defined eq-cong-cons, expressing that if the tails of two lists are equal, and the heads of the lists are identical, the lists are equal.

eq : list -> list -> type.
%mode eq +Ls -Ls'.
eq/ref : eq Ls Ls.
%worlds () (eq _ _).
%freeze eq.

eq-symm : eq Ls Ls' -> eq Ls' Ls -> type.
%mode eq-symm +Q -Q'.
- : eq-symm eq/ref eq/ref.
%worlds () (eq-symm _ _).
%freeze eq-symm.
%total {} (eq-symm _ _).

eq-trans : eq Ls Ls' -> eq Ls' Ls'' -> eq Ls Ls'' -> type.
%mode eq-trans +Q +Q' -Q''.
- : eq-trans eq/ref eq/ref eq/ref.
%worlds () (eq-trans _ _ _).
%freeze eq-trans.
%total {} (eq-trans _ _ _).

eq-cong-cons : {E} eq L1 L2 -> eq (cons E L1) (cons E L2) -> type.
%mode eq-cong-cons +E1 +E2 -E3.
- : eq-cong-cons _ eq/ref eq/ref.
%worlds () (eq-cong-cons _ _ _).
%total {} (eq-cong-cons _ _ _).

Reversal

There are at least two very common operations on lists: Reverse and Append. Lists form a semigroup with the opeation append and the empty list as right and left unit. If we define an operation then reverse is an isomorphism between the semigroups (lists,,nil) and (lists,f,nil).

Definition

I will use the standard logic programming way of encoding reversal. In the following rev will be a ternary relation where the first two elements are input and the third is output. The invariant is , where is concatenation, thus is obtained by rev a nil b. We will later see that can be thought of as .

rev : list -> list -> list -> type.
%mode rev +Ls +Ls'' -Ls'.
rev/nil : rev nil Ls' Ls'.
rev/cons : rev (cons E Ls) Ls'' Ls'
               <- rev Ls (cons E Ls'') Ls'.
%worlds () (rev _ _ _).
%freeze rev.
%total D (rev D _ _).

can-rev : {Ls} {Ls'} rev Ls Ls' Ls'' -> type.
%mode can-rev +Ls +Ls' -R.
- : can-rev nil _ rev/nil.
- : can-rev (cons E Ls) Ls' (rev/cons Ls'')
            <- can-rev Ls (cons E Ls') Ls''.
%worlds () (can-rev _ _ _).
%freeze can-rev. 
%total D (can-rev D _ _).

Equality

rev-eq : eq L1 L2 -> eq L3 L4 -> eq L5 L6 -> rev L1 L3 L5 -> rev L2 L4 L6 -> type.
%mode rev-eq +E1 +E2 +E3 +R1 -R2.
- : rev-eq eq/ref eq/ref eq/ref R R.
%worlds () (rev-eq _ _ _ _ _).
%total {} (rev-eq _ _ _ _ _).

Determinism

As the Twelf definition only states that rev is a relation we need to prove that it indeed is a function. Namely .

rev-determ : rev Ls Ls' Ls3 -> rev Ls Ls' Ls4 -> eq Ls3 Ls4 -> type.
%mode rev-determ +R +R' -Q.
- : rev-determ rev/nil _ eq/ref.
- : rev-determ (rev/cons R) (rev/cons R') Q
         <- rev-determ R R' Q.
%worlds () (rev-determ _ _ _).
%freeze rev-determ.
%total D (rev-determ D _ _).

Double reversal

Reverse is an isomorphism that turn out to be its own inverse. .

revrev-id-lem : rev Ls Ls' Ls'' -> rev Ls'' nil Ls4 -> rev Ls' Ls Ls6 -> eq Ls6 Ls4 -> type.
%mode revrev-id-lem +R +R' +R'' -Q.

- : revrev-id-lem rev/nil F F' Q
          <- rev-determ F' F Q.
- : revrev-id-lem (rev/cons R) R' R'' Q
          <- revrev-id-lem R R' (rev/cons R'') Q.

%worlds () (revrev-id-lem _ _ _ _).
%freeze revrev-id-lem.
%total D (revrev-id-lem D _ _ _).

revrev-id : rev A nil B -> rev B nil A -> type.
%mode revrev-id +R -R'.
- : revrev-id R R'
  <- can-rev _ nil R1
  <- revrev-id-lem R R1 rev/nil E
  <- eq-symm E E'
  <- rev-eq eq/ref eq/ref E' R1 R'.
%worlds () (revrev-id _ _).
%freeze revrev-id.
%total {} (revrev-id _ _).

Injectivity

As reverse has an inverse it is injective .

rev-injective : rev Ls nil Ls' -> rev Ls'' nil Ls' -> eq Ls Ls'' -> type.
%mode rev-injective +R +R' -Q.
- : rev-injective (R : rev Ls nil Ls') R' Q
      <- revrev-id R R1
      <- revrev-id R' R1'
      <- rev-determ R1 R1' Q.
%worlds () (rev-injective _ _ _).
%freeze rev-injective.
%total D (rev-injective D _ _).

Append

Definition

append : list -> list -> list -> type.  %name append A.

append/nil : append nil L L.
append/cons : append (cons E L1) L2 (cons E L3)
     <- append L1 L2 L3.

%freeze append.

can-append : {L1}{L2} append L1 L2 L3 -> type.
%mode can-append +L1 +L2 -A.

- : can-append nil L append/nil.
- : can-append (cons E L1) L2 (append/cons A)
     <- can-append L1 L2 A.

%worlds () (can-append _ _ _).
%total D (can-append D _ _).

Equality

append-eq : eq L1 L2 -> eq L3 L4 -> eq L5 L6 -> append L1 L3 L5 -> append L2 L4 L6 -> type.
%mode append-eq +E1 +E2 +E3 +A1 -A2.

- : append-eq eq/ref eq/ref eq/ref A A.

%worlds () (append-eq _ _ _ _ _).
%total {} (append-eq _ _ _ _ _).

Units

We need to prove that nil is the right and left unit of the semigroup . The later is by axiom and the former is by this lemma.

append-eq-nil : {L1} append L1 nil L1 -> type.
%mode append-eq-nil +L -A.

- : append-eq-nil nil append/nil.
- : append-eq-nil (cons E L) (append/cons A) 
     <- append-eq-nil L A.

%worlds () (append-eq-nil _ _).
%total D (append-eq-nil D _).

Sometimes it is helpful to reason with equalities like .

append-eq-nil : append L1 nil L2 -> eq L1 L2 -> type.
%mode append-eq-nil +A -E.

- : append-eq-nil append/nil eq/ref.
- : append-eq-nil (append/cons A) E
     <- append-eq-nil A E1
     <- eq-cong-cons _ E1 E.
%worlds () (append-eq-nil _ _).
%total D (append-eq-nil D _).

Determinism

As with reverse we need to show that append is indeed a function .

append-determ : append L1 L2 L3 -> append L1 L2 L4 -> eq L3 L4 -> type.
%mode append-determ +A1 +A2 -E.

- : append-determ append/nil append/nil eq/ref.
- : append-determ (append/cons A1) (append/cons A2) E
       <- append-determ A1 A2 E2
       <- eq-cong-cons _ E2 E.

%worlds () (append-determ _ _ _).
%total D (append-determ D _ _).

Associativity

We need to prove that append is associative .

append-assoc1 : append L1 L2 L3 -> append L3 L4 L5 -> append L2 L4 L6 -> append L1 L6 L5 -> type.
%mode append-assoc1 +A1 +A2 -A3 -A4.

- : append-assoc1 append/nil A1 A1 append/nil.
- : append-assoc1 (append/cons A1) (append/cons A2) A3 (append/cons A4)
      <- append-assoc1 A1 A2 A3 A4.

%worlds () (append-assoc1 _ _ _ _).
%total D (append-assoc1 D _ _ _).

append-assoc2 : append L1 L2 L3 -> append L3 L4 L5 -> append L2 L4 L6 -> append L1 L6 L7 -> eq L5 L7 -> type.
%mode append-assoc2 +A1 +A2 +A3 +A4 -E.

- : append-assoc2 A1 A2 A3 A4 E
      <- append-assoc1 A1 A2 A3' A4'
      <- append-determ A3 A3' E3
      <- append-eq eq/ref E3 eq/ref A4 A4''
      <- append-determ A4' A4'' E.

%worlds () (append-assoc2 _ _ _ _ _).
%total {} (append-assoc2 _ _ _ _ _).

Append and reversal

I promissed to prove that rev is an isomorphism. Lets start by a few lemmas. First .

append-rev1 : append L1 L2 L3 -> rev L1 L4 L5 -> rev L2 L5 L6 -> rev L3 L4 L6 -> type.
%mode append-rev1 +A +R1 +R2 -R3.

- : append-rev1 append/nil rev/nil R R.
- : append-rev1 (append/cons A) (rev/cons R1) R3 (rev/cons R2) 
 <- append-rev1 A R1 R3 R2.

%worlds () (append-rev1 _ _ _ _).
%total D (append-rev1 D _ _ _).

And second . If we let then we get , which shows how we can think of as .

append-rev2 : rev L1 L2 L3 -> append L2 L4 L5 -> append L3 L4 L6 -> rev L1 L5 L6 -> type.
%mode append-rev2 +R +A +A' -R'.

- : append-rev2 rev/nil A1 A2 R
  <- append-determ A1 A2 E
  <- rev-eq eq/ref eq/ref E rev/nil R.

- : append-rev2 (rev/cons R) A1 A2 (rev/cons R2)
  <- append-rev2 R (append/cons A1) A2 R2.

%worlds () (append-rev2 _ _ _ _).
%total D (append-rev2 D _ _ _).

And here we go. which boils down to , whence reverse is a homeomorphism. This combined with the fact that reverse is its own inverse we get that reverse is an isomorphism.

append-rev : rev L1 L2 L3 -> rev LA LB LC -> append LC L3 LT -> rev L2 L1 L3' -> 
             rev LB LA LC' -> append L3' LC' LT' -> rev LT' nil LT -> type.
%mode append-rev +R1 +R2 +A1 +R3 +R4 +A2 -R3.

- : append-rev R1 (rev/cons R2) A1 R3 R4 A2 R5
    <- append-rev R1 R2 A1 R3 (rev/cons R4) A2 R5.

- : append-rev (rev/cons R1) rev/nil A1 R2 R3 A2 R5
    <- append-rev R1 rev/nil A1 (rev/cons R2) R3 A2 R5.

- : append-rev rev/nil rev/nil A1 R3 R4 A2 R5
  <- append-rev2 R3 append/nil A2 RC
  <- append-rev1 A1 R4 RC RB 
  <- revrev-id RB R5.

%worlds () (append-rev _ _ _ _ _ _ _).
%total [D E] (append-rev E D _ _ _ _ _).

See the Twelf code for this example - See Twelf's output


Read more Twelf case studies and other Twelf documentation.