## Stream: math-comp users

### Topic: Cases modulo n

#### Guillaume Dubach (Apr 16 2021 at 09:01):

How can one do a case analysis on the possible values of some x modulo some d ? For instance, say I want to check that x^2 %% 8 is never 7, and do so by just checking the 8 possible cases for (x %% 8) ? (x %% d) has type nat and not some finite Type, but on the other hand the fact that x %% d < d is in the library, so perhaps one could use this together with induction on nat? Is there some more elegant way to proceed?

#### Cyril Cohen (Apr 16 2021 at 09:08):

I would do something like

``````by move: n (ltn_mod n 8); do 8![case=> //].
``````

#### Cyril Cohen (Apr 16 2021 at 09:10):

(no need for induction here, you want to explore a finite number of cases exhaustively)

#### Guillaume Dubach (Apr 16 2021 at 09:57):

Thanks! I see how `do 8![case=> //].` does the first 8 cases in `n`. But it doesn't conclude (on the trivial example of x^2 %% 8 not being 7). I still need to check: `n.+4.+4 ^ 2 %% 8 <> 7`. So it didn't use `ltn_mod n 8`to see that there were only these 8 cases to check... How do I help it conclude?

#### Guillaume Dubach (Apr 16 2021 at 10:01):

I guess it could do the case analysis on the possible values of `n %% 8`, check the first 8 cases with some help to deduce `n^2 %% 8`, and then dismiss the other cases thanks to `ltn_mod`?

#### Cyril Cohen (Apr 16 2021 at 10:03):

Oh yes sorry, it is slightly more complicated... I did not open Coq to try it before sending you the message

#### Cyril Cohen (Apr 16 2021 at 10:04):

One would need to substitute `n` for `n %% 8` in the goal.

#### Cyril Cohen (Apr 16 2021 at 10:06):

`by rewrite -modnXm; move: (n %% 8) (ltn_mod n 8); do 8![case=> //].`

#### Cyril Cohen (Apr 16 2021 at 10:06):

``````From mathcomp Require Import all_ssreflect.

Lemma test n : n ^ 2 %% 8 != 7.
by rewrite -modnXm; move: (n %% 8) (ltn_mod n 8); do 8![case=> //].
Qed.
``````

#### Guillaume Dubach (Apr 16 2021 at 10:07):

Oh, excellent. Thank you very much!

Last updated: Jul 25 2024 at 16:02 UTC