The Coq mailing list

["Ekaterina Komendantskaya" <komendantskaya AT gmail.com>]

Dear Samuel,

we have completed several experiments on formalising non-guarded functions in Coq.
We included the function dTimes for Lazy Differentiation that you mentioned in your posting.
Here http://hal.inria.fr/inria-00322331/en/ you can find the definition of dTimes that is accepted by Coq.
(We used "Zip (plus)" function instead of dPlus for uniformity, but you will be able to switch from one to another...)

Best wishes,
Katya

Samuel Bronson wrote:

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".

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
 

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club