Stream: Coq users

Topic: nat mod sub


view this post on Zulip 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? *)

view this post on Zulip 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 <- Nat.Div0.add_mod_idemp_l.
    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.

view this post on Zulip 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).
  rewrite Nat.add_comm, Nat.sub_add.
  + apply (Nat.mod_same _ Hn).
  + apply Nat.lt_le_incl.
    apply (Nat.mod_upper_bound _ _ Hn).
Qed.

view this post on Zulip Notification Bot (Oct 31 2023 at 15:21):

Karl Palmskog has marked this topic as resolved.

view this post on Zulip Notification Bot (Oct 31 2023 at 15:36):

Pierre Jouvelot has marked this topic as unresolved.

view this post on Zulip 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.

view this post on Zulip Julio Di Egidio (Oct 31 2023 at 15:45):

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

view this post on Zulip 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.
  rewrite <- Nat.Div0.add_mod_idemp_l.
  rewrite Nat.add_comm.
  rewrite Nat.sub_add.
  - apply Nat.Div0.mod_same.
  - apply Nat.lt_le_incl.
    apply Nat.mod_upper_bound.
    apply Hn.
Qed.

CC: @Karl Palmskog

view this post on Zulip 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