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



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.
>>>
> 





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