The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Hi Guillaume and Pierre,

Thanks for the help. I now have:

Theorem readEvalLoop_ind : forall steps blk t,

let blk' := augmentBlk (blk ++ issueVerdicts t) t in

let t' := commitBlock blk' (updateRunningCounters blk' t) in

readEvalLoop (steps + 3) propose blk t =

readEvalLoop steps propose blk' t'.

Proof.

intros.

induction steps.

rewrite add_0_1; reflexivity.

generalize (eq_refl (S steps)).

generalize (S steps) at -2; intro n.

induction n.

intuition.

generalize dependent (S n); intro n0.

Abort.

With the following hypotheses/goals:

• steps: nat
• blk: list registration
• t: serverState
• blk':= augmentBlk (blk ++ issueVerdicts t) t : block
• t':= commitBlock blk' (updateRunningCounters blk' t) : serverState
• IHsteps: readEvalLoop (steps + 3) propose blk t = readEvalLoop steps propose blk' t'
• n: nat
• IHn: n = S steps -> readEvalLoop (n + 3) propose blk t = readEvalLoop n propose blk' t'
• n0: nat

• 1/1n0 = S steps -> readEvalLoop (n0 + 3) propose blk t = readEvalLoop n0 propose blk' t'

Ofcourse, I'm unable to unify with `IHn`, because `n` and `n0` are superficially different. How am I supposed to convince Coq that they're really the same? I've included some additional code because Pierre requested it.

(* 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.

Cheers.

Ram