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.

No I hadn't loaded Arith.

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: Oct 13 2024 at 01:02 UTC