Re: [isabelle] Another newbie question...case-based proofs



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

> On 12 Mar 2019, at 08:24, Christian Sternagel <c.sternagel at gmail.com> wrote:
> 
> 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
> 
> On 3/11/19 7:00 PM, Peter Lammich wrote:
>> 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.
>> 
>> --
>>   Peter
>> 
>> 
>> On Mo, 2019-03-11 at 17:33 +0000, Nagashima, Yutaka wrote:
>>> 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
>>> ________________________________________
>>> From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bo
>>> unces at lists.cam.ac.uk] on behalf of Thomas Sewell [sewell at chalmers.se
>>> ]
>>> Sent: Saturday, 9 March 2019 8:08 PM
>>> To: John F. Hughes; Cl-isabelle Users
>>> Subject: Re: [isabelle] Another newbie question...case-based proofs
>>> 
>>> 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
>>> 
>>> 
>>> 
>>> ________________________________
>>> From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bo
>>> unces at lists.cam.ac.uk> on behalf of John F. Hughes <jfh at cs.brown.edu>
>>> Sent: Saturday, March 9, 2019 6:44:04 PM
>>> To: Cl-isabelle Users
>>> Subject: [isabelle] Another newbie question...case-based proofs
>>> 
>>> 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
>>> 2. Where x0 is not equal to x1, in which case I can compute the slope
>>> and
>>> intercept and construct an ordinary line to show existence.
>>> 
>>> 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.
>> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.