The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Thanks! I managed to do one more step.

Now I'm left with

Lemma map_nil : forall (a b : Type) (f : a -> b), map f nil = nil.

Proof.

Admitted.

Lemma list_add_nil : forall A (a b : list A),

a ++ b = a -> b = nil.

Proof.

Admitted.

Lemma augmentBlk_zServerState : forall blk, augmentBlk blk zServerState = blk.

Proof.

intros.

unfold augmentBlk.

induction blk.

rewrite map_nil.

simpl.

reflexivity.

apply list_add_nil in IHblk.

Admitted.

And

• a: registration
• blk: list registration
• IHblk: concat (concatListOption (map (fun reg : registration => augmentReg reg zServerState) blk)) = nil

• 1/1(a :: blk) ++ concat (concatListOption (map (fun reg : registration => augmentReg reg zServerState) (a :: blk))) = a :: blk

I think I need to throw away the information about (a :: blk) having atleast one element? `rewrite IHblk` isn't able to match anything in the current goal.

Thanks.

Ram

On Thu, Jan 11, 2018 at 5:34 PM, Hiroki Oshikawa <oshi.hiroki.ml AT gmail.com> wrote:

`list_add_nil` cannot be applied to `IHblk`, because it requires `blk` has at least one element, but `blk` can be `nil`.

Changing the definition of `list_add_nil` to

```

Lemma list_add_nil : forall A (a b : list A),

    a ++ b = a -> b = nil.

```

may solve the problem.

best

2018-01-12 9:52 GMT+09:00 Ramkumar Ramachandra <artagnon AT gmail.com>:

Hi folks,

I have this code:

Lemma map_nil : forall (a b : Type) (f : a -> b), map f nil = nil.

Proof.

Admitted.

Lemma list_add_nil : forall A (a : A) (b c : list A),

(a :: b) ++ c = a :: b -> c = nil.

Proof.

Admitted.

Lemma augmentBlk_zServerState : forall blk, augmentBlk blk zServerState = blk.

Proof.

intros.

unfold augmentBlk.

induction blk.

rewrite map_nil.

simpl.

reflexivity.

Admitted.

And these are my hypotheses/goals:

• a: registration
• blk: list registration
• IHblk: blk ++ concat (concatListOption (map (fun reg : registration => augmentReg reg zServerState) blk)) = blk

• 1/1(a :: blk) ++ concat (concatListOption (map (fun reg : registration => augmentReg reg zServerState) (a :: blk))) = a :: blk

Looks pretty straightforward, but I'm not able to figure out how to apply list_add_nil to either IHblk or the goal. What am I missing?

Thanks.

Ram