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 aflz 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 aflz 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 af 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
)
We prove the following properties of l @ l'.
append.total.List added as introduction rule (abbrev: append
, options: -i -t
)
append.rnil.List added as equation
append.associative.List added as equation
We define :
map.nil.List added as equation
map.cons.List added as equation
map.total.List added as introduction rule (abbrev: map
, options: -i -t
)
map.append.List added as equation
head.cons.List added as equation
tail.cons.List added as equation
head.total.List added as introduction rule (abbrev: head
, options: -t
)
tail.total.List added as introduction rule (abbrev: tail
, options: -i -t
)
cons_head_tail.List added as equation
Exists.lcons.List added as introduction rule (abbrev: Exists.lcons
, options: )
Exists.rcons.List added as introduction rule (abbrev: Exists.rcons
, options: )
Exists.nil.List added as elimination rule (abbrev: Exists.nil
, options: )
Exists.elim_cons.List added as elimination rule (abbrev: Exists_cons
, options: )
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 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 DforallD [].
It is also the case of the following facts.
List_increasing added as elimination rule (abbrev: inc
, options: -t
)
All facts are trivially derived as particular cases of analogous ones with Exists .
Mem.lcons.List added as introduction rule (abbrev: Mem.lcons
, options: )
Mem.rcons.List added as introduction rule (abbrev: Mem.rcons
, options: )
Mem.nil.List added as elimination rule (abbrev: Mem.nil
, options: )
Mem.elim_cons.List added as elimination rule (abbrev: Mem_cons
, options: )
./list_nat.tex ./list_nat_ax.tex
QuotientChristophe RaffalliParis VII & Paris XII university