Email Gateway (Aug 22 2022 at 19:18): Email Gateway (Aug 22 2022 at 19:18):From: "John F. Hughes" <jfh@cs.brown.edu>
I'd like to write an Isar proof about lines in the cartesian plane in a
deliberately basic way.
I've got distinct points (x0,y0) and (x1, y1), and want to show that
there's a line between them. "lines" are represented either by a pair (m,
b), describing the line y = mx + b, or by a number c, representing the line
x = c.
The natural proof for me as a mathematician splits into two cases: 1. where
x0 = x1 (in which case we know that y0 is not equal to y1, and can build
the vertical line at x = x0) , or
I've made choices about datatypes that you may find non-idiomatic, but I
made them on purpose, and I suspect that every if they're not idiomatic,
they should be usable --- they don't seem to me to express anything that's
an incorrect model of my geometric question. My real question is about
how to write case-based proofs of the kind described above.
So here's what I tried:
datatype a2pt = A2Point "real" "real"
datatype a2ln = A2Ordinary "real" "real"
| A2Vertical "real"
lemma A2_a1: "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
When I typed
proof cases
I was offered a template for case-proofs, namely
proof cases
case True
then show ?thesis sorry
next
case False
then show ?thesis sorry
qed
but the line 'case True' (which I frankly don't understand) was highlighted
with the response 'Illegal schematic variable(s) in case "True" '
I tried editing a little, to
proof
fix x0 y0 assume "P = (A2Point x0 y0)"
fix x1 y1 assume "Q = (A2Point x1 y1)"
proof cases
...but that got me a "Illegal application of proof command in "state" mode"
error, which I cannot find in any of the explanatory material I've seen
about Isabelle (indeed, the term "state mode" eludes me as well).
Putting the two "fix" lines within the cases proof helped a little:
proof cases
fix x0 y0 assume "P = (A2Point x0 y0)"
fix x1 y1 assume "Q = (A2Point x1 y1)"
case True
then show ?thesis sorry...
but the "case True" still produced an error. I thought maybe I could state
a case that actually meant what I intended, so I tried
lemma A2_a1: "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
proof cases
fix x0 y0 assume "P = (A2Point x0 y0)"
fix x1 y1 assume "Q = (A2Point x1 y1)"
case "(x0 = x1)"
...
but that base statement generated an error "Undefined case: "(x0 = x1)"⌂".
I'd appreciate any hints you can give.
Email Gateway (Aug 22 2022 at 19:18):From: "John F. Hughes" <jfh@cs.brown.edu>
Gene Stark points out that without the whole Theory file, it's not clear
what I'm up to. I've attached it here, in hopes that this gets it to the
rest of the distribution list.
-John
Question4.thy
Email Gateway (Aug 22 2022 at 19:18):From: Thomas Sewell <sewell@chalmers.se>
Hi John. It's raining where I am, so I had a go at your proof.
BTW, when posting examples like this, it can be useful to include all relevant definitions. I had to guess at your definition of "a2meets", so it's possible my proof script below won't work for you.
It looks like you've hit a few cases involving unexpected defaults.
Firstly, to explain your problem, when you type "proof cases" the system has gone into a strange state involving a thing called a schematic variable. It's not actually irrecoverable, but you generally don't want this. Usually cases takes an argument, which is a term whose type has a case-division principle. In the absence of an argument, it's picked an unknown (schematic) value of type bool, with cases True and False.
In one of your later attempts, BTW, you've hit another slightly unusual default. If you just type "proof" without saying what kind of proof, the system tries to perform one step by a default rule. Here it picked the rule ex1I, which you can have a look at ( type thm ex1I somewhere ). Until you understand the system better, I'd recommend you type "proof -", which is proof without any steps.
One more note on your email, if you tick the "Proof state" box in the output panel, you'll see that parser for structure proofs alternates between "proof (state)" mode and "proof (prove)" mode. I would describe the first as forward-style, where you're expected to state some new fact to prove, and the second as backward-style, where you're expected to work on a goal that has been somehow stated.
Anyway. Since we want to use ex1I eventually, I had a go at building a structured proof in which I construct the required premises. The thesis in each case is then proven "by auto", which knew to use the default rules. I haven't proven all the bits, and if your a2meets definition is different to mine then my proof steps might not apply. I hope that clarifies a bit.
Cheers,
Thomas.
fun pt_x :: "a2pt ⇒ real" where
"pt_x (A2Point x y) = x"
fun pt_y :: "a2pt ⇒ real" where
"pt_y (A2Point x y) = y"
definition
"a2meets P l = (case l of A2Ordinary m b ⇒ pt_y P = (m * pt_x P) + b
| A2Vertical c ⇒ pt_x P = c)"
lemma A2_a1: "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
proof (cases "pt_x P = pt_x Q")
case True
assume PQ: "P ≠ Q"
define l where "l = A2Vertical (pt_x P)"
have meets: "a2meets P l ∧ a2meets Q l"
by (simp add: l_def a2meets_def True)
from PQ True have iff: "a2meets P l' ∧ a2meets Q l' ⟶ l' = l" for l'
apply (clarsimp simp: a2meets_def l_def split: a2ln.split)
apply (cases P; cases Q; clarsimp)
done
from meets iff show ?thesis
by auto
next
case False
define m where "m = (pt_y Q - pt_y P) / (pt_x Q - pt_x P)"
have "∃b. a2meets P (A2Ordinary m b) ∧ a2meets Q (A2Ordinary m b)"
apply (simp add: a2meets_def m_def)
apply (simp add: algebra_simps)
sorry
then obtain b where b: "a2meets P (A2Ordinary m b) ∧ a2meets Q (A2Ordinary m b)"
..
define l where "l = A2Ordinary m b"
note meets = b[folded l_def]
have iff: "a2meets P l' ∧ a2meets Q l' ⟶ l' = l" for l'
sorry
from meets iff show ?thesis
by auto
qed
Email Gateway (Aug 22 2022 at 19:19):From: "John F. Hughes" <jfh@cs.brown.edu>
Thanks, this is great. I do seem to have a knack for colliding with the
rough edges of things, alas. Your explanations help here.
You correctly guessed the meaning of a2meets, although my version
fun a2meets :: "a2pt ⇒ a2ln ⇒ bool" where
"a2meets (A2Point x y) (A2Ordinary m b) = (y = m*x + b)" |
"a2meets (A2Point x y) (A2Vertical xi) = (x = xi)"
is less pretty than yours.
I think that with your structure, I can probably fill in the rest, but in
at least one respect, I'll be just copying-without-understanding. When you
write
from PQ True have iff: "a2meets P l' ∧ a2meets Q l' ⟶ l' = l" for l'
can you tell me what the "for l' " at the end means? It appears redundant
to me, but I'm sure it's not.
--John
Email Gateway (Aug 22 2022 at 19:19):From: Thomas Sewell <sewell@chalmers.se>
Ah yes, it's really a for-all. It's another technicality. If you type a free variable in a normal lemma statement, it becomes free in the resulting theorem. The equivalent doesn't happen by default for inner statements within proof blocks because the variable scopes are a bit more complicated.
It would have been simpler if I'd stated the goal as have iff: "∀l'. a2meets P l' ∧ a2meets Q l' ⟶ l' = l"
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 19:19):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
John -
I had a go at it as well, and came up with the attached.
I didn't try to streamline it more. I am not very good at the use of the cases
feature, so things are probably more verbose here than what they need to be.
- Gene Stark
theory Question4
imports Complex_Main
begin
datatype a2pt = A2Point "real" "real"
datatype a2ln = A2Ordinary "real" "real"
| A2Vertical "real"
text "Ordinary m b represents the line y = mx+b; Vertical xo is the line x = xo "
fun a2meets :: "a2pt ⇒ a2ln ⇒ bool" where
"a2meets (A2Point x y) (A2Ordinary m b) = (y = m*x + b)" |
"a2meets (A2Point x y) (A2Vertical xi) = (x = xi)"
lemma A2_a1: "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
proof -
assume P_ne_Q: "P ≠ Q"
show "∃! l . a2meets P l ∧ a2meets Q l"
proof (cases P, cases Q)
fix px py qx qy
assume P: "P = A2Point px py"
assume Q: "Q = A2Point qx qy"
show "∃! l . a2meets P l ∧ a2meets Q l"
proof (cases "px = qx")
assume eq: "px = qx"
show "∃!l. a2meets P l ∧ a2meets Q l"
proof
show "a2meets P (A2Vertical px) ∧ a2meets Q (A2Vertical px)"
using P Q eq by simp
show "⋀l. a2meets P l ∧ a2meets Q l ⟹ l = A2Vertical px"
proof -
fix l
show "a2meets P l ∧ a2meets Q l ⟹ l = A2Vertical px"
proof (cases l)
show "⋀m b. a2meets P l ∧ a2meets Q l ⟹ l = A2Ordinary m b ⟹ l = A2Vertical px"
using P Q P_ne_Q eq by simp
show "⋀x. a2meets P l ∧ a2meets Q l ⟹ l = A2Vertical x ⟹ l = A2Vertical px"
using P by simp
qed
qed
qed
next
assume neq: "px ≠ qx"
show "∃!l. a2meets P l ∧ a2meets Q l"
proof
let ?m = "(qy - py)/(qx - px)"
let ?b = "py - ?m * px"
have *: "py = ?m * px + ?b ∧ qy = ?m * qx + ?b"
proof -
have "?m * qx - ?m * px + py = ?m * (qx - px) + py"
by argo
also have "... = qy - py + py"
using neq by simp
also have "... = qy"
by simp
finally show ?thesis by simp
qed
show "a2meets P (A2Ordinary ?m ?b) ∧ a2meets Q (A2Ordinary ?m ?b)"
using * P Q by simp
show "⋀l. a2meets P l ∧ a2meets Q l ⟹ l = A2Ordinary ?m (py - ?m * px)"
proof -
fix l
assume l: "a2meets P l ∧ a2meets Q l"
show "l = A2Ordinary ?m (py - ?m * px)"
proof (cases l)
case (A2Ordinary m b)
assume 1: "l = A2Ordinary m b"
have "py = m * px + b ∧ qy = m * qx + b"
using P Q l 1 by simp
hence "m = ?m ∧ b = ?b"
using neq by (smt "" crossproduct_noteq) ( Found with sledgehammer *)
thus "l = A2Ordinary ?m ?b"
using 1 by simp
next
case (A2Vertical x)
assume 1: "l = A2Vertical x"
then show "l = A2Ordinary ?m ?b"
(*
* This is false, something of the form A2Vertical cannot equal
* something of the form A2Ordinary (the datatype is freely generated
* by its constructors).
*
* So uniqueness fails because if l = A2Vertical x with x = px and x = qx
* then a2meets P l and a2meets Q l according to your definition.
*)
sorry
qed
qed
qed
qed
qed
qed
end
Question4.thy
Email Gateway (Aug 22 2022 at 19:19):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Oops, it is true. I was a bit too hasty and overlooked the assumption in force:
next
case (A2Vertical x)
assume 1: "l = A2Vertical x"
then show "l = A2Ordinary ?m ?b"
using 1 P Q l neq by simp
qed
(erroneous previous posting)
Email Gateway (Aug 22 2022 at 19:19):From: "Nagashima, Yutaka" <Yutaka.Nagashima@uibk.ac.at>
Hi Dr. Wenzel and other Isabelle developers,
One more note on your email, if you tick the "Proof state" box in the output panel,
you'll see that parser for structure proofs alternates
between "proof (state)" mode and "proof (prove)" mode.
Would it be possible to have this "proof state" box ticked by default in the next official Isabelle distribution?
It is a small thing that could help new Isabelle users, I think.
Last week I gave an introductory lecture about Isabelle to Mathematics students.
With the "proof state" box unticked, all the four students were confused about their proof attempts,
until I looked into their displays and told them to tick the box.
...And it was their second Isabelle session.
I saw a similar confusion when my (CS) colleagues installed Isabelle for the first time.
Regards,
Yutaka
Email Gateway (Aug 22 2022 at 19:19):From: Peter Lammich <lammich@in.tum.de>
I second this request, but I remember that, a few years ago, there were
strong arguments for using Isabelle without the output display at all,
and use mouse hovering over the squiggly lines to review errors and
warnings ... I never got used to this, in particular b/c of the waiting
time until the tooltip pops up after hovering and the keyboard/mouse
switching. It simply interferes with my workflow.
Email Gateway (Aug 22 2022 at 19:19):From: Makarius <makarius@sketis.net>
I have introduced this default some years ago specifically for new users
(notable those who have not been spoilt yet by old-style TTY-based proof
assistants). At the same time I also introduced the State dockable as
alternative to it. Current users can rather trivially arrange their
default GUI for the preferred setup: either old-style Output with proof
state enabled, or new-style State which is specifically for the proof state.
I've given several 1-2 day courses of Isabelle where the first 1/2 day
worked very well without ever showing Output or its old-fashioned proof
state within it. Recall that Isabelle/Isar is about proof documents, not
"proof scripts". So there is one main document editor where you compose
your text; everything else is somewhere in the background.
Further note that the State panel has various technological advantages
over implicit output of states via the Output panel: the State GUI can
interact more directly with the prover, without requiring changes to
commands in the text. In the next round of refinement, the State panel
will get more buttons and options to help interactive development of
proof documents in the main buffer.
The optional proof state in the Output panel will not participate in
further upgrades, and might eventually fall out of use.
Makarius
Email Gateway (Aug 22 2022 at 19:19):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
The output panel is the most useful panel in the entire display.
Maybe even more useful than the source panel.
- Gene Stark
Email Gateway (Aug 22 2022 at 19:20):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Until I read your e-mail I hadn’t known that there was a “State
dockable”: the output tab is visible by default, the state dockable is
not.
Now I tried out the State dockable and found that it showed either
nothing or the text that was also shown in the Output tab. Thus I don’t
know currently what the advantage of the State dockable over the Output
tab is.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:20):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
just as another data point.
I am currently using the approach advertised (I think) by Makarius that
Peter mentioned before, in an Isabelle course.
Up to now there was only a single (3 hour) session, but maybe the first
one is most critical.
In this session I never even opened either the output or state panels
(neither did I use "apply", for that matter).
Instead I told students to start from a proof attempt along the lines of
by (induction ...) auto
and then consult the resulting error message (click on the squiggly
underline) for what they might be missing.
By the end of the session all (18) students had solved all exercises and
I am not aware of any confusion caused by not using the output panel.
cheers
chris
Email Gateway (Aug 22 2022 at 19:20):From: Lawrence Paulson <lp15@cam.ac.uk>
I only use the output panel for one thing: the “explore” tool. (A very useful add-on: it transforms your current proof state into explicit Isar text for writing your structured proof.) That’s because the formatting is better from the output panel. I certainly hope that “explore” will find its way into a release soon.
Larry
Email Gateway (Aug 22 2022 at 19:21):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Dear all,
Big proofs related to very low level operations like proofs on VAMPasm
operations in the VerifSoft project are almost impossible without an output
panel.
Similar to any functional correctness proofs related to system level
operations.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 19:21):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
This means they have to use the mouse and explicitly close error message
windows. Such a workflow would be pretty uncomfortable for me.
In general, I’d appreciate it a lot if the Isabelle IDE could be made
more comfortable for people who mostly use the keyboard and can get on
speed with it. In particular, it would be great if the completion
mechanism could be improved.
Currently you have to wait a bit before you can complete macros for
symbols with the tab key. That’s very annoying if you are used to type
fluently, because you have to make artificial breaks in your typing. In
order to not delay your typing more than necessary, you have the
incentive to make those breaks as short as possible, but this may lead
to too short a break, with the consequence that you have to delete
several characters and start over again.
Another problem with the completion mechanism is that a completion list
sometimes pops up when you don’t need it (typically after entering a
quotation mark), and then you cannot navigate the cursor up or down.
Could this situation be improved, or are these things too much wired
into jEdit?
By the way, have there been any attempts so far to integrate Isabelle
into Vim?
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:21):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
For auto completion, there is an option somewhere in preferences that make
it faster. And sorry could not remember where exactly (emailing from my
phone).
Best wishes
Email Gateway (Aug 22 2022 at 19:21):From: Peter Lammich <lammich@in.tum.de>
Hi
In general, I’d appreciate it a lot if the Isabelle IDE could be made
more comfortable for people who mostly use the keyboard and can get
on
speed with it. In particular, it would be great if the completion
mechanism could be improved.
You can set "completion delay" to 0 in the options ... that's one of
the first things I do when I set up a new Isabelle version! The upside
is that hardcoded completions (eg unicode symbols) come up immediately.
The downside is that dynamic completions (eg lemma names) that come
from Isabelle through PIDE are not yet there ... you'll have to press
CTRL-B (or whatever shortcut you have for auto-completion), to also
make these completions appear.
Another problem with the completion mechanism is that a completion
list
sometimes pops up when you don’t need it (typically after entering a
quotation mark), and then you cannot navigate the cursor up or down.
I think you can configure this in etc/symbols. The one on quotation
marks was introduced to remember the user that cartouches should be
used where possible, instead of quots.
Email Gateway (Aug 22 2022 at 19:21):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
This is the first time I hear that inner syntax parts can be enclosed by
cartouches instead of quotation marks. That also backquotes can be
replaced by cartouches was something I learned only after using Isabelle
for several months. Could the prog-prove tutorial be updated to
reflect these new conventions? I think this tutorial is the best
document to get into Isabelle and consequently should be up to date.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:28):From: Makarius <makarius@sketis.net>
No, Isabelle is moving in the opposite direction.
I recommend HOL4 in that respect.
Makarius
Email Gateway (Aug 22 2022 at 19:30):From: Makarius <makarius@sketis.net>
See Isabelle2091-RC0/src/HOL/ex/Sketch_and_Explore.thy with these
experimental commands by Florian Haftmann. The use of Output is
accidental: since these are old-fashioned commands typed into the source
buffer, output is displayed as on a TTY.
I've recently had a private discussion with Florian about this topic.
We both agreed that the proper way is to integrate such a feature into
the State GUI panel, i.e. to continue it towards an interactive
sketchpad for goal-oriented proof development. When this happens, the
Output panel will be de-emphasized one step further (because it will
stay unchanged and not follow this trend).
Makarius
Email Gateway (Aug 22 2022 at 19:31):From: Mathias Fleury <mathias.fleury12@gmail.com>
On 5. Apr 2019, at 12:21, Makarius <makarius@sketis.net> wrote:
On 12/03/2019 17:15, Wolfgang Jeltsch wrote:
By the way, have there been any attempts so far to integrate Isabelle
into Vim?No, Isabelle is moving in the opposite direction.
As long as Isabelle supports the language server protocol, it is possible to make vim interact with Isabelle (with some limitations; e.g., there are no colours in the equivalent of the 'buffer+output buffer'). However, the integration requires some work. I don't know anything about the internals of vim, but, at least in emacs, the lack of multithreading is an issue.
Otherwise, VSCode probably has a mode with vim keybindings.
Mathias
I recommend HOL4 in that respect.
Makarius
Email Gateway (Aug 22 2022 at 19:31):From: Makarius <makarius@sketis.net>
On 05/04/2019 13:31, Mathias Fleury wrote:
As long as Isabelle supports the language server protocol, it is possible to make vim interact with Isabelle (with some limitations; e.g., there are no colours in the equivalent of the 'buffer+output buffer'). However, the integration requires some work. I don't know anything about the internals of vim, but, at least in emacs, the lack of multithreading is an issue.
I would say that is rather theoretical. A really working Prover IDE
requires a lot of polishing and finishing beyond such standardized (and
limited) protocols.
Otherwise, VSCode probably has a mode with vim keybindings.
It has one, but vim users have told me that it is not very serious. I
also see a vi mode in IntelliJ IDEA, but cannot say anything about its
quality.
Generally, one needs to understand that Isabelle came out of an Emacs
environment, but in the past 7 years that has been lost its relevance.
Since 4.5 years there is no way to get back to it.
Vi never had a role in the Isabelle community. It is a plain text
editor, not the basis of a multithreaded IDE.
Makarius
Email Gateway (Aug 22 2022 at 19:32):From: Christian Sternagel <c.sternagel@gmail.com>
Just as historic fun fact: in 2007 I supervised a bachelor project that
developed a vim plugin ("Plugvim") for interacting with "Isabelle". It
kind of worked at that time (when Isabelle itself was in the end just a
REPL), but never for serious work. Anyway, it is long forgotten (or
rather never took of in the first place) and even though I am using vim
for most everything except when working with Isabelle, I am not looking
back: The continuous and parallel proof checking and semantic
information that comes with the Prover IDE is just too valuable.
cheers
chris
Last updated: Apr 26 2024 at 01:06 UTC