## Stream: Coq users

### Topic: Transitivity of Nat.modulo

#### Julin S (Jun 09 2022 at 07:03):

I was trying to prove transitivity of `Nat.modulo` operation.

(Such a proof is not part of the standard library, is it?

Is there a way to search lemmas in libraries which aren't explicitly loaded as well?)

This is what I started:

``````Theorem modulo_trans : forall a b n:nat,
Nat.modulo n a = 0-> Nat.modulo a b = 0 -> Nat.modulo n b = 0.
Proof.
intros.
induction n.
``````

at this point, the goal was:

``````2 subgoals

a, b : nat
H : Nat.modulo 0 a = 0
H0 : Nat.modulo a b = 0

========================= (1 / 2)

Nat.modulo 0 b = 0

========================= (2 / 2)

Nat.modulo (S n) b = 0
``````

How could we proceed from here?

#### Julin S (Jun 09 2022 at 07:04):

`Nat.modulo 0 n = 0 ` for any `n`. But how can that be used here?

#### Julin S (Jun 09 2022 at 07:08):

I tried a lemma for that:

``````Lemma modulo_0 : forall n:nat, Nat.modulo 0 n = 0.
Proof.
intros.
induction n.
- reflexivity.
- simpl.
``````

But for this the goal became:

``````1 subgoal

n : nat
IHn : Nat.modulo 0 n = 0

========================= (1 / 1)

n - n = 0
``````

I thought `n-n=0` would be cake, but couldn't do it.

`Search (_ - _)` didn't give anything.

#### Julin S (Jun 09 2022 at 07:11):

Then I made another lemma and was able to okay `modulo_0`.

``````Lemma minus_n_n_0 : forall n:nat, n - n = 0.
Proof.
intros.
induction n.
- reflexivity.
- simpl.
exact IHn.
Qed.

Lemma modulo_0 : forall n:nat, Nat.modulo 0 n = 0.
Proof.
intros.
induction n.
- reflexivity.
- simpl.
exact (minus_n_n_0 n).
Qed.
``````

#### Julin S (Jun 09 2022 at 07:12):

I guess induction isn't the right way to prove `modulo_trans`?

#### Guillaume Melquiond (Jun 09 2022 at 07:21):

Julin S said:

I thought `n-n=0` would be cake, but couldn't do it.

`Search (_ - _)` didn't give anything.

Have you loaded the arithmetic libraries using `Require Import Arith`? Because `Search (_ - _)` certainly gives a ton of results, including `minus_n_O`.

#### Julin S (Jun 09 2022 at 07:24):

Guillaume Melquiond said:

Julin S said:

I thought `n-n=0` would be cake, but couldn't do it.

`Search (_ - _)` didn't give anything.

Have you loaded the arithmetic libraries using `Require Import Arith`? Because `Search (_ - _)` certainly gives a ton of results, including `minus_n_O`.

Got the search results after importing it. Thanks.

#### Julin S (Jun 09 2022 at 07:25):

Is there a way to get hints as to the possible modules that might have the results that we are searching for?

I suppose there is no way other than to get familar with the modules themselves?

#### Julin S (Jun 09 2022 at 07:26):

Found some results involving `mod` as well after importing `Arith`, but not for transitivity.

#### Guillaume Melquiond (Jun 09 2022 at 07:29):

You might want to use `Nat.divide` instead of `Nat.modulo`, in which case you have `Nat.divide_transitive`.

#### Julin S (Jun 09 2022 at 07:31):

Is there something similar in the `Type` world? `divide` results in `Prop`.

#### Julin S (Jun 09 2022 at 07:31):

Or is there a way to make boolean out of Prop?

#### Julin S (Jun 09 2022 at 07:33):

Found `is_true` but that makes `Prop` out of a `bool`.

#### Julin S (Jun 09 2022 at 07:33):

I guess there's no way to decide for a `Prop` (or something like that), right?

#### Guillaume Melquiond (Jun 09 2022 at 07:34):

No, but you can go from `Nat.modulo` (for computability) to `Nat.divide` (for proofs) and vice versa, using `Nat.mod_divide`.

#### Julin S (Jun 09 2022 at 07:40):

From `Nat.divide` to `Nat.modulo` as well?

#### Guillaume Melquiond (Jun 09 2022 at 07:40):

Yes.

Last updated: Jun 15 2024 at 05:01 UTC