The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Hi Agnishom,

Agnishom Chattopadhyay 
<agnishom AT cmi.ac.in>
 writes:

> 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?

In addition to the other answers in the thread, you can indeed reflect a
(boolean) forall on an efficiently enumerable finite type to something
that will compute OK.

Using math-comp:

8<-----------------------------------------------------------------------8<
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma FFP n (f1 f2 : nat -> nat) :
  [forall x : 'I_n, f1 x == f2 x] = all [pred x | f1 x == f2 x] (iota 0 n).
Proof.
apply/eqfunP/allP=> eqf x; last by apply/eqP/eqf; rewrite mem_iota /=.
by rewrite mem_iota; case/andP=> ? hx; have /= -> := eqf (Ordinal hx).
Qed.

Lemma can_be_brute_forced : forall (n : 'I_10), n == (n ^ 5) %[mod 10].
by apply/forallP; rewrite (FFP _ _ (fun x => x ^ 5 %% 10)); compute.
Qed.
8<-----------------------------------------------------------------------8<

Beware I wrote the FFP function in a hurry long time ago, likely the
code is not very good and math-comp may already provide that lemma in
one form or another.

Kind regards,
Emilio