Как в Coq использовать мод-арифметику (в частности, теорему Zplus_mod) для натуральных чисел?

Я хочу применить теорему библиотеки:

Theorem Zplus_mod: forall a b n, (a + b) mod n = (a mod n + b mod n) mod n.

где a b n, как ожидается, будет иметь тип Z.

В моей цели есть подвыражение (a + b) mod 3 с a b : nat.

rewrite Zplus_mod выдает ошибку Found no subterm matching

rewrite Zplus_mod with (a := a) выдает ошибку "a" has type "nat" while it is expected to have type "Z".

Поскольку натуральные числа также являются целыми числами, как использовать теорему Zplus_mod для аргументов nat?


mod logic coq coq-tactic
person mercury0114    schedule 14.06.2020    source источник
comment
Чтобы быстро ответить на этот вопрос, нам нужно знать, какие именно модули вы потребовали и импортировали. Так что было бы неплохо получить минимальный рабочий пример.   -  person Yves    schedule 15.06.2020

Ответы (1)


arrow_upward
1
arrow_downward

Вы не можете применить эту теорему, потому что нотация mod относится к функции натуральных чисел Nat.modulo в контексте, где вы используете натуральные числа, а нотация mod относится к Z.modulo, когда вы ссылаетесь на целые числа типа Z.

Используя команду Search, вы можете искать теоремы о Nat.modulo и (_ + _)%nat, и вы увидите, что некоторые существующие теоремы действительно близки вашим потребностям (Nat.add_mod_idemp_l и Nat.add_mod_idemp_r).

Вы также можете найти теорему, связывающую Z.modulo и Nat.modulo. Это дает mod_Zmod. Но это заставляет работать с целыми числами:

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  *)

Один из выходов - найти теорему, которая говорит вам, что функция Z.of_nat инъективна. Я нашел его, набрав следующую команду.

Search Z.of_nat "inj".

В составленном длинном списке соответствующей теоремой является Nat2Z.inj, затем вам нужно показать, как Z.of_nat взаимодействует со всеми задействованными операторами. Большинство этих теорем требуют, чтобы n было ненулевым, поэтому я добавляю это как условие. Вот пример.

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.

Это отвечает на ваш вопрос, но, честно говоря, я считаю, что вам лучше использовать леммы Nat.add_mod_idemp_l и Nat.add_mod_idemp_r.

person Yves    schedule 15.06.2020