Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] [HELP] Induction over lists

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [HELP] Induction over lists


Chronological Thread 
  • From: Ramkumar Ramachandra <artagnon AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] [HELP] Induction over lists
  • Date: Thu, 11 Jan 2018 18:01:08 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=artagnon AT gmail.com; spf=Pass smtp.mailfrom=artagnon AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f175.google.com
  • Ironport-phdr: 9a23:DuJZ+RE6ko9hJ40KwMQP6p1GYnF86YWxBRYc798ds5kLTJ78ps2wAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODw38G/XhMJ+j79Vrgy9qBFk2YHYfJuYOeBicq/Bf94XQ3dKUMZLVyxGB4Oxd5cBAPAEPeZbson9okEBrQGjDgewHuzvzyVHiWP23aIg1eQuDBvG0xY9FN8JqnvUtsn1O70dUeCzy6nIyy7Ob/xT2Tjn6YjIdgotru2LXbJ1aMfcz1QkGQDdjliIt4DpIzeY2v4OvmWb9eZsSOOih3M9pw1soDWixsEhgZTTiI0P0FDL7yB5zZ41JdKmTE57ZsapEJ5KuCGbM4t6W8MjQm90tCojxL0KpJy2cSgQxJQowB7fbPOHc4yW7R75SOmRJjJ4iGpkeLK5mRmy7VCtxvPgWsSwylpHrSpInsPRun0MyhDf8NWLR/l980u53DaAzQHT6uVKIUAukqrbLoYszaQqlpoPq0vDESn2mELwjKKNeUUk//Kn6+XjYrn8upCcMIp0hhnkMqsygsy/Hfg4Mg8WUmeH/uS8zaTv8lH9QLVXlfI7ibLZsZDfJcQDvKG1GQ5V0oA56xa+FTiqytoYnWNUZG5CLRmAls3iP0zECPH+F/a2xVq2wxlxwPWTBLTkAYjIJ2KLqr7kdL194khQ0gN7mdlF+5tbDLYHCP32U0718tffC0lqYESP3+/7BYAlhcslUmWVD/rBafKAgRqz/usqZtK0SsoQsTf5JeIi4qe333A8kF4ZO6Ku2MlOMSzqLrFdO0ycJEHUrJIZC25T51gxSeXrjBuJVjsBPy/vDZJ53SkyDcedNamGRo2ph+bfjiKyH5kTd38eT17VTiqueIKDVPMBLimVJ505nw==

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





Archive powered by MHonArc 2.6.18.

Top of Page