Coq: Как доказать a=b -> nat_compare a b = Eq.?

Пытаясь понять, что такое Coq, я оказался в ситуации, когда мне по сути нужно доказать, что a=b -> nat_compare a b = Eq.

Я могу получить удобное начало, выполнив:

Coq < Theorem foo: forall (a:nat) (b:nat), a=b->nat_compare a b=Eq.
1 subgoal

============================
forall a b : nat, a = b -> nat_compare a b = Eq

foo < intros. rewrite H. destruct b.

что дает мне:

2 subgoals
a : nat
H : a = 0
============================
nat_compare 0 0 = Eq

subgoal 2 is:
nat_compare (S b) (S b) = Eq

Первый банален:

foo < simpl. reflexivity.

Но следующая цель ставит меня в тупик:

1 subgoal

a : nat
b : nat
H : a = S b
============================
nat_compare (S b) (S b) = Eq

я могу сделать

foo < rewrite <- H.

который дает:

1 subgoal

a : nat
b : nat
H : a = S b
============================
nat_compare a a = Eq

(Я также могу добраться до этой точной точки через simpl, что кажется более логичным.)

Теперь, с ручкой на бумаге, я бы просто заявил, что вот мое доказательство по индукции.

Правильно ли я подхожу к этому? Где мне лучше всего научиться делать это правильно?


theorem-proving coq
person aleator    schedule 30.10.2013    source источник
comment
@jozefg Сравнивает два ната. Он определен в стандартной библиотеке coq как Fixpoint nat_compare n m := match n, m with | O, O => Eq | O, S _ => Lt | S _, O => Gt | S n', S m' => nat_compare n' m' end.. Поскольку я абсолютный новичок в Coq, эта функция может быть совершенно неправильной для использования при сравнении чисел, но...   -  person aleator    schedule 30.10.2013

Ответы (1)


arrow_upward
2
arrow_downward

Я смог доказать это с помощью

Theorem triv : forall a b, a = b -> nat_compare a b = Eq.
  intros; subst; induction b; auto.
Qed.

Хитрость здесь в том, чтобы оставить индуктивную гипотезу лежать без дела. destruct — это более слабая форма induction, которая не дает вам индуктивной гипотезы, необходимой для этого доказательства.

person Daniel Gratzer    schedule 30.10.2013
comment
Спасибо! Я пробовал induction ранее, но это не помогло, когда я использовал rewrite H вместо subst. Если я дополнительно clear гипотезу и ссылку на a, induction работает с rewrite. Почему мне нужно сначала очистить гипотезу? - person aleator; 30.10.2013