The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Apologies for answering myself here.

> [...]
> functions which are defined and accepted in Coq terminates. Can the system
> check space and time upper bounds, i.e. O(f) bounds?
> 
> Take for example the addition of the Coq 8 library:
> (** Addition *)
> 
> Fixpoint plus (n m:nat) {struct n} : nat :=
>   match n with
>   | O => m
>   | S p => S (plus p m)
>   end.
> 
> We have:
>    (plus n m) in time O(n)
> and:
>    (plus n m) in space O(n + m)
>    (* the result has this length *)
> 
> How can this be checked in or by Coq?

First, define the data which describes the excact resource consumption.

   Inductive Complexity : Set :=
      complexity : forall (input internal output matches 
applications:nat),Complexity.
   (*                        |      |     |       |       |
                             |      |     |       |       +--> number of 
applications
                             |      |     |       +--> number of matches
                             |      |     +--> size of result
                             |      +--> maximal additional size during 
evaluation
                             +--> size of input
   *)

Second, translate plus into plus_complexity (and all called functions also).

   Comments "The constants for space consumption may not be accurate here.".
   Fixpoint plus_complexity (n m:nat) {struct n} :
      nat * Complexity
   := match n with
      | 0   => (m,complexity (m+2) 0 (m+1) 1 0)
      | S p => let (res,c) := plus_complexity p m in
               let (i, int, o, mat, app) := c in
               (S res,complexity (n+m+2) (2+int) (o+1) (mat+1) (app+1))
      end.

Third, look at some examples.

   Eval compute in (plus_complexity 1 1).
   Eval compute in (plus_complexity 11 1).
   Eval compute in (plus_complexity 1 11).

Finally, you can prove theorems about plus_complexity which provide complexity
class estimates like big-O, o, \theta, etc.

Regards,
-- 
Stefan