НОД и мод в Coq

Я застрял в проблеме в Coq, было бы здорово, если бы у кого-нибудь были какие-то советы о том, как разбить проблему на более мелкие шаги. Лемма такова:

Lemma gcd_prime : forall (a b : Z), a > 1 -> b > 1 -> 
  Z.gcd a b = 1 -> Zmod a b <> 0

То есть, если a и b взаимно просты и выше, чем 1, a mod b не 0.

Вот где я застрял:

 p : positive
 p0 : positive
 H : Z.pos p > 1
 H0 : Z.pos p0 > 1
 H1 : Z.gcd (Z.pos p) (Z.pos p0) = 1
  ============================
  Z.pos p mod Z.pos p0 <> 0

После вступления и индукции удалил очевидные случаи.

Может, лучше перефразировать часть mod на remainder? Или мне заменить H1 на что-нибудь послабее, например p <> p0?

Выполнение SearchAbout Zmod. возвращает множество лемм, но я не уверен, как их адаптировать.

С Уважением

Олле


modulo greatest-common-divisor coq
person Olle Härstedt    schedule 26.10.2014    source источник
comment
Я считаю, что обычно помогает, когда я застреваю на доказательстве Coq, написать, как я докажу это с помощью традиционного доказательства в прозе. Вы можете написать это здесь? Это поможет нам понять, какой следующий шаг вы хотите предпринять.   -  person jbapple    schedule 26.10.2014
comment
@jbapple не знаю. Думаю, мне нужны более простые отношения между gcd и модом. Или разверните определения, чтобы они были более точными.   -  person Olle Härstedt    schedule 26.10.2014
comment
По моему опыту, если я не знаю, как делать бумажное доказательство, полученное доказательство Coq не имеет для меня особой ценности. Я предлагаю вам сначала сделать бумажное доказательство. В моем прозаическом доказательстве я бы использовал личность Безу: en.wikipedia.org/wiki / B% C3% A9zout% 27s_identity   -  person jbapple    schedule 26.10.2014

Ответы (1)


arrow_upward
3
arrow_downward

SearchAbout и omega - ваши друзья. Помните, что вы можете искать вещи, которые упоминают сразу несколько определений, например Z.gcd и 0. Вот решение:

Require Import ZArith.

Open Scope Z_scope.

Lemma gcd_prime : forall (a b : Z), a > 1 -> b > 1 ->
  Z.gcd a b = 1 -> Zmod a b <> 0.
Proof.
  intros a b Ha Hb Hgcd Hmod.
  rewrite (Z_div_mod_eq a b), Hmod, Zplus_0_r in Hgcd; try omega.
  rewrite Z.gcd_comm, Z.gcd_mul_diag_l in Hgcd; omega.
Qed.
person Arthur Azevedo De Amorim    schedule 26.10.2014
comment
Как вы нашли все соответствующие леммы для этого доказательства? За исключением использования SearchAbout и т. Д. - person Olle Härstedt; 03.11.2014
comment
Кроме того, когда я запускаю SearchAbout Z_div_mod_eq, coq ничего не печатает. Сообщений об ошибках тоже нет. - person Olle Härstedt; 03.11.2014
comment
Первый вопрос: я обычно думаю о каком-то свойстве, которое может быть доступно в виде леммы и полезно для моего доказательства, а затем пытаюсь SearchAbout вещи, в которых упоминаются соответствующие определения. Например. Я мог бы сказать, что если мод b = 0, тогда мы знаем, что a = k * b, а затем делаем SearchAbout Zmod 0., чтобы посмотреть, что, если найдет. Второй вопрос: эта команда заставляет Coq искать леммы, которые о Z_div_mod_eq, то есть лемму о лемме. Это не ошибка, но он ничего не может найти, поэтому не отвечает. Вы, вероятно, захотите что-то вроде предыдущей команды, чтобы получить то, что вы хотите. - person Arthur Azevedo De Amorim; 03.11.2014