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.

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.

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 !

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

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:

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

Application : operations on lists

The append function

We prove the following properties of l @ l'.

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

The map functional

We define :

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

Head and tail of a list as partial functions

Basic facts

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

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

Quantifiers bounded on lists.

Existence in a list

Introduction rules

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

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

Elimination rules

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

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

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

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

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.

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

Membership in a list

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

Introduction rules

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

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

Elimination rules

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

./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