Difference between revisions of "Datatype Rules"
imported>Nicolas m (corrected typos) |
imported>Nicolas m (applying DC to directions) |
||
Line 48: | Line 48: | ||
=== Application to directions === | === Application to directions === | ||
− | |||
− | + | Starting from goal | |
+ | <math>\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y</math> | ||
+ | |||
+ | we can free variables x,y,d then apply Distinct Case: | ||
+ | |||
+ | | | ||
+ | | south | ||
+ | | west | ||
+ | The resulting sequent is | ||
+ | <math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=east \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=south \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=west \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math> | ||
+ | |||
+ | further simplifications depend on the existence of rules about move and the various directions. | ||
=== Application to lists === | === Application to lists === | ||
Line 64: | Line 74: | ||
{{TODO}} | {{TODO}} | ||
+ | !l,v,r. t = node(l,v,r) => height(l) < height(t) | ||
== Induction == | == Induction == | ||
{{TODO}} | {{TODO}} |
Revision as of 16:46, 6 September 2010
Datatype rules may seem a bit difficult to understand at first sight. Here are a few examples intended to make them clearer.
Contents
Datatypes used
The rules will be applied to the following datatypes:
Directions:
direction ::= north | east | south | west
Let us have a function
first two arguments are a start position, third is a direction, result is the end position.
Lists:
list(T) ::= nil | cons( head : T, tail : list(T) )
Let us have a predicate
meaning that the first argument is a member of the list.
Trees:
tree(T) ::= empty | node( left : tree(T), value : T, right : tree(T) )
Let us have a function
defining the height of a tree
Distinct Case
The rule states
Application to directions
Starting from goal
we can free variables x,y,d then apply Distinct Case:
| | south | west
The resulting sequent is
further simplifications depend on the existence of rules about move and the various directions.
Application to lists
TODO
!l oftype list(\Z). #x. member(x,l) & (!y. member(y,l) => y <= x)
evidence that nil list has been forgotten in the predicate
Application to trees
TODO
!l,v,r. t = node(l,v,r) => height(l) < height(t)
Induction
TODO