The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Burak,

When using cofix (or fix) for nested recursive types, there is an additional subtlety that the allowed positions for guarded calls are determined by the coinductive type being produced. In this case, a cofix producing a stream can only make a recursive call in the tail, not the head of the stream.

The workaround is to define a cofix on U first, which may then contain a cofix on stream U. This usually involves a bit of code duplication which can be refactored with an intermediate definition. See code below.

There's an equivalent situation with inductive types, described in this CPDT chapter (section Nested Inductive Types): http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html

Cheers,
Li-yao

---

CoInductive stream (A: Type): Type :=
  | nils : stream A
  | conss: A -> stream A -> stream A.

Arguments nils {_}.
Arguments conss {_} _ _.

CoInductive T: Type :=
  | c1: T
  | c2: list T -> T.

CoInductive U: Type :=
  | c3: U
  | c4: stream U -> U.

Definition MkT2Us (T2U : T -> U) (s : T) : stream U :=
  match s with
  | c1 => conss c3 nils
  | c2 l =>
    let cofix next l :=
      match l with
      | nil => nils
      | cons u xs => conss (T2U u) (next xs)
      end
    in next l
  end.

CoFixpoint T2U (s : T) : U :=
  let T2Us := MkT2Us T2U in
  c4 (T2Us s).

Definition T2Us : T -> stream U :=
  MkT2Us T2U.

On 2023-08-29 9:05 AM, Burak Ekici wrote:

Dear All,

I am trying to implement a corecursive function T2U: T -> U in the following manner:

CoFixpoint T2U (s: T): stream U :=
  match s with
    | c1   =>  conss c3 nils
    | c2 l =>
      let cofix next l :=
        match l with
          | nil       => nils
          | cons u xs => conss (c4 (T2U u)) (next xs)
        end
      in next l
  end.

Coq however rejects the definition raising "Recursive call on a non-recursive argument of constructor -- c4 (T2U u)" error. It is due to the violation of the guardedness condition as it gets accepted when the guard check is disabled. How can I work this around? Any advice or insights would be greatly appreciated.

Here are the definitions for the types T, U, and the stream used in the implementation:

CoInductive stream (A: Type): Type :=
  | nils : stream A
  | conss: A -> stream A -> stream A.

Arguments nils {_}.
Arguments conss {_} _ _.

CoInductive T: Type :=
  | c1: T
  | c2: list T -> T.

CoInductive U: Type :=
  | c3: U
  | c4: stream U -> U.

Thanks a lot.

Yours,

―

Burak.