Re: [isabelle] Another newbie 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.



fun pt_x :: "a2pt ⇒ real" where
  "pt_x (A2Point x y) = x"

fun pt_y :: "a2pt ⇒ real" where
  "pt_y (A2Point x y) = y"

  "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)
  from meets iff show ?thesis
    by auto
  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)
  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'
  from meets iff show ?thesis
    by auto

From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of John F. Hughes <jfh at>
Sent: Saturday, March 9, 2019 6:44:04 PM
To: Cl-isabelle Users
Subject: [isabelle] Another newbie 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
    case False
    then show ?thesis sorry

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