coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How do I handle computational parts of a proof?

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] How do I handle computational parts of a proof?
Date: Mon, 8 Jul 2019 16:31:14 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:KMCAPBOMPp5E4LI1N+kl6mtUPXoX/o7sNwtQ0KIMzox0Lf/5rarrMEGX3/hxlliBBdydt6sezbaO+P+/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCejbb9oIxi6sQrdu8sUjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksN/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b4wKD+cZIetYoI/9p1oVrRu+AgmsAf7kxyFIhnDswa06z+MhERnc0wM9H9IPsG7brdXoP6oVS++1w6/IzTTYb/NW3jf97ZPFfQwkofGNR75/a9bexVMuFwPDl1idr5HuMTCN1ukVrmSX8eRtWfiuhmMpsQ19vCSjy8k2hoXXm44Z1EjI+TtlzIsxP9G1S052bcS5HJZRtiyWLYR7T8AkTmp1oig10KcGtoS+fCUSyJQo2Rrfa/uffoiN+B3jVeKRLS1ki3JgebKznQy9/lS6xu39UMm4yFdKrixbndnQrn0BygLf58adRvZ88EqtwyiD2xzd5+1eP0w4iLTXJ4YkwrEql5oTtUrDHjXxmEXzlKKZbEok+u6p6+T8YrXmoZqcOpRohQH7M6QigNawDvgiPggPWWiX4f6826H7/U3lXLVKieU7nbXesJDDPMgUuqq5AxJO3Ys48Ba+DzKm0MwCknUdLVJFfgiHj4nzNF3ULvD4F6T3v1P5mzBygvvCI7fJA5PXL3GFnq2yU6x67ht1xwwy1tBY4tp/CrgdPPXrU0PxpdXJRkswPAq12ObgDf1204JYUGnJA6nPY/CaikOB+u96e7rEX4QSojuoc6F0tc6rtmcwnBomRYfs2JIWbH6iGfE/eheSZHuqi9xHEGFY51NiHtyvs0WLVHtoX1j3R7g1v2hpA4enS47IAIGr0uTYgXWLW6ZOb2UDMWiiVHflc4LdBaUJYSOWZMRkk3oNXv6gTd152A==

Hi;

I am trying to prove the following statement:

Lemma can_be_brute_forced : forall (n : nat), n < 10 -> n mod 10 = (n ^ 5) mod 10.

Now, this is a computational proof, which requires mostly evaluation, and noticing the fact that only 10 cases need to be worked out.

How do I prove this lemma without writing `destruct` 10 times?

--Agnishom

[Coq-Club] How do I handle computational parts of a proof?, Agnishom Chattopadhyay, 07/08/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Dominique Larchey-Wendling, 07/08/2019
  - Re: [Coq-Club] How do I handle computational parts of a proof?, Laurent Thery, 07/08/2019
    - Re: [Coq-Club] How do I handle computational parts of a proof?, Dominique Larchey-Wendling, 07/08/2019
      - Re: [Coq-Club] How do I handle computational parts of a proof?, Laurent Thery, 07/09/2019
        
        Re: [Coq-Club] How do I handle computational parts of a proof?, Dominique Larchey-Wendling, 07/09/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Emilio Jesús Gallego Arias, 07/09/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Laurent Thery, 07/09/2019