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



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

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 \<Rightarrow> a2ln \<Rightarrow> 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 \<noteq> Q \<Longrightarrow> \<exists>! l . a2meets P l \<and> a2meets Q l"
  proof -
    assume P_ne_Q: "P \<noteq> Q"
    show "\<exists>! l . a2meets P l \<and> 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 "\<exists>! l . a2meets P l \<and> a2meets Q l"
      proof (cases "px = qx")
        assume eq: "px = qx"
        show "\<exists>!l. a2meets P l \<and> a2meets Q l"
        proof
          show "a2meets P (A2Vertical px) \<and> a2meets Q (A2Vertical px)"
            using P Q eq by simp
          show "\<And>l. a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Vertical px"
          proof -
            fix l
            show "a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Vertical px"
            proof (cases l)
              show "\<And>m b. a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Ordinary m b \<Longrightarrow> l = A2Vertical px"
                using P Q P_ne_Q eq by simp
              show "\<And>x. a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Vertical x \<Longrightarrow> l = A2Vertical px"
                using P by simp
            qed
          qed
        qed
        next
        assume neq: "px \<noteq> qx"
        show "\<exists>!l. a2meets P l \<and> a2meets Q l"
        proof
          let ?m = "(qy - py)/(qx - px)"
          let ?b = "py - ?m * px"
          have *: "py = ?m * px + ?b \<and> 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) \<and> a2meets Q (A2Ordinary ?m ?b)"
            using * P Q by simp
          show "\<And>l. a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Ordinary ?m (py - ?m * px)"
          proof -
            fix l
            assume l: "a2meets P l \<and> 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 \<and> qy = m * qx + b"
                using P Q l 1 by simp
              hence "m = ?m \<and> 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



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