Email Gateway (Aug 22 2022 at 18:44): Email Gateway (Aug 22 2022 at 18:44):From: Ed.Pierzchalski@data61.csiro.au
Hi all,
I'm currently working on extracting theorem dependencies from proof terms. I've noticed that the prop one gets from Thm.full_prop_of sometimes doesn't match the prop in the topmost proof body of a thm. As an example, the following two props are different:
theory Scratch
imports Main
begin
declare [[show_sorts]]
ML \<open>
val prop1 = Thm.full_prop_of @{thm refl};
val prop2 = @{thm refl}
|> Thm.proof_body_of
|> (fn (PBody {thms, ...}) => thms)
|> List.hd
|> snd
|> Proofterm.thm_node_prop;
\<close>
In particular, prop2 has the type_class sort constraint pulled out as a premise, whereas prop1 leaves it as a constraint on types in the term. As far as I can tell, the transformation only occurs in proof bodies as part of a post-processing step introduced by Proofterm.thm_proof.
I ran into the above while attempting to disambiguate the names that occur in proof bodies. That is, if a proof body refers to a prop p with name "foo_1", I need to distinguish between p being proven by the first theorem in a thm list (foo(1)) or by a thm with the actual name foo_1. Since Thm.full_prop_of and proof bodies sometimes disagree, the easiest solution at the time was to use the proof body terms as a 'normal form', which seems unsatisfying. So, for my own education:
foo vs. a theorem named foo_1?Regards,
--Ed
Email Gateway (Aug 22 2022 at 18:45):From: Makarius <makarius@sketis.net>
I occasionally ask myself the same questions. After so many years the
situation of proof terms is still not quite clear.
In particular, the concept did not catch up with the "authentic fact
name" reform from some years ago: In distant past, a fact name in the
theory was just a comment, and the slightly odd "disambiguation" wrt.
the proposition was used to make sense of in as proof terms. Now the
fact environment of the context is authentic, but proof terms still have
a rather weak notion of derivation name internally.
There are other fine points that don't quite work, e.g. see the
implementation of the commands 'thm_deps' and 'unused_thms'.
As usual, one needs to look very closely at the status-quo, and figure
out if a particular application has the chance to go through.
Which leaves the canonical question: What application do you have in mind?
Makarius
Email Gateway (Aug 22 2022 at 18:45):From: Ed.Pierzchalski@data61.csiro.au
Which leaves the canonical question: What application do you have in mind?
We're looking for stray unused lemmas in the seL4 verification proofs. These are (in some parts) old and (in all parts) large collections of proofs that have undergone more than a few refactorings. The technique of using proof node names to loosely infer "real" lemma names and their usage relationships, as well as proof node props to disambiguate/confirm those inferences, seems to be working so far, so I suppose I have no real issue yet.
I occasionally ask myself the same questions. After so many years the
situation of proof terms is still not quite clear.
In particular, the concept did not catch up with the "authentic fact
name" reform from some years ago: In distant past, a fact name in the
theory was just a comment, and the slightly odd "disambiguation" wrt.
the proposition was used to make sense of in as proof terms. Now the
fact environment of the context is authentic, but proof terms still have
a rather weak notion of derivation name internally.
There are other fine points that don't quite work, e.g. see the
implementation of the commands 'thm_deps' and 'unused_thms'.
As usual, one needs to look very closely at the status-quo, and figure
out if a particular application has the chance to go through.
Which leaves the canonical question: What application do you have in mind?
Makarius
Last updated: Apr 20 2024 at 01:05 UTC