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.