The Coq mailing list

[Jasper Stein <J.Stein AT cs.ru.nl>]

Dear all,

I want to evaluate stuff. So I do, e.g., Eval cbv beta in ((fun (n:nat) => n) 
(S O)), getting me the proper answer 1%nat.

Now. Since I want to do more complicated reductions with more elaborate 
reduction flags as well, I turned to the Coq manual. Here are my questions.

Firstly. I see there is a reduction flag evar that tries to instantiate 
existential variables. Does this come up at all in an out-of-proof-mode 
context? If so, how? In proof-mode, how does it do instantiation, does it 
just pick any old term from the context having the right type? Does it try to 
generate terms? Can anyone show a small example where evar makes a 
difference? In short, what does it do?

Also. How is the zeta flag supposed to work? I get 

Eval cbv zeta in (let (a,b):=(conj I I) in a). 
     = let (a, _) := conj I I in a
     : True

while I was expecting the answer "=I : True". Why doesn't it say this? Isn't 
it supposed to? Why not?

Then. I see "simpl" is supposed to do beta iota, then delta, and then another 
beta iota. How do I know which constants get unfolded by the delta bit? When 
I do

Eval simpl in (sweep_rows Qm_2_2_is_one).

I get an immediate answer, while doing

Eval cbv beta iota delta beta iota in (sweep_rows Qm_2_2_is_one).

seems to loop (even without the second beta iota flags). "top" reveals that 
Coq's memory use increases hugely, so I suppose lots of constants get 
unfolded - far too many, apparently. I'd like to know how to mimic simpl. 
(I'm not sure if this is actually a bug. It looks like it. I always have to 
interrupt after a while, and it is not uncommon for coq to grow up to several 
100s of MBs in that period; I can't tell if Coq actually terminates by 
itself.)

Finally. Is there a way to do something like Eval (red;hnf) in expr. or Eval 
unfold const in (Eval simpl in expr).  ...?

Jasper
-- 
The problem with having an open mind is that people toss in garbage