I want to apply the library theorem:
Theorem Zplus_mod: forall a b n, (a + b) mod n = (a mod n + b mod n) mod n.
where a b n are expected to have the type Z.
I have a subexpression (a + b) mod 3 in my goal, with a b : nat.
rewrite Zplus_mod gives an error Found no subterm matching
rewrite Zplus_mod with (a := a) gives an error "a" has type "nat" while it is expected to have type "Z".
Since natural numbers are also integers, how to use Zplus_mod theorem for nat arguments?
You can't apply this theorem, because the notation mod refers to a function on natural numbers Nat.modulo in a context where you are using natural numbers, while the notation mod refers to Z.modulo when you are referring to integers of type Z.
Using the Search command ou can search specifically for theorems about Nat.modulo and (_ + _)%nat and you will see that some existing theorems are actually close to your needs (Nat.add_mod_idemp_l and Nat.add_mod_idemp_r).
You can also look for a theorem that links Z.modulo and Nat.modulo. This gives mod_Zmod. But this forces you to work in the type of integers:
Require Import Arith ZArith.
Search Z.modulo Nat.modulo.
(* The answer is :
mod_Zmod: forall n m, m <> 0 -> Z.of_nat (n mod m) =
(Z.of_nat n mod Z.of_nat m)%Z *)
One way out is to find a theorem that tells you that the function Z.of_nat is injective. I found it by typing the following command.
Search Z.of_nat "inj".
In the long list that was produced, the relevant theorem is Nat2Z.inj, you
then need to show how Z.of_nat interacts with all of the operators involved. Most of these theorems require n to be non-zero, so I add this as a condition. Here is the example.
Lemma example (a b n : nat) :
n <> 0 -> (a + b) mod n = (a mod n + b mod n) mod n.
Proof.
intro nn0.
apply Nat2Z.inj.
rewrite !mod_Zmod; auto.
rewrite !Nat2Z.inj_add.
rewrite !mod_Zmod; auto.
rewrite Zplus_mod.
easy.
Qed.
This answers your question, but frankly, I believe you would be better off using the lemmas Nat.add_mod_idemp_l and Nat.add_mod_idemp_r.