[isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem



First, I ask a straightforward question.

If I declare a type, such as

    typedecl sT,

am I effectively creating a non-empty set, which has a power set associated with it? I've read several times that a type can be interpreted as a non-empty set.

Second, I try to bump up the value of this email with some setup information for Nitpick and Sledgehammer. I'm in the "learn how to setup and use Nitpick and Sledgehammer" mode. I'm almost out of it, but I try to explore it in depth so that when I get back to the drudgery of working through tutorials and exercises, I know how to use these automated tools for my own tangents. And, certain logics can never be used to prove their own consistency, so I might as well run Nitpick on everything, and to check the more likely scenario that I've introduced inconsistency.

Third, if you want to read that far, I have a type, a constant, a predicate, one axiom, and one theory, and I get a counterexample from Nitpick. The answers to my questions on that may be obvious, but I ask them anyway. Not understanding subtleties can cause me to have a too simple view of the universe, which might take me months to find out.

NITPICK STUFF

If you run "nitpick [verbose]" under a theorem, you'll get this message (at least for Cygwin):

The following solvers are configured: "MiniSat_JNI", "CryptoMiniSat_JNI", "Lingeling_JNI", "SAT4J", "SAT4J_Light".

Jasmine Blanchette rates these SAT solvers like this:

"SAT4J is very slow, but the others are roughly equivalent, with Lingeling slightly better than CryptoMiniSat, and CryptoMiniSat slightly better than vanilla MiniSat."

Though CryptoMiniSat_JNI and Lingeling_JNI show up, to use them you need Kodkodi 1.5.2, from Blanchette's site:

http://www4.in.tum.de/~blanchet/#software <http://www4.in.tum.de/%7Eblanchet/#software>

The install instructions for a Kodkodi upgrade are on page 3 of nitpick.pdf.

If you want to be compulsive, after setting some options with something like "nitpick_params [verbose,timeout=120,user_axioms=true]", which will also lists how all the options are set in the output window, you can run all the SATs under a theorem with something like:

  nitpick[verbose,user_axioms,sat_solver=MiniSat_JNI]
  nitpick[verbose,user_axioms,sat_solver=CryptoMiniSat_JNI]
  nitpick[verbose,user_axioms,sat_solver=Lingeling_JNI]
  nitpick[verbose,user_axioms,sat_solver=SAT4J]
  nitpick[verbose,user_axioms,sat_solver=SAT4J_Light]

SLEDGEHAMMER STUFF

On Jasmin's site are also the upgrades to the Sledgehammer solvers CVC3, E, SPASS, and Z3. So far, I haven't been big on wanting to change the default Isabelle2012 distribution, but I'll work on doing this, which will keep me in the "learn the auto-tools mode" for another day.

In the folder Isabelle2012/contrib, you can see the versions of Kodkodi, CVC3, E, SPASS, and Z3 to see what versions you have.

SLEDGEHAMMER YICES

Working hard to do more than ask questions, I am the official liaison of important, breaking news on [isabelle-dev], which is a joke, of course.

Put YICES_INSTALLED="yes" in your "~/Isabelle2012/etc/settings" file, and yices will be one of the available solvers when you use the command "sledgehammer supported_provers" under a theorem. The pertinent thread is "sledgehammer / yices":

http://www.mail-archive.com/search?q=sledgehammer+%2F+yices&l=isabelle-dev%40mailbroy.informatik.tu-muenchen.de <http://www.mail-archive.com/search?q=sledgehammer+%2F+yices&l=isabelle-dev%40mailbroy.informatik.tu-muenchen.de>

NITPICK'S COUNTERX: PENCIL & PAPER LOGIC vs. ISABELLE'S LOGIC

The foundation of the traditional "pencil & paper" logic can never be exactly the same as Isabelle's logic foundation. Our brain maps formulas to a value of either true or false. Isabelle uses typed lambda calculus to map formulas to true or false. I understand that the two lowest-level foundations for the two logics aren't exactly the same.

Suppose I have an "extreme minimalist ZF sets logic". I've been given the same logical symbols, the same non-logical symbols, and the same rules for using them as ZF sets.

I write one formula as an axiom, "(1) there exists a set which contains no elements", (? x. ! y. ~(y IN x)).

I write one formula as a theorem, "(2) the set described by (1) is unique", (! u. ((! x. ~(x IN u)) --> u = emptyS)).

Setting aside that I'm taking liberties with (2) by using a constant name, though I can't prove (2) because I haven't defined "=" with an axiom, I would be very surprised if someone told me that a counterexample could be found for (2) using the single formula of (1), which is all that's available to be used. Well, not quite. The FOL specification requires that "=" is given as a logical symbol, but I do need some sets available for a counterexample.

Alright, but with Isabelle, I can never be so minimalist. My minimalist logic on top of HOL needs a declared type, and the "=" is given as the FOL logical symbol which is (partly or fully) axiomatized by four axioms starting at line 196 of src/HOL/HOL.thy. I understand the first 2 axioms, but not the second 2.

My logic needs a declared type, "typedecl sT", and I assume I effectively introduce a non-empty set by doing that, which means there are sets available for a counterexample.

I show my minimalist world below and I attache it as a file. The theorem "emS_is_unique1" fails Nitpick. After "=" is defined for sets, "emS_is_unique2" doesn't fail Nitpick, and is proved by metis.

Some responses, whether sent or thought, might be:

"There's not a problem, don't make a mountain out of a molehill. Define equality like you have to do anyway."

Or, "If a consistency results because your setup is too simplistic, you'll probably find out. If it takes you 6 months to find it out, well, that's the cost of doing business in the world of proof assistants."

Regards,
GB

theory sTs_Empty_Exist_Nitpick
imports Main
begin
declare[[show_brackets=true]]
typedecl sT
consts emS::sT
consts inS::"sT => sT => bool" (infixl "IN" 55)

axiomatization where
  eeA:"!x. ¬(x IN emS)"

theorem emS_is_unique1:
  "!u. (!x. ~(x IN u)) --> u = emS"
  nitpick[verbose,user_axioms] oops

axiomatization where
  exA: "!u. !v. ((!x. x IN u <-> x IN v) --> u = v)"

theorem emS_is_unique2:
  "!u. (!x. ~(x IN u)) --> u = emS"
  by (metis eeA exA)
end







theory sTs_Empty_Exist_Nitpick
imports Main
begin
declare[[show_brackets=true]]
typedecl sT
consts emS::sT
consts inS::"sT => sT => bool" (infixl "IN" 55)

axiomatization where
  eeA:"!x. \<not>(x IN emS)"

theorem emS_is_unique1:
  "!u. (!x. ~(x IN u)) --> u = emS"
  nitpick[verbose,user_axioms] oops

axiomatization where
  exA: "!u. !v. ((!x. x IN u <-> x IN v) --> u = v)"

theorem emS_is_unique2:
  "!u. (!x. ~(x IN u)) --> u = emS"
  by (metis eeA exA)
end


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