Как сделать алгебраические манипуляции в Coq проще? - PullRequest
Новая
       44

Как сделать алгебраические манипуляции в Coq проще?

1 голос
/ 29 марта 2019

Я экспериментирую со стандартными библиотеками Coq для целых и рациональных чисел. Пока мои доказательства очень трудоемки и выглядят ужасно. Я предполагаю, что скучаю по некоторым важным методам доказательства. Такие простые леммы не должны быть такими длинными, чтобы доказать. Есть намеки?

Вот пример: 

Require Import ZArith.
Require Import QArith.
Open Scope Q_scope.

Theorem q_less: forall x y z, (0 <= x <= y)%Z -> x # z <= y # z.
Proof. intros. destruct H as [Hl Hr]. rewrite (Zle_Qle x y) in Hr.
       rewrite <- (Qmult_le_l (inject_Z x) (inject_Z y) (/ inject_Z (Zpos z))) in Hr. simpl in Hr.
       - rewrite Qmult_comm in Hr. rewrite Qmult_comm with (x := / inject_Z (Z.pos z)) in Hr.
         unfold inject_Z in Hr. unfold Qinv in Hr. destruct (Qnum (Z.pos z # 1)) eqn:ZV.
         + simpl in ZV. discriminate.
         + simpl in Hr. simpl in ZV. injection ZV. intro ZP. unfold Qmult in Hr. simpl in Hr.
           rewrite <- ZP in Hr. rewrite Z.mul_1_r in Hr. rewrite Z.mul_1_r in Hr. exact Hr.
         + simpl in ZV. discriminate.
       - unfold Qinv. simpl. apply Z.lt_0_1.
Qed.

1 Ответ

2 голосов
/ 29 марта 2019

У меня не хватило смелости проанализировать ваше длинное доказательство, но я вижу, вы решили использовать стиль forward proof. Контрольным признаком является тот факт, что у вас есть несколько rewrite ... in ... в вашем сценарии. Большинство библиотек теорем разработано для работы в обратном стиле доказательства.

Сравните это с моим предложением о том же доказательстве: 

Theorem q_less: forall x y z, (0 <= x <= y)%Z -> x # z <= y # z.
Proof.
intros x y z cmp; rewrite !Qmake_Qdiv.
apply Qmult_le_compat_r.
  rewrite <- Zle_Qle; tauto.
apply Qinv_le_0_compat; replace 0 with (inject_Z 0) by easy.
now rewrite <- Zle_Qle; apply Zle_0_pos.
Qed.

Вот как я поступаю. Во-первых, x # z является обозначением для очень специфической формы разделения: той, которая появляется в основной дроби. Есть много шансов, что эта конкретная форма деления менее хорошо охвачена теоремами в библиотеке, поэтому я решил заменить ее регулярным делением между рациональными числами. Чтобы найти теорему, я просто использую запрос Search с шаблонами (_ # _) (_ / _). Это дает мне Qmake_Qdiv.

Тогда я просто ожидаю, что есть теорема, выражающая a <= b -> a / c <= b / c при подходящих условиях. Я использую Search (_ / _ <= _ / _)., чтобы найти такую ​​теорему. Увы, ничего не найдено. Итак, я помню, что деление часто описывается как умножение на обратное, поэтому я ищу другую возможность Search (_ * _ <= _ * _). Это дает мне Qmult_le_compat_r. Я пытаюсь применить это, и это работает.

Вот что я имею в виду, работая в обратном стиле доказательства: я смотрю на заключение и думаю какая теорема могла бы помочь мне получить это заключение? Я постараюсь выполнить его условия.

Есть два условия. Первый - (inject_Z x <= inject_Z y). Так что теперь мне нужна теорема, касающаяся сравнения в Z и сравнения в Q через функцию inject_Z. Чтобы найти его, я набираю Search inject_Z (_ <= _). Это дает мне Qmult_le_compat_r. Обратите внимание, что ваша гипотеза слишком сильна: вам не нужно x, чтобы быть позитивным. Автоматическая тактика tauto получает правильное условие из вашей гипотезы (которую я назвал cmp).

Последнее условие (0 <= inject_Z (Z.pos z)). Я могу повторно использовать ту же теорему, что и выше, потому что, безусловно, 0 должно совпадать с inject_Z 0.

Несмотря на это, я не рекомендую использовать QArith для математических рассуждений (тот тип алгебраических рассуждений, который вы здесь показывает), потому что он менее популярен, чем другие библиотеки. Если вы хотите работать с числами и объяснять их, вы должны использовать math-comp или Reals: вы найдете больше теорем, которые уже доказаны для вас.

...