The Coq mailing list

[Claude Marche <Claude.Marche AT inria.fr>]

Hi Taimoor,

Since your Coq goal comes from the Why3 system, I suggest you send your 
question to the Why3 Club instead.

To answer your question: since the add0 function is axiomatized, Coq 
cannot compute with it, so you must perform "evaluation" manually. A 
tactic like

repeat (rewrite add0_def; auto with *).

might do the job.

- Claude

Le 29/05/2012 14:58, 
mtkhan AT risc.jku.at
 a écrit :
> Hi,
>
> I have the following sketch of the premises of my proof.
>
> ...
> Parameter add0: (list or_integer_float) ->  Z ->  Z ->  Z.
>
> Axiom add0_def : forall (e:(list or_integer_float)) (i:Z) (j:Z) ...
> ....
>
> H0 : result =
>       add0
>         (Cons (Integer 5)
>            (Cons (Real (33 / 10))
>               (Cons (Integer 8) (Cons (Real (4 / 10)) (Cons (Integer 9)
> Nil)))))
>         0
>         (length
>            (Cons (Integer 5)
>               (Cons (Real (33 / 10))
>                  (Cons (Integer 8)
>                     (Cons (Real (4 / 10)) (Cons (Integer 9) Nil))))))
> ...
>
>
> And the goal is
>
> result = 13%Z.
>
> As a matter of fact the goal can easily be proved by just an application of
> the function
> add0 defined above. But it does not work for me. Can someone help me how we
> can
> prove such stuff, where we just need to compute the result of a function
> application.
>
> Thanks.
>
> tk

--
Claude Marché                          | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |