## Stream: Coq users

### Topic: nat mod sub

#### Karl Palmskog (Oct 31 2023 at 11:26):

OK, I was thinking this was going to be straightforward to prove but (a) I'm strapped for time and (b) Stdlib seemingly has nothing connecting `mod` and `sub` for nats except `Nat.mod_eq` and `Nat.divmod_spec`. If anyone can pitch in and formulate a general lemma connecting `mod` and `sub`, I volunteer to submit to Stdlib as Coq PR (unless I missed something):

``````From Coq Require Import Arith.
Lemma add_sub_mod_0 : forall m n : nat, n <> 0 -> (m + (n - m mod n)) mod n = 0.
Proof.
(* induction not likely to help much? *)
``````

#### Julio Di Egidio (Oct 31 2023 at 13:57):

Not sure how much it helps, but I have managed to write this (I suppose it can be improved: for one thing I have not been agonizing much with Search and finding a most direct/simplest way):

``````Require Import Coq.Arith.Arith.

Lemma add_sub_mod_0 : forall m n : nat,
n <> 0 -> (m + (n - m mod n)) mod n = 0.
Proof.
intros m n H.
destruct m.
- rewrite Nat.Div0.mod_0_l.
rewrite Nat.sub_0_r.
rewrite Nat.Div0.mod_same.
reflexivity.
rewrite <- (Arith_prebase.le_plus_minus_stt
(S m mod n) n).
+ apply Nat.Div0.mod_same.
+ apply Nat.lt_le_incl.
apply Nat.mod_upper_bound.
apply H.
Qed.
``````

#### Karl Palmskog (Oct 31 2023 at 15:10):

thanks, here is a shorter version, I'll see if I can figure out some lemma to extract from this:

``````Lemma add_sub_mod_0 : forall m n : nat, n <> 0 -> (m + (n - m mod n)) mod n = 0.
Proof.
intros m n Hn; destruct m.
- rewrite (Nat.mod_0_l _ Hn).
rewrite Nat.sub_0_r.
apply (Nat.mod_same _ Hn).
- rewrite <- (Nat.add_mod_idemp_l _ _ _ Hn).
+ apply (Nat.mod_same _ Hn).
+ apply Nat.lt_le_incl.
apply (Nat.mod_upper_bound _ _ Hn).
Qed.
``````

#### Notification Bot (Oct 31 2023 at 15:21):

Karl Palmskog has marked this topic as resolved.

#### Notification Bot (Oct 31 2023 at 15:36):

Pierre Jouvelot has marked this topic as unresolved.

#### Pierre Jouvelot (Oct 31 2023 at 15:37):

In fact, the `destruct` is not required:

``````From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma add_sub_mod_0 : forall m n : nat, n <> 0 -> (m + (n - m %% n)) %% n = 0.
Proof.
move=> m n /eqP ne0.
by rewrite -modnDml subnKC ?modnn // ltnW // ltn_mod lt0n.
Qed.
``````

#### Julio Di Egidio (Oct 31 2023 at 15:45):

@Pierre Jouvelot : but that requires mathcomp, not just Arith/the stdlib...

#### Julio Di Egidio (Oct 31 2023 at 15:54):

But you are absolutely right, indeed here it is:

``````Require Import Coq.Arith.Arith.

Lemma add_sub_mod_0 : forall m n : nat,
n <> 0 -> (m + (n - m mod n)) mod n = 0.
Proof.
intros m n Hn.
- apply Nat.Div0.mod_same.
- apply Nat.lt_le_incl.
apply Nat.mod_upper_bound.
apply Hn.
Qed.
``````

CC: @Karl Palmskog

#### Pierre Rousselin (Oct 31 2023 at 19:04):

Nice, let's see what lemmas and in which form can be transferred from ZArith to Arith. I hope I can help.

Last updated: Jun 13 2024 at 21:01 UTC