## Stream: Coq users

#### 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).
``````

``````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: Jun 22 2024 at 16:02 UTC