listLib.FOLDR

STRUCTURE

SYNOPSIS

Computes by inference the result of applying a function to the elements of a list.

DESCRIPTION

FOLDR_CONV takes a conversion conv and a term tm in the following form:

   FOLDR f e [x0;...xn]

It returns the theorem

   |- FOLDR f e [x0;...xn] = tm'

where tm' is the result of applying the function f iteratively to the successive elements of the list and the result of the previous application starting from the tail end of the list. During each iteration, an expression f xi ei is evaluated. The user supplied conversion conv is used to derive a theorem

   |- f xi ei = e(i+1)

which is used in the next iteration.

FAILURE

FOLDR_CONV conv tm fails if tm is not of the form described above.

EXAMPLE

To sum the elements of a list, one can use FOLDR_CONV with ADD_CONV from the library num_lib.

   - load_library_in_place num_lib;
   - FOLDR_CONV Num_lib.ADD_CONV (--`FOLDR $+ 0 [0;1;2;3]`--);
   |- FOLDR $+ 0[0;1;2;3] = 6

In general, if the function f is an explicit lambda abstraction (\x x'. t[x,x']), the conversion should be in the form

   ((RATOR_CONV BETA_CONV) THENC BETA_CONV THENC conv'))

where conv' applied to t[x,x'] returns the theorem

   |-t[x,x'] = e''.

SEEALSO

FOLDL_CONV, list_FOLD_CONV