Email Gateway (Nov 03 2022 at 16:12): Email Gateway (Nov 03 2022 at 16:12):From: Nicolas Méric <nicolas.meric@lri.fr>
Dear Isabelle's users,
I try to use the Isabelle's Metalogic by Tobias Nipkow and Simon Roßkopf
(https://www.isa-afp.org/entries/Metalogic_ProofChecker.html)
with Isabelle/DOF (https://zenodo.org/record/6810799).
I want to write a reification function of terms and proofterms in ML to
this metalogic, to offer a kind of introspection over proofterms or
the possibility to add metadata to proofterms to maybe make
their rewriting to other ITPs easier.
But I do not understand some part of the definition of the proof
datatype in proofterm.ML, the constructor PAxm for example,
and the implementation of PAxm in the metalogic.
In Pure we have (in proofterm.ML):
datatype proof =
MinProof
| PBound of int
| Abst of string * typ option * proof
| AbsP of string * term option * proof
| % of proof * term option
| %% of proof * proof
| Hyp of term
| PAxm of string * term * typ list option
| PClass of typ * class
| Oracle of string * term * typ list option
| PThm of thm_header * thm_body
and proof_body = PBody of
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
proof: proof}
Of what use is the typ list option for PAxm?
In the metalogic, we have a similar contructor (in ProofTerm.thy):
type_synonym tyinst = "(variable × sort) × typ"
datatype proofterm = PAxm "term" "tyinst list"
| PBound nat
| Abst "typ" proofterm
| AbsP "term" proofterm
| Appt proofterm "term"
| AppP proofterm proofterm
| OfClass "typ" "class"
| Hyp "term"
variable in tyinst is defined in Core.thy:
datatype variable = Free name | Var indexname
So, for a proofterm in Pure,
it seems to me that the typ list option of the PAxm constructor
in ML should be translated to the tyinst list of the PAxm constructor
in the metalogic.
Is this the idea?
Then, for PAxm in the metalogic, are the variable and the sort in tyinst
an extract of the typ also in tyinst?
If no, how are they linked?
Best regards.
Nicolas Méric
Email Gateway (Nov 03 2022 at 18:18):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I am not aware of documentation on this, but during my own work in
translating proofterms, I found that the following seems consistent:
The typ-list-option argument is the instantiation for the TVar's
occurring in the axiom's proposition (the term argument). The order of
those arguments is the reverse order of what Term.add_tvars returns.
So you should get the tyinst argument with roughly the following code:
PAxm (name, prop, typ_args) => zip (rev (add_tvars prop []), typ_args)
(up to a conversion to the type "variable" in the Metalogic, I don't
know what it is exactly since I am not familiar with the Metalogic.)
Best wishes,
Dominique.
Email Gateway (Nov 09 2022 at 15:33):From: Nicolas Méric <nicolas.meric@lri.fr>
Hi Dominique,
thanks for the info and the tip. It helped a lot.
I have a related question.
During my few tests, I did not find any schematic variables (Tvars) with
a sort other than Nil in the PAxms' proposition (the term argument) or
in the PThms' prop (inside the thm_header argument).
A basic example with Pure.symmetric:
ML‹
val thm = @{thm "Pure.symmetric"}
val PAxm (name, term, typ_list_option) % t % u = Thm.proof_of thm
val tvars = rev (Term.add_tvars term [])
›
Do you an idea of an axiom or theorem whose sort of Tvars of the
proposition will not be a Nil list, i.e, will have some classes?
Best regards.
Nicolas.
Email Gateway (Nov 09 2022 at 16:23):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,
again, what I'm saying now is purely based on my experiments:
There are two ways to get proofterm. One is to get a theorem from the
theory (e.g., Proof_Context.get_thm) and then get the proofterm from
that (e.g., Thm.proof_of). I haven't checked right now, but I believe if
you apply this to a theorem with sorts, you get sorts in the prop of
that theorem.
The second way is to take the proofterm gotten like this, and to descend
to the first PThm. This is always a very shallow proof, and you get a
PThm with the same name (in the header) as the name you gave to
Proof_Context.get_thm. But that PThm contains a prop that has been
processed. All sorts have been removed and instead explicit
"OFCLASS(...)" assumptions have been added. This is logically
equivalent. The proof of the processed theorem has no sorts whatsoever
(all the typeclass-logic is encoded using explicit assumptions in the
theorems). The advantage of this is that, if you want to check a proof,
you will never have to export deal with sorts.
The same seems to hold for axioms, too. They also do not contain sorts.
I do not know whether it is possible for exceptions to this to occur or
whether the kernel ensures that a pthm always contains a cleaned proof
and that an axiom does not contain a sort ever.
The approach that I am taking is to ignore the unprocessed theorems
altogether and to implement proofterm translation without typeclasses.
By the way: I did a quick check: all the axioms and theorems recursively
encountered when checking the proof of Nat.add_0_right do not contain
sorts. (Assuming my check-code does not have a bug, of course.)
Another note: constant types (gotten via Sign.const_typargs) sometimes
seem to have sorts (and not only HOL.type). Since the corresponding
axioms do not have sorts, these sorts seem to be more informative than
binding. I am ignoring them.
Best wishes,
Dominique.
Email Gateway (Dec 20 2022 at 11:53):From: Nicolas Méric <nicolas.meric@lri.fr>
Dear Dominique,
I had some time to work on that again.
Thanks again for the explanation.
I have another question and maybe you'll accept to share your knowledge,
one more time.
In the metalogic, the PAxm constructor takes a typ list and not a typ
list option as in the Isabelle PAxm.
I was wondering how to deal with that, and I found the
Proof_Syntax.standard_proof_of function in proof_syntax.ML. It seems
that this function reconstructs the proofs (using,
Thm.reconstruct_proof_of) and, in the case of a PAxm, updates the typ
list option argument, at least if the list is NONE.
An example with Pure.symmetric:
ML‹
val full = false
val thm = @{thm "Pure.symmetric"}
val proof_of = Thm.proof_of thm
val standard_proof = Proof_Syntax.standard_proof_of
{full = full, expand_name = Thm.expand_name thm} thm
›
Here, proof_of will have the value:
val proof_of =
PAxm ("Pure.symmetric",
Const ("Pure.imp", "prop ⇒ prop ⇒ prop") $
(Const ("Pure.eq", "?'a::{} ⇒ ?'a::{} ⇒ prop") $
Var (("x", 0), "?'a::{}") $ Var (("y", 0), "?'a::{}")) $
(Const ("Pure.eq", "?'a::{} ⇒ ?'a::{} ⇒ prop") $
Var (("y", 0), "?'a::{}") $ Var (("x", 0), "?'a::{}")),
NONE) %
NONE % NONE:
proof
And standard_proof will have the value:
val standard_proof =
PAxm ("Pure.symmetric",
Const ("Pure.imp", "prop ⇒ prop ⇒ prop") $
(Const ("Pure.eq", "?'a::{} ⇒ ?'a::{} ⇒ prop") $
Var (("x", 0), "?'a::{}") $ Var (("y", 0), "?'a::{}")) $
(Const ("Pure.eq", "?'a::{} ⇒ ?'a::{} ⇒ prop") $
Var (("y", 0), "?'a::{}") $ Var (("x", 0), "?'a::{}")),
SOME ["?'a::{}"]) %
NONE % NONE:
proof
We can see that the typ list option has been updated with a schematic
variable.
Do you think this is a good idea to deal with the typ list option
argument of a PAxm in the same way, and then be able to reify a PAxm
even when the typ list option is NONE, as the PAxm in the metalogic does
not take and option as argument?
Maybe standardizing the proof (I don't really know what Stefan Berghofer
means by that) with the standard_proof_of function will also deal with
the other option types in the proof datatype, like the typ option
argument of the Abst constructor, or the term option of the % constructor.
Best regards,
Nicolas
Email Gateway (Dec 20 2022 at 12:01):From: Simon Roßkopf <rosskops@in.tum.de>
Hi,
In the metalogic, the PAxm constructor takes a typ list and not a typ
list option as in the Isabelle PAxm.
This is mostly because the formalization does not support compressed
proof terms (where the typ instantiation info is omitted). In general,
all the _ option types in the proofterms are for information that could
be omitted for compression. In my experience it is enough to get the
fully reconstructed proof terms using for example
Thm.reconstruct_proof_of and work with them.
Regards
Simon Roßkopf
Email Gateway (Dec 27 2022 at 08:50):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hello,
as I understand it, the option arguments in Isabelle proof terms are
used to omit redundant information. Basically, None can be inserted
whenever it is possible to reconstruct what should be there if we know
what theorem the proofterm proves (basically type-inference on the
proofterm level). While if everything is filled in, then for any
proofterm, we can find out what it proves without additional
information. After Thm.reconstruct_proof_of, there should be no None
left in the proofs.
I do not know what Proof_Syntax.standard_proof_of does (or what a
standard proof is) but I would be interested to know...
Best wishes,
Dominique.
Last updated: Apr 25 2024 at 04:18 UTC