Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
In examining the proof of HOL.less_max_iff_disj I came upon something
I found strange, which indicates I don't understand this aspect of
the proof term:
In all the other proofs I've seen up to this point (and I've seen
hundreds),
all the free TVars were contained in the conclusion or premises of
the theorem. Moreover, all of these
TVars had index 0 (as part of the "indexname" type) In this case,
there is a free TVar deep in the proof "'t" with index "111". Now I
have
no idea where this came from, nor the significance of the index,
especially
such a seemingly strange one as this.
Can anyone explain what is going on here? I thought the index was
just for some
nonlogical optimization.
Thanks!
Sean
Email Gateway (Aug 17 2022 at 13:28):From: Lawrence Paulson <lp15@cam.ac.uk>
The index is a variable-renaming mechanism, known as "standardizing
apart" in the resolution world. The TVar is present because the
second step of the proof introduces it:
apply (insert linorder_less_linear)
You can eliminate the TVar if you make this step instantiate the type
variable to the one used in the theorem statement:
apply (insert linorder_less_linear [where ?'a ='a])
Larry Paulson
Email Gateway (Aug 17 2022 at 13:28):From: Stefan Berghofer <berghofe@in.tum.de>
Sean McLaughlin wrote:
Hello,
In examining the proof of HOL.less_max_iff_disj I came upon something
I found strange, which indicates I don't understand this aspect of the
proof term:In all the other proofs I've seen up to this point (and I've seen
hundreds),
all the free TVars were contained in the conclusion or premises of the
theorem. Moreover, all of these
Hello Sean,
this kind of "subformula property" need not hold in general. In particular,
it does not hold if the proof is not in "normal form", i.e. contains
detours. Due to the fact that type variables that are not contained in the
main goal may appear during the proof of a theorem, Isabelle's theorem
datatype also contains a list of sort hypotheses (see section 5.1.7 of the
Isabelle Reference manual).
TVars had index 0 (as part of the "indexname" type) In this case,
there is a free TVar deep in the proof "'t" with index "111". Now I have
no idea where this came from, nor the significance of the index,
especially
such a seemingly strange one as this.
Since type information can be reconstructed, the proof terms of theorems
stored in Isabelle's theorem database do not contain any type information.
The type reconstruction algorithm first inserts type variables in place of
the omitted types, which are then instantiated via unification. In order
to be able to generate fresh variables easily, the reconstruction algorithm
simply increments the index every time it generates a variable, which may
lead to "strange" indices like the one you have encountered.
If a type variable (with "?") remains after reconstruction, this means that
the choice of the type does not influence the correctness of the proof.
The index has no particular significance - one could add a postprocessing stage
to the reconstruction algorithm that replaces these "strange" variables
by "nicer" ones.
Greetings,
Stefan
Last updated: May 03 2024 at 12:27 UTC