The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

If you want do try an induction on the list e, you should not
introduce too much variables as in your proof start:
intros e j (h1,h2) n h3.

Just try:

Proof.
induction e.

Then look at the generated goals (empty list, list obtained by consing
some value of type or_integer_float to a list e0).
In the last case, you may have a look at the induction hypothesis on e0.

Then you have a lot of things to do : Instantiate (if needed) some universally
quantified hypotheses, case analysis on type or_integer_float, destruct the
conjonctions in your axioms, etc.

By the way, which libraries do you use on lists ? Standard Library's List ?

Pierre






Quoting 
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