[isabelle-dev] Typing problem in autogenerated axiom

[Dominique Unruh]

Dear all,

Alexander Krauss wrote:

> "a few months" is probably the most realistic option on your list. But if you like, we can make our current code available to you... at your own risk, of course.

That would be nice. Then I could continue my experiments.


>>    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:

> What you are describing is essentially the dictionary construction. We are doing essentially the same thing, passing dictionaries around explicitly. With a bit of luck, you could then avoid doing this
> yourself, and just need to recover the implicit arguments setup somehow...

Yes, I agree. But let me give an example where the difficulty lies:

Let's say, we have the theorem "x::'a::order <= x" (which, of course,
follows trivially from the corresponding axiom).

This theorem would perhaps be written as follows in the dictionary
approach in Isabelle:
(1) "order_axioms(?less_eq,?less) ==> ?less_eq ?x ?x".

In Coq, we need to close all terms, so we would get:
(2) "forall (a:Type) (less_eq:a=>a=>bool) (less:a=>a=>bool) (x:a),
order_axioms(less_eq,less) -> less_eq x x"

This is logically equivalent to the way we would express type classes in Coq:
(3) "forall (a:Type) (inst:order a) -> less_eq inst x x"
where "order a" is (approximately) a type containing all pairs of
(less_eq,less) such that order_axioms(less_eq,less) holds. And
"less_eq" is an accessor constant such that "less_eq inst" returns the
first component of inst.

Now I have two options: I convert all terms within Isabelle proof
terms to the (2)-form or to the (3)-form. Converting to the (2)-form
should work nicely but the (2)-form is not the natural formulation of
type classes in Coq. Converting to the (3)-form should work for most
theorems, namely those that nicely have the "order_axioms" hypotheses
in the beginning of the theorem, and that do not use less_eq with any
type that does not have a corresponding order_axioms-hypothesis. But
some theorems might not be of this form. A proof term might contain a
theorem like "order_axioms(?less_eq,?less) ==>
order_axioms(?less_eq,(%x y. ?less_eq x y & x!=y))". Such a theorem
cannot be translated into (3)-form. I would have to use (2)-form. But
as soon as I mix (2)- and (3)-forms within a single proof term, I
would have to perform conversions all the time. Also, even if all
theorems can be converted to (3)-form, the order of arguments of the
theorems might be different in Coq and Isabelle (e.g., the (2)-form
would first have the "forall"-stuff for all type variables, and then
the "order_axioms"-stuff for each type variable, while the (3)-form
would first have all stuff for the first type variable, then
everything for the second). This would considerable alter the
structure of the proof terms, making the conversion tricky.

Thus, I have two approaches.

A) If Isabelle uses axiomatized sorts, I would translate all theorems
into (3)-form. But this only works when no theorems such as
"less_eq::T=>T=>bool == less_eq" with T not of sort ord ever occur.
But since some parts of the proof term are strip_sorted, such terms
could occur. So a conversion to (3)-form would work nicely only if the
sorts of constants would be enforced by the type system. (Also, I need
to replay the instance-proofs in Coq, too, but this should be doable.)

B) If Isabelle uses internalized sorts, I would translate all theorems
into (2)-form. This gives me correct, but hard to use theorems in Coq.
Then, in a second step, I would generate user-friendly versions of
each definition and each (named) theorem. These user-friendly theorems
use (3)-form and are derived directly from the theorems in (2)-form
(without replaying any proof terms). Theorems that cannot be converted
into (3)-form are just skipped, but this is not a problem because such
theorems are probably not intended for the user anyway.

Considering the future plans for completely removing sorts from
Isabelle, I tend towards approach B.



2009/12/2 Andreas Schropp <schropp at in.tum.de>:
> Perhaps we can offer a flag to turn this elimination off globally, if you
> really need it. But as more people use proofterms this is likely to result
> in confusion, and more complexity anyways.

I agree, such a switch would only make matters more complicated. And
just having the switch would also not help me because Isabelle would
still use strip_sorted constants which would break my approach A.


> I think I understand where you come from. The problem you get is with
> instance, subclass and arity "proofs" by users.
> Users prove the internalization of the corresponding judgement, and then
> this judgement is axiomatized in the type system. So if you don't follow the
> internalization path, you have to take those on good faith or reinterpret
> the proofs in your setting. I guess this asks for trouble, but would be cool
> actually.

Yes, this was what I was planning in approach A. Actually, I do not
think that this would lead to too much trouble, because the users
prove statements "OFCLASS(T,class)" that are already almost the thing
we need for producing the instance objects in Coq. So we would just
replay the proof of "OFCLASS(T,class)" in Coq first, leading to a
Coqified version of the theorem, and then use a function in Coq that
maps (T:Type) and (x:OFCLASS(T,class)) to an element of (class T).
Coq's type system should be rich enough to do define such a function.


>> and that
>> Isabelle proof terms may contain free variables (which implies that in
>> Pure all terms
>> are inhabited) while Coq proof terms may not.)

> You mean types? And I guess your reasoning refers to hidden term variables
> which occur in the proof, but not in the proved proposition?

Yes, that what I meant. These are produced for example if we use "fix
x::'a" in Isar and then only use x to show non-emptiness of 'a.


>> 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.)
>>
> The way I handle this case is by abstracting out "unresolved overloading"
> into "dictarg" variables which get quantified on the outside.

Yes, I think it is possible. The problem is just that the Coq-view on
type classes does not allow to separate the dictionary from the proof
of the class axioms (the Coq instance is a single record containing
both constants and proofs of axioms). This is why splitting the
unoverloading from the type classes is awkward in Coq.


> Most of our problems stem from HOL and Pure sharing a function space,
> whereas ZF has its own set theoretic one, which is of course very different
> from the Pure one. I solved this by a stratification of types into HOL/Pure
> parts, and carrying this stratification schematically through the whole
> translation process, which works because proof constants are only
> schematically polymorphic.

Yes, the nice thing about Coq is that it is almost an exact superset
of what is available in HOL (at least when we use the various optional
Coq-axioms like excluded-middle and extensionality-of-equality).




So overall, I think the best approach for me is approach B, because it
should work well and be compatible with the current plans for the
Isabelle kernel.

Best,
Dominique