The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

Let me seize the opportunity of this question to survey some aspects
of the question of extensional equality in Coq.

> Suppose one wanted to define isomorphisms in the following slightly
> unusual fashion:
> 
>    Inductive Dir : Set := R | L.
>    Definition swap (d:Dir) := match d with R => L | L => R end.
>    
>    Module Type Iso.
>      Parameter S : Dir -> Set.
>      Parameter f : forall d, S d -> S (swap d).
>      Axiom isoAx : forall d x, f (swap d) (f d x) = x.
>    End Iso.
>    
> (...)
> 
> Unfortunately, this definition doesn't typecheck: the term
> 
>     f (swap d) (f d x)
>     
> has type S (swap (swap d)), not S d, which is the type of x.  Of
> course, swap (swap d) is provably equal to d for every d, but not
> convertible. 
> 
> What to do?  We've seen the discussion of John Major equality in
> CoqArt... is this our only hope, or is there a lighter way?

The Calculus of Inductive Constructions (CIC) definitely lacks some
"kind of support" for extensional equality so that dependent types get
useful in any situations. What can we do?

Relying on the ongoing research works around, I see basically two
possible research directions for supporting some form of extensional
equality in Coq.

* The explicit approach typically relies on Nicolas Oury's PhD
results. It says that any derivation that implicitly uses extensional
equalities (such as "swap (swap d) = d") for typing can be turned into
a derivation of the same judgment up to the insertion of explicit type
casts made from "eq_rect". In the present case, this would give:

Axiom isoAx : forall d x, {f d (f d x)}_(swap_involutive d) = x.

where "swap_involutive" proves "forall d, swap (swap d) = d" and 
"{p}_(H)" is a notation for "eq_rect _ _ p _ H".

Nicolas Oury showed that we need to extend the Calculus of
Constructions (CC) with (only) a few simple axioms (JMeq_eq +
congruence properties of JMeq if I'm correct) to be able to simulate
the extension of CC that uses extensional equalities in typing. I make
the assumption that the result can be extended to CIC.

The main problems with this approach are:
- how to transparently manage the type casts without having the user
  to have to see them and have his hands get dirty?
- the type casts a priori block the computations.

In Oury's system, the congruence properties of JMeq (which means, if I
understand correctly, that "eq_rect" commutes with the constructors of
CC/CIC) allows to release the blocked redexes and to make the
computations progress. We cannot freely allow all commutations of
"eq_rect" since otherwise we may loop (under the assumption that bool
= bool->bool, one may for instance build a fixpoint with a blocked
redexes and the computation will loop if we are allowed to
unrestrictedly lift the blocking type cast out).

To address this problem, an approach could be to restrict free
commutation of the type casts to those equations that are true (and
thus compatible with normalization) in one of the "standard"
normalization models. A simple criterion for being true, and hence for
safely lifting the type casts in computations, just seems to have an
axiom-free proof. In that way, one would cover most of the interesting
cases starting from "swap_involutive" above and continuing e.g. with
the standard arithmetical equational properties.

The only modification to the Coq core type-checker would be the
introduction of a subclass of "computationally transparent"
"eq_rect"-style type casts and an procedure to make them commute
during evaluation (or to simply remove them entirely during conversion). 
All the concrete job of inserting type casts would then be delegated
to the type inference, hopefully in a mostly automatized way. E.g., a
smart enough type inference algorithm would be able to automatically
interpret "f d (f d x) = x" as "{f d (f d x)}_(swap_involutive d) = x"
as soon as "swap_involutive" has for instance being proved beforehand
in the context. Of course, this would require the type inference
algorithm to incorporate new strategies for deciding true equalities,
e.g. by making it rely on decision procedures known currently only at
the tactic level.

* The implicit approach aims at natively integrating larger and larger
subsets of decidable equational theories in the Coq kernel (since
type-checking in the full extensional theory is undecidable, see
e.g. NuPrl).

Typical examples of such theories are:
- the equational part of Presburger's arithmetic, as studied by
  Pierre-Yves Strub in his PhD thesis,
- extensionality (eta) on finite types (as cited in muad's mail),
- the first-order theory of constructors (as used in Agda for typing
  pattern-matching),
- variants of Blanqui-Jouannaud-Okada's Calculus of Algebraic
  Constructions (CAC) which, under some conditions of compatibility
  with the beta conversion, natively supports a large set of
  equational theories expressible as a confluent and (provably)
  terminating set of rewrite rules.

Talking about Presburger, an experiment is on the way by Pierre-Yves
Strub who is hard-wiring a certified Presburger decision procedure in
a prototype version of Coq. Somehow, one heads here for some
convergence of proof checkers and certified model checking, what is
exciting. On the other side, an issue often raised is whether the
trust in the kernel type-checker is weakened or not by doing so.

So as to be as generic as possible, one could also imagine the kernel
being able to dynamically use decision procedures that would have
themselves been certified in Coq (by reflection) but this then poses
the question of how to smoothly combine such decision procedures. For
instance, can we show that if the decision procedures are on different
domains (like nat and bool), they will provably be mixable?

Another possible approach is to marry the CIC and the CAC and to
extend the Coq kernel with techniques from rewriting theory so that it
is able to verify the soundness and effective usability (preservation
of termination) of the equations with which the type-checker is
dynamically extended. An experiment was started on this topic a few
years ago but for logistic reasons, it had to be stopped.

Extensionality in finite types is interesting (even if I don't see how
it could scale to arithmetic) and may actually be quite easy to
implement.  This goes in the same direction as our objective to
eventually support eta-conversion (in Pi-types) on top of the
CIC.


All this does not preclude also investigating the CIC extended with
commutative cuts ("match-associativity"). The general case (with
dependencies and fixpoints) is difficult, if not impossible, but
supporting commutative cuts in the non dependent case should be
studied more thoroughly (notwithstanding the risk of size explosion
due the duplication of pieces of context over "match"s on more than
one constructors). Even in the simple cases of tuples, it may happen
to be quite useful (consider e.g. "fst (let (y,z) := x in (z,y))" that
would become convertible to "snd" with commutative cuts).

Hugo