Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



On Wed, 30 May 2012, Bill Richter wrote:

I'd be happy for you to post there about miz3 ocaml dirty code cache issues.

Better not. I did not really follow that detail of this highly complex thread. It is part of the miz3 philosophy to do things in a certain way, and Freek has a right to take his preferred way.


  The Isabelle/Pure framework is centered around higher-order natural
  deduction, and Isabelle/Isar as a proof language continues these
  ideas. To understand these things properly, you should first blot
  out "FOL", then get used to Pure + Isar, then add HOL as
  object-logic, and then rediscover what predicate logic (including
  FOL) will do for you here via some add-on tools.

I'm not opposed to learning Pure + Isar, but it would be a whole lot
easier for me to learn if I knew in advance how it related to FOL,
which as a mathematician I have a rudimentary (but not practical)
understanding of.

In my rough "education plan" above, the relation to FOL was the last step, not the first one. It is easier to get started with a clear mind.


 Let me make a rudimentary FOL point:

I think writing down strict axiomatic FOL proofs would really be
tedious because e.g. you have manually substitute variables every time
you want to use an axiom.  I don't have a full list of the tedium
strict FOL can cause.  But I'm only willing to write up FOL-type
proofs if the proof assistant will automate that tedium.  Do similar
issues arise with Pure + Isar?

I can only guess what you mean by "strict axiomatic FOL proof". There are many ways to define what a logical inference system is, and how proofs are done.

In Isabelle Pure it is done over lambda-calculus as syntax, and via backchaining of natural deduction rules with implicit unification to solve the instantiation problems arising here. BTW, Isar means "Intelligible semi-automated reasoning", because the only proof automation built into the proof language is unification, which is typically used together with implicit selection of rules from the context (library etc.) as determined from the structure of the text. That's the whole secret of it.

Any other proof automation is quoted explicitly in the Isar text, via "proof methods": blast, simp, auto, metis, smt, ... ad infinitum. You go to the store and order the kind of washing machine you prefer, or do things purely by hand ...


Also, as you may have observed on hol info, I know next to nothing
about HOL.  Basically I understand the 20 pages of set theory John
explains in his reference manual.  Isn't Isabelle HOL much the same as
HOL as in HOL Light HOL?  Where is a good place to learn about HOL?

You should not spend to much time with that. If you take HOL as a simplified version of set-theory with explicit syntactic types it is OK as a start. Foundationally, HOL is not so interesting than it was in 1940 or 1950.


  In principle any of the HOL systems could provide their own locale
  mechanism, or something similar.  It is not possible to "just" do
  it, though.  Isabelle has required 10+ years to get this all done
  right. It is also a matter of culture.  John Harrison would
  certainly not add such complexity to his system.  You have to use
  Isabelle or Coq for such sophisticated module concepts, or maybe
  Mizar.

Sure, but I really dislike the Mizar type system, and I want to
lightly typed sets to avoid any hard typing.

Note that HOL typing is particularly hard. Every type is its own isolated universe, although a rather small one. You need explicit morphisms to travel between such distinct worlds.


  > But instead we could look at all models of Tarski's axioms, a
  > model being some sets and functions with some properties.  Can
  > you do this in Isabelle too?

  If this means you want to study the meta-theory of Tarski axioms,
  then any of the HOL systems -- Isabelle/HOL included -- can do this
  for you, if you define the syntax and inference system more
  concretely (via datatypes and inductive relations).

Great, but I don't know what meta-theory means.  A model of Tarski's
geometry axioms is be a set S (of points), a 3-ary relation Between on
S and a 4-ary relation Equiv on S satisfying Tarski's axioms (so far I
only use his first 7 axioms, and you coded them up in Isabelle).  So
there might be a predicate TarskiModel(S, Between, Equiv), and
theorems in a Tarski model would begin

You get such a predicate already from the locale tarski_first7 that I've produced for you. It is called "tarski_first7" and can be used within the logical language:

  term "tarski_first7"

The system will check that and print the most general type for it:
"('a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ bool". You can also hover over the formal term to get it explained.

Note that the type is naturally curried as everything by default in Isabelle Pure -- just like in good HOL families.

Moreover your carrier set S is actually modeled as a type here, in the usual manner in HOL. You can relativize it to a set over the base type, but that is a different story of the larger HOL family.


assume TarskiModel(S, Between, Equiv)...

This is what the locale context "begin" does for you implicitly, and then you start to define derived things and state theorems and do proofs from it. This means you are developing a concrete "theory", but this is not meta-theory.

Meta theory means you speak about things, by stepping aside or outside from it. Here is an arbitrary example from AFP, which I have happened to have browsed two weeks ago with a student: http://afp.sourceforge.net/entries/Completeness.shtml

The example develops the logical inference system and semantics of a version of first-order logic in the usual way, almost literally from the book (I don't know which one). There are just the usual formalization tweaks to represent it as concrete formal things inside HOL (and a slight tendency of redundant copies of basic mathematical HOL concepts used in the development).


I don't understand HOL well enough to actually pull this off, but John
explained how to get started.  My point is that I don't think any
typing is involved here, beyond maybe something rudimentary like

new_type("point",0);;
new_type_abbrev("TarskiPlane",`:point->bool`);;

That is a global axiomatic theory. In Isabelle/HOL is would look like this:

axiomatization
Cong :: "point ⇒ point ⇒ point ⇒ point ⇒ bool" ("_ _ ≐ _ _" [1000, 1000, 1000, 1000] 50) and
  Cong3  ("_ _ _ ≐≐ _ _ _" [1000, 1000, 1000, 1000, 1000, 1000] 50) and
  Bet :: "point ⇒ point ⇒ point ⇒ bool"
where
  Cong3_def: "a b c ≐≐ x y z ≡ a b ≐ x y ∧ a c ≐ x z ∧ b c ≐ y z"
    and A1: "a b ≐ b a"
    and A2: "a b ≐ p q ⟹ a b ≐ r s ⟹ p q ≐ r s"
    and A3: "a b ≐ c c ⟹ a = b"
    and A4: "∃x. Bet q a x ∧ a x ≐ b c"
    and A5: "a ≠ b ⟹ Bet a b d ⟹ Bet a' b' d' ⟹ a b c ≐≐ a' b' c' ⟹
      b d ≐ b' d' ⟹ c d ≐ c' d'"
    and A6: "Bet a b a ⟹ a = b"
    and A7: "Bet a p c ⟹ Bet b q c ⟹ ∃x. Bet p x b ∧ Bet q x a"

Showing that publicly on isabelle-users, most people should frown upun it -- shudder. There are all these sophisticated ways to make things local in Isabelle ...


	Makarius


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