The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Please give a SELF CONTAINED code. So that we can replay your code.
Best
Pierre

2018-01-17 0:14 GMT+01:00 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