Changing Data Representation in Type Theory

Downloading the tool, getting it up and running

• The prototype consists in some Ocaml files to be linked with Coq existing code in order to build a new toplevel.
  It can be downloaded here: CDR.tar.gz (version compatible with coq-8.0pl2 and coq-8.0pl3).

• Compiling and generating a new toplevel (mytop.out)
  • untar CDR.tar.gz (tar -zxvf CDR.tar.gz)
  • go into the new directory CDR and run make init COQTOP=<YOUR_COQ_DIR>
  • You can then run the new toplevel ./mytop.out or compile a .v file with it, e.g. coqc -image ./mytop. out example.v

New Coq commands (immediately available in the new toplevel mytop.out)

• AddIso t1 t2. 

  Adds an entry connecting t1 to t2 in the translation table.

• CheckIso t. 

  Shows the name associated to t in the translation table if such an entry exists.

• ShowIso.

  Prints all entries in the translation table.

• Translate t.

  Removes case analysis constructs (see RemoveCases below), makes explicit all computational (implicit) steps in the proof term denoted by t and then translates the resulting term using the translation table. The new term name can be specified using Translate t1 into t2. By default, the new name is t'.

• RemoveCases t. (debugging tool)

  Analyses the term denoted by t and replaces all occurences of match ... with by the application of the appropriate recursion operator. It does not define a new constant for this term but simply prints it out.

A Basic Example (example.v)

Parameter NAT:Set.
Parameter ZERO:NAT.
Parameter SUCC:NAT->NAT.

AddIso nat NAT.
AddIso O ZERO.
AddIso S SUCC.
Parameter INDUCTION:
  forall P:NAT->Prop,
    (P ZERO) -> (forall n:NAT, P n ->P (SUCC n)) -> forall n:NAT, P n.

AddIso nat_ind INDUCTION.

Parameter PLUS: NAT -> NAT -> NAT.

Axiom PLUS_1 : forall n:NAT, (PLUS ZERO n)=n.
Axiom PLUS_2 : forall n m:NAT, (PLUS (SUCC n) m)=(SUCC (PLUS n m)).

AddIso plus PLUS.
Hint Rewrite PLUS_1 : simplification.
Hint Rewrite PLUS_2 : simplification. 

Translate plus_n_O into PLUS_n_O.
(* translates a proof plus_n_O that forall n:nat, plus n O=n *)
(* into a proof PLUS_n_O that forall n:NAT, (PLUS n ZERO)=n  *)

Case studies

• Coq Arith library: from nat to bin (from unary to binary representation of positive integers)
• Coq Arith library: from nat to {x:Z|0<=x}
• Coq Lists library: cons lists to snoc lists
• Changing functions representation (recursive, tail-recursive and cps) and updating proofs accordingly

Bug reports, comments

Related papers

• Nicolas Magaud. Changing Data Representation within the Coq System. In David A. Basin and Burkhart Wolff, editors, TPHOLs'2003, volume 2758. LNCS, Springer-Verlag, 2003. © Springer-Verlag.

• Nicolas Magaud and Yves Bertot. Changing data structures in type theory:a study of natural numbers. In Paul Callaghan, Zhaohui Luo, James McKinna, and Randy Pollack, editors, TYPES'2000, volume 2277. LNCS, Springer-Verlag, 2000. © Springer-Verlag.