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: Laurent Thery <Laurent.Thery AT inria.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 17:12:11 +0200
Autocrypt: addr=thery AT sophia.inria.fr; prefer-encrypt=mutual; keydata= mQENBE3a3V8BCADTeORKU7I7UmBBcs4VhSCq1IgKD8vdmdrGAlF3IJSFng7Fk8+MgS2gWYcS Ukf5t+rjNM3Z6brfYXc1naZlf2JPGHvAGiz8+TkXL+/ZA6+gAoIKy/iKyD+hCD8m92WH3rPH vCX6EJ44FEI7gUJ37GlTjvuP0I55vaFcwEg8nDgkALaCJvrSHtePuPKR1Q+9q2dgR7fTObal HYGMAsgT6k6n2ofe4Q6VFRLJhruU02qAfV5zgIoa3xgrTwSr4RRDILHttAw7EN6aLG6JycJ7 sPsPsiQzrd/tFsNbiHYeojJCkU2pDSQ3pBtXAJL/z2pMWTeTXvA60l9w0sDO7M3mkC3vABEB AAG0J0xhdXJlbnQgVGjDqXJ5IDxMYXVyZW50LlRoZXJ5QGlucmlhLmZyPokBOAQTAQIAIgUC TdrdXwIbAwYLCQgHAwIGFQgCCQoLBBYCAwECHgECF4AACgkQHHaWvRTi0tpIgggAnSUYcU2N uchXkGGwmPuLmvSUMiLkyFPs9GF2YF1ONOuJtpnQMcpsseCkcmIjESz0h5OpknpyraUXvbh0 ZdFqaLC2E+GyV8/YQi71wSsTPgWP450u0XUt0ysjwkKW6aIxIhSzrtgNp4E6w5KzXVJxA/yM V5RNFHg/5uifgfv4b7xaGHV8L93NbSvedk1O7yje5Hqgfab0t6J5Kf0M3sG+pB3gEkDVK9B7 +0fhe7/5u1Nj5HoLWid8UNZfFzJzb18Xe2ckzNye0KdDtQFac8qGUzhLbEYt3ScYjRYTq9/d V4Cin39j7Oo64Nk71iiLBISyuk0Q9D+Jq7nwwcQr/R8s1rkBDQRN2t1fAQgA7H6aX6BfdO/X Vlf4EGEoyFQ5u/JDe+giIHWSS34YWDWVUYyp320CrAYAkh9lQ1Nvh1tsmgiUh5xnY7wY0tOi wJSm94XlYAmHrddmWVNXRn09GvZJhfI2LdVBg3oxPfc8+bV+Hz83z/5BMPLOogxB22QMPJ6e iD2EsUMPNsuCVQ8WNo6ZmueuuYe7vEUXLYdRXNumJJgekEuG/q1BD4xgfzWpWfUODm6WygWZ oov50DomcDcAHW03bgnHlqnYu20Qg00GqgR3FKlORTvnOxD5TMCXe+eLUxkQfvnjbIPhtrnJ hgJMKVkRBEoaQ/XA4FdvxloInYPbqxNZ72yd09BbewARAQABiQEfBBgBAgAJBQJN2t1fAhsM AAoJEBx2lr0U4tLaWNQH/2/fIaF9ngbKPBJbDxYa7glJuCfamJgy3R8mJ//VYsS4RbdroSX3 29EgWlTx2reu1b4C5n5k7l4KpLgsRIc3bLUasGv15nf8BqmKIMulidzsxJv86S2imY/0870Q NOiO9SElHE7/2q4J1m2ew77SegiqGVWHl6Zs+4ROfOILTy24o26BQMAZhPX7jEs04Atv6yjw OUIPbzFO+XRuKqkBwHn9S8+GQelT0Gh84Dc5D2jIF0+kWY7uHqe2O+2LPfgO2CYhqmVfr/Ym mZv2xUyhJ7gui2hYaggncQ96cM2KhnKlgMw8nStY0GTqVXLEjPYblz8mqtF8aBPRSk/DjjrF QeI=
Openpgp: preference=signencrypt

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.

[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