Coq: Докажите, что Prop подразумевает арифметические отношения натурального числа - PullRequest
Новая
       36

Coq: Докажите, что Prop подразумевает арифметические отношения натурального числа

0 голосов
/ 29 сентября 2018

Я пытаюсь доказать следующую лемму в coq - 

Lemma less_than_two_equivalent: forall x, less_than_two x = true -> x < 2.

на основе приведенного ниже определения. 

Fixpoint less_than (a b:nat): bool:=
match a, b with
|0, 0 => false
|0, _ => true
|S a', 0 => false
|S a', S b' => less_than a' b'
end.

Fixpoint less_than_two (x:nat) : bool  := if less_than x 2 then true else false.

Математически существует только 2 случая, 0 или1. И destruction должен быть молотком, но информации о S x будет недостаточно для дальнейшего рассуждения.

Должен ли я изменять less_than в типы индуктивных данных?Если нет, то как решить это?

1 Ответ

0 голосов
/ 30 сентября 2018

Позвольте мне начать с переопределения less_than_two.Во-первых, он не рекурсивный, поэтому нет смысла определять его как Fixpoint.Далее, if less_than x 2 then true else false по сути то же самое, что и less_than x 2.И в этот момент я бы не стал вводить новое определение, поэтому ваша лемма становится 

Lemma less_than_two_equivalent x: less_than x 2 = true -> x < 2. 
Proof.
  do 2 (destruct x; auto); simpl.
  destruct x; discriminate.
Qed.

Я не знаю, что именно пошло не так с вашим доказательством, но вы, возможно, забыли уничтожить x еще раз.Когда вы видите less_than x 0 = true -> S (S x) < 2, вы все равно не можете использовать discriminate для достижения цели, потому что оценка заблокирована по переменной - less_than первое совпадение с шаблоном по параметру a и только затем проверяется b.Уничтожение x разблокирует вычисление и позволяет Coq увидеть, что в качестве предпосылки вы выбрали false = true, поэтому цель становится доказуемой.

Обратите внимание, что это зависит от конкретной реализации функции сравнения.Если бы вы выбрали этот 

(* (!) the [struct] annotation is important here, as well as as
   the order of the parameters [b, a] in the match expression *)

Fixpoint less_than' (a b : nat) {struct b} : bool :=
  match b, a with
  | 0, _ => false
  | _, 0 => true
  | S b', S a' => less_than' a' b'
  end.

, у вас было бы немного более простое доказательство (на один меньше destruct): 

Lemma less_than_two_equivalent x: less_than' x 2 = true -> x < 2. 
Proof.
  do 2 (destruct x; auto).
  discriminate.
Qed.
...