The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Greetings,

I will explain my problem with very simple example. Example is stupid
because my actual environment is very complex and very long:

(*Definitions and declarations:*)
Section A.
Parameter y : nat.
Let x:=3 : nat.
Definition funkcija y := y*y.

(*Goal:*)

Goal (y = funkcija x -> 1=1) /\ (y = funkcija x -> 1<>1).

(*Tactics:*)

compute;split;intro H;try tauto.

After tactics one subgoal remains unproved. After that I have hypothesis H
: y = 9. This result is important for me and I will store this result
("9") on some list. What I need is to repeat all (environment and proof of
Goal with the same tactics) but with new value "9" for x. Problem is
because I need to have "Let" or global "Parameter" definition for x. From
some reasons I can't work with Hypotheses.
So, my question is: Is it possible to store result 9 on list and then to
repeat all with "Let x:=9 : nat" (instead "Let x:=9 : nat"). I now this
require some kind of rewriting in constants but maybe is it possible to
solve with opening and closing of Sections or something else.
Everything sound like recursive function but from another reason it can
not be function.
I spend two days to find a way but I didn't find solution.

Thank you very much,

Marko Malikoviæ