Возникли проблемы с неравенствами с рациональными числами - PullRequest
Новая
       6

Возникли проблемы с неравенствами с рациональными числами

0 голосов
/ 12 ноября 2018

Я пытаюсь доказать, что если у, рациональное число, больше нуля, то у не равно нулю. Я выделил две теоремы, которые, на мой взгляд, будут полезны, в частности, Qlt_not_eq и QOrder.neq_sym, но у меня возникают проблемы с выяснением, как использовать теорему QOrder.neq_sym. Кажется, я не могу передать это аргументами с помощью тактики «Проверка». Например, когда я пытаюсь сделать: 

Check (QOrder.neq_sym y 0)

Это дает мне ошибку, и я не уверен, почему. 

Require Import QArith.
Require Import QOrderedType.

Theorem test : forall (x y : Q),
    y > 0 -> ~ y == 0.
Proof.
    intros.
    (* This works OK *)
    Check QOrder.neq_sym.  
    (* But this gives me an error *)
    Check (QOrder.neq_sym y 0).

Буду признателен за любые указания о том, как использовать теорему QOrder.neq_sym, или за любые другие предложения о том, как добиться прогресса в этом доказательстве, которое я мог бы пропустить.

1 Ответ

0 голосов
/ 12 ноября 2018

Это не очень полезно для вас, но альтернативой является использование библиотеки математических компонентов;в этой постановке сформулированы теоремы для абстрактных алгебраических структур, из которых действительно являются рациональные числа.

У вас есть много теорем, которые утверждают, что вы хотите в этом случае, включая прямую: 

lt0r_neq0 (R : numDomainType) (x : R), 0 < x -> x != 0

Ваша первоначальная цель может быть доказана с помощью: 

Theorem test (y : Q) : y > 0 -> ~ y == 0.
Proof. now intros y_gt0; apply QOrder.neq_sym, Qlt_not_eq. Qed.
...