The Coq mailing list

["Chung Kil Hur" <ckh25 AT cam.ac.uk>]

Dear coq-users,

 

I have developed a library, called Heq, to support reasoning about heterogeneous equality.

 

It is available at
 
     http://www.pps.jussieu.fr/~gil/Heq/

 

It includes a detailed tutorial. Please have a look.

 

If you have any questions or comments, please don't hasitate to contact me at ( gil AT pps DOT jussieu DOT fr ).

 

 

--------------

 

Heq is a library supporting

 

- rewriting for heterogeneous equality; and
- manipulation of casts.

 

We take equality of dependent pairs as a notion of heterogeneous
equality, which is equivalent to eq_dep but has some advantages over
it.

 

Heq library only assumes Streicher's Axiom K, which is planned to be
interalized in a later version of Coq.

 

The goal of Heq is to make as little as possible the overhead of
reasoning about heterogeneous equality. The slogan is

 

- reasoning about heterogeneous equality as if it is a leibniz equality.

 

As an example, we turned the Coq standard library for List (about 2000
lines) into a library for Vector in a few hours without understanding
the proofs, \ie, by chaning the syntax and adding some extra tactics
to manipulate casts (this overhead is almost zero). Indeed, the
definitions, functions and proof structures of List and Vector are
almost identical.

 

We also turned the Hugo Herbelin's merge sort of List and its
correctness into a merge sort of Vector and its correctness in the
same way. (The proof scripts are almost identical.)

 

We also supports deeply dependent types, like heterogeneous vector
'vectorH' of type

 

vectorH : forall (U:Type) (P:U -> Type) (n : nat), vector U n -> Type

 

In the tutorial, we will see how to reason about vectors, matrices,
heterogeneous vectors and matrices using Heq.

 

Note: we also simplified the strongly-typed formalization of system F [1]
using the Heq library, and formalized the proof of strong
normalization of system F given in the book 'proofs and types' [2].

 

[1] Nick Benton, Chung-Kil Hur, Andrew Kennedy and Conor McBride.
    Strongly typed term representations in Coq. Submitted, 2009.

 

[2] Jean Y. Girard, Paul Taylor, Yves Lafont.
    Proofs and Types. Cambridge University Press, 1989.

 

Note: we have developed a complete, simple and fast algorithm (tactic)
to find dependent occurrences of a term C in a term T, which plays a
key role in this work.

 

Note: if we assume the injectivity of inductive type constructors, we
can use JMeq instead of Heq, but we have shown that in general it is
inconsistent with the law of excluded middle, or the existence of
impredicative type like Prop (see Agda and Coq-Club mailing list).

 

Acknowledgement: we are very grateful to Hugo Herbelin for many useful
discussions.

 

----------------

 

 

Thanks,

 

Chung-Kil Hur
Laboratoire Preuves Programmes Systemes
CNRS & Universite Paris Diderot