The Coq mailing list

[Burak Ekici <ekcburak AT hotmail.com>]

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.