Блог

Я экспериментирую со стандартными библиотеками 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.
  

У меня не хватило смелости проанализировать ваше длинное доказательство, но я вижу, что вы решили использовать стиль прямого доказательства. Характерным признаком является тот факт, что в вашем скрипте их несколько 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 : вы найдете больше теорем, которые уже доказаны для вас.