Yiming Xu (Sep 13 2024 at 19:34): Yiming Xu (Sep 13 2024 at 19:34):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_in_worlds: "satis M w f ⟹ world M w"
proof (induct rule:form.induct)
case (DISJ x1a x2)
then show ?case by auto
next
case (DIAM x)
then show ?case
by fastforce
qed simp_all
fun plts :: "form ⇒ num set" where
"plts (VAR a) = {a}"
| "plts FALSE = {}"
| "plts (NOT f) = plts f"
| "plts (DISJ f1 f2) = union (plts f1) (plts f2) "
| "plts (DIAM f) = plts f"
lemma exercise_1_3_1 :
"frame.truncate M1 = frame.truncate M2 ⟹
(⋀p. p ∈ plts f ⟹ valt M1 p = valt M2 p) ⟹
(satis M1 w f ≡ satis M2 w f)"
proof (induct f rule: form.induct)
case (VAR x)
then show ?case apply simp sorry
next
case FALSE
then show ?case sorry
next
case (DISJ x1a x2)
then show ?case sorry
next
case (NOT x)
then show ?case sorry
next
case (DIAM x)
then show ?case sorry
qed
On the goal
case (VAR x)
then show ?case apply simp sorry
sledgehammer does not solve it, but I believe it is straightforward. What can sledgehammer see? I think maybe because I do not expand some theorems relevant to the record type?
Yiming Xu (Sep 13 2024 at 19:36):
Yiming Xu (Sep 13 2024 at 19:38):It is saying: if we evaluate two modal formulas on two models with only differs on valuation of propositional letters (and the underlying set and the relation on the underlying set are both the same). Then if the two models agree on all the propositional letter in a formula f, then M1,w |= f iff M2,w |=f.
Mathias Fleury (Sep 13 2024 at 19:45):The hard lesson to learn: Sledgehammer is not magic
Mathias Fleury (Sep 13 2024 at 19:45):It is great, but it is not magic
Mathias Fleury (Sep 13 2024 at 19:46):There are a lot of things it is bad at
Mathias Fleury (Sep 13 2024 at 19:46):including records
Mathias Fleury (Sep 13 2024 at 19:47):At some point you have to look at the theorem and wonder: how can I prove this on paper
Mathias Fleury (Sep 13 2024 at 19:47):Then you search for useful lemmas, like:
find_theorems world frame.truncate
Okay! Sledgehammer is already very impressive (in a positive sense, in contrast to the induction stuff).
Yiming Xu (Sep 13 2024 at 19:49):So:
found 1 theorem(s):
test.frame.defs(4): frame.truncate ?r ≡ ⦇world = world ?r, rel = rel ?r⦈
is what I can only get.
Mathias Fleury (Sep 13 2024 at 19:50):… yeah and now you have to use it ;-)
Mathias Fleury (Sep 13 2024 at 19:51):I do not want to spoil it, I think learning it is part of the experience
Yiming Xu (Sep 13 2024 at 19:51):Let me try it tomorrow! Thanks for teaching this command:
find_theorems world frame.truncate
multiple patterns, very helpful.
Mathias Fleury (Sep 13 2024 at 19:51):if you really do not manage, but please try to
Yiming Xu (Sep 13 2024 at 19:52):Thanks! I swear I will not click it before trying it enough by myself!
Yiming Xu (Sep 14 2024 at 06:19):Mathias Fleury said:
if you really do not manage, but please try to
I solved it, but mine is a bit different. I searched the application of unfolding:
case (VAR x)
then show ?case unfolding test.frame.defs(4) by simp
The meaning is a bit different. You unfold then simplify, I simplify and allow to unfold, but the effect is the same: the goal is solved!
Mathias Fleury (Sep 14 2024 at 06:21):I am not very consistent with it, but usually I try to write it as: unfolding important_stuff_from_my_development by (simp add: boring_background_stuff)
Yiming Xu (Sep 14 2024 at 06:22):I see. I appreciate the style of remarking on significant things.
Last updated: Dec 21 2024 at 16:20 UTC