Stream: Beginner Questions

Topic: Why this goal cannot be solved automatically?

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

I have the following goal:
image.png
It seems to be straightforward but all of simp/auto/metis fails.
As a naive guess, I think it is because the implications here are all meta-implications and I maybe they have to be put in the assumption list before automatic tools can use them in the intended way. So how should I do this?

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

First it is easier to include the code here for copy-paste

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

forall x. P x \/ Q x is not the same as (forall x. P x) \/ (forall x. Q x)

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

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"

fun satis :: "'a model ⇒ 'a ⇒ form ⇒ bool"
where
"satis M w (VAR p) ⟷ (valt M p w ∧ world M w)"
| "satis M w FALSE ⟷ False"
| "satis M w (NOT f) ⟷ world M w ∧ ¬ satis M w f"
| "satis M w (DISJ f1 f2) ⟷ satis M w f1 ∨ satis M w f2"
| "satis M w (DIAM f) ⟷ world M w ∧ (∃ v. rel M w v ∧ world M v ∧ satis M v f)"

lemma satis_only_in_worlds: "∀w. satis M w f ⟹ world M w"
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 apply simp done sorry
next
case (NOT x)
then show ?case by simp
next
case (DIAM x)
then show ?case simp
qed

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

think of forall n::natural number. even n \/ odd n.

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

Oh the second w is blue!

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

I see, I need more parentheses.

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

Actually, the easiest solution is to drop the forall completely

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

stuff get explicitly meta-quantified

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

and yes green = bound, blue = free

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

 case (DISJ x1a x2)
  then show ?case apply simp
    by blast

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

That works. But how would a mature user write it?

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

"by" should be an abbreviation of apply and done. But if I change it, Isabelle complains about the syntax again.

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

image.png

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

Mathias Fleury said:

stuff get explicitly meta-quantified

Great reminder, I should do that.

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

lemma satis_only_in_worlds: "satis M w f ⟹ world M w"
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 apply simp by blast
next
  case (NOT x)
  then show ?case by simp
next
  case (DIAM x)
  then show ?case
  by fastforce
qed

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

So here is a complete Isar proof that merely works! I had no experience with Isar and actually, any theorem prover that supports forward, readable proof. I would like suggestions to make this proof neater according to Isar conventions.

Jan van Brügge (Sep 11 2024 at 21:17):

What I usually do in cases like this where I have a bunch of cases that are just calls to simp, is to do them all at the end:

lemma satis_only_in_worlds: "satis M w f ⟹ world M w"
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 apply simp by blast
+  then show ?case by auto (* not sure if this works, but auto is roughly simp + blast *)
-next
-  case (NOT x)
-  then show ?case by simp
next
  case (DIAM x)
  then show ?case
  by fastforce
-qed
+qed simp_all

Yiming Xu (Sep 12 2024 at 07:37):

Jan van Brügge said:

What I usually do in cases like this where I have a bunch of cases that are just calls to simp, is to do them all at the end:

lemma satis_only_in_worlds: "satis M w f ⟹ world M w"
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 apply simp by blast
+  then show ?case by auto (* not sure if this works, but auto is roughly simp + blast *)
-next
-  case (NOT x)
-  then show ?case by simp
next
  case (DIAM x)
  then show ?case
  by fastforce
-qed
+qed simp_all

Thanks! The auto works. That is good to know.

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

in general you can use try0 at a proof to see what isabelle methods can finish the proof

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

Thanks! I will try out how powerful it is soon.

Last updated: Dec 21 2024 at 16:20 UTC