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



Hi Dr. Wenzel and other Isabelle developers,

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

Would it be possible to have this "proof state" box ticked by default in the next official Isabelle distribution?
It is a small thing that could help new Isabelle users, I think.

Last week I gave an introductory lecture about Isabelle to Mathematics students.
With the "proof state" box unticked, all the four students were confused about their proof attempts,
until I looked into their displays and told them to tick the box.
...And it was their second Isabelle session.

I saw a similar confusion when my (CS) colleagues installed Isabelle for the first time.

Regards,
Yutaka
________________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] on behalf of Thomas Sewell [sewell at chalmers.se]
Sent: Saturday, 9 March 2019 8:08 PM
To: John F. Hughes; Cl-isabelle Users
Subject: Re: [isabelle] Another newbie question...case-based 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.


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.