The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

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