The Coq mailing list

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

I don't think you use generalize the right way. The effect of
"generalize T." here is to transform "a::e" into "l". That is a
generalization since "l" catches more possibilites than "a::e".

Here you *need* to keep the information about a::e.

Theorem runningCounters_noUpdate : forall e t,
  noUpdateRunningCounters e <-> updateRunningCounters e t = t.
Proof.
  intros.
  induction e; simpl.
  - intuition.
    unfold noUpdateRunningCounters; simpl.
    trivial.
  - split;intro.

then you are left with two subgoal that look OK but need some more
work to be proved.

One last remark:

Definition noUpdateRunningCounters (e : block) : Prop :=

why don't you use an inductive to define this property? You would have
more tools to deduce things (inversion, destruct, induction).

Here is a more or less idiomatic way of doing things (ony one
direction proved sorry lack of time):

Inductive noUpdateRunningCounters : block -> Prop :=
| noup1: noUpdateRunningCounters nil
| noup2: forall e n, noUpdateRunningCounters e ->
noUpdateRunningCounters (B n::e).


Theorem runningCounters_noUpdate : forall e t,
  noUpdateRunningCounters e <-> updateRunningCounters e t = t.
Proof.
  intros e t.
  split;intro h.
  - induction h.
    + cbn. reflexivity.
    + lazy beta delta [updateRunningCounters].
      rewrite (fold_right_app _ (B n :: nil) e).
      replace (fold_right
       (fun (reg : registration) (acc : serverState) =>
        match reg with
        | A _ => match acc with
                 | {| q := a |} => {| q := S a |}
                 end
        | B _ => t
        end) t e) with (updateRunningCounters e t) by reflexivity.
      cbn.
      reflexivity.
  -

2018-01-18 3:04 GMT+01:00 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
>
>