# [isabelle] Sledge and 0; green & blue; ATPs lovin' quantifiers

Hi,

`Embarrassing mistakes are embarrassing, but green and blue variables can
``help prevent them, at least if you don't tell others.
`

`It's in the story below that I tell about going from vaguely noticing
``blue variables when I edit a formula, to discovering another great
``feature of jEdit, that green variables are bound variables and blue
``variables are free variables. Did I know that? If I did, I forgot it.
`

`Color coded variables even help with respectable mistakes, like when I
``go through and change all my variables for a different naming convention.
`

`Since starting this email, I noticed another blue variable that
``should've been green. Yet, in spite of the misnamed variable, the
``theorem was still true.
`

`It's always a scary thought when Sledgehammer proves a theorem which
``isn't what I think it is.
`
*FORMAL PROOFS FORCING THE EXPLICIT USE OF THE SEPARATION AXIOM*

`(This is a tangent. I had led into it from the last section, but then I
``deleted a lot of the last section. It follows the general pattern of,
``"Dude, this is great stuff.")
`

`In real life, there's the Axiom of Separation, which requires we use a
``set which already exists to create new sets, but most every one is
``oblivious to it.
`

`Set theorists are a rare breed of people, but I know one who was a
``former professor. I emailed him and asked, "Trey, everyone is oblivious
``to the Axiom of Separation, which requires both an existing set and a
``property, but most people mindlessly only specify the property. How many
``proofs do you think are out there where they think they're using a set,
``but they're really using a class?"
`

`He emailed me back a simple response. He said, "Well, most people are
``working in the big areas of math, like algebra and real analysis, so the
``sets they're using have been proved to exists, so those people are safe."
`

`The great thing about formal proofs, as things are turning out, is that
``I can force the code to always require the explicit use of the Axiom of
``Separation.
`

`Do you want to use my set builder notation? Then you have the choice of
``{A. P} or the more traditional notation {x IN A. P x}. Either way, you
``explicitly have to specify the set A that you're going to get your
``elements from, where A is tied into the axiom
`
!A. !P. ?B. (!x. x IN B <-> (x IN A & P x)).
BACK TO THE BLUE VARIABLE
So for a simple example, I had,
!q. empty_set not_in {x IN u. x notEq empty_set}

`where "u" was blue. It turned out the same, since "q" wasn't used and
``"u" is a free variable, but it's definitely bad style.
`
*NON-EMPTY SETS & SLEDGE NOT MAKING THE CLASSIC HUMAN MISTAKE*

`Today, the blue variable awareness came because I ran Sledgehammer on an
``existence theorem. Like many times, multiple ATPs gave multiple results,
``where the axioms and theorems used by the different ATPs fell into groups.
`

`First, here's the ATPs which regularly produce results for the FOL heavy
``theorems I'm doing:
`
metis, vampire, e, spass_new, remote_e_sine, z3_tptp, and z3.
And frequent enough to notice:
satallax, cvc3.
And not frequent, but not totally absent, like other ATPs:
yices.

`Anyway, I think it was vampire which proved the existence of unordered
``pairs using only the existence of the empty set.
`

`I said, "That's no good. What a classic mistake, to forget about the
``trivial case of the empty set."
`

`I added the condition that my set is non-empty, and I had a "by(auto)"
``below them theorem, and auto proved the theorem after I edited it.
`
I said, "That's no good."

`Well, I had made another classic mistake. There were two "z"s, where one
``was outside the scope of the quantifier, where it originally had been
``inside the scope.
`

`It was at this point that I noticed one green "z" and one blue "z". I
``thought, "That Makarius, giving us green variables and blue variables,
``is that great, or what?"
`
*A BLUE VARIABLE EXAMPLE ANSWERS A FORMER QUESTION*
This eventually tied into me trying to sort out some set notation.

`From Set.thy, I got this the basic idea for this notation for my
``ordered pairs function, S_se :: "sT => (sT => bool) => sT":
`
"{q. P}" == "CONST S_se q P"
"{x : q. P_x}" => "{q. (%x. P_x)}"

`This is simple stuff, but everything is hard until you understand it, so
``I was working through some examples where I was starting with the set
``builder notation, {x : q. P_z}, and translating into the two other
``equivalencies, where it's all related to the formula
`

` !q. !z. z IN {x : q. P_x} <-> (z IN q /\ (%x. P_x) z) <-> z IN
``{q. P}.
`

`One of the main things I was trying to explain was the relationship
``between P_x and P.
`

`Basically, P_x is a first-order formula with a free variable x, so what
``happens if I make a mistake? And don't name my free variable x?
`
I worked up my trivial examples, the first being
(1) theorem "{0} = {x : {0}. x = 0}"
by(metis singleton_as_a_separation_set),
where 0 is the empty set, and P_x == (x = 0)

`Now, my fluency in the Isar proof language is comparable to my fluency
``in Spanish, where I know how to say "by auto" and "by metis", along with
``"burrito", "taco", hombre, and adios. So I'm much more ahead in Spanish
``than I am in Isar, but I'm learning things about Isabelle that I need to
``learn anyway, and I'm not stuck now completely in tutorial purgatory.
`

`Sledgehammer makes mincemeat out of (1), so I messed it up so there's a
``blue variable, y, which results in a false variation of (1):
`
(2) theorem "~(!y. {0} = {x : {0}. y = 0})"
by(metis (mono_tags) Ax_P separation_set_uniqueness).

`I put the quantifer in to show effectly what happens when my P_x == (y =
``0), which results in no free variable x in P_x.
`*
THIRD BIG LESSON: FIRST-ORDER ATPs WANT FIRST-ORDER LOGIC*

`There was the lesson on remembering to consider the trivial case of the
``empty set.
`

`There was the lesson of getting visual feedback to see if my variables
``are bound or free.
`

`The third lesson had to do with my past question, up until today, of
``whether to leave a variable free, or make it a bound universally
``quantified variable.
`

`This was no small question, and my inclination was to go through the
``formalities for a while of explicitly using universal quantifiers, and
``then loosening up and using free variables.
`
It's all the same, right?

`No. All the ATPs above that easily proved (2) timed out on the version
``that has a free variable, which is this theorem:
`
theorem "~({0} = {x : {0}. y = 0})"

`Maybe there's something I'm missing, but what I'm thinking is that the
``ATPs that are good at proving FOL, work best when they're given explicit
``FOL.
`

`If that's what they want, who am I to deny them what they want? I do
``what I can to make ATPs happy, so they'll help me out.
`
Regards,
GB

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