Stream: Beginner Questions

Topic: Why it seems like Isabelle does not get my definition

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:19):

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


fun demodalize :: "form ⇒ form"
  where
    "demodalize FALSE = FALSE"
  | "demodalize (VAR p) = VAR p"
  | "demodalize (DISJ form1 form2) = DISJ (demodalize form1) (demodalize form2)"
  | "demodalize (NOT form) = NOT (demodalize form)"
  | "demodalize (DIAM form) = demodalize form"


fun propform :: "form ⇒ bool"
  where
   "propform FALSE = True"
 | "propform (VAR p) = True"
 | "propform (DISJ f1 f2) = (propform f1 ∧ propform f2)"
 | "propform (NOT f) = propform f"
 | "propform (DIAM f) = False"

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:19):

Problem is:

lemma propform_demodalize : "propform (demodalize f)"
proof (induct rule:form.induct)
  case (VAR x)
  then show ?case by simp
next
  case FALSE
  then show ?case by simp
next
  case (DISJ x1a x2)
  then show ?case by simp
next
  case (NOT x)
  then show ?case by simp
next
  case (DIAM x)
  then show ?case sorry
qed

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:20):

"propform" says a modal formula is a propositional formula. "demodalize" discards all modal operators "DIAM" of a formula.

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:21):

It seems like it does not understand the definition of demodalize because it thinks I should prove:
image.png

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:25):

It seems to completely ignore the "demodalize", and asks to prove every formula is propositional. Here is the goal list generated:
image.png

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:25):

It should not happen and may be my stupid, but I do not see now.

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:42):

Specify the variable you are doing induction on instead of letting Isabelle guessing it (which sometimes like here goes wrong)…

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:43):

Actually (induction rule: demodalize.induct) is probably the most natural induction principle and then the guess is correct… ah no

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:44):

But here is only one variable? What does it guess?

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:45):

image.png

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:45):

Mathias Fleury said:

Actually (induction rule: demodalize.induct) is probably the most natural induction principle and then the guess is correct… ah no

Why no ... Let me try.

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:45):

it still picks the wrong thing

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:46):

If I write "(induct f rule:form.induct)" instead, it does work!

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:46):

I am just curious why it can even make a wrong guess.

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:46):

Small list of stupid thinks to induce on:

apply (induction "demodalize f")
apply (induction "propform f")
apply (induction "propform (demodalize f)")
apply (induction "demodalize (demodalize f)")

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:47):

all of these inductions are possible

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:47):

and the induction has some heuristics to pick the right one

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:47):

Ah? I told it to use rule: form.induct.

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:47):

Yeah and? form.induct works on everything of type form

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:47):

image.png

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:48):

So Isabelle is not doing unification with the theorem in the screenshot?!

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:48):

sure it does

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:49):

but there are many possible P

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:49):

P is the whole goal, right? I am proving by induction on propform (demodalize f).

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:50):

Take P = %_. propform (demodalize f)

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:50):

then you are doing induction on a variable that is not in the goal

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:51):

Oh it then thinks the f is a fixed free variable... And want to unify with "!x. propform (demodalize f)"?

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:51):

That is exactly why you can specify the variable with (induction f rule: form.induct). Avoid confusing

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:52):

Mathias Fleury said:

then you are doing induction on a variable that is not in the goal

That's awful... I wonder if there exists a case of "inducting on a variable that is not in the goal" to be useful.

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:52):

Never which is why induction did not pick that ;-)

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:52):

Mathias Fleury said:

That is exactly why you can specify the variable with (induction f rule: form.induct). Avoid confusing

Given the situation, surely I will from now on...

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:53):

instead it decided to generalize the demodalize f to form and do induction on that

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:54):

Although in general induction f rule: demodalize.induct is better here as you pick the version adapted to demodalize

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:54):

Mathias Fleury said:

instead it decided to generalize the demodalize f to form and do induction on that

Ah? So what happens is that it is proving !f. f = demodalize form ==> propform (demodalize form)?

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:55):

Try this silly version of the definition to see what happens:

