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

Я читаю Software Foundations книгу и в Imp.v файл, есть это определение теоремы eq_id_dec следующим образом:Что означает ∀id1 id2: id, {id1 = id2} + {id1 ≠ id2}?

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 типа идентификатора, как id1 = id2 и id1! = id2 не может случиться? Я не уверен.

источник

2015-05-03 elysefaulkner

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

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

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

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

источник

2015-05-03 04:57:38 Ptival

Итак, если мне нужно вызвать эту функцию, я должен передать значение идентификатора типа. Id - Id: nat -> id. Как бы я это сделал. Я делаю Eval Compute в (eq_id_dec (id 4) (id 5)). и не получается – elysefaulkner

Eval вычисляется в (eq_id_dec (Id 4) (Id 5)). – Ptival

-1

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

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

источник

2015-05-03 04:58:10

За исключением того, что в интуиционистской структуре, такой как Coq, 'P \/~ P' не обязательно истинно (вы можете добавить исключенный средний как аксиому). Вы должны доказать, что равенство разрешимо (следовательно, 'dec' в имени теоремы) в типе' id1' и 'id2'. – Virgile

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

ответ

Смежные вопросы