The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Have you tried coqhammer? It might be helpful in these cases.

On Sat, Feb 9, 2019 at 6:20 PM Laurent Thery 
<Laurent.Thery AT inria.fr>
 wrote:
>
>
>
> 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.
>
> ===============================================================