Pattern and Copattern matching
The induction principle for algebraic data types is in automated theorem
proving tools often represented by termination checked pattern matching,
i.e. possibly iterated case distinctions on the choice of constructors for
an element of this data type. The dual of induction is coinduction, which
is an introduction rule. It can be represented by its dual copattern
matching, which means by determing the result of applying the destructors
to this element.
We will introduce the theory of nested pattern and copattern matching
(joint work with Andreas Abel, Brigitte Pientka and David Thibodeau).
We will discuss how nested pattern and copattern matching can be reduced,
at least in case it should pass a strict termination checker, to primitive
induction and coinduction.
We will present as well a little theorem, which restricts what can be achieved
in intensional type theory regarding decidable type checking. Even assuming
that streams are equal if their heads and tails are equal forces an equality
on streams to be undecidable.