OOP
Let's see another interface, the one of finite types
Sub types
A sub type extends another type by adding a property.
The new type has a richer theory.
The new type inherits the original theory.
Let's define the type of homogeneous tuples
We instrument Coq to automatically promote
sequences to tuples.
Reamrk how t is a tuple, then it becomes a list by going
trough rev and map, and is finally promoted
back to a tuple
by this Canonical magic.
Now we the tuple type to form an eqType,
exactly as seq does.
Which is the expected comparison for tuples?
Given that propositions are expressed (whenever possible)
as booleans we can systematically prove that proofs
of these properties are irrelevant.
As a consequence we can form subtypes and systematically
prove that the projection to the supertype is injective,
that means we can craft an eqType.
Tuples is are part of the library, that also contains
many other promotions
Tuples is not the only subtype part of the library.
Another one is 'I_n, the finite type of natural
numbers smaller than n.
It is easy to combine these bricks by subtyping (and specialization
)
Sum up
- subtypes add properties and inherit the theory of the supertype
thanks to boolean predicates (UIP).
In some cases the property can be inferred by Coq, letting one apply
a lemma about the subtype on terms of the supertype.