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?

`Nat.modulo 0 n = 0 `

for any `n`

. But how can that be used here?

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.

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

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

?

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`

.

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`

.

No I hadn't loaded Arith.

Got the search results after importing it. Thanks.

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?

Found some results involving `mod`

as well after importing `Arith`

, but not for transitivity.

You might want to use `Nat.divide`

instead of `Nat.modulo`

, in which case you have `Nat.divide_transitive`

.

Is there something similar in the `Type`

world? `divide`

results in `Prop`

.

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

Found `is_true`

but that makes `Prop`

out of a `bool`

.

I guess there's no way to decide for a `Prop`

(or something like that), right?

No, but you can go from `Nat.modulo`

(for computability) to `Nat.divide`

(for proofs) and vice versa, using `Nat.mod_divide`

.

From `Nat.divide`

to `Nat.modulo`

as well?

Yes.

Last updated: Jun 15 2024 at 05:01 UTC