The Coq mailing list

[mtkhan AT risc.uni-linz.ac.at]

Hi All,

I have a Coq goal, which is in fact translated from Why3 system.
I tried the induction on list but could not succeed. Can some
one please hint the possible proof tactics in Coq for the
following snippet of the corresponding proof.

...
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)).

(* Why3 goal *)
Theorem add_int_right : forall (e:(list or_integer_float)) (j:Z),
  ((0%Z <= j)%Z /\ (j < (length e))%Z) -> forall (n:Z), ((nth j
  e) = (Some (Integer n))) -> ((add_int e (j + 1%Z)%Z) = ((add_int e
  j) + n)%Z).
intros e j (h1,h2) n h3.

which shows the following 1 goal to be proved

1 subgoal
e : list or_integer_float
j : Z
h1 : (0 <= j)%Z
h2 : (j < length e)%Z
n : Z
h3 : nth j e = Some (Integer n)
______________________________________(1/1)
add_int e (j + 1) = (add_int e j + n)%Z


Thanks.

regards,
tk