Next: Basic definitions Up: User's manual of the Previous: Basic definitions and properties Contents

Subsections

Defining functions by induction on lists

Definition

In order to introduce definition of functions by structural induction on list we will use the operator of definite description. We then first introduce the following predicate.

The predicate DEF_I L^rec a f l z defines a function which maps the list l to z using structural induction on the list l with a as base case (when l = []) and f for the cons case.

$\begin{definition}[ definition by induction on lists : predicate version ]~ \beg... ...b}śdef_rec_P.List a f l zś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Note: you should remark the use of x to use lists of *anything* !

We prove then that DEF_I L^rec a f l z effectively defines a function.

The main theorem about untyped list is the following.

$\begin{fact}[% \afdmath{}\text{\rm True}.\text{\rm List}\endafdmath{}]Untyped li... ....2em}{2.em} \text{\it l}\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

True.List added as introduction rule (abbrev: True , options: -o 1.0 )

We add it as an introduction rule.

Using the definite description, we can now define an operator def_I L^rec that introduces a function symbol def_I L^rec a f for any definition by induction on lists !

$\begin{definition}[ definition by induction on list ]~ \begin{center}% \afdmath{... ...{Verb}śdef_rec.List a f lś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Using the properties of the definite description, we can prove the following.

$\begin{fact}[ Characteristic properties of definitions by induction ]\hspace{1cm... ...ons}.\text{\rm List}\endafdmath{} added as equation \par \end{itemize}\end{fact}$

These theorems are added as rewriting rules and then the definition of def_I L^rec is closed

We can now prove the totality of any definition by induction:

$\begin{fact}[% \afdmath{}\text{\rm def}\_\text{\rm rec}.\text{\rm total}.\text{\... ...em} \text{\it l}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

def_rec.total.List added as introduction rule (abbrev: def_rec , options: -t )

Application : operations on lists

The append function

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\it l}\hspace{0.29em}\math... ...{} \SaveVerb{Verb}śl @ l'ś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

We prove the following properties of l @ l'.

$\begin{fact}[ Characteristic properties of % \afdmath{}\mathbin{@}\endafdmath{}]... ...ons}.\text{\rm List}\endafdmath{} added as equation \par \end{itemize}\end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm append}.\text{\rm total}.\text{\rm List}\enda... ...m} \text{\it l}'\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

append.total.List added as introduction rule (abbrev: append , options: -i -t )

$\begin{fact}[% \afdmath{}\text{\rm append}.\text{\rm rnil}.\text{\rm List}\endaf... ...3em}{2.em} \text{\it l}\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

append.rnil.List added as equation

$\begin{fact}[% \afdmath{}\text{\rm append}.\text{\rm associative}.\text{\rm List... ...xt{\it z}\endprettybox{}\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

append.associative.List added as equation

The map functional

We define :
$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm map}\hspace{0.2em} \te... ...} \SaveVerb{Verb}śmap f lś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{fact}[ Characteristics properties of % \afdmath{}\text{\rm map}\endafdmat... ...ybox{}\endprettybox{}\endprettybox{}\endafdmmath{}} \par \end{itemize}\end{fact}$

map.nil.List added as equation

map.cons.List added as equation

$\begin{fact}[% \afdmath{}\text{\rm map}.\text{\rm total}.\text{\rm List}\endafdm... ...em} \text{\it l}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

map.total.List added as introduction rule (abbrev: map , options: -i -t )

