coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] need help with proof that indexes of true bools in list do index true bools

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] need help with proof that indexes of true bools in list do index true bools
Date: Wed, 22 Jul 2020 23:29:57 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f176.google.com
Ironport-phdr: 9a23:JRq0AB1TWGArwg68smDT+DRfVm0co7zxezQtwd8ZseMWLfad9pjvdHbS+e9qxAeQG9mCtbQZ06GL6ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhTexe7N/IAm5oQjRq8UdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnZhMJwkqxVvRGvqRtwzIHIb4+YL+Z+frrHcN8GX2dNQthdWipcCY28dYsPCO8BMP5Wo4n/oFsOqxq+BQqyC+Pr1DBHmGT73aI/0+s7EAHG2BYsEM4JsHTRotn+KaAfUeKyzKnOzDXDbO1Z2TPj54fWaR0hrvSMUqhxccrV00UgCwTFjlCJpIHjIjia2fgDvXKB4Op8SeKglXQnqwdprzag28shiInEi4MJxl3Y+it0wYg7KNm2RkN4fdKpEIVcuiWGO4V4TM0uXWNltDg4x7AHu5O1cjUHxZsnyRDQa/KKdZWD7BH7VOuJPzt0mHZodKi8ihuy60Ss1PPwWteu3FpXrCdIk8HAum4M2hDP98SKT+Zx80O91juK2A3e6/1ILVwxmKfUMZEt36A8m58OvUnAAiP6hkD7g7GUe0Uq9Oil7urnbav7qZKdMoJ5jhzxP6swlcG5HO82KBIBX3KB9uS5zLDj/VP2QLFNjvAul6nWqpHaJcACqq6gAA9Zz58v6xiiAzqk0dkUh3YHLFVCeBKIi4jmJUvCL+z/Dfe6m1iskTFryO7aPrD5HJnBMnzOnK3icLt98UJQ1hQ/wc5F655JCLwMIer/Wkrru9zZCh85PRa0w+HiCNhl1IMeXmSPAq6aMKzMtV+H+PwgLvKDZI8Qojn9Kvwl6+Tygn8+nF8RZbOp0ocPaHCkAvRmJF2UbmbrgtcYCGsFog4+TPHxh1CZSj5SZ3OyX7om6T0hCYKmC53DRoG3j7Cb0ie7BM4eWmcTAVeVVHzsao/MD/wLcWeZJtJruj0CT7moDYE7g0KArgj/nvBlKezV+SAcuJ/L29185umVnhY3v3QgDcOb0mKAS2x5tmwNTj4ymqt4pBoumR+4zaFkjqkARpRo7PRTX1JibM+O/6lBE9n3Hzn5UJKMQVeiTM+hBGhoHN00yt4KJU16Hof7102R72+RG7YQ0oezKtk0/6bbhSajIs98zzPf1/BkgQB5HI1AMmqpgqM5/A/WVdaQzxep0p2yfKFZ5xbjsX+ZxDPX7k5dWQ90F67CWCJHaw==

I know there is a trick to this kind of proof, and I may have seen it a
few times, but I don't remember it. I would appreciate anyone's help
with this:

From Coq Require Import Lists.List.
Import ListNotations.

Fixpoint truebits(i:nat)(lb:list bool) : list nat :=
match lb with
| true :: lb => i :: truebits (S i) lb
| false :: lb => truebits (S i) lb
| nil => nil
end.

(*list of indexes of true in lb*)
Definition all_truebits lb := truebits 0 lb.

(*if all indexes in ln are indexes of true in lb*)
Fixpoint are_truebits(ln:list nat)(lb:list bool) : Prop :=
match ln with
| i :: ln => (nth i lb false) = true /\ are_truebits ln lb
| nil => True
end.

Theorem all_truebits_are_truebits:
forall lb, are_truebits (all_truebits lb) lb.
(*How to prove this?*)

[Coq-Club] need help with proof that indexes of true bools in list do index true bools, jonikelee AT gmail.com, 07/23/2020
- Re: [Coq-Club] need help with proof that indexes of true bools in list do index true bools, Jason Gross, 07/23/2020
  - Re: [Coq-Club] need help with proof that indexes of true bools in list do index true bools, jonikelee AT gmail.com, 07/23/2020