3
$\begingroup$

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.
$\endgroup$
1
  • $\begingroup$ Does repeat work? $\endgroup$
    – Trebor
    Jul 12, 2022 at 10:47

1 Answer 1

5
$\begingroup$

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.
$\endgroup$
1
  • $\begingroup$ 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 $\endgroup$ Aug 1, 2022 at 14:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.