The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Laurent,

I do not think Boolean's are really required here ...
just a variation around your proposal though 

Best,

D.

Require Import Arith Omega.

Section bounded_forall.

  Implicit Type (P : nat -> Prop).

  Fixpoint bounded_forall P n := 
    match n with 
      | 0 => True
      | S n => P 0 /\ bounded_forall (fun i => P (S i)) n
    end.

  Fact bounded_forall_spec P n : bounded_forall P n -> forall i, i < n -> P i.
  Proof.
    revert P.
    induction n as [ | n IHn ]; simpl; intros P Hn i Hi; try omega.
    destruct i as [ | i ]; try tauto.
    apply IHn with (P := fun i => P (S i)); try tauto.
    omega.
  Qed.

End bounded_forall.  

Lemma can_be_brute_forced : forall (n : nat), n < 10 -> n mod 10 = (n ^ 5) 
mod 10.
Proof.
  now apply bounded_forall_spec.
Qed.


----- Mail original -----
> De: "Laurent Thery" 
> <Laurent.Thery AT inria.fr>
> À: "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Lundi 8 Juillet 2019 17:12:11
> Objet: Re: [Coq-Club] How do I handle computational parts of a proof?

> On 7/8/19 4:36 PM, Dominique Larchey-Wendling wrote:
>> 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.
> 
> 
> If you want to program your proof as a single computation here is an
> alternative
> 
> Require Import Arith Lia.
> 
> Fixpoint icheck (n : nat) P Q :=
> ((P n =? Q n) &&
> (match n with O => true | S n1 => icheck n1 P Q end))%bool.
> 
> Lemma icheck_correct m P Q :
>  icheck m P Q = true ->
>  forall n, n < S m -> P n = Q n.
> Proof.
> induction m as [|m IH]; simpl.
> - intros HP [|n] H; try lia.
>  now destruct (Nat.eqb_spec (P 0) (Q 0)).
> - intros H1 n H.
>  destruct (Nat.eqb_spec (P (S m)) (Q (S m))); try discriminate.
>  assert (H2 : n = S m \/ n < S m) by lia.
>  destruct H2; subst.
>  + now destruct (Nat.eqb_spec (P (S m)) (Q (S m))).
>  + now apply IH.
> Qed.
> 
> Lemma can_be_brute_forced : forall (n : nat), n < 10 -> n mod 10 = (n ^
> 5) mod 10.
> Proof.
> now apply icheck_correct.
> Qed.