Stream: Beginner Questions

Topic: Syntax for proving termination of this recursive predicate

Yiming Xu (Oct 31 2024 at 09:13):

Code for copy and paste:

datatype ('m,'p) cform = cVAR "'p"
  | cFALSE
  | cDISJ "('m,'p) cform" "('m,'p) cform"
  | cNOT "('m,'p) cform"
  | cDIAM 'm "(('m,'p) cform) list" ("♢_ _" [0, 0])


abbreviation ops :: "'m set × ('m ⇒ nat) ⇒ 'm set" where
"ops τ ≡ fst τ"

abbreviation arity :: "'m set × ('m ⇒ nat) ⇒ ('m ⇒ nat)" where
"arity τ ≡ snd τ"

type_synonym ('m,'p) sig =
"('m set × ('m ⇒ nat)) × 'p set "

abbreviation props ::
"('m set × ('m ⇒ nat)) × 'p set ⇒ 'p set" where
"props sig ≡ snd sig"

abbreviation mops ::
"('m set × ('m ⇒ nat)) × 'p set ⇒ 'm set" where
"mops sig ≡ fst (fst sig)"

abbreviation marity ::
"('m set × ('m ⇒ nat)) × 'p set ⇒ 'm ⇒ nat" where
"marity sig ≡ snd (fst sig)"

inductive wff :: ‹('m set × ('m ⇒ nat)) × 'p set ⇒ ('m, 'p) cform ⇒ bool›
  for sig :: "('m set × ('m ⇒ nat)) × 'p set"
  where
    "wff sig cFALSE"
  | "p ∈ props sig ⟹ wff sig (cVAR p) "
  | "wff sig (cDIAM m fl) "
    if "m ∈ mops sig" "length fl = (marity sig m)" "∀f. f ∈ list.set fl ⟹
      wff sig f"
  | "wff sig (cNOT f)" if "wff sig f"
  | "wff sig (cDISJ f1 f2)" if "wff sig f1"
  "wff sig f2 "

type_synonym ('m,'p,'a) model =
"'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool)"

abbreviation world ::
"'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool)
 ⇒ 'a set" where
"world M ≡ fst M"

abbreviation
rel :: "'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool)
 ⇒ ('m ⇒ 'a list ⇒ bool)" where
"rel τ ≡ fst (snd τ)"

abbreviation
valt :: "'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool)
⇒ ('p ⇒ 'a ⇒ bool)" where
"valt τ ≡ snd (snd τ)"


function csatis :: "('m set × ('m ⇒ nat)) × 'p set ⇒ 'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool) ⇒
              'a ⇒ ('m,'p) cform ⇒ bool"
  where
   "csatis sig M w cFALSE ⟷ False"
 | "csatis sig M w (cVAR p) ⟷ p ∈ props sig ∧ w ∈ world M ∧ valt M p w"
 | "csatis sig M w (cDISJ f1 f2) = (csatis sig M w f1 ∨ csatis sig M w f2)"
 | "csatis sig M w (cNOT f) = (w ∈ world M  ∧ ¬ csatis sig M w f)"
 | "csatis sig M w (cDIAM m fl) =
   (m ∈ mops sig ∧ marity sig m = length fl ∧
     w ∈ world M ∧ (∃vl. length vl = length fl ∧ rel M m (w # vl) ∧
     (∀i. i < length vl ⟶ csatis sig M (vl ! i) (fl ! i))))"
 apply auto
  using cform.exhaust by blast
termination sorry

I define the predicate csatis and have trouble proving its termination. The goal is as follows:

proof (state)
goal (5 subgoals):
 1. wf ?R
 2. ⋀sig M w f1 f2. ((sig, M, w, f1), sig, M, w, cDISJ f1 f2) ∈ ?R
 3. ⋀sig M w f1 f2. ((sig, M, w, f2), sig, M, w, cDISJ f1 f2) ∈ ?R
 4. ⋀sig M w f. ((sig, M, w, f), sig, M, w, cNOT f) ∈ ?R
 5. ⋀sig M w m fl x xa. xa < length x ⟹ ((sig, M, x ! xa, fl ! xa), sig, M, w, ♢m fl) ∈ ?R

I believe the relation ?R should be on the size of the formula. I would like to write:
"wf {((a,b,c,d),e,f,g,h). size d < size h}", then I would have size f1 < size (cDISJ f1 f2), etc.

I am not sure if it is the canonical flow for doing these sort of things. For the proof, I tried to write

have "wf {((a,b,c,d),e,f,g,h). size d < size h}" apply auto

to see what remains. But Isabelle refuses to apply auto for me, and complains

Failed to apply proof method⌂:
goal (1 subgoal):
 1. wf {((a, b, c, d), e, f, g, h). size d < size h}

May I please ask what I am suggested to do here?

I tried type "termination" to look for examples, but I opened several files and only find this word on the comment... If someone would think there is a good example, it would be helpful to give the name of the file I should look at as well.

Fabian Huch (Oct 31 2024 at 09:48):

Here are some termination examples

Yiming Xu (Oct 31 2024 at 10:42):

It is a very useful website, thanks a lot for sharing! I am making progress by looking at it.

Fabian Huch (Oct 31 2024 at 10:45):

You're welcome -- have a look at isabelle.systems for an overview over helpful Isabelle resources!

Yiming Xu (Oct 31 2024 at 10:48):

Fabian Huch said:

You're welcome -- have a look at isabelle.systems for an overview over helpful Isabelle resources!

Thanks again!

Yiming Xu (Oct 31 2024 at 10:50):

I tried to use "measure" on formula size and here is the only subgoal that is not killed by auto:

goal (1 subgoal):
 1. ⋀sig M m fl x xa.
       xa < length x ⟹
       size_cform sig M (fl ! xa) < Suc (sig m + size_list (size_cform sig M) fl)

I expect to be able to use a lemma saying each item in the list has smaller size than the whole list. I tried " sledgehammer(add:cform.size(5) Groups_List.monoid_add_class.size_list_conv_sum_list)" but it finds nothing. I expect this to be a common pattern, what do people do for this?

Yiming Xu (Oct 31 2024 at 10:54):

I can try fix ... assume... show... Let me see how it goes...

Yiming Xu (Oct 31 2024 at 10:57):

have "size_cform sig M (fl ! xa) ≤ size_list (size_cform sig M) fl"
using Groups_List.monoid_add_class.size_list_conv_sum_list
sledgehammer
found no proof. I think I need help here.

Mathias Fleury (Oct 31 2024 at 13:39):

First: most theorems in Isabelle are written with ?x ∈ set ?xs instead of list, so searching for a useful lemma requires to try both.
~> size_list_estimation' is helpful here

Mathias Fleury (Oct 31 2024 at 13:41):

Second: there is an issue in the lemma, which explains why sledgehammer cannot prove it. Either you can see it or you will find when proving:

lemma ‹... ⟹ ...›
  using size_list_estimation'[of ‹fl ! xa› fl ‹size_cform sig M (fl ! xa)›  ‹size_cform sig M›, OF nth_mem]
  by auto

Mathias Fleury (Oct 31 2024 at 13:47):

Maybe rewriting the forall as ∀(x,y) ∈ set (zip vl fl). csatis sig M x y helps

Yiming Xu (Oct 31 2024 at 13:49):

I just saw that! But why it is giving xa < length x instead of fl? I expect the generated goal for my definition to have the pre-condition xa < length fl.

Yiming Xu (Oct 31 2024 at 13:49):

My definition says (∀i. i < length vl ⟶ csatis sig M (vl ! i) (fl ! i))).

Yiming Xu (Oct 31 2024 at 13:50):

Mathias Fleury said:

Maybe rewriting the forall as ∀(x,y) ∈ set (zip vl fl). csatis sig M x y helps

Does it mean editing the definition in terms of zip?

Yiming Xu (Oct 31 2024 at 13:53):

Or is it possible within the goal?

Mathias Fleury (Oct 31 2024 at 13:56):

Yiming Xu (Oct 31 2024 at 13:57):

If I edit the definition it will give me a provable goal. But I think I like the original one better. Does it seem possible to keep the original definition? Otherwise I should prove the original version as derived.

Yiming Xu (Oct 31 2024 at 13:57):

goal (5 subgoals):
 1. wf ?R
 2. ⋀sig M w f1 f2. ((sig, M, w, f1), sig, M, w, cDISJ f1 f2) ∈ ?R
 3. ⋀sig M w f1 f2. ((sig, M, w, f2), sig, M, w, cDISJ f1 f2) ∈ ?R
 4. ⋀sig M w f. ((sig, M, w, f), sig, M, w, cNOT f) ∈ ?R
 5. ⋀sig M w m fl x xa xb.
       (xa, xb) ∈ list.set (zip x fl) ⟹ ((sig, M, xa, xb), sig, M, w, ♢m fl) ∈ ?R

Yiming Xu (Oct 31 2024 at 13:58):

It would be helpful to know according to which principle does Isabelle generate the goals for termination. Seems not written down anywhere.

Mathias Fleury (Oct 31 2024 at 13:59):

I do not really know why termination is doing this. I just have learned over the years to use as few nth as possible

Yiming Xu (Oct 31 2024 at 14:00):

I am curious, except for the generated goals, is there any other thing that nth is bad to work with?

Mathias Fleury (Oct 31 2024 at 14:00):

It is loosely documented https://isabelle.in.tum.de/doc/functions.pdf for user

Mathias Fleury (Oct 31 2024 at 14:01):

Yiming Xu said:

I am curious, except for the generated goals, is there any other thing that nth is bad to work with?

Generally everything that forces an order on things when the order is not relevant. Like list vs set.

Mathias Fleury (Oct 31 2024 at 14:01):

(or list vs multiset to be more accurate)

Yiming Xu (Oct 31 2024 at 14:08):

Emmm... I am not sure if I get it. For my cases, I do need the order on the list vl and fl and they need to match up. But indeed, the point of (∀i. i < length vl ⟶ csatis sig M (vl ! i) (fl ! i)) is just to pair things up. So the relation R cares the order, but (∀i. i < length vl ⟶ csatis sig M (vl ! i) (fl ! i)) does not.

Yiming Xu (Oct 31 2024 at 14:11):

I am going to try this since I feel like it may make me more comfortable. Thanks for the elaboration on this!

Yiming Xu (Oct 31 2024 at 14:13):

Is that a better style for practical reason to write "∀(x,y) ∈ set (zip vl fl). csatis sig M x y" over "∀x y. (x,y)∈ set (zip vl fl). csatis sig M x y", or is it purely atheistical?

Mathias Fleury (Oct 31 2024 at 14:14):

On paper, I am used to the first notation (like in math proof with "\in \R"), so I usually go for the first one

Mathias Fleury (Oct 31 2024 at 14:14):

but internally they are the same

Mathias Fleury (Oct 31 2024 at 14:15):

Yiming Xu said:

Emmm... I am not sure if I get it. For my cases, I do need the order on the list vl and fl and they need to match up. But indeed, the point of (∀i. i < length vl ⟶ csatis sig M (vl ! i) (fl ! i)) is just to pair things up. So the relation R cares the order, but (∀i. i < length vl ⟶ csatis sig M (vl ! i) (fl ! i)) does not.

Not really right? once you paired the elements, the order in the list does not matter anymore

Yiming Xu (Oct 31 2024 at 14:23):

It is indeed true that once I pair the elements, the order in the list does not matter anymore. It seems to be a convincing argument to avoid anything related to ordering here. We only need the order to make sure to pair a world with a formula in a way that only correct pairs are created. But once we have done the procedure of pairing, the order in the zip list does not matter anymore.

Yiming Xu (Oct 31 2024 at 14:24):

Mathias Fleury said:

but internally they are the same

I see. That's good to know.

Last updated: Dec 21 2024 at 16:20 UTC