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



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.