Stream: math-comp users

Topic: Cases modulo n


view this post on Zulip 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?

view this post on Zulip Cyril Cohen (Apr 16 2021 at 09:08):

I would do something like

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

view this post on Zulip Cyril Cohen (Apr 16 2021 at 09:10):

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

view this post on Zulip 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 8to see that there were only these 8 cases to check... How do I help it conclude?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Apr 16 2021 at 10:04):

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

view this post on Zulip Cyril Cohen (Apr 16 2021 at 10:06):

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

view this post on Zulip 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.

view this post on Zulip Guillaume Dubach (Apr 16 2021 at 10:07):

Oh, excellent. Thank you very much!


Last updated: Feb 08 2023 at 08:02 UTC