The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Hi Pierre,

There's way too much code there to fit in an email to coq-club (the mailing list rejects messages larger than a certain size). Let me attempt to hand you a reduced case.

From Coq Require Import

Lists.List

Arith.PeanoNat.

Inductive registration : Type :=

| A : nat -> registration

| B : nat -> registration.

Record serverState : Type := mkServerState {

q : nat

}.

Definition block := list registration.

Definition updateRunningCounters (e : block) (t : serverState) : serverState :=

fold_left (fun acc reg =>

match reg with

| A _ => (match acc with

| mkServerState a => mkServerState (S a)

end)

| _ => t

end) e t.

(* Proposition not defined in terms of implementation; needs to be proved *)

Definition noUpdateRunningCounters (e : block) : Prop :=

fold_left (fun acc reg =>

acc \/ match reg with

| A _ => False

| _ => True

end) e True.

Theorem runningCounters_noUpdate : forall e t,

noUpdateRunningCounters e <-> updateRunningCounters e t = t.

Proof.

intros.

induction e; simpl.

intuition.

unfold noUpdateRunningCounters; simpl.

trivial.

generalize (a :: e); intro l.

Admitted.

The hypotheses/goals look like:

• a: registration
• e: list registration
• t: serverState
• IHe: noUpdateRunningCounters e <-> updateRunningCounters e t = t
• l: list registration

• 1/1noUpdateRunningCounters l <-> updateRunningCounters l t = t

Now what?

Thanks!

Ram

On Wed, Jan 17, 2018 at 3:46 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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