The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 2/9/19 3:43 PM, Gert Smolka wrote:
> Is there tactic support for proving lemmas involving division over nat, for 
> instance


Unfortunately, it seems you need to populate the assumptions with
instances of Nat.div_mod and Nat.mod_upper_bound for nia to do
something.

Here is how you can solve "automatically" your 3 examples:

=================================================================

Require Import Psatz.
Require Import Arith.

Lemma bound_nat a b :
 (b = 0 /\ a / b = 0) \/ (0 < b /\ a = b * (a / b) + a mod b /\ a mod b
< b).
Proof.
destruct b; [left | right].
  now destruct a; simpl; lia.
repeat split; try lia.
  apply Nat.div_mod; lia.
apply Nat.mod_upper_bound; lia.
Qed.

Ltac rm_div :=
match goal with
|- context [ ?a / ?b] =>
     let tmp := fresh "Hl" in
     let u := fresh "dd" in
     let v := fresh "mm" in
     assert (tmp := bound_nat a b);
     set (u := a / b) in *;
     set (v := a mod b) in *
|
|- context [ ?a mod ?b] =>
     let tmp := fresh "Hl" in
     let u := fresh "dd" in
     let v := fresh "mm" in
     assert (tmp := bound_nat a b);
     set (u := a / b) in *;
     set (v := a mod b) in *
end.

Ltac dnia := repeat rm_div; nia.

Goal forall k x, 1 <= k <= x -> x / k >= 1.
intros.
dnia.
Qed.

Goal forall k x y, x <= y -> k >= 1 -> x / k <= y / k.
intros.
dnia.
Qed.

Goal forall k x, k >= 1 -> (k * x) / k = x.
intros.
dnia.
Qed.

===============================================================