Guillaume Dubach (Apr 16 2021 at 09:01): 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=> //].
(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 8to 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.
Oh, excellent. Thank you very much!
Last updated: Feb 08 2023 at 08:02 UTC