Stream: Beginner Questions

Topic: simps changes to psimps after editing

Yiming Xu (Oct 13 2024 at 06:52):

I corrected a wrong definition. After the correction, Isabelle cannot automatically prove it is a function, and hence requires me to change from fun to function. Moreover, after the editing, I find the definition is not applied automatically by simp anymore, causing some proof to break.

Yiming Xu (Oct 13 2024 at 06:52):

The correct definition, i.e., the new version, is like this:

function satis :: "('m set × ('m ⇒ nat)) × 'p set ⇒ 'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool) ⇒
              'a ⇒ ('m,'p) form ⇒ bool"
  where
   "satis (τ,Φ) (W,R,V) w TRUE ⟷ w ∈ W"
 | "satis (τ,Φ) (W,R,V) w FALSE ⟷ False"
 | "satis (τ,Φ) (W,R,V) w (VAR p) ⟷ p ∈ Φ ∧ w ∈ W ∧ V p w"
 | "satis (τ,Φ) (W,R,V) w (CONJ f1 f2) =
   (satis (τ,Φ) (W,R,V) w f1 ∧ satis (τ,Φ) (W,R,V) w f2)"
 | "satis (τ,Φ) (W,R,V) w (DISJ f1 f2) =
   (satis (τ,Φ) (W,R,V) w f1 ∨ satis (τ,Φ) (W,R,V) w f2)"
 | "satis (τ,Φ) (W,R,V) w (IMP f1 f2) ⟷ w ∈ W ∧
   (satis (τ,Φ) (W,R,V) w f1 ⟶ satis (τ,Φ) (W,R,V) w f2)"
 | "satis (τ,Φ) (W,R,V) w (NOT f) ⟷ (w ∈ W  ∧ ¬ satis (τ,Φ) (W,R,V) w f)"
 | "satis (τ,Φ) (W,R,V) w (BOX m fl) ⟷
    (m ∈ fst τ ∧ (snd τ) m = length fl ∧
     w ∈ W ∧ (∀vl. length vl = length fl ∧ R m (w # vl) ⟶
     (∃i. i < length vl ∧
     satis (τ,Φ) (W,R,V) (vl ! i) (fl ! i))))"
 | "satis (τ,Φ) (W,R,V) w (DIAM m fl) ⟷
    (m ∈ fst τ ∧ (snd τ) m = length fl ∧
     w ∈ W ∧ (∃vl. length vl = length fl ∧ R m (w # vl) ∧
     list_all2 (λ f v. satis (τ,Φ) (W,R,V) v f) fl vl))"
 apply auto
  using form.exhaust by blast

Yiming Xu (Oct 13 2024 at 06:54):

The only difference between it and the previous one is on the clause for "BOX". Previously, I had:

satis (τ,Φ) (W,R,V) w (BOX m fl) ⟷
    (m ∈ fst τ ∧ (snd τ) m = length fl ∧
     w ∈ W ∧ (∀vl. length vl = length fl ∧ R m (w # vl) ⟶
     list_all2 (λ f v. satis (τ,Φ) (W,R,V) v f) fl vl) )"

Yiming Xu (Oct 13 2024 at 06:54):

And the previous version can be automatically proved to be a function.

Maximilian Schäffeler (Oct 13 2024 at 07:00):

function requires you to also prove termination (fun does it automatically).
Only after you prove termination, you will have access to simps.
You can find more details in the tutorial "Defining Recursive Functions in Isabelle/HOL" (in jedit on the left, click on Documentation, then Isabelle Tutorials, then functions.

Yiming Xu (Oct 13 2024 at 07:00):

May I please ask for suggestions on how to deal with that? I would like simp to automatically work for it. I tried "grep" with "function" and "simp" on my mac to see how to add the definition to the simp set, but zsh does not find the command, indicating maybe it does not find the correct path...

Also if I can write is a fun instead of function, it might automatically change back to simp?

Yiming Xu (Oct 13 2024 at 07:02):

Maximilian Schäffeler said:

function requires you to also prove termination (fun does it automatically).
Only after you prove termination, you will have access to simps.
You can find more details in the tutorial "Defining Recursive Functions in Isabelle/HOL" (in jedit on the left, click on Documentation, then Isabelle Tutorials, then functions.

Thank you very much! But it seems to me that Isabelle is already happy with the termination?

Yiming Xu (Oct 13 2024 at 07:02):

Here is the interactive window, it accepts it as a constant and does not give me any goal.

Yiming Xu (Oct 13 2024 at 07:02):

image.png

Maximilian Schäffeler (Oct 13 2024 at 07:03):

Yes, it accepts it as a constant, but the psimp lemmas have an additional assumption, that basically states that the function terminates on this input.

Yiming Xu (Oct 13 2024 at 07:04):

Oh I see, despite the fact that Isabelle does not ask, I have to write:
termination proof -
show ?thesis sorry
qed
to start the proof.

Maximilian Schäffeler (Oct 13 2024 at 07:04):

You may also prove termination much later, or never at all. The only problem is that in this case, you know much less about how satis behaves on arbitrary inputs.

Yiming Xu (Oct 13 2024 at 07:06):

Thanks! I see. I think the quantification on vl might be the reason it cannot automatically proved to terminate.

Yiming Xu (Oct 13 2024 at 07:07):

I am hesitating whether I would change to inductive instead. It will take some thoughts...

Maximilian Schäffeler (Oct 13 2024 at 08:23):

Note that if you use function, Isabelle does not even try to prove termination automatically.

Yiming Xu (Oct 13 2024 at 08:25):

Thanks! I recently learned that if termination can be proved automatically, then fun is enough, but I was indeed not aware of the other way around: i.e. if fun is not enough then I have to type "termination" by hand. It i good to know.

Last updated: Dec 21 2024 at 16:20 UTC