2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Как проверить на равенство два объекта в Coq?
Сообщение25.12.2015, 18:35 


26/08/12
45
Вроде элементарная операция в обычных языках программирования, но не пойму как её выполнить в Coq.
Т.е. проверить на равенство два произвольных объекта одного типа, ну например, хотя бы два натуральных числа.

Как это сделать вручную используя Check понятно.
Есть функция eq типа forall A : Type, A -> A -> Prop,
соответственно равенство строится, например так: eq nat 5 5 или eq nat 5 6, следовательно этот объект будет типа Prop.
Тип eq A x x имеет единственного обитателя, который строится конструктором eq_refl типа forall (A : Type) (x : A), eq A x x.
Например, чтобы доказать что верно eq nat 5 5 мы показываем, что он обитаем конструируя его обитателя eq_refl nat 5 типа eq nat 5 5, т.е. равенство верно. А для eq nat 5 6 мы не можем построить его обитателей, т.е. тип необитаем, значит не верно что равенство верно.
Просто выполняя Check (@eq_refl nat 5):(@eq nat 5 5), что проходит без ошибок, а Check (@eq_refl nat 5):(@eq nat 5 6) с ошибкой.

Но как это написать такую функцию для самого языка, т.е. зависимого типизированного лямбда-исчисления неясно, и как писать программы без такой элементарной операции тоже не понятно.
eq nat 5 5 не даст значения True, а просто есть какое-то значение из Prop.
Ведь обычно происходит вычисление сравниваемых объектов и сравнение их записей, и всё выдаётся true или false, в том же Хаскеле операция сравнения всегда происходила у меня без проблем.

 Профиль  
                  
 
 Re: Как проверить на равенство два объекта в Coq?
Сообщение29.12.2015, 11:53 


26/08/12
45
Для натуральных нашёл алгоритм сравнения, свёл к получению у чисел предыдущего числа и если
это приводит к тому, что у обоих чисел значение равно нулю, то числа равны. Но в общем случае, похоже придётся также индивидуально писать сравнение для каждого типа, хотя по сути объекты равны если они графически одинакового записаны..

Fixpoint eq_nat a b :=
match a, b with
| O, O => true
| S a', S b' => eq_nat a' b'
| _,_ => false
end.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 2 ] 

Модераторы: Karan, Toucan, PAV, maxal, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group