The Coq mailing list

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

Dear All,

First, Dear Stefan O'Rear - I know my goal as written is false, but it is
not important now. I said that my example is stupid and now is not
important his validity. But I think I found solution by itself:

So, my solution is (with a little different goal (but goal is not
important in this moment - again)):

Section A.
Definition funkcija x:=x*x.
Let x:=5.
Goal 2=3 -> x=10.
Let y:=funkcija x.
Goal 2=3 -> y=10.
compute in y.
clear x.
rename y into x.

From this we get:

Coq < Section A.

Coq < Definition funkcija x:=x*x.
funkcija is defined

Coq < Let x:=5.
x is defined

Coq < Goal 2=3 -> x=10.
1 subgoal

  x := 5 : nat
  ============================
   2 = 3 -> x = 10

Unnamed_thm < Let y:=funkcija x.
Warning: Local definition y is not visible from current goals
y is defined

Unnamed_thm < Goal 2=3 -> y=10.
1 subgoal

  x := 5 : nat
  y := funkcija x : nat
  ============================
   2 = 3 -> y = 10

Unnamed_thm0 < compute in y.
1 subgoal

  x := 5 : nat
  y := 25 : nat
  ============================
   2 = 3 -> y = 10

Unnamed_thm0 < clear x.
1 subgoal

  y := 25 : nat
  ============================
   2 = 3 -> y = 10

Unnamed_thm0 < rename y into x.
1 subgoal

  x := 25 : nat
  ============================
   2 = 3 -> x = 10

Unnamed_thm0 <

And this is what I wanted. Goal on the beginning was "2=3 -> x=10" with
local definition for x: "x := 5 : nat" but after all actions the goal is
the same "2=3 -> x=10" but with different local definition for x: "x := 25
: nat" and now I can solving the same goal with value 25 for x instead
value 5 on the beginning (some kind of iteration).

Just one thinks I don't understand:

In the last opened goal "Unnamed_thm0", I have:

Unnamed_thm0 < Print x.
*** [x := 5 : nat]

but:

Unnamed_thm0 < compute.
1 subgoal

  x := 25 : nat
  ============================
   2 = 3 -> 25 = 10

Can somebody explain me this ambiguity? All is in one section but where is
"x := 5 : nat" and where is "x := 25 : nat"?

Thank you very much and greetings from Croatia,

Marko Malikoviæ

Marko Malikoviæ reèe:
> 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æ
>