Stream: Coq users

Topic: ✔ Non strictly positive occurrence in recursive record?


view this post on Zulip Julio Di Egidio (Nov 03 2023 at 00:37):

Julio Di Egidio said:

BTW, at a first glance I am puzzled that checking the parent does not lead to Coq complaining: doesn't that amount to an infinite loop? But I am in a rush, I'll have to come back to this later...

I was quite puzzled because I had not yet realized that checkvalid is in Prop, not in bool...

I am marking this question resolved. I intend to post the example I was talking about, but as a separate topic.

Thanks again @Gaëtan Gilbert for your help.

view this post on Zulip Notification Bot (Nov 03 2023 at 00:38):

Julio Di Egidio has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Nov 03 2023 at 08:22):


I was quite puzzled because I had not yet realized that checkvalid is in Prop, not in bool...

You can write it in bool if you want

view this post on Zulip Julio Di Egidio (Nov 03 2023 at 12:49):

I could, but it's another topic: your code and the way you change things and in ways that are not even easy to spot at a glance is simply off a tangent. Never mind, I will be asking so many more question... ;)

view this post on Zulip Julio Di Egidio (Nov 04 2023 at 12:17):

[I am not in fact sure if I should be opening a new thread for the following, as it is unrelated to my original question, but I'd lose all context so I am not doing it, I am just not reopening the question... If anybody has a more preferred approach to suggest/indicate, please let me know.]

Julio Di Egidio said:

I see, thank you!
BTW, at a first glance I am puzzled that checking the parent does not lead to Coq complaining: doesn't that amount to an infinite loop? But I am in a rush, I'll have to come back to this later...

Coq does complain, at least with the code below, which I find reassuring. :)

But now I am puzzled that your code compiles at all (@Gaëtan Gilbert : though of course it does, I have tried it)? Except for the fact that you have wrapped something in a section, I cannot tell the two codes apart... (Maybe I am missing something obvious, my eyesight isn't getting any better...)

Require Import List.

Inductive fsItem : Set := FSItem
{
  (* attrs *)
  isDir : bool;
  (* tree *)
  parent : option fsItem;
  children : option (list fsItem);
}.

Definition fsValidItem (item : fsItem): Prop :=
  item.(children) = None <-> item.(isDir) = false.

Fail Fixpoint fsValidTree (item : fsItem): Prop :=
  fsValidItem item /\
  match item.(parent) with
  | None    => True
  | Some p' => fsValidTree p'
  end /\
  match item.(children) with
  | None     => True
  | Some cs' => Forall fsValidTree cs'
  end.
(*
  The command has indeed failed with message:
  Recursive definition of fsValidTree is ill-formed. [...]
  Recursive call to fsValidTree has not enough arguments.
*)

Fixpoint LForall {A} (P : A -> Prop) (l : list A) :=
  match l with
  | nil      => True
  | cons a l => P a /\ LForall P l
  end.

Fail Fixpoint fsValidTree (item : fsItem): Prop :=
  fsValidItem item /\
  match item.(parent) with
  | None    => True
  | Some p' => fsValidTree p'
  end /\
  match item.(children) with
  | None     => True
  | Some cs' => LForall fsValidTree cs'
  end.
(*
  The command has indeed failed with message:
  Recursive definition of fsValidTree is ill-formed. [...]
  Recursive call to fsValidTree has not enough arguments.
*)

view this post on Zulip Paolo Giarrusso (Nov 04 2023 at 12:24):

The "infinite loop" itself isn't possible because you can't create cyclic data structures if you just use inductives.

view this post on Zulip Julio Di Egidio (Nov 04 2023 at 12:29):

That we cannot in fact call that function and actually get Coq hanging is different from the function being an infinite loop...

view this post on Zulip Gaëtan Gilbert (Nov 04 2023 at 12:37):

that's a classic issue with fixpoints and nested inductives https://github.com/coq/coq/issues/16040
basically the section way of defining the fixpoint is equivalent to Definition LForall {A} P := fix LForall l := ... (A and P outside the fix) which allows for more analysis when doing the guard checking

view this post on Zulip Julio Di Egidio (Nov 04 2023 at 12:48):

Very interesting: something like an analysis that is able to detect "cyclic definitions" IIUC [I am referring to fsItem here], whence the definition [of fsValidTree] passes. I am not sure I understand the implications of that, except that using sections changes the semantics of definitions... But I guess that's yet another topic.

Thanks again for your help, Gaëtan, very much appreciated.

view this post on Zulip Paolo Giarrusso (Nov 04 2023 at 12:53):

Julio Di Egidio said:

That we cannot in fact call that function and actually get Coq hanging is different from the function being an infinite loop...

That's a matter of naming, isn't it? But even addition on nats would be an infinite loop if you could create a cyclic natural... So the standard jargon is to reserve "infinite loop" for functions for which there exists an input causing a loop.


Last updated: Jun 23 2024 at 04:03 UTC