Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

On Fri, 25 May 2012, Bill Richter wrote:

Makarius's port proved a theorem that's false, the last theorem below,
C1.  The problem seems to be Makarius's axiom

A5: "a ≠ b ⟹ Bet a b c ⟹ Bet a' b' c' ⟹ a b c ≐≐ a' b' c' ⟹
     b d ≐ b' d' ⟹ c d ≐ c' d'"

I think this is my error, from my Isabelle file 6Tarski.thy, which I
think I posted here.  My deepest apologies!  I should have written

and A5: "∀ a b c d a' b' c' d' . not(a = b) ∧ B a b d ∧ B a' b' d'
             ∧ a b ≡ a' b' ∧ b c ≡ b' c' ∧ a d ≡ a' d' ∧ b d ≡ b' d'
                       =⇒ c d ≡ c' d'"

which is basically Tarksi's version of the SAS axiom (which Tarski
cleverly defined without having angles!), which I got right in miz3

Of course the theorem was true under the given assumptions. It happens routinely in formalizations that something else is formalized than expected. This is why unguarded axiomatizations are so dangerous. Here we made a locale definition instead, and in the worst case the corresponding predicate tarski_first7 could turn out to be always False, not more no less.

I made the change, and now jedit gives an error, with do-not-enters on the last 4 lines:

 with neq Bet Bet have "y x ≐ y y" using `b x ≐ b y` by (rule A5)
 then show ?thesis by (rule A3)


So I uncommented the assumption
   and "Bet a b x"
but I still get these 4 do-not-enters.  Uh, would you try try again?

Here is my proof with the amended locale definition:

lemma C1:
  assumes neq: "a ≠ b"
    and Bet1: "Bet a b y"
    and Bet2: "Bet a b x"
    and b: "b x ≐ b y"
  shows "y = x"
proof -
  have "y x ≐ y y"
  using neq Bet2 Bet1 _ b
  proof (rule A5)
    show "a b y ≐≐ a b y" ..
  then show ?thesis by (rule A3)

We are doing precise single step reasoning here, which means all the slots for the rules need to be filled in the correct order. This is not Mizar or any of the Mizar modes for HOL, which are centered around classic predicate logic with some builtin proof automation to bridge larger gaps.

Note that the precise natural deduction of the Pure Isar proof has exhibited the mistake in the A5 specification, in the first place.

A few things confuse me about your code, e.g.

 defines "a b c ≐≐ x y z ≡ a b ≐ x y ∧ a c ≐ x z ∧ b c ≐ y z"

So ≡ means "if and only if", which in HOL-Light is <=>?

No it is Pure equality. Unlike 'definition', the 'defines' element cannot work with object-level =.

Two of Tarski's first 7 axioms are constructive (some point x exists),
A4 and A7, and you proved rules for them, using what I thought was a
very powerful automation tool blast:

lemma A4_rule: obtains x where "Bet q a x" and "a x ≐ b c"
 using A4 by blast

and then used A4 by e.g. writing

obtain x where x: "Bet q a x" "a x ≐ a a" by (rule A4_rule)

Hmm, you don't have to do that in Mizar or Freek's miz3.

The locale definition only allows closed Pure rule statements, not the open Isar form with fixes/assumes--shows/obtains, so I proved them as lemmas later on in the context. By doing that, the heavy-duty classical reasoning of blast was clearly isolated in some derived rules. In Mizar or miz3, it would have intruded the proof, and the mistake in your A5 would not have been discovered. (You did not have it in the miz3 version that you sent me, but in the Isabelle attempt.)

Let me explain why your last result shouldn't be true:

lemma C1:
 assumes neq: "a ≠ b"
   and Bet: "Bet a b y"
(*  and "Bet a b x"    -- "FIXME unused"  *)
   and "b x ≐ b y"
 shows "y = x"
proof -
 have 1: "a b ≐ a b" ..
 have 2: "b y ≐ b y" ..
 have "a b y ≐≐ a b y" ..
 with neq Bet Bet have "y x ≐ y y" using `b x ≐ b y` by (rule A5)
 then show ?thesis by (rule A3)

Tarski's axioms hold in the plane R^2, in which the result means this.

Let `l' be the line containing two distinct points `a' and `b'.  Take
`y' to be a point on `l' so that b is between a and y.  (That means
that y can equal b.)   Now take a point x in the plane so that
length bx = length by.
Then x = y.

Of course that's false (unless y = b). There's a whole circle of such points x, with center b and radius length by.

That is an informal argument. It merely motivates why something in the formalization had to be amended.


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