[isabelle-dev] Typing problem in autogenerated axiom
Andreas Schropp
schropp at in.tum.de
Wed Dec 2 11:44:37 CET 2009
Dominique Unruh wrote:
> Dear all.
>
>
>
>> 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, ...)?
Like Alex said, "a few months" seems realistic. The patch itself is
working already, we are mostly engaged in porting and consolidation.
> 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.
>
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.
>
>
>> 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.
>
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.
>
>
>> 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
You mean types? And I guess your reasoning refers to hidden term
variables which occur in the proof, but not in the proved proposition?
> 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.
>
Sounds cool. ^^
As our type-class inferences are really simple and regular, I guess that
should be possible.
What remains is the problem to translate instantiation, subclass and
arity relation proofs, which are done for the internalized sort/type
judgement.
> 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.
>
That sounds like the unoverloading transformation which I prefix, but
this handles raw overloading when type classes are already gone.
> 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.
>
>> 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.
>
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.
>
>> 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.
>
Yes.
> 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?
>
I think yes. The thing I am concerned with is to have as few special
cases as possible. ^^
> Best,
> Dominique.
>
More information about the isabelle-dev
mailing list