Противоречие с нулевым тестом натурального числа - PullRequest
Новая
       6

Противоречие с нулевым тестом натурального числа

1 голос
/ 05 октября 2019

У меня есть натуральное число, которое не равно нулю. Я хочу доказать, что если он равен нулю, то он дает ложь. 

Lemma notzero : 
  forall n, 
    n <> 0 ->
    n =? 0 = false.
Proof.
  intro n. inversion H.

Ответы [ 2 ]

2 голосов
/ 06 октября 2019

Вместо использования инверсии в каждом доказательстве, я считаю, что доказательства в большей степени поддерживаются в долгосрочной перспективе, если вы используете булево отражение. В библиотеках есть много полезных лемм, которые вы можете использовать, они часто называются чем-то со словами «refle», «решить», «dec» или «spec», как в спецификации, поэтому вы можете, например, искать леммы, связанные с <, с помощью Search (_ < _) "spec".

Леммы об отражении предназначены для одновременного 1) уничтожения логического термина в вашем контексте доказательства и 2) добавления соответствующего Prop в ваш контекст, что упрощает использование затем lia, omega и т. Д. Для завершения доказательства.

В вашем случае вы можете использовать Nat.eq_spec (из Require Import PeanoNat.). Do 

destruct (Nat.eq_spec n 0).

Это создаст две ветви, в одной n ?= 0 заменяется на true и n=0 добавляется в контекст, а в другом n =? 0 заменяется на falseи n<>0 добавляется в контекст. Теперь доказать доказательство очень легко, поскольку контекст первой цели содержит противоречие n=0 и n<>0, а вторая цель - false=false. Вы можете использовать тактику автоматизации now, поэтому полное доказательство будет 

now destruct (Nat.eq_spec n 0).

Если вы хотите использовать целые числа Z, вместо этого доказательство становится now destruct (Z.eq_spec n 0).. поскольку модуль Z имеет много соответствующих лемм с соответствующими именами.

0 голосов
/ 05 октября 2019

Как правило, вы можете использовать тот факт, что =? отражает равенство натуральных чисел (Nat.eqb_spec). Вы намеренно используете два понятия равенства? Обратите внимание, что n <> 0 является обозначением для n = 0 -> False. 

Lemma notzero : 
  forall n, 
    n <> 0 ->
    n =? 0 = false.
Proof.
  intros n h. destruct (Nat.eqb_spec n 0).
  - exfalso. apply h. assumption.
  - reflexivity.
Qed.

. Существует также возможность простого анализа n. Если это 0, то вы можете использовать свою гипотезу для вывода, а если она равна S m, тогда ваша цель будет доказана с помощью reflexivity. 

Lemma notzero : 
  forall n, 
    n <> 0 ->
    n =? 0 = false.
Proof.
  intros n h. destruct n.
  - contradiction.
  - reflexivity.
Qed.
...