coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] [HELP] Induction over lists

From: Ramkumar Ramachandra <artagnon AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] [HELP] Induction over lists
Date: Thu, 11 Jan 2018 16:52:34 -0800
Authentication-results: mail2-smtp-roc.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-f178.google.com
Ironport-phdr: 9a23:oNn0iBwJ8GhKTD/XCy+O+j09IxM/srCxBDY+r6Qd1OoRIJqq85mqBkHD//Il1AaPAd2Craocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HObwlSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHohikJNCM3/n/LhcFrlq1XvAisqgZjz4LIYoyYMud1cKPHfdMdQGpMRtpfWDZEAoO/cosPCvAOPfxFpIfhvVQOqAGxChWsBOz1zD9Hm2X20rcn2OkmCw7GxhAgEMgBsHTSq9X1MrwfUe+wzKbSzDXDa+la1iv66IjNax0sp+yHU7FoccfJ10UjCwfIgk+TpIHlJT+Zy+UAv3WB4+Z9V++iiGgqoBxrrDe13McjkIzJi5oVyl/a8SV5x544JdiiR056Zd6oCZtRti+GO4dvTMMuXmNltSUgxr0Jvp67eycKyJA5yBLFd/OHdI2I7griVOaXPzh4mGpodKyjixu260Stye3xWtOp3FtLsyZJiMTAu3IO2hDL78iIUPp9/kOv2TaV0ADT7/lJLloularHMZEhzbgwlp0VsUnYES/2nV/5jK6Sdkk+5ueo7OHnbq38ppCAL490lh3+MqM2l8OjBuQ4KxECUHSf+eShz7Lu5lb5QbVPjv0uiKbVqpHaJcIBpq64GQBZyIgj6wzsRwuhhd8fhDwMKE9PUBOBlYngfV/Uc97iCvLquV2pkypuzuqOBLTkC57NJ37Pir6pKb9n90dTzg015d9a7pNQTLoGJaSgCQfKqNXEA0phYESPyOH9BYAlj9JMaSe0GqacdZjqnxqN7+MrLfOLYdZM6jn4IvkhofXpiC1gwANPTeySxZISLUuAMLF+OUzAOCjjh94AFSEBuQ9sFLW32m3HaiZaYjOJZ4x55jw/D9j4X4LKR4TokaPZmSniQc0QaWdBBVSBV3zvctfcVg==

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