coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Castéran Pierre <pierre.casteran AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] : Proving "simple lemmas" with Functions or Program fixpoints
- Date: Sun, 22 Aug 2021 17:37:50 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.casteran AT gmail.com; spf=Pass smtp.mailfrom=pierre.casteran AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f45.google.com
- Ironport-hdrordr: A9a23:CuCic6xPqZo1c+fqqg4pKrPw8r1zdoMgy1knxilNoH1uA7GlfqWV98jzuiWYtN8uYgBEpTn+AtjnfZqxz+8X3WBpB8bEYOCEghrTEGgB1/qf/9SIIUSXygdg79YDT0AVYOeAdmSS5fyb3ODSKbkdKbe8nJxArN2ut0uEJWlRGthdBqlCYDpyeyVNNW177OICdaZ0nfAomwad
- Ironport-phdr: A9a23:DpPfvBNsJQ7iu0s6Fbcl6nauDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv60r3QaCANqTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yfy+94fXbglVizawYbF/JwiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjULxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4LpxSBLwiCkIKzE2/nzZhMx+kqxUohGvqRtkzoHOfI2VMeBzfqPBcd4YQ2dKQ8ZfVzZGAoO5d4YCEfAOPf1Er47nvVsBtx2+ChG2CuPu1DBInGX20rMn2OkmCQHG3RIvH8gUsHvKttn6KL0dUfupzKbW1zXMdfVW1Czy6IjNaB8hoPWMUahsfsrWzEkiDgXIhUifpoL5JT2azPgNs3SF4Op6U+Kik3Arph9wrzWzxMohhZXEip4Rx13F+yh3wIk4KcOmREJmfNKpDpteuiCZOoZ2Tc0vTW9mtikmx7AFp5K2fjUGxYghyhXCaPKHa5CF7gz/WOuVOzt1h3JodKiiixqs8kWs0OLxW8ms3FpUtCVJjsTAu3UR2BPI98SKTv5w80W61juP0g3e5P9LLVwomafeNZEu36Q/m5kWvEvYHyL7lkD7gaCLekgl5uel7vnrba7iq5OBMYJ/lxvwPb40msOlBOQ1KggOUHaf+eS7zLDj+Ff2QLROjvEvnKjZtY3WKd0VpqO2AwJZyIkj6xG4Dzep1NQXg2MLI05CeBKCl4TpOlfOL+7kDfqnnVigjDNmy+rFM7DhGJnBM2bPnbT7cbty60NQ0A8zwspe55JQBLEBOvXzWkrpudzADx82LRa0w/z5B9lnyowRQ3mPArOHP6PIq1CI4PkiI+aJZIAPuTb9L+Ip6OLpjX88gVMdZ7Wm3YMLaHCkGfRrO1mWYX31gtsYDWgKuhc+Q/fxhV2ZUT9TYm6yULgm6jE6DoKmF4bDSZq3jLyPxifoVqFRM2tBExWHFWriX4SCQfYFLiyIceF7lTlRfrG6Vw473BeZjA730aBqZr7M+yACr5+l39Fu++DJnBca+jl9DsDb2GaIGTIn1lgUTiM7ifgs6Xd2zU2OhPAQaxlwGtla5vcPWQA/Z8a0JwNSBNX7WwaHddCMGg/OqjSOBDgwSpcuxoZLbRogXdqliR/H0myhBLpHz9S2
Hello,
Using Search, Coq gives you some lemmas proved by Function (works with Equations too).
Msubstr_equation allows you to finish your proof.
Lemma test: forall a s n, msubstr (String a s) (S n) = msubstr s n.
Proof.
intros. Search msubstr.
rewrite msubstr_equation.
cbn.
Search (_-0).
rewrite Nat.sub_0_r.
reflexivity.
Qed.
Hope this helps,
Pierre
Le 22 août 2021 à 17:27, Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com> a écrit :Lemma test: forall a s n, msubstr (String a s) (S n) = msubstr s n.
- [Coq-Club] : Proving "simple lemmas" with Functions or Program fixpoints, Wendlasida Ouedraogo, 08/22/2021
- Re: [Coq-Club] : Proving "simple lemmas" with Functions or Program fixpoints, Castéran Pierre, 08/22/2021
Archive powered by MHonArc 2.6.19+.