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?
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)
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?
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
Oh yes sorry, it is slightly more complicated... I did not open Coq to try it before sending you the message
One would need to substitute
n %% 8 in the goal.
by rewrite -modnXm; move: (n %% 8) (ltn_mod n 8); do 8![case=> //].
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