Defining inductive predicate: fun vs primrec vs inductive? · Beginner Questions

Stream: Beginner Questions

Topic: Defining inductive predicate: fun vs primrec vs inductive?

Yiming Xu (Sep 11 2024 at 08:13):

I would like to translate the following type declaration into Isabelle/HOL.

Yiming Xu (Sep 11 2024 at 08:13):

Yiming Xu (Sep 11 2024 at 08:15):

The definitions above serves for evaluating a modal formula in the basic modal language. I defined formula, frame and model in Isabelle as follows. (Is everything good up to now?)

Yiming Xu (Sep 11 2024 at 08:15):

datatype form = VAR "num"
| FALSE
| DISJ "form" "form"
| NOT "form"
| DIAM "form"

record 'a frame =
world :: "'a ⇒ bool"
rel :: "'a ⇒ 'a ⇒ bool"

record 'a model = "'a frame" +
valt :: "num ⇒ 'a ⇒ bool"

Yiming Xu (Sep 11 2024 at 08:16):

But then I think I get confused on the translation of the "satis" predicate. It seems to be a bunch of options. There are primrec, fun and inductive. Is there any consideration that I should take before picking one?

Yiming Xu (Sep 11 2024 at 08:18):

I am attempting to do "fun". I wrote:
fun satis :: "'a model ⇒ 'a ⇒ form ⇒ bool"
where
"satis M w (VAR p) = M.valt p v ∧ M.frame.world w
| satis M w FALSE = false"

And it already started complaining:
image.png

Yiming Xu (Sep 11 2024 at 08:18):

May I please ask if there is any quick fix? Thanks in advance!

Yong Kiam (Sep 11 2024 at 08:30):

I'm not so familiar with record syntax in Isabelle, but that should be valt M

Yiming Xu (Sep 11 2024 at 08:59):

Yong Kiam said:

I'm not so familiar with record syntax in Isabelle, but that should be valt M

Thanks so much! The underscore before disappears.

Yiming Xu (Sep 11 2024 at 09:00):

Now I type (world (frame M)) and it does not look correct:
image.png

Yiming Xu (Sep 11 2024 at 09:01):

The "frame" is green, and may I please ask a "human language" translation of the error message?

Mathias Fleury (Sep 11 2024 at 13:41):

= is binding to strongly. Use statis M w ... <--> ... or statis M w ... = (...)

Mathias Fleury (Sep 11 2024 at 13:41):

And it is False

Mathias Fleury (Sep 11 2024 at 13:41):

instead of false

Yiming Xu (Sep 11 2024 at 16:29):

Thanks! I changed it into False and <-->.
image.png

Yiming Xu (Sep 11 2024 at 16:30):

Any clue why it thinks "frame" is green? M.frame also does not work.

Yiming Xu (Sep 11 2024 at 16:31):

Not obvious from https://isabelle.in.tum.de/doc/isar-ref.pdf how can we extract fields of a record term.

Mathias Fleury (Sep 11 2024 at 17:42):

frame is a type, you cannot use it as a function in a term

Mathias Fleury (Sep 11 2024 at 17:42):

I do not even know what you are trying to achieve

Yiming Xu (Sep 11 2024 at 17:47):

I would like the effect to be "a model consists of a frame and a valuation". So I should be able to type M.frame to extract the field "frame" from "M" and then type (M.frame).world to extract the field "world" from the frame "M.frame". But your comment does give a hint! I have just figured out the type "model" will not take "frame" as its field. So what I need is just "world M". Thank you!

Yiming Xu (Sep 11 2024 at 18:01):

image.png

Yiming Xu (Sep 11 2024 at 18:01):

For the type declaration, I wrote:

record 'a frame =
world :: "'a ⇒ bool"
rel :: "'a ⇒ 'a ⇒ bool"

record 'a model = "'a frame" +
valt :: "num ⇒ 'a ⇒ bool"

Yiming Xu (Sep 11 2024 at 18:03):

The same recipe of writing rel M to be the field "rel" of M does not seem to work.

Yiming Xu (Sep 11 2024 at 18:03):

Sorry if it turns out to be stupid, but I am confused again.

Yiming Xu (Sep 11 2024 at 18:13):

It seems that Isabelle does not complain about rel M w v, it is complaining about te quantification.

image.png

Yiming Xu (Sep 11 2024 at 18:13):

What's wrong here?

Mathias Fleury (Sep 11 2024 at 18:17):

add parentheses. And binds too strongly

Yiming Xu (Sep 11 2024 at 18:19):

Thank you for the swift answer, it solves my problem.
image.png
Now Isabelle is happy.

Yiming Xu (Sep 11 2024 at 18:20):

(But I feel its strength to this extent is a bit weird.)

Yiming Xu (Sep 12 2024 at 03:52):

Regarding what to choose to use among fun/definition/primrec. I find an answer here:
https://courses.grainger.illinois.edu/cs576/sp2015/lectures/3-4/04-Isabelle-syntax-2x3.pdf slides 5.

Jan van Brügge (Sep 12 2024 at 18:04):

usually definition for stuff that does not recurse, fun for everything else

Jan van Brügge (Sep 12 2024 at 18:05):

there is rarely a reason to use primrec

Yiming Xu (Sep 12 2024 at 18:06):

Got it. I will just not use it for the foreseeable future then.

John Hughes (Jan 30 2025 at 14:34):

Last September, Jan van Brügge answered a question about fun/definition/primrec with the advice "usually definition for stuff that does not recurse, fun for everything else". I note from the Isar reference manual (p. 221) that

Also note that definitional packages like datatype, primrec, fun routinely declare Simplifier rules to the target context, while plain definition is an exception in not declaring anything.

Does this mean that I should be changing

