Email Gateway (Aug 23 2022 at 08:18): Email Gateway (Aug 23 2022 at 08:18):From: Makarius <makarius@sketis.net>
Note that the statement is only recorded for Proofterm.proofs 1 or 2.
Many years ago, it was also done for 0 (the default), but that could lead into
bad situations: some ambitious users were using oracles to shortcut formal
reasoning and ended up with rather slow inferences due to large number of
oracles being merged all the time.
Following the existing policies of Proofterm.proofs I have now added more
position information for Proofterm.proofs 1 or 2, see
https://isabelle-dev.sketis.net/rISABELLE910a081cca74 -- this will be in the
forthcoming Isabelle2020-RC1.
Makarius
Email Gateway (Aug 23 2022 at 08:28):From: Dominique Unruh <unruh@ut.ee>
Hello,
the following fragment proves False using sorry:
theory Scratch
imports Main
begin
ML ‹
Proofterm.proofs := 2
›
class false = fixes x::'a assumes xx: "x≠x"
instance int :: false sorry
lemma f: False
using xx by simp
thm_oracles f
end
Therefore, thm_oracles should list skip_proof as one of the oracles. (If
I understood the NEWS entry correctly that says "In particular, the
formal tagging with "Pure.skip_proofs" of results stemming from
"instance ... sorry" is now propagated properly").
However, no oracles are listed:
If we replace "using xx" by "using xx[where 'a=int]", it works
correctly. I assume the reason for the problem is that in my proof, the
step that uses the incorrect instantiation never uses "CLASS(int,false)"
but instead just uses the fact that false is an inhabited sort for
removing the sort hypothesis. (Evidence for this is that if we remove
the instance command, we get an error about sort hypotheses.)
Best wishes,
Dominique.
Email Gateway (Aug 23 2022 at 08:28):From: Makarius <makarius@sketis.net>
Thanks for testing it thoroughly. There is indeed something missing:
Thm.strip_shyps implicitly performs a type instantiation and thus needs to
participate in the new management of sort constraints. I have amended that here:
https://isabelle-dev.sketis.net/rISABELLE439410bf451
How did you figure out the above example? Just by accident or do you have
actual applications with notable coverage of theorems and their derivations?
I recall that you were trying to work with thm oracles before it was properly
supported. Do the various ML operations for it now make sense to you (e.g.
Thm_Deps.all_oracles_of, Thm_Deps.has_skip_proof)?
Side-remark: Your Proofterm.proofs := 2 did not make sense here and is fragile
in the face of parallel checking (if required see session option record_proofs
in HOL-Proofs). Thm dependencies are always recorded and don't need such a flag.
Makarius
Email Gateway (Aug 23 2022 at 08:28):From: Makarius <makarius@sketis.net>
I've done further reading of the surrounding sources, and may have to rethink
some details of the approach.
(NB: "RC0" is not even a release candidate yet, just an odd repository snapshot).
Makarius
Email Gateway (Aug 23 2022 at 08:28):From: Makarius <makarius@sketis.net>
On 17/02/2020 12:12, Makarius wrote:
On 16/02/2020 20:35, Makarius wrote:
However, no oracles are listed:
Thanks for testing it thoroughly. There is indeed something missing:
Thm.strip_shyps implicitly performs a type instantiation and thus needs to
participate in the new management of sort constraints. I have amended that here:
https://isabelle-dev.sketis.net/rISABELLE439410bf451How did you figure out the above example? Just by accident or do you have
actual applications with notable coverage of theorems and their derivations?I recall that you were trying to work with thm oracles before it was properly
supported. Do the various ML operations for it now make sense to you (e.g.
Thm_Deps.all_oracles_of, Thm_Deps.has_skip_proof)?I've done further reading of the surrounding sources, and may have to rethink
some details of the approach.
I have made a second round to study the situation, and it should be fine for
now, see also https://isabelle-dev.sketis.net/rISABELLEb2c9f94e025f
Included are exotic corner cases concerning a proven class relation a <= b.
Both examples work correctly, but the second might be surprising: the user has
written a non-normal sort {a,b} and the abstract syntax turns that into {a}
without formal reasoning. Thus the statement of the theorem is different from
what is written in the text, and consequently there is no trace of 'sorry' in
the result. Thus it serves as a reminder that the inference kernel is not
everything: many things don't go through it.
NB: "RC0" is not even a release candidate yet, just an odd repository snapshot.
I reckon that we can start with regular Isabelle2020-RC1 in approx. 2 weeks.
Still missing right now: update of NEWS, CONTRIBUTORS, ANNOUNCE.
Makarius
Scratch.thy
Email Gateway (Aug 23 2022 at 08:28):From: Dominique Unruh <unruh@ut.ee>
Hello,
Thanks for testing it thoroughly. There is indeed something missing:
Thm.strip_shyps implicitly performs a type instantiation and thus needs to
participate in the new management of sort constraints. I have amended that here:
https://isabelle-dev.sketis.net/rISABELLE439410bf451
Nice. I did not test it yet. (Because I don't have a build of the
development version installed / configured.) I noticed one thing in the
diff, though: The code uses Sorts.minimal_sorts, which, as far as I
understand, relies on subclass proofs. I may be wrong (because I have
not looked at all the related code) but doesn't that mean that oracles
from those subclass proofs need to included, too?
How did you figure out the above example? Just by accident or do you have
actual applications with notable coverage of theorems and their derivations?
More or less by accident. I was curious about the new oracle tracking
code and tried out a few corner cases. That I hit on the sort hypothesis
removal was pure accident because "using xx" was shorter to type than
"using xx[where 'a=int]".
I recall that you were trying to work with thm oracles before it was properly
supported. Do the various ML operations for it now make sense to you (e.g.
Thm_Deps.all_oracles_of, Thm_Deps.has_skip_proof)?
Yes, thm_oracles is basically what I used the old all_oracles_of for.
With the goal of being able to track progress in a large development
with many sorry's. My code had one additional feature: it would record
also the position and an optional comment in the oracle (by implementing
my own variant of sorry that records those additional things into the
term that is sent to the oracle). Then one can ctrl-click in the oracle
list to jump to the position where the corresponding oracle call occurs.
If required, I can share code for that.
Side-remark: Your Proofterm.proofs := 2 did not make sense here and is fragile
in the face of parallel checking (if required see session option record_proofs
in HOL-Proofs). Thm dependencies are always recorded and don't need such a flag.
I somewhat suspected that but included it just in case in this example
to make sure the problem did not depend on the proofterms recording level.
Best wishes,
Dominique.
Email Gateway (Aug 23 2022 at 08:29):From: Makarius <makarius@sketis.net>
Yes, I did that already in my second amendment:
https://isabelle-dev.sketis.net/rISABELLEb2c9f94e025f
I first thought that I need to revisit many more similar situations of
implicit subclass reasoning, but did not find any. 10 years ago we have
already put almost everything into an almost clear state.
Makarius
Email Gateway (Aug 23 2022 at 08:29):From: Makarius <makarius@sketis.net>
I was actually considering to add official positions to oracle invocations,
but that would also mean that much more information needs to be stored within
the derivation object because there will be more duplicates.
Makarius
Email Gateway (Aug 23 2022 at 08:30):From: Dominique Unruh <unruh@ut.ee>
Would there be more duplicates? I would have thought almost all oracle
invocations would lead to distinct entries anyway (even without
position) because they record the statement that is proven by oracle.
(And my guess is that this statement would be the same in two oracle
calls only in rare coincidences.)
Best wishes,
Dominique.
Last updated: Apr 20 2024 at 04:19 UTC