List Definitions

The basic file contains the definition of list and the usual elimination, reduction, iteration and double elimination rules plus the characterisation theorems.

Older versions of the library have the element type parameter explicit throughout, but with the cons constructor named cons1, and cons with implicit parameter defined subsequently. The use of conditional visibility enables the desired effect to be achieved directly, so that the parameter is explicit for list and nil, but implicit for cons and list_elim. cons1 is defined in attempt to alleviate some backwards compatibility problems, however, the change in parameter visibility for list_elim may necessitate some small adjustments in proof scripts.

 ** Module lib_list Imports lib_eq_basics
 $list : (Type)->Type(list)
 $nil : {t:Type}list t
 $cons : {t|Type}t->(list t)->list t
 $list_elim :
    {t|Type}{C_list:(list t)->Type}(C_list (nil t))->
    ({x1:t}{x2:list t}(C_list x2)->C_list (cons x1 x2))->{z:list t}
    C_list z
 ** Label (!list!) list
 ** Label (!list elim!) list_elim
 ** Label (!list nil!) nil
 ** Label (!list cons!) cons
[[t|Type][C_list:(list t)->Type][f_nil:C_list (nil t)]
 [f_cons:{x1:t}{x2:list t}(C_list x2)->C_list (cons x1 x2)][x1:t]
 [x2:list t]
    list_elim C_list f_nil f_cons (nil t)  ==>  f_nil
 || list_elim C_list f_nil f_cons (cons x1 x2)  ==>
    f_cons x1 x2 (list_elim C_list f_nil f_cons x2)]

  cons1 = ... : {t:Type}t->(list t)->list t
  list_rec = ... : {s|Type}{t|Type}t->(s->(list s)->t->t)->(list s)->t
  list_iter = ... : {s|Type}{t|Type}t->(s->t->t)->(list s)->t
  list_ind = ... :
    {s|Type}{P:(list s)->Prop}(P (nil s))->
    ({x:s}{l:list s}(P l)->P (cons x l))->{l:list s}P l
  list_double_elim = ... :
    {s|Type}{T:(list s)->(list s)->Type}(T (nil s) (nil s))->
    ({x:s}{l:list s}(T (nil s) l)->T (nil s) (cons x l))->
    ({x:s}{l:list s}({l':list s}T l l')->T (cons x l) (nil s))->
    ({x:s}{l:list s}({l':list s}T l l')->{y:s}{l':list s}
     (T (cons x l) l')->T (cons x l) (cons y l'))->{l,l':list s}T l l'
  is_nil = ... : {t|Type}(list t)->Prop
  is_cons = ... : {t|Type}(list t)->Prop
  nil_or_cons = ... : {t|Type}{l:list t}(is_nil l \/ is_cons l)
  nil_not_cons = ... :
    {t|Type}{l:list t}{x:t}not (Eq (nil t) (cons x l))