Changes of Data Type in the Calculus of Inductive Constructions
Nicolas Magaud
INRIA Sophia-Antipolis
Abstract:
In a logical framework such as the calculus of inductive constructions,
the choice of a particular representation (as an inductive data-type)
to describe mathematical
concepts strongly influences the way operations on them are defined.
It also determines how proofs of properties involving these concepts are
carried out.
Switching from a concrete representation to another for the same mathematical
object requires redefining the operations and rebuilding the proofs of
properties of these operations. These transformations are tedious,
especially because of the lack of similarity between the ways proofs
are usually developed in the different settings.
We study methods making it possible to reuse proofs when we change
the concrete representation of data.
We propose a partially automatized method to structurally translate
proof terms using one representation d of a data-type D to proof
terms using another representation d'.
Performing such a transformation requires a new induction principle
on the target concrete data-type in order to keep the proof structure.
We sketch the translation algorithm.
We consider a proof p of a statement T using d as a concrete
representation for D.
- we make explicit the reduction steps involving iota-conversion in p;
- we abstract p and T into a proof p' of T' for an abstract data-type
for D;
- we instantiate this abstraction on a new concrete representation, e.g. d',
of D.
The last step requires equations stating that translations
of two iota-convertible terms in the initial representation
d are equal (even if not convertible any more) in
the new representation d'.
The method we propose here is still being investigated. A prototype has
been implemented in the Coq system and has been successfully applied
to the translation of some theorems and their proofs from Peano arithmetic
to binary arithmetic.
Back to schedule.
Marieke Huisman
Last modified: Mon Apr 23 16:58:50 MEST 2001