coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.best2018-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
- [Coq-Club] [HELP] Induction over lists, Ramkumar Ramachandra, 01/12/2018
- Re: [Coq-Club] [HELP] Induction over lists, Hiroki Oshikawa, 01/12/2018
- Re: [Coq-Club] [HELP] Induction over lists, Ramkumar Ramachandra, 01/12/2018
- Re: [Coq-Club] [HELP] Induction over lists, Hiroki Oshikawa, 01/12/2018
Archive powered by MHonArc 2.6.18.