The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Oct 14, 2004 at 10:09:20AM +0200, Jasper Stein wrote:

> 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".

You need to throw in iota-reduction: conj is a constructor of an
inductive type, the reduction that "attacks" this is iota. Your let is
not quite "just" a local definition, it is a destructive let; you
destroy the conj to give names to its two subterms. That's actually
alternative syntax for case analysis when there is only one case
(section 1.2.13 of manual).

Compare with:

Coq < Eval cbv zeta in (let a:=(conj I I) in a).
     = conj I I
     : True /\ True


> 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).

This is different:

Cbv foo bar

does foo-bar normalisation, not foo-normalisation and then
bar-normalisation. The flags of Cbv form a set, not a list. It meant
it works until neither a foo step, nor a bar step can be done.

simpl is (from what you say) supposed to be:
cbv beta iota; cbv delta; cbv beta iota.

This is different from cbv beta iota delta: In the former, the result
is a beta-iota normal form, but not necessarily a delta-normal
form. If the "last" beta-iota step creates a delta-redex, this
delta-redex is not reduced, while it is with the latter.

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

"unfold" is simply delta-reduction, isn't it? I'd expect:

Eval cbv delta [const] in (Term)

to do the job.

-- 
Lionel