The Coq mailing list

["Samuel Bronson" <naesten AT gmail.com>]

I'm trying to implement
http://conal.net/blog/posts/beautiful-differentiation/ but having
trouble with the guardedness condition -- at least, that's what I
think it must be. My latest attempt is:

Section Foo.
  Variable N : Type.
  Variable zero : N.
  Variable plus : N -> N -> N.
  Variable times : N -> N -> N.
  Variable opp : N -> N.

  Infix    "+"   := plus    : N_scope.
  Infix    "*"   := times   : N_scope.
  Notation "- x" := (opp x) : N_scope.

  Bind Scope N_scope with N.

  (* <roconnor> SamB: how about
   *   x@(D x0 x') * y@(D y0 y') = D (x0 * y0) (x' * y) + D 0 (x * y')
   *)

  CoInductive Dif :=
   D : N -> Dif -> Dif.

  Delimit Scope Dif_scope with Dif.
  Bind Scope Dif_scope with Dif.

  CoFixpoint dZero := D zero (dZero).

  CoFixpoint dOpp (x : Dif) : Dif :=
    match x with
      D x0 x' => D (-x0) (-x')%Dif
    end
  where "- x" := (dOpp x).

  CoFixpoint dPlus (x y : Dif) : Dif :=
    match x, y with
      D x0 x', D y0 y' => D (x0 + y0) (x' + y')%Dif
    end
  where "x + y" := (dPlus x y).

  CoFixpoint dTimes (x y : Dif) : Dif :=
    match x, y with
      D x0 x', D y0 y'
        => D (x0 * y0) (x' * y + x * y')
    end%Dif
  where "x * y" := (dTimes x y).
End Section.

but the definition of dTime fails, with the error message:

Error:
Recursive definition of dTimes is ill-formed.
In environment
N : Type
zero : N
plus : N -> N -> N
times : N -> N -> N
opp : N -> N
dTimes : Dif -> Dif -> Dif
x : Dif
y : Dif
x0 : N
x' : Dif
y0 : N
y' : Dif
Unguarded recursive call in
"cofix dPlus (x y : Dif) : Dif :=
   match x with
   | D x0 x' => match y with
                | D y0 y' => D (x0 + y0) (x' + y')
                end
   end".
Recursive definition is:
"fun x y : Dif =>
 match x with
 | D x0 x' =>
     match y with
     | D y0 y' => D (x0 * y0) (dTimes x' y + dTimes x y')
     end
 end".