definition parallel::"'l ⇒ 'l ⇒ bool"  (infix "||" 5)  where
  "parallel l m = (if (l ∈ Lines ∧ m ∈ Lines)
  then l = m ∨ ¬ (∃ P. P ∈ Points ∧ meets P l ∧ meets P m) else undefined)"

definition parallel::"'l ⇒ 'l ⇒ bool"  (infix "||" 5)  where [simp]:
  "parallel l m = (if (l ∈ Lines ∧ m ∈ Lines)
  then l = m ∨ ¬ (∃ P. P ∈ Points ∧ meets P l ∧ meets P m) else undefined)"

perhaps? Or is adding non-recursive function-definitions to the simplifier a bad idea in general? Is there any general advice here?

Jan van Brügge (Jan 30 2025 at 15:05):

Like most things, it depends. If you just want to use the definition as a shorthand, but want to automation to always look under it you can do that however at that point I would probably use abbreviation instead.
With a definition you can define theorems about the definition where you can be sure that the automation will actually be able to apply them as there is no way that the definition got expanded too early. If you do want to expand the definition for a theorem, you can just add it to the simpset for that particular spot.

Mathias Fleury (Jan 30 2025 at 17:57):

Remark that I sometimes go the opposite way and I use fun with [simp del] to not automatically get the unfolding

Mathias Fleury (Jan 30 2025 at 17:58):

fun test where
  [simp del]: ‹test (a, b) = a + b›

lemmas test_def = test.simps


lemma ‹test (A, 0) = A›
  by (simp add: test_def)

John Hughes (Jan 30 2025 at 17:58):

Following up on this, I tried to substitute a definition for a fun and it seems to break my locale definition. Here's a version with fun, which checks out OK, but if you comment that out and include the definition version, you get a type error. This baffles me (as, frankly, does anything that mentions weak types).

theory Affine_test
  imports Complex_Main
begin

locale affine_plane_data =
  fixes Points :: "'p set" and Lines :: "'l set" and meets :: "'p ⇒ 'l ⇒ bool"
  fixes join:: "'p ⇒ 'p ⇒ 'l"
  fixes find_parallel:: "'l ⇒ 'p ⇒ 'l"
begin
  fun parallel :: "'l ⇒ 'l ⇒ bool" (infix "||" 50) where
  "l || m = (if (l ∈ Lines ∧ m ∈ Lines)
  then l = m ∨ ¬ (∃ P. P ∈ Points ∧ meets P l ∧ meets P m) else undefined)"

(* replace the "fun" version of "parallel" with this one and see the next locale-description fail.*)
(*
definition parallel::"'l ⇒ 'l ⇒ bool"  (infix "||" 5)  where
  "parallel l m = (if (l ∈ Lines ∧ m ∈ Lines)
  then l = m ∨ ¬ (∃ P. P ∈ Points ∧ meets P l ∧ meets P m) else undefined)"*)

fun collinear :: "'p ⇒ 'p ⇒ 'p ⇒ bool"
    where "collinear A B C = (if A ∈ Points ∧ B ∈ Points ∧ C ∈ Points
  then (∃ l. l ∈ Lines ∧ meets A l ∧ meets B l ∧ meets C l) else undefined)"
end

locale affine_plane =
    affine_plane_data  +
    assumes
    a1a: "⟦P ≠ Q; P ∈ Points; Q ∈ Points⟧ ⟹ join P Q ∈ Lines ∧ meets P (join P Q)  ∧ meets Q (join P Q)" and
    a1b: "⟦P ≠ Q; P ∈ Points; Q ∈ Points; meets P m; meets Q m⟧ ⟹ m = join P Q" and
    a2: "⟦¬ meets P l; P ∈ Points; l ∈ Lines⟧ ⟹ find_parallel l P ∈ Lines ∧ ( find_parallel l P) || l ∧ meets P (find_parallel l P)" and
    a3: "∃P Q R. P ∈ Points ∧ Q ∈ Points ∧ R ∈ Points ∧ P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ (collinear P Q R)"
begin
end
end

Can someone explain this? And perhaps more usefully, can someone explain how I might work out for myself what's happening in situations like this in the future?

Mathias Fleury (Jan 30 2025 at 17:58):

It is useful when you want pattern matching

Mathias Fleury (Jan 30 2025 at 17:59):

~~I do not see an error, which Isabelle version is that?~~
I just replace fun by definition and it worked

Mathias Fleury (Jan 30 2025 at 18:01):

Copy-paste error:

fun parallel :: "'l ⇒ 'l ⇒ bool"   (infix "||" 50) where
definition parallel::"'l ⇒ 'l ⇒ bool"  (infix "||" 5)  where

50 vs 5

Mathias Fleury (Jan 30 2025 at 18:05):

John Hughes said:

Can someone explain this? And perhaps more usefully, can someone explain how I might work out for myself what's happening in situations like this in the future?

I got lucky to see that definition but in general I reduce the term to become as small as possible, here: term ‹f || l ∧ H›

Mathias Fleury (Jan 30 2025 at 18:05):

Then from the error message

Type unification failed

Type error in application: incompatible operand type

Operator:  (||) f :: 'l ⇒ bool
Operand:   l ∧ H :: bool

you can see how it is parsed

John Hughes (Jan 30 2025 at 18:34):

Actually not a copy-paste error --- the "definition" version comes from a different (working!) copy of very similar code, in which I reduced the priority for some reason that presumably felt very good at the time. :) Presumably there are other differences that made things work in that copy. And it's nice to know that the problem was benign, and simple enough that I could have figured it out myself if I hadn't been spooked by the warning about weak types.

Thanks!

Last updated: Feb 01 2025 at 20:19 UTC