coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How do I handle computational parts of a proof?
Date: Mon, 8 Jul 2019 16:36:40 +0200
Organization: LORIA

Le 08/07/2019 à 16:31, Agnishom Chattopadhyay a écrit :
> Lemma can_be_brute_forced : forall (n : nat), n < 10 -> n mod 10 = (n ^
> 5) mod 10.

Require Import Arith Omega.

Lemma can_be_brute_forced : forall (n : nat), n < 10 -> n mod 10 = (n ^
5) mod 10.
Proof.
intros n.
do 10 (destruct n as [ | n ]; [ trivial | ]); omega.
Qed.

[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