fun propform :: "form ⇒ bool"
  where
   "propform FALSE = True"
 | "propform (VAR p) = True"
 | "propform (DISJ (VAR f1) f2) = (propform f2)"
 | "propform (DISJ f1 f2) = (propform f1 ∧ propform f2)"
 | "propform (NOT f) = propform f"
 | "propform (DIAM f) = False"

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:55):

Yiming Xu said:

Mathias Fleury said:

instead it decided to generalize the demodalize f to form and do induction on that

Ah? So what happens is that it is proving !f. f = demodalize form ==> propform (demodalize form)?

No, as you though it is proving that propform form

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:55):

(do not ask me why, I have no interest to check the code of the induction tactic)

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:56):

I won't. I will just try your example and I may check later...

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:57):

Mathias Fleury said:

Yiming Xu said:

Mathias Fleury said:

instead it decided to generalize the demodalize f to form and do induction on that

Ah? So what happens is that it is proving !f. f = demodalize form ==> propform (demodalize form)?

No, as you though it is proving that propform form

I will remember, this is an impressive design...

view this post on Zulip Yiming Xu (Sep 13 2024 at 16:57):

Mathias Fleury said:

Try this silly version of the definition to see what happens:

fun propform :: "form ⇒ bool"
  where
   "propform FALSE = True"
 | "propform (VAR p) = True"
 | "propform (DISJ (VAR f1) f2) = (propform f2)"
 | "propform (DISJ f1 f2) = (propform f1 ∧ propform f2)"
 | "propform (NOT f) = propform f"
 | "propform (DIAM f) = False"

You mean use this and use induction f rule: demodalize.induct?

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:58):

Take that definition and compare:

lemma propform_demodalize : "propform (demodalize f)"
  apply (induction f rule: form.induct)
  apply auto
  oops


lemma propform_demodalize : "propform (demodalize f)"
  apply (induction f rule: demodalize.induct)
  apply auto
  oops

view this post on Zulip Mathias Fleury (Sep 13 2024 at 16:59):

ah no sorry wait

view this post on Zulip Mathias Fleury (Sep 13 2024 at 17:00):

fun demodalize :: "form ⇒ form"
  where
    "demodalize FALSE = FALSE"
  | "demodalize (VAR p) = VAR p"
  | "demodalize (DISJ (VAR form1) form2) = DISJ (VAR form1) (demodalize form2)"
  | "demodalize (DISJ form1 form2) = DISJ (demodalize form1) (demodalize form2)"
  | "demodalize (NOT form) = NOT (demodalize form)"
  | "demodalize (DIAM form) = demodalize form"


fun propform :: "form ⇒ bool"
  where
   "propform FALSE = True"
 | "propform (VAR p) = True"
 | "propform (DISJ f1 f2) = (propform f1 ∧ propform f2)"
 | "propform (NOT f) = propform f"
 | "propform (DIAM f) = False"

thm form.induct
lemma propform_demodalize : "propform (demodalize f)"
  apply (induction f rule: demodalize.induct)
          apply auto
  oops


lemma propform_demodalize : "propform (demodalize f)"
  apply (induction f rule: form.induct)
          apply auto
  oops

view this post on Zulip Yiming Xu (Sep 13 2024 at 17:05):

image.png

view this post on Zulip Yiming Xu (Sep 13 2024 at 17:06):

I think this is what I expected? Identical to HOL4.

view this post on Zulip Yiming Xu (Sep 13 2024 at 17:07):

Oh I see.

view this post on Zulip Yiming Xu (Sep 13 2024 at 17:07):

If the definition of demodalize is changed, than if we induct on formula, we need to do case splitting on DISJ case.

view this post on Zulip Yiming Xu (Sep 13 2024 at 17:08):

But if we just induct on demodalize, then the IH does the case splitting.

view this post on Zulip Yiming Xu (Sep 13 2024 at 17:09):

Yes I agree! In that case, inducting with demodalize will be better.

view this post on Zulip Yiming Xu (Sep 13 2024 at 17:10):

I am not confident enough to claim "it works better <=> the inductive definition of a constructor of the datatype requires a case splitting". But so far I believe.

Last updated: Dec 21 2024 at 16:20 UTC