fpl bill algorithm

fplbill.v

(** tries to reverse engineer FPL billing algorithm: given x watt consumption what should be the bill?
the bill is printed in cents.
it comes within 100cents in the test cases
but doesnt exactly match, even though all computations except the last one to print in decimal (error < 1 cent) are exact.
*)

Require Import QArith.
Require Import Coq.Classes.DecidableClass.
Definition Qmax (a b:Q) : Q :=
  if ((Qle_bool a b)) then b else a.
Definition Qmin (a b:Q) : Q :=
  if ((Qle_bool a b)) then a else b.

Definition Nsubtract (a b: Q) : Q := Qmax (a-b) 0.

(* section "taxes and charges" *)
Definition taxrate : Q:= Eval compute in 41.92/1925.

Require Import Coq.Lists.List.
Import ListNotations.
Definition fplBill (watts: Q) : list Q :=
  let tax:= Qred taxrate*watts in
  [8.99 +
  (Qmin watts 1000)*(0.073710+0.034870)
  + (Nsubtract watts 1000)*(0.083710+0.044870)
  + tax; tax]
.

Definition digits (q:Q) : Z :=
  Qnum q * 100 / (Zpos (Qden q)).

Definition fplbillDigits (watts:Q) : list Z := List.map digits (fplBill watts).

Compute (flat_map fplbillDigits [1925; 233;1024;1864;1067]).