$\begin{fact}[% \afdmath{}\text{\rm map}.\text{\rm append}.\text{\rm List}\endafd... ...ettybox{}\endprettybox{}\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

map.append.List added as equation

Head and tail of a list as partial functions

Definitions

$\begin{definition}[ graph of head ]~ \begin{center}% \afdmath{}\text{\rm headP}\... ...\SaveVerb{Verb}śheadP l aś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{definition}[ graph of tail ]~ \begin{center}% \afdmath{}\text{\rm tailP}\... ...SaveVerb{Verb}śtailP l l'ś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{definition}[ head ]~ \begin{center}% \afdmath{}\text{\rm head}\hspace{0.2... ...{} \SaveVerb{Verb}śhead lś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{definition}[ tail ]~ \begin{center}% \afdmath{}\text{\rm tail}\hspace{0.2... ...{} \SaveVerb{Verb}śtail lś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Basic facts

$\begin{fact}[% \afdmath{}\text{\rm head}.\text{\rm cons}.\text{\rm List}\endafdm... ...3em}{2.em} \text{\it a}\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

head.cons.List added as equation

$\begin{fact}[% \afdmath{}\text{\rm tail}.\text{\rm cons}.\text{\rm List}\endafdm... ...3em}{2.em} \text{\it l}\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

tail.cons.List added as equation

$\begin{fact}[% \afdmath{}\text{\rm head}.\text{\rm total}.\text{\rm List}\endafd... ...ext{\it l}\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm tail}.\text{\rm total}.\text{\rm List}\endafd... ...ext{\it l}\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

head.total.List added as introduction rule (abbrev: head , options: -t )

tail.total.List added as introduction rule (abbrev: tail , options: -i -t )

$\begin{fact}[% \afdmath{}\text{\rm cons}\_\text{\rm head}\_\text{\rm tail}.\text... ...em} \text{\it l}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

cons_head_tail.List added as equation

Quantifiers bounded on lists.

Existence in a list

Definition

$\begin{definition}[ there exists x:D in l ]~ \begin{center}% \afdmath{}\text{\rm... ...SaveVerb{Verb}śExists D lś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Introduction rules

$\begin{fact}[% \afdmath{}\text{\rm Exists}.\text{\rm lcons}.\text{\rm List}\enda... ...ext{\it l}\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm Exists}.\text{\rm rcons}.\text{\rm List}\enda... ...;\; \text{\it l}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

Exists.lcons.List added as introduction rule (abbrev: Exists.lcons , options: )

Exists.rcons.List added as introduction rule (abbrev: Exists.rcons , options: )

Elimination rules

$\begin{fact}[% \afdmath{}\text{\rm Exists}.\text{\rm nil}.\text{\rm List}\endafd... ...{0.2em}{2.em} []\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm Exists}.\text{\rm elim}\_\text{\rm cons}.\tex... ...em} \text{\it l}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

Exists.nil.List added as elimination rule (abbrev: Exists.nil , options: )

Exists.elim_cons.List added as elimination rule (abbrev: Exists_cons , options: )

Existence in append

$\begin{fact}[% \afdmath{}\text{\rm Exists}.\text{\rm lappend}.\text{\rm List}\en... ...xt{\it l}'\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm Exists}.\text{\rm rappend}.\text{\rm List}\en... ...m} \text{\it l}'\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

Exists.lappend.List added as introduction rule (abbrev: Exists.lappend , options: )

Exists.rappend.List added as introduction rule (abbrev: Exists.rappend , options: )

$\begin{fact}[% \afdmath{}\text{\rm Exists}.\text{\rm elim}\_\text{\rm append}.\t... ...m} \text{\it l}'\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

Exists.elim_append.List added as elimination rule (abbrev: Exists.elim_append , options: )

Universal quantifer bounded on a list

Universal closure of the predicate D on the list l is exactly List D l

$\begin{definition}[ Forall x such that D in l ]~ \begin{center}% \afdmath{}\text... ...{} \SaveVerb{Verb}śForallś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Results on list can then be reinterpreted, for instance D I L_ D [] is D forall D [].

It is also the case of the following facts.

$\begin{fact}[% \afdmath{}\text{\rm List}\_\text{\rm increasing}\endafdmath{}]int... ...l}\endprettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

List_increasing added as elimination rule (abbrev: inc , options: -t )

$\begin{fact}[% \afdmath{}\text{\rm List}\_\text{\rm conjunction}\endafdmath{}]li... ...em} \text{\it l}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

Membership in a list

All facts are trivially derived as particular cases of analogous ones with Exists .

Introduction rules

$\begin{definition}[ membership in list ]~ \begin{center}% \afdmath{}\text{\rm Me... ...} \SaveVerb{Verb}śMem x lś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{fact}[% \afdmath{}\text{\rm Mem}.\text{\rm lcons}.\text{\rm List}\endafdm... ...;\; \text{\it l}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm Mem}.\text{\rm rcons}.\text{\rm List}\endafdm... ...;\; \text{\it l}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

Mem.lcons.List added as introduction rule (abbrev: Mem.lcons , options: )

Mem.rcons.List added as introduction rule (abbrev: Mem.rcons , options: )

Elimination rules

$\begin{fact}[% \afdmath{}\text{\rm Mem}.\text{\rm nil}.\text{\rm List}\endafdmat... ...{0.2em}{2.em} []\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm Mem}.\text{\rm elim}\_\text{\rm cons}.\text{\... ...em} \text{\it l}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

Mem.nil.List added as elimination rule (abbrev: Mem.nil , options: )

Mem.elim_cons.List added as elimination rule (abbrev: Mem_cons , options: )

Membership in append

$\begin{fact}[% \afdmath{}\text{\rm Mem}.\text{\rm lappend}.\text{\rm List}\endaf... ...xt{\it l}'\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm Mem}.\text{\rm rappend}.\text{\rm List}\endaf... ...m} \text{\it l}'\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm Mem}.\text{\rm elim}\_\text{\rm append}.\text... ...m} \text{\it l}'\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

./list_nat.tex ./list_nat_ax.tex

QuotientChristophe RaffalliParis VII & Paris XII university

Next: Basic definitions Up: User's manual of the Previous: Basic definitions and properties Contents

Christophe Raffalli 2005-03-02