The Coq mailing list

[Lasse Blaauwbroek <lasse AT blaauwbroek.eu>]

You might be interested in the paper A Coq Library For Internal Verification of Running-Times. It touches on most of the issues you raise.

On 12-07-2022 21:41, mukesh tiwari wrote:

Hi everyone,

What are some nice ways to reason about the complexity/cost of Coq functions?

In more detail:

I want to reason about the complexity/cost of simple programs so the easiest way is to count the number of primitive instructions, during the execution of the program, and return it as an extra value. For example, the 'repeat_op_ntimes_rec' returns an extra argument, the number of steps it takes to execute for input n.

Fixpoint repeat_op_ntimes_rec (e : T) (n : positive) : T * N :=
      match n with
      | xH => (e, N0)
      | xO p =>
        let (ret, w) := repeat_op_ntimes_rec e p
        in (ret * ret, N.add 1 w)
      | xI p =>
        let (ret, w) := repeat_op_ntimes_rec e p
        in (e * (ret * ret), N.add 1 w)
      end.

Now, I can prove that the number of steps is bounded by a logarithm of n.

Lemma repeat_op_ntimes_rec_bound :
  forall n e, (snd (repeat_op_ntimes_rec e n) <= N.log2 (N.pos n))%N.

It is nice because if I compose two such functions, I can return the combined cost of functions. But now I am stuck with an extra return value just because I want to reason about the cost, so I can take another approach and write the same function in a normal way, without any counter:

(* Function without counter *)
 Fixpoint repeat_op_ntimes_rec_w (e : T) (n : positive) : T :=
      match n with
      | xH => e
      | xO p =>
        let ret := repeat_op_ntimes_rec_w e p
        in ret * ret
      | xI p =>
        let ret := repeat_op_ntimes_rec_w e p
        in e * (ret * ret)
      end.

Then I write an inductive data type to capture the cost

 (* Inducive Type to capture the complexity of  *)

Inductive complexity_repeat_op_ntimes_rec (e : T) :

     positive -> T -> N -> Prop :=

 | xH_case : complexity_repeat_op_ntimes_rec e xH e N0
 | xO_case p ret w : complexity_repeat_op_ntimes_rec e p ret w ->
      complexity_repeat_op_ntimes_rec e (xO p) (ret * ret) (N.succ w)
 | xI_case p ret w : complexity_repeat_op_ntimes_rec e p ret w ->
      complexity_repeat_op_ntimes_rec e (xI p) (e * (ret * ret)) (N.succ w).

Finally, I can prove that the execution of 'repeat_op_ntimes_rec' is bounded by logarithm of input by the following lemma

Lemma correct_complexity_repeat_op_ntimes_rec :
      forall n e,  complexity_repeat_op_ntimes_rec e n
        (repeat_op_ntimes_rec_w e n)  (N.log2 (N.pos n)).

This is nice because my function is free from an extra return value, but unfortunately, it does not, as I understand, compose. (I don't think I can compose two inductive datatypes to reason about combined cost).  Therefore, what is the best middle way to do this?

Best,

Mukesh