auto_diff.v

(* sample code of automatic differentiation in Coq *)

Require Import QArith.
Open Scope Q_scope.

Definition QFunc := Q -> Q.

Parameter der_rel : QFunc -> QFunc -> Prop.

Axiom add_der : forall f g f' g', der_rel f f' -> der_rel g g' ->
  der_rel (fun x => f x + g x) (fun x => f' x + g' x).
Axiom scalar_der : forall c f f', der_rel f f' -> der_rel (fun x => c * f x) (fun x => c * f' x).
Axiom leibnitz_der : forall f g f' g', der_rel f f' -> der_rel g g' ->
  der_rel (fun x => f x * g x) (fun x => f' x * g x + f x * g' x).
Axiom comp_der : forall f g f' g', der_rel f f' -> der_rel g g' ->
  der_rel (fun x => f (g x)) (fun x => f' (g x) * g' x).
Axiom const_der : forall (c : Q), der_rel (fun _ => c) (fun _ => 0).
Axiom id_der : der_rel (fun x => x) (fun _ => 1).

Parameter exp : Q -> Q.
Axiom exp_der : der_rel exp exp.

Ltac calc_der := eexists;
 repeat (apply add_der || apply scalar_der || apply leibnitz_der || apply const_der || apply id_der || apply exp_der || apply comp_der).

(* differentiate x^2 *)
Example derivative_x_sq : { f | der_rel (fun x => x * x) f }.
  calc_der.
Defined.
Eval simpl in proj1_sig derivative_x_sq.
(*
     = fun x : Q => 1 * x + x * 1
     : QFunc
*)

(* differenciate cx + b *)
Example derivative_linear (b c : Q) : { f | der_rel (fun x => c * x + b) f }.
  calc_der.
Defined.
Eval simpl in proj1_sig (derivative_linear (inject_Z 3) (inject_Z 2)).
(*
     = fun _ : Q => inject_Z 2 * 1 + 0
     : QFunc
*)

Example derivative_hoge : { f | der_rel (fun x => x * exp x + x * x) f }.
  calc_der.
Defined.
Eval simpl in proj1_sig derivative_hoge.
(*
     = fun x : Q => 1 * exp x + x * exp x + (1 * x + x * 1)
     : QFunc
*)

Example derivative_fuga : { f | der_rel (fun x => exp (x * x + x) + (inject_Z 2)*x) f }.
  calc_der.
Defined.
Eval simpl in proj1_sig derivative_fuga.
(*
     = fun x : Q => exp (x * x + x) * (1 * x + x * 1 + 1) + inject_Z 2 * 1
     : QFunc
*)