Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question regarding nitpick


view this post on Zulip Email Gateway (Dec 11 2020 at 09:24):

From: Leon Hansen <lhansen@uni-bremen.de>
Hello everybody,

I am currently writing my master thesis and I am trying to fetch entries
from a list that fulfil some properties. Similar to a query on a
database or an ontology.

My first approach looked like this:

datatype room = LivingRoom | Kitchen | SleepingRoom
consts connectedRooms:: "room ⇒ room ⇒ bool"
axiomatization where
 a1: "connectedRooms LivingRoom Kitchen"

lemma patheval2: "connectedRooms X SleepingRoom"
nitpick[satisfy,show_consts,user_axioms] oops

In this case nitpick answers "X = LivingRoom" even though that is not
correct.

What can i do about that?

My other approach was to avoid axiomatisation completely and use
datatypes like this:

datatype ID = NewID nat
datatype Thing = Bed (height: nat) ID
definition bed1 where
"bed1 ≡ Bed 2 (NewID 1)"
definition bed2 where
"bed2 ≡ Bed 8 (NewID 3)"
definition bed3 where
"bed3 ≡ Bed 2 (NewID 5)"
definition bedList where
"bedList ≡ [bed1, bed2, bed3]"
lemma "List.filter (%c::Thing. ∃x. c = (Bed 2 (NewName x))) bedList =
res" nitpick sorry

However this becomes very slow for larger lists. Is there a way to do
this more efficiently?

Kind regards

Leon Hansen

view this post on Zulip Email Gateway (Dec 11 2020 at 12:11):

From: "John F. Hughes" <jfh@cs.brown.edu>
I believe that the problem here is that you've specified what
"connectedRooms" does only when applied to LivingRoom and Kitchen, but
have not specified its value on any other pair of rooms. Nitpick says "Hey,
assigning "connectedRooms LivingRoom SleepingRoom" to be "true" is
consistent with all the axioms. I guess I'm done!"

So axiom 1 needs to be much richer --- either a complete enumeration of the
9 possibilities, or something with an "if" that says "if we're in this one
special case, then true; otherwise false."

NB: You could additionally specify a symmetry axiom ---

connectedRooms a b => connectedRooms b a [I'm forgetting the correct
syntax here]

and then safely have an enumeration of only 6 items instead of all 9.

-John

view this post on Zulip Email Gateway (Dec 11 2020 at 12:24):

From: Leon Hansen <lhansen@uni-bremen.de>
I do have the reflexivity and transitivity in there already:

axiomatization where
  refl: "connectedRooms x x" and
  trans: "connectedRooms x y ∧ connectedRooms y z ⟶ connectedRooms x z"

I just shortend the example by a lot. For that reason it is not possible
to list every possibility as well.

I would need to add something like the "connectedRooms _ _ = False" that
would work if it were a function and not an axiomatisation.

-Leon

view this post on Zulip Email Gateway (Dec 18 2020 at 14:55):

From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Leon,

My first approach looked like this:

datatype room = LivingRoom | Kitchen | SleepingRoom
consts connectedRooms:: "room ⇒ room ⇒ bool"
axiomatization where
a1: "connectedRooms LivingRoom Kitchen"

lemma patheval2: "connectedRooms X SleepingRoom" nitpick[satisfy,show_consts,user_axioms] oops

In this case nitpick answers "X = LivingRoom" even though that is not correct.

Although it doesn't correspond to your expectations, Nitpick's behavior is correct. Your "nitpick" command is asking for a model of the formula. Nitpick finds one. In that model, "connectedRooms LivingRoom SleepingRoom" is true. This is perfectly consistent with your axiomatization. It is not entailed by the axiomatization, but it is clearly consistent with it.

If you want to find a value X such that "connectedRooms X SleepingRoom" is provable -- in other words, a witness for X in "EX X. connectedRooms X SleepingRoom", I'm afraid there's no tool that will reliably give you that in Isabelle. The existential formula would be a candidate for Sledgehammer, but in general you wouldn't get the witness out of the proof.

Is there a way to do this more efficiently?

The problem is that I don't clearly understand what "this" refers to. I'm starting to suspect that your axiomatization above is wrong; you probably also want to say "~ connectedRooms LivingRoom SleepingRoom" etc., if you mean that these are not connected. (Otherwise, they'll be connected in some models of the formulas and not in others.)

Typically a better approach is to avoid low-level mechanisms such as "consts" and "axiomatization" and instead rely on the definitional mechanisms, like "inductive" (which is probably your best option here), "fun", and "definition". With "inductive", what you don't explicitly make true is automatically false, which is very convenient. You also don't need to worry about models; there's only one model.

I hope this helps.

Cheers,

Jasmin

view this post on Zulip Email Gateway (Dec 19 2020 at 10:03):

From: Leon Hansen <lhansen@uni-bremen.de>
Dear Jasmin,

thank you for your detailed response.

If you want to find a value X such that "connectedRooms X SleepingRoom" is provable -- in other words, a witness for X in "EX X. connectedRooms X SleepingRoom", I'm afraid there's no tool that will reliably give you that in Isabelle. The existential formula would be a candidate for Sledgehammer, but in general you wouldn't get the witness out of the proof.
That confirmation is very helpful for me. I thought I was just doing it
completely wrong.
The problem is that I don't clearly understand what "this" refers to.
My goal is to embed knowledge from an owl ontology in an Isabelle theory
and be able to retrieve it again in reasonable time.
Typically a better approach is to avoid low-level mechanisms such as "consts" and "axiomatization" and instead rely on the definitional mechanisms, like "inductive" (which is probably your best option here), "fun", and "definition". With "inductive", what you don't explicitly make true is automatically false, which is very convenient. You also don't need to worry about models; there's only one model.

That is more or less what i did in my second approach where i used
"datatype" and "definition" only. Thank you for the tip with
"inductive". For small theories nitpick returns the requested
information reliably and fast. For theories with a few hundred lines it
was taking way to much time. I hoped there was a simple way to limit
nitpicks search space and speed up the search for witnesses for X in "EX
X. connectedRooms X SleepingRoom" for example.

Kind regards,

Leon


Last updated: Sep 25 2021 at 09:17 UTC