The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 19.03.2013 11:39, schrieb 
mtkhan AT risc.uni-linz.ac.at:
> (j + 1%Z)
Btw, for a minor technical improvement it might help to write (1 + j) or 
(S j), since plus is defined by recursiono n the left operand.
While the structure of 1 is well known to Coq (it's S O), the structure 
of j is not.
Thus the structure of (1 + j) is known to Coq (S j), but the structure 
of (j + 1) is not.

In any case,
I recommend using the following instead of this:

> Parameter add_int: (list or_integer_float) -> Z -> Z.
> ...
> Axiom add_int_def : forall (e:(list or_integer_float)) (j:Z),
>    ((j <= 0%Z)%Z -> ((add_int e j) = 0%Z)) /\ ((~ (j <= 0%Z)%Z) ->
> ((add_int e j) = match e with
>    | Nil => 0%Z
>    | (Cons (Integer n) t) => (n + (add_int t (j - 1%Z)%Z))%Z
>    | (Cons _ t) => (add_int t (j - 1%Z)%Z)
>    end)).


Use something like:

Fixpoint add_int (e : list or_integer_float) (j : Z) : Z := ....

Or even better, try to use fold_left and firstn 
(http://coq.inria.fr/library/Coq.Lists.List.html)

Definition add_int (e ...) (j ...) : Z := fold_left _ _ (fun a b => match b with 
(Integer n) => (a + n)%Z | _ => a end)
(firstn j e) 0%Z

(I'm not sure on the syntax with Z and I haven't tried putting it into Coq, 
so regard this as pseudo-coq)

Have fun with Coq,
Jonas