Email Gateway (Aug 22 2022 at 17:57): Email Gateway (Aug 22 2022 at 17:57):From: Michal Wallace <michal.wallace@gmail.com>
You were complaining that nobody answers your questions. I'm not sure
that's true, but I do think I can answer this one. :)
(Warning: I'm pretty much a newbie myself)
On Thu, Aug 9, 2018 at 3:44 AM Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
wrote:
Right at the moment I'm trying to understand what the documentation is
talking about when it refers to facts. Which it does in quite a lot
of places, so I'm surprised you refer to it as low-level exploration.
At (almost) any point in your document in isabelle/jEdit, type the
following line:
print_facts
Then put your cursor on that line and open the "output" panel to see what
the current facts are.
Further to the above question, where I have a proof state as follows
proof (state)
this:
Dgoal (1 subgoal):
1. A ==> B & C & Dwhat does
this:
D
mean?
notepad begin
assume "D"
print_facts
end
It means that D is a fact in the current context, and also that the name
"this" is bound to it.
"this" is special variable that's something like "the set of facts that you
just proved."
it allows you to forward chain from one statement to the next ("from this"
/ "hence")
(Looking at an example is great if you know what it is an example of,
eg adding to, or removing from, or using, the list of current facts or
local facts or method facts or goal facts or any other sort of facts
that the system uses; but without any explanation of what the example is
showing, then may often not be of any use).
Don't just look at it. Load it into the system and put your cursor on
different places in the file
and observe the proof state.
eg running through this example doesn't tell me what are, at each stage,
the current facts or local facts or method facts or goal facts or any
other sort of facts, and which of these have the same meaning, etc.(1) what does the \<proof> mean?
"\<proof>" is pretty much the same as "sorry" as far as Isabelle is
concerned, but
but is meant to indicate to the reader that the proof is essentially
unimportant or
intentionally left out, whereas "sorry" indicates that the thing proved by
it is important
and there really ought to be a proof there but... well... sorry, there
isn't.
(you'll notice that when a "proof outline" is generated in AFP, all the
actual proofs are
replaced with "\<proof>")
(2) what does
this
A1
A2
B1
B2
B3
mean?Ie does it mean that "this" refers to A1 or to all of A1 A2 B1 B2 B3?
Or to something else? Are all of these facts?
Yes. try using the 'print_facts' command before and after.
(incidentally, if you just type "print_" and let isabelle/jEdit
autocomplete, there's a bunch of other inspectors like these)
(3) what does "picking this" mean? At this point (ie after "from a")
what are the facts at the point? Is something which is once a fact
always a fact, or does it cease to become one? Since just A1 and A2 are
printed, does that mean that just those two are facts?(4) After the "have C" the proof state includes "using this A1 A2".
What are the facts at this point?(5) After the "using b" the proof state becomes "using this A1 A2 B1 B2
B3"? Same questions.(6) After proof ... we get method_facts A1 A2 B1 B2 B3. Are
method_facts the same as facts? If not, what is the difference?(7) After show ?thesis \<proof> it says something has been proved, but
it's not apparent what (I'm guessing C) or how (though I assume it must
be that it has used C to prove C, though I can't see where it has been
told to do that).
I feel like all of thees have the same answers... Just click and look.
Which, combined with other questions you've asked, makes me wonder if you
are just completely
ignoring the jEdit component, and trying to use Isabelle only from the
console?
I can certainly imagine how the other systems you've mentioned using would
lead you to do that,
but it must be terribly frustrating.
I think (maybe?) modern Isabelle is just a very different thing than what
you want/expect it to be.
It is still very possible to extend Isabelle with ML, but maybe it's worth
taking a step back and
telling yourself that what you're dealing with isn't ML. It's a new
language/environment/system
all its own that just happens to have ML as a sub component...
Email Gateway (Aug 22 2022 at 17:58):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Michal,
At (almost) any point in your document in isabelle/jEdit, type the
following line:print_facts
Then put your cursor on that line and open the "output" panel to see
what the current facts are.thanks - that is very helpful.
Don't just look at it. Load it into the system and put your cursor on
different places in the file
and observe the proof state.I meant I'd looked at the result of running the example.
Your answer to (1) I think also clarifies (7). And for some reason I'd
thought
that what is printed after "using" or "using this" is the facts, which is
apparently not so.
But do you know what it is that is printed after "using" or "using this"?
(6) After proof ... we get method_facts A1 A2 B1 B2 B3. Are
method_facts the same as facts? If not, what is the difference?
I've discovered that at several places in the file I can insert
apply (print_fact method_facts)
and what it gives is different from what is printed by print_facts
(which is described as local facts).
Do you know what method facts or local facts are? Presumably they
are of some relevance, different from them simply being facts.
Which, combined with other questions you've asked, makes me wonder if
you are just completely
ignoring the jEdit component, and trying to use Isabelle only from the
console?I've certainly tried to do as much as I can from the console, but as for
running the file that my questions were based on and viewing the output
at each step, I think I must have used jedit, I don't think I know how
to do that using the console.
I can certainly imagine how the other systems you've mentioned using
would lead you to do that,
but it must be terribly frustrating.
As a matter of fact, being able to jump back and forth in a proof is
very nice for doing exactly what you suggest (re print_facts) but
generally it's not worth the sluggishness of jedit, and having to
enclose everything in ML {* ... *}, and only seeing a few lines of
output at a time, and so forth.
Thanks again for your answers
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 17:58):From: Makarius <makarius@sketis.net>
Before this thread is again diverging into non-sense, just a reminder of
the most basic facts of Isabelle2018:
* You do need to use Isabelle/jEdit for almost everything. Don't try
to bail out into the "isabelle console" tool, which is merely a leftover
for certain low-level system debugging.
* "enclose everything in ML {* ... *}" is misleading. You rarely need
Isabelle/ML to use the system properly. ML is the system extension
language, and using it for that purpose, Isabelle/jEdit is actually more
convenient than anything before in the history of Isabelle.
* "sluggishness of jedit": The Isabelle/jEdit application normally
works smoothly on decent hardware. You need 2-4 CPU cores and 8-16 GB
RAM, i.e. cheap mid-range consumer hardware. If you don't want to invest
in that, you should not use Isabelle2018.
Also note that the Isabelle/jEdit application title in Isabelle2018 is
now "Isabelle2018/HOL" (or another logic image). It means that at first
approximation "Isabelle2018" and "Isabelle/jEdit of Isabelle2018" are
the same thing: there is practically no escape from it, and no point to
try it. If you don't like that, you should be honest to yourself use a
different proof assistant.
Makarius
Email Gateway (Aug 22 2022 at 17:59):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
I never observe the proof state, I just read my own Isar code as if I was
writing a paper in LaTex. The slogan is: Isar is not a video game like Coq,
but a typewriter like LaTex.
To understand the theory behind the proof is the key to write readable
proofs in Isar. In my case, I follow the following steps (without regarding
any textbook, just having an idea of the theory in mind):
I write my theorem and I write sorry in its proof.
I write the lemmas that I need to prove my theorem, with sorry in the
proof of each one.
I write the proof of my theorem assuming the lemmas as true.
I repeat the previous steps with each lemma with sorry as proof.
Jose M.
Email Gateway (Aug 22 2022 at 18:10):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi,
I find that for a given proof state,
Proof.the_facts can indicate a non-empty list of facts, but
(#facts o Proof.goal) gives an empty list of facts.
Why is this, and what do these two functions return? Are there two
different sorts of facts?
Variously the documentation refers to "current facts" and "incoming
facts". What does this terminology mean?
Method.get_facts and Method.set_facts refer to sets of facts which it
would seem belong to a proof context, rather than to a Proof state. How
do these relate to the sets of facts mentioned above which would seem to
be are part of the proof state?
thanks
Jeremy
Email Gateway (Aug 22 2022 at 18:11):From: Makarius <makarius@sketis.net>
This looks like a low-level exploration of Isabelle/Isar internals.
What are you trying to do abstractly. What is your application?
Makarius
Email Gateway (Aug 22 2022 at 18:11):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Right at the moment I'm trying to understand what the documentation is
talking about when it refers to facts. Which it does in quite a lot of
places, so I'm surprised you refer to it as low-level exploration.
Jeremy
Email Gateway (Aug 22 2022 at 18:13):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Further to the above question, where I have a proof state as follows
proof (state)
this:
D
goal (1 subgoal):
1. A ==> B & C & D
what does
this:
D
mean?
I guessed from the documentation that it means that D is a fact. Is
that right?
But when I try Proof_Context.print_local_facts on the proof context
derived from that proof state, it gives nothing.
(Proof_Context.print_local_facts appears to the the ML function which
implements the Isar command print_facts)
Thanks
Jeremy
Email Gateway (Aug 22 2022 at 18:13):From: Makarius <makarius@sketis.net>
A fact is the most fundamental result produced in a proof context, it is
a multi-thm, i.e. a list of things that hold in a certain context.
Facts are defined in the theory or proof context via names, just like
constants or types. Within a proof, fact names are optional and the last
fact is always called "this". This allows to use forward-chaining of a
fact towards the next goal statement. Facts chained into a goal are
presented to proof methods as the primary "facts" argument.
Attached is an example that illustrates this.
Makarius
Scratch.thy
Email Gateway (Aug 22 2022 at 18:14):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Well, thanks - but that raises more questions than it answers.
(Looking at an example is great if you know what it is an example of,
eg adding to, or removing from, or using, the list of current facts or
local facts or method facts or goal facts or any other sort of facts
that the system uses; but without any explanation of what the example is
showing, then may often not be of any use).
eg running through this example doesn't tell me what are, at each stage,
the current facts or local facts or method facts or goal facts or any
other sort of facts, and which of these have the same meaning, etc.
(1) what does the \<proof> mean?
(2) what does
this
A1
A2
B1
B2
B3
mean?
Ie does it mean that "this" refers to A1 or to all of A1 A2 B1 B2 B3?
Or to something else? Are all of these facts?
(3) what does "picking this" mean? At this point (ie after "from a")
what are the facts at the point? Is something which is once a fact
always a fact, or does it cease to become one? Since just A1 and A2 are
printed, does that mean that just those two are facts?
(4) After the "have C" the proof state includes "using this A1 A2".
What are the facts at this point?
(5) After the "using b" the proof state becomes "using this A1 A2 B1 B2
B3"? Same questions.
(6) After proof ... we get method_facts A1 A2 B1 B2 B3. Are
method_facts the same as facts? If not, what is the difference?
(7) After show ?thesis \<proof> it says something has been proved, but
it's not apparent what (I'm guessing C) or how (though I assume it must
be that it has used C to prove C, though I can't see where it has been
told to do that).
Thanks
Jeremy
Last updated: Nov 21 2024 at 12:39 UTC