[isabelle] Canonical Proof Props

[E***@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:

- What is the canonical way to get the dependencies of a thm?
- What is the canonical way to disambiguate between the first theorem of `foo` vs. a theorem named `foo_1`?

Regards,
--Ed

[Makarius]

On 14/11/2018 08:18, ***@data61.csiro.au wrote:
>
> 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:
>
> - What is the canonical way to get the dependencies of a thm?
> - What is the canonical way to disambiguate between the first theorem of `foo` vs. a theorem named `foo_1`?

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

[E***@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.
________________________________________
From: Makarius <***@sketis.net>
Sent: Thursday, November 15, 2018 12:58 AM
To: Pierzchalski, Ed (Data61, Kensington NSW); cl-isabelle-***@lists.cam.ac.uk
Subject: Re: [isabelle] Canonical Proof Props

On 14/11/2018 08:18, ***@data61.csiro.au wrote:
>
> 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:
>
> - What is the canonical way to get the dependencies of a thm?
> - What is the canonical way to disambiguate between the first theorem of `foo` vs. a theorem named `foo_1`?

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