Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Guardedness check sensitive to use of section variables?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Guardedness check sensitive to use of section variables?


Chronological Thread 
  • From: Colin Stebbins Gordon <colin.s.gordon AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Guardedness check sensitive to use of section variables?
  • Date: Mon, 10 Jun 2019 20:36:19 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=colin.s.gordon AT gmail.com; spf=Pass smtp.mailfrom=colin.s.gordon AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f178.google.com
  • Ironport-phdr: 9a23:+RA2sBAfria/7LVHHmtWUyQJP3N1i/DPJgcQr6AfoPdwSPv+o8bcNUDSrc9gkEXOFd2Cra4d0qyP7vurAjdIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK5+IA+roQjRuMQajoVvJ6gswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9UrxKvqRJ8zYDJfo+aKOFzcbnBcd4AX2dNQtpdWi5HD4ihb4UPFe0BPeNAooTjoFsOqRq+BQ+xD+3y1j9HmGT50rY70+QnCgHNwQ0uH9UUsHvJq9X1MroZXOepw6nPyTXDbvVW1S3m6ITSfRAhpuuMUq93ccrX0kQvGAbFgU+RqYzhJT+ayuMNs22C4udmSOmhiHYnphlvrjSzwsogkIrEi4IPxlza6yl13pw5KcC6RUN4Z9OvDYFeuDuAN4RsR8MvW2Fotzg+yr0BoZO7eTIFyJUjxxLGcvyHcJWE7gvtVOqMIzp1h2hpeL24hxa1/kigzvPzWtOo31ZNqypJitjMtnYT2BzP8sWLVOdx80O71TuM1w3f8P9ILV4qmabBNpIswL09moIWsUvZHy/2nEv2jLWRdkUh4uWn9+PnYrHnpp+aLYN0kRvyMqspmsylHOs4NQ4OUnOU+eS5zrLj/En5TK9Wgf0xl6nVqIraKtgDpq6lHw9V1Z4u5Aq4Dze/ydgXgX0HLE9edx+clIjoO1TOIOjiAvulglSsli1rx/HcMbH7DJXNNCuLrLC0drFkrkVY1QAbzNZF5psSBKtSDuj0Xxras9jZCFcCLwG+yefhE51S0ZkSXmTHVqSeNKLU90TO6eU1L+6KTIAQsTf5bfMi4qi93jcChVYBcPzxjtMsY3eiE6E+ehjLUT/Xmt4EVFwykE8+Qejt0gPQVDdSYzOrXPt56GhkWMSpCoDMQo3ri7uEjn/iT89mI1teA1XJKk/GMoCNWvMCciWXe5YznTkNVLznQIgkh0j36F3KjoF/J++RwRU28Ir53YEsteLWnBA2szdzCpbF3g==

I've been working with a structure that is essentially a coinductive data type that contains a coinductive collection of itself.  While defining cofixpoints on this structure, I kept bumping into a weird behavior where a seemingly sensible productive definition would be rejected for my chosen coinductive collection, but accepted for the streams in the standard library.  Eventually I tracked it down to how the notion of map is declared: of two seemingly equivalent ways of defining things, one passes the guardedness check, and the other is rejected.

Here's a self-contained definition of (possibly-finite) streams, along with two definitions of map:

Set Implicit Arguments.

Section Streams.
Variable A : Type.
CoInductive Stream : Type :=
    Cons : A -> Stream -> Stream
   | Nil : Stream.
End Streams.

Section Map.
Polymorphic Variables A B : Type.
Polymorphic Variable f : A -> B.
Polymorphic CoFixpoint smap (s:Stream A) : Stream B :=
  match s with
  | Nil _ => Nil _
  | Cons x xs => Cons (f x) (smap xs)
  end.
End Map.

Section Map2.
Polymorphic Variables A B : Type.
(*Polymorphic Variable f : A -> B.*)
(* Notice that now instead of making f a variable, it is not an argument to smap(2) *)
Polymorphic CoFixpoint smap2 (f : A -> B) (s:Stream A) : Stream B :=
  match s with
  | Nil _ => Nil _
  | Cons x xs => Cons (f x) (smap2 f xs)
  end.
End Map2.

Unset Implicit Arguments.


The only difference between smap and smap2 is that one is defined with f as a section variable, while the other takes it as a parameter.

Now if I define a simplification of what I was working with:

(* A simple coinductive structure with (1) data and (2) a container of itself *)
CoInductive wtree : Set :=
| node : nat -> Stream wtree -> wtree.


I can try to define two versions of the same cofixpoint, one accepted and one rejected:

(* The following is accepted by the guardedness checker, using smap defined with a Variable *)
CoFixpoint incr (w : wtree) : wtree :=
  match w with
  | node n ls => node (S n) (Cons w (smap incr ls))
  end.

(* The following is *rejected* by the guardedness checker, using smap2 defined with an argument *)
CoFixpoint incr2 (w : wtree) : wtree :=
  match w with
  | node n ls => node (S n) (Cons w (smap2 incr2 ls))
  end.


The error message I get for incr2 is:

Recursive definition of incr2 is ill-formed.
In environment
incr2 : wtree -> wtree
w : wtree
n : nat
ls : Stream wtree
Unguarded recursive call in
"cofix smap2 (f : wtree -> wtree) (s : Stream wtree) : Stream wtree :=
   match s with
   | Cons x xs => Cons (f x) (smap2 f xs)
   | Nil _ => Nil wtree
   end".
Recursive definition is: "fun w : wtree => match w with
                                           | node n ls => node (S n) (Cons w (smap2 incr2 ls))
                                           end".


The only difference is the use of the section variable when defining the map.  I realize syntactic guardedness checks are brittle by nature, but this still surprised me: I would not expect this particular change to affect the guardedness check.  Is this by design, a quirk of the current implementation (this is 8.9.0), or is there a subtle reason I'm missing that one (or both?) should actually be rejected?

Thanks,
Colin





Archive powered by MHonArc 2.6.18.

Top of Page