The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Hi,

I have the following problem, which I found very difficult to proceed with, without the use of `generalize`:

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 (S steps).

intro n; replace n with steps.

induction steps.

rewrite add_0_1; reflexivity.

generalize dependent (S steps).

intro n0; replace n0 with steps.

apply IHsteps0.

Abort.

Here, readEvalLoop is a Fixpoint, which has three evaluation steps. Unfortunately, my strategy leaves me 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
• n: nat
• IHsteps0: readEvalLoop (steps + 3) propose blk t = readEvalLoop steps propose blk' t' -> readEvalLoop (steps + 3) propose blk t = readEvalLoop steps propose blk' t'
• n0: nat

• 1/2steps = n0
• 2/2steps = n

What are n0 and n? Where are they used? Can I somehow use `specialize`?

I'm having a hard time imagining where `generalize` would be useful, because it seems like you'll always end up with absurd things like this to prove.

Thanks.

Ram