*To*: cl-isabelle-users at lists.cam.ac.uk, "John F. Hughes" <jfh at cs.brown.edu>*Subject*: Re: [isabelle] Another newbie question...case-based proofs*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Sat, 9 Mar 2019 16:58:08 -0500*In-reply-to*: <69fc6488-5305-7831-8fef-3e01fa3f66c3@starkeffect.com>*References*: <CAJ=ZMJK4d0xDP4ULTqEFWwXcHdfPN4yLVqRdPV_nht9VHAWbkQ@mail.gmail.com> <2315a38013d645bfa7ed4a7a37948817@chalmers.se> <CAJ=ZMJLT2V_aA2FtsaoQNz0shuVZgcUYMVO7GSN+aKQre+Eznw@mail.gmail.com> <b37ec21f186c4e609d0bfe68b676c422@chalmers.se> <69fc6488-5305-7831-8fef-3e01fa3f66c3@starkeffect.com>*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.5.1

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) > 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 > On 3/9/19 3:57 PM, Eugene W. Stark wrote: > 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 > > On 3/9/19 2:52 PM, Thomas Sewell wrote: >> 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. >> >> ________________________________ >> From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of John F. Hughes <jfh at cs.brown.edu> >> Sent: Saturday, March 9, 2019 8:30:55 PM >> To: Cl-isabelle Users >> Subject: Re: [isabelle] Another newbie question...case-based proofs >> >> 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 >> >> On Sat, Mar 9, 2019 at 1:08 PM Thomas Sewell <sewell at chalmers.se> wrote: >> >>> 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-bounces 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. >>> >

**References**:**[isabelle] Another newbie question...case-based proofs***From:*John F. Hughes

**Re: [isabelle] Another newbie question...case-based proofs***From:*Thomas Sewell

**Re: [isabelle] Another newbie question...case-based proofs***From:*John F. Hughes

**Re: [isabelle] Another newbie question...case-based proofs***From:*Thomas Sewell

**Re: [isabelle] Another newbie question...case-based proofs***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] Another newbie question...case-based proofs
- Next by Date: Re: [isabelle] References about mistakes and gaps in papers
- Previous by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Next by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Cl-isabelle-users March 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list