The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

- the fix tactic is for defining fixpoints, see 
https://coq.inria.fr/distrib/current/refman/tactics.html#hevea_tactic127

- each fixpoint has a principal argument, indicated in the {struct} 
annotation. It will reduce only when applied such that the principal 
argument is a constructor (or something that reduces to a constructor). 
So if you do "destruct steps" or "induction steps" it should reduce once.

Gaëtan Gilbert

On 12/01/2018 22:05, Ramkumar Ramachandra wrote:
> Hi folks,
>
> This is my code:
>
> (* stageHandler will take a given block and run it through a single 
> stageStep *)
> Definition stageHandler (s : stageStep) (blk : block) (t : serverState)
> : (stageStep * serverState) :=
> match s with
> | propose => let blk' := blk ++ (issueVerdicts t) in
> (preVote (augmentBlk blk' t), t)
> | preVote blk => ((preCommit blk), t)
> | preCommit blk => (propose, (commitBlock blk (updateRunningCounters blk 
> t)))
> end.
>
> (* readEvalLoop will run for a given number of steps: in real-world, 
> forever *)
> Fixpoint readEvalLoop (steps : nat) (s : stageStep) (blk : block) (t : 
> serverState)
> : serverState :=
> match steps with
> | O => t
> | (S n') => let (s', t') := stageHandler s blk t in readEvalLoop n' s' 
> blk t'
> end.
>
> Theorem readEvalLoop_ind : forall steps blk t,
> let blk' := augmentBlk (blk ++ issueVerdicts t) t in
> readEvalLoop (steps + 3) propose blk t =
> readEvalLoop steps propose blk' (commitBlock blk' (updateRunningCounters 
> blk' t)).
> Proof.
> intros.
> unfold readEvalLoop; unfold stageHandler.
> fix readEvalLoop 1.
> Abort.
>
> If I have `steps` fixed at O, the proof completes pretty easily. 
> However, in this case, I get:
>
> Ltac call to "fix (ident) (natural)" failed. Ltac call to "fix (ident) 
> (natural)" failed. Not enough products.
>
> What does this mean, and how am I supposed to reduce `fix` terms? None 
> of the other tactics seem to work.
>
> Thanks.
>
> Ram