Lemma about N.div_eucl · Coq users

Stream: Coq users

Topic: Lemma about N.div_eucl

Rodolphe Lepigre (Oct 29 2023 at 13:17):

I need to prove the following involving N.div_eucl:

Lemma xxx (b q r : N) : (r < b)%N → N.div_eucl (b * q + r)%N b = (q, r).

This seems to me like the most trivial imaginable property about that function, but I cannot seem to be able to prove it using existing lemmas. Is it just that there are not enough lemmas in the standard library, or am I missing something obvious?

Gaëtan Gilbert (Oct 29 2023 at 13:37):

doesn't look like there are lemmas about N.div_eucl other than N.div_eucl_spec which isn't strong enough AFAICT

Olivier Laurent (Oct 29 2023 at 13:59):

There are more results on the projections:

Definition div a b := fst (div_eucl a b).
Definition modulo a b := snd (div_eucl a b).

This leads to:

From Coq Require Import NArith.
Open Scope N.

Lemma xxx (b q r : N) : (r < b) -> N.div_eucl (b * q + r) b = (q, r).
Proof.
intro Hr.
rewrite (surjective_pairing (N.div_eucl (b * q + r) b)). f_equal.
- symmetry. apply (N.div_unique (b * q + r) _ _ _ Hr). reflexivity.
- symmetry. apply (N.mod_unique (b * q + r) _ q _ Hr). reflexivity.
Qed.

Paolo Giarrusso (Oct 29 2023 at 14:02):

I'd consider adding some N.div_eucl_eq lemma to help discovery, _and_ xxx itself

Lemma div_eucl_eq a b :
  N.div_eucl a b = (N.div a b, N.modulo a b).
Proof. rewrite /N.div /N.modulo. by destruct N.div_eucl. Qed.

Paolo Giarrusso (Oct 29 2023 at 14:03):

I believe N.div_eucl_eq worthwhile even if I already happened to know N.div had more results (I'd seen them in the past).

Paolo Giarrusso (Oct 29 2023 at 14:05):

(I'm afraid I won't get to send a PR myself so I won't judge others)

Olivier Laurent (Oct 29 2023 at 14:37):

It is also possible to go through N.div_eucl_spec:

From Coq Require Import NArith.
Open Scope N.

Lemma xxx (b q r : N) : r < b -> N.div_eucl (b * q + r) b = (q, r).
Proof.
intro Hr.
assert (Hspec := N.div_eucl_spec (b * q + r) b).
destruct (N.div_eucl (b * q + r) b) as (q', r') eqn:Hdiv_eucl.
apply N.div_mod_unique in Hspec as [-> ->]; [ reflexivity | assumption | ].
change r' with (snd (q', r')). rewrite <- Hdiv_eucl. apply N.mod_lt.
intros ->. exact (N.nlt_0_r _ Hr).
Qed.

Last updated: Oct 13 2024 at 01:02 UTC