Proof by Exhaustive Computation for small initial segment of natural numbers (in Coq)

I have two functions f, g : nat -> nat. Let's pretend that f and g are cheap to compute.

I would like to prove something like

Lemma upto_20 (n : nat):
n <= 20 -> f n = g n.


For the proof, I could write destruct n 20 times, but that seems suboptimal. Is there some way with which I can finish the proof like this?

Proof.
compute n from 0 to 20.
Qed.

• Does repeat work?
– Trebor
Jul 12, 2022 at 10:47

You can prove in userland that these kind of problems are decidable (I am not too familiar with the stdlib so it can probably be golfed down):

Require Nat.

Definition Decidable (t : Prop) : Prop := t \/ (t -> False).

Lemma dec_bounded
(P : nat -> Prop) (Pdec : forall k, Decidable (P k))
(bound : nat) : Decidable (forall (k : nat), k <= bound -> P k).
Proof.
induction bound as [|n  IHn].
- destruct (Pdec O) as [PO | nPO].
+ left; intros k klt; inversion klt; assumption.
+ right; intro nPk; apply nPO; auto.
- destruct (Pdec (S n)) as [PSn | nPSn].
+ destruct IHn as [Pk | nPk].
* left; intros k klt; inversion klt; auto.
* right; intro nPSk; apply nPk; auto.
+ right; auto.
Defined.


For your special case, I also need to prove that equality of natural numbers is decidable. I am using Defined everywhere so that Coq will happily compute with all of these things.

Definition dec_nat (k : nat) : forall (n : nat), Decidable (k = n).
Proof.
induction k as [|k IHk]; intro n; destruct n.
- left; reflexivity.
- right; inversion 1.
- right; inversion 1.
- destruct (IHk n) as [Pk | nPk].
+ left; auto.
+ right; intro contra; apply nPk; inversion contra; auto.
Defined.


And then you can add a little glue to grab the goal, run the decision procedure and apply the resulting proof:

Ltac bounded_equality := match goal with
|- ?n <= ?bnd -> ?f ?n = ?g ?n =>
let k := fresh "k" in
let val := ltac:(eval compute in (dec_bounded (fun k => f k = g k) (fun k => dec_nat (f k) (g k)) bnd)) in
match val with
| (or_introl ?prf) => eapply prf
| ?p => idtac "Couldn't find a proof"
end
end.


In action it looks something like this:

Definition double (n : nat) := n + n.

Lemma upto_20 (n : nat) :
n <= 20 -> double n = 2 * n.
bounded_equality.
Qed.

• This is great. Indeed I would like to know if there are any more succinct techniques using stdlib or ssreflect tactics that does not require rolling your own Aug 1, 2022 at 14:09