Что означает ∀id1 id2: id, {id1 = id2} + {id1 ≠ id2}?

Я читаю книгу "Основы программного обеспечения" и в файле Imp.v приведено следующее определение теоремы eq_id_dec:

Theorem eq_id_dec : forall id1 id2 : id, {id1 = id2} + {id1 <> id2}.
Proof.
   intros id1 id2.
   destruct id1 as [n1]. destruct id2 as [n2].
   destruct (eq_nat_dec n1 n2) as [Heq | Hneq].
   Case "n1 = n2".
     left. rewrite Heq. reflexivity.
   Case "n1 <> n2".
     right. intros contra. inversion contra. apply Hneq. apply H0.
Defined.

Означает ли эта теорема, что для любых идентификаторов id1 и id2 типа id не может происходить как id1=id2, так и id1!= Id2? Я не уверен.

Источник

2 ответа

Нет, это не исключает случая, когда равенство и неравенство являются истинными одновременно (хотя на практике это имеет место и здесь).

Тип sumbool A B, обозначений {A} + {B}, характеризует процедуру принятия решения, которая докажет либо A или же B,

Так это eq_id_dec это термин, который займет два ids в качестве входных данных и либо возвращают доказательство того, что они равны, либо доказательство их отличия.

Подробнее о сумбуле здесь: https://coq.inria.fr/distrib/current/stdlib/Coq.Bool.Sumbool.html

Источник

Для всех id1 и id2 id1 = id2 или id1 не равен id2.

Довольно просто - либо равно id2, либо нет, что по определению всегда будет истинно, поэтому оно верно для всех id1/id2.

Источник
Другие вопросы по тегам