The Coq mailing list

[AUGER <(e6fa90e88c%hidden_head%e6fa90e88c)Cedric.Auger(e6fa90e88c%hidden_at%e6fa90e88c)lri.fr(e6fa90e88c%hidden_end%e6fa90e88c)>]

Le Wed, 16 Dec 2009 15:19:58 +0100, Keiko Nakata  
<(e6fa90e88c%hidden_head%e6fa90e88c)keiko(e6fa90e88c%hidden_at%e6fa90e88c)kurims.kyoto-u.ac.jp(e6fa90e88c%hidden_end%e6fa90e88c)> a écrit:

> Hello,
>
> Trying to define a function with the Program command,
> I got an error
>
> The variable s0' was not found in the current environment.

This kind of error can occur in case you overwrite some variable,
coq doesn't do it and generate another variable with same prefix
(I bet you have a `s'` variable somewhere in your program).

Try the following:
------------------------------------
Definition truc (a : option bool) :=
match a with
| Some a => a = None
| None => a = Some true
end.
-------------------------------------
There is an obvious error, and the error is:
-------------------------------------
Error: In environment
a : option bool
a0 : bool
The term "None" has type "option ?13" while it is expected to have type
 "bool".
-------------------------------------
as you can see, a variable a0 is created and doesn't appear in your  
program;
in fact, coq rewrites your function in:
------------------------------------
Definition truc (a : option bool) :=
match a with
| Some a0 => a0 = None
| None => a = Some true
end.
-------------------------------------
with more complex definitions (for example with dependant types, this  
error refers explicitly to a0)
-------------------------------------
Definition succ (n : nat) : {m : nat | m = S n } :=
match n as n return {m : nat | m = S n} with
| O => exist _ (S O) (refl_equal _)
| S n => exist _ (S n) (refl_equal _)
end.
-------------------------------------
returns an error with n0 which doesn't appear
-------------------------------------
Error: In environment
n : nat
n0 : nat
The term "exist ?72 (S n0) (eq_refl ?74)" has type "sig ?72"
 while it is expected to have type "sig (fun m : nat => eq m (S (S n0)))".
--------------------------------------
With huge terms it is not easy to debug, renaming the overwritting  
variables may be sufficient:
--------------------------------------
Definition succ (n : nat) : {m : nat | m = S n } :=
match n as n_return return {m : nat | m = S n_return} with
| O => exist _ (S O) (refl_equal _)
| S n_pred => exist _ (S n_pred) (refl_equal _)
end.
---------------------------------------
Now errors are clear.
It is sad, but these renaming are necessary, since the overwritten  
variable cannot be generally
removed from environnement, as it may be used by other useful terms  
defined before the overwritting.
What should be done is to inform in the error report that s0' comes from  
s'.

But in your case if a variable is generated, it should be defined in the  
environnement.
If you show us your code, maybe we can solve your problem.

This error may also be due to things I don't think of...

> But my code does not contain any occurrence of s0'.
> What would be my problem?
>
> I am not sure if this is relevant,
> but I am defining a corecursive function, i.e. Program CoFixpoint.
>
> Best,
> Keiko
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay