Stream: General

Topic: [fundef_cong] causes exception CYCLES

Yushuo Xiao (Jul 05 2024 at 10:30):

Hi all,

I am trying to give a higher-order function a congruence rule so that it can be used in recursive functions. I give the congruence rule the [fundef_cong] attribute, as stated in the function definition tutorial. However, the next function definition that follows the congruence lemma, no matter what it is, always fails with a "CYCLES" exception.

The code below is a minimal example.

theory Cong
  imports Main
begin

primrec option_fold :: "('a ⇒ 'b) ⇒ 'b ⇒ 'a option ⇒ 'b"
  where
    "option_fold f e (Some x) = f x"
  | "option_fold f e None = e"

lemma option_fold_cong [fundef_cong]:
  "(¬ Option.is_none x ⟹ ¬ Option.is_none y ⟹ f (the x) = g (the y)) ⟹
   (Option.is_none x ⟹ ¬ Option.is_none y ⟹ a = g (the y)) ⟹
   (¬ Option.is_none x ⟹ Option.is_none y ⟹ f (the x) = b) ⟹
   (Option.is_none x ⟹ Option.is_none y ⟹ a = b) ⟹
   option_fold f a x = option_fold g b y"
  by (metis Option.is_none_def option.collapse option_fold.simps(1) option_fold.simps(2))

fun foo :: "nat ⇒ nat" where
  "foo x = x"

end

Isabelle reports exception CYCLES [[1, 0, 1]] raised (line 298 of "General/graph.ML") on the line where fun foo is defined. The signature and the body of this function do not seem to matter. I could have some other content after the congruence lemma and the first function after it always fails with the same exception.

I am not sure what this exception means. Is it an internal error or some restrictions on [fundef_cong]? Or am I defining the congruence rule in the correct way? I found the Isabelle manual to be very brief about this part.

Any help would be appreciated. Thanks!

Jan van Brügge (Jul 05 2024 at 11:16):

The congruence rule has the wrong format. I think it should look like this:

lemma option_fold_cong[fundef_cong]: "x = y ⟹ a = b ⟹ (⋀a. a ∈ set_option x ⟹ f a = g a) ⟹ option_fold f a x = option_fold g b y"
  by (metis elem_set not_Some_eq option_fold.simps(1) option_fold.simps(2))

Jan van Brügge (Jul 05 2024 at 11:16):

That at least does not throw an error for the foo function

Yushuo Xiao (Jul 05 2024 at 11:35):

Thank you! It helps a lot. The lemma also makes the termination proof work. I also had the feeling that the congruence rule should be in certain format, after once I changed another congruence rule in some way to make it work. So where can I get more information on the exact format requirement for congruence rules? Currently I'm just writing something randomly and hope it works.

Jan van Brügge (Jul 07 2024 at 13:10):

The higher-order functions usually work on some sort of container, so the fundef_cong rule needs to make sure that if the functions agree on the contents of the container, the behavior for the whole container is the same. You can look at the theorems for standard datatypes, e.g. list.map_cong

Yushuo Xiao (Jul 12 2024 at 08:11):

Thanks! I see. I will have a look at the congruence rules for standard datatypes and try to figure out the pattern.

Jan van Brügge (Jul 12 2024 at 08:34):

In general if you don't have to use primrec, I would always just use fun even for simple functions as it correctly adds all the relevant theorems

Yushuo Xiao (Jul 15 2024 at 08:40):

I see. Thanks for the extra tip!

Last updated: Dec 21 2024 at 16:20 UTC