[isabelle-dev] Typing problem in autogenerated axiom

[Dominique Unruh]

Dear all.

> It looks like you only replied to me. ^^

Indeed. But since your mail contains a complete quote of mine
(thanks), I will not repost my mail here. This time, I think, I am
more successful.

> Let me put this into perspective, in the light of a forthcoming kernel
> extension/modification:
>  in this kernel patch, all sort constaints and type class reasoning steps
> are eliminated in proofterms on theorem boundaries, and strip_sorted
> variants of the axioms are asserted on the proofterm side. So what remains
> is a proof which sort and typeclass reasoning internalized into the logic.

Just to make sure I understand this correctly: The proof term that is
stored with a theorem will contain no nonempty sorts at all (not even
in intermediate proof steps)?

Can you give me a very rough estimate for when this patch is planned
(like in a few days, months, years, decades, eras, ...)? It probably
does not make sense if I try embedding type classes into Coq before
this patch, because my embedding would have to change considerably
after the patch, anyway.


> From my POV this is needed to translate HOL into logics not involving
> Isabelle-style type classes.

Actually, I am not completely sure. I think it depends. The advantage
of having internalized type classes is, of course, that one does not
need to translate type classes at all (since they do not really exist
in the logic). The advantage of having explicit type classes in the
proof terms is the following: When translating internalized type
classes, the way how type classes are represented in the target logic
is fixed by the way how type classes are internalized in Isabelle. If
the type classes are explicit, on the other hand, one can choose the
encoding in the target logic that feels more natural in the target
logic.


> BTW: I would like to hear about your experiences translating HOL->Coq. How
> are you handling type class reasoning and overloading (I prefix an
> unoverloading step) in your HOL->Coq translation?

(The following is very preliminary!)

The basic translation is simple since an Isabelle proof term is
(almost) a valid Coq proof term.
If we just assert any axiom we find in the proof term as an axiom in
Coq, we are essentially done. (The only problem is that Isabelle
treats eta-convertible terms as equal while Coq doesn't, and that
Isabelle proof terms may contain free variables (which implies that in
Pure all terms are inhabited) while Coq proof terms may not.)

This, however, is not satisfying, because axioms generated by
definitions, type definitions, type classes etc. should be translated
into a definition + a proof of the axiom in Coq.

For an unoverloaded definition, this is trivial, since the axiom tells
us what value the constant must have to be able prove the
definition-axiom.

Unrestricted overloading, can, I think, not be translated. Although we
might be able to make a definition like "Definition test {T} := if T =
int then 1 else if T = nat then 2"  (ignoring certain issues like that
"T=bool" is not of the right type for the if statement), this
definition is not usuable, because to show that on type T=nat, we have
test=2, we would have to show that "nat!=int" in Coq. And I think
there is no way to do this.

Disciplined overloading (i.e., where the overloaded only occurs in
combination with instance-declarations of type classes), however, can
be done. To see this, we have to understand how Coq handles type
classes:

The Coq logic itself does not have type classes. But type classes can
be expressed. For example, the type class "order" would be expressed
(roughly) as follows: We define the type "order T" as a type of pairs
(less_eq,less) with less_eq:T=>T=>bool and less:T=>T=>bool such that
less_eq and less satisfy the order-axioms. Then any proposition or
constant that contains a free type variable T of sort order would be
represented as a function taking two arguments T and S where T is the
type, and S is of type "order T" and that returns the corresponding
proposition or constant with the type and the functions less,less_eq
instantiated. Doing an instance proof (say nat :: order) corresponds
to finding an element X_nat of the type "order nat". When
instantiating a sorted type variable T with nat, one has to apply the
parametric lemma or constant to T and X_nat. Fortunately, all this
applying is hidden behind the scenes by Coq's mechanism for inferring
implicit arguments, one can use type classes in Coq in a way that
looks similar to the way we do it in Isabelle (the feature is,
however, still classified as "(extremely) experimental" in the Coq
reference manual). See also
http://coq.inria.fr/refman/Reference-Manual024.html.

When embedding a sorted Isabelle proposition into Coq, we add a type
argument T_a to the target proposition for each type variable 'a, and
an argument of type "cls T_a" for each type class cls of in the sort
of 'a. This encodes Isabelle type classes in Coq, and as a side effect
it solves the problem of disciplined overloading: Since all constants
that are fixed by type classes cls are actually just fields of the
record of type "cls T" that is given as argument to the proposition,
there is no need to globally specify two conflicting definitions.
Instead, we define less_eq differently in the instance X_nat and in
X_int. Since the proposition gets X_nat or X_int or whatever is
appropriate as argument, it always gets the appropriate definition of
less_eq.

However, for this approach to go through nicely, we need that less_eq
(in Isabelle) is of type 'a::ord=>'a::ord=>bool, not of
'a::{}=>'a::{}=>bool. Otherwise in the Isabelle proof term the
constant less_eq might occur in situations where 'a is instantiated
with a non-ord-type, and the above translation does not work because
there is no X_a giving us a definition for less_eq. (I think this can
be worked around by defining an auxiliary type class order_scheme
first that declares only constants but no axioms. This class can
always be instantiated. But this approach might be less beautiful.)

> How do you handle the
> interactions between Pure and HOL, or is this even a problem when
> translating into another type theory?

I am not sure what interactions you mean. Do you mean things like the
relation between --> and ==> and the relation between = and ==? As far
as I see, there are no problems there. For example, one can map -->
and ==> to the same Coq constant, and then all the HOL/Pure
interrelation axioms (like impI) are trivial lemmas in Coq.

> I would actually like it if even axiomatized constants would get topsorted
> declared types in consts.ML

If I understand correctly, the constant typing rule makes the sorts of
constants completely irrelevant from the logical point of view anyway.
So it seems that giving sorts to a constant does not have any other
effect than declaring a constraint for that constant. Am I right?

Best,
Dominique.