Home
кококо
coq@conference.jabber.ru
Среда, 1 января 2014< ^ >
zert установил(а) тему: кококо
Логи: http://chatlogs.jabber.ru/coq@conference.jabber.ru/
http://www.cis.upenn.edu/~bcpierce/sf/ годная книга, как и всё, что пишет Пирс. Упор на тактики и доказательства.
http://adam.chlipala.net/cpdt/ годная книга. Доказательств мало, программирования много.
http://www.labri.fr/perso/casteran/CoqArt/index.html просто годная книга.
Конфигурация комнаты
Участники комнаты

GMT+4
[08:40:08] ForNeVeR вошёл(а) в комнату
[08:56:56] ForNeVeR вышел(а) из комнаты
[08:56:58] ForNeVeR вошёл(а) в комнату
[09:48:47] ForNeVeR вышел(а) из комнаты: Disconnected: No route to host
[09:52:57] ForNeVeR вошёл(а) в комнату
[12:03:04] ermine вошёл(а) в комнату
[12:35:14] olibjerd вошёл(а) в комнату
[12:41:37] olibjerd вышел(а) из комнаты: Logged out
[15:47:42] ForNeVeR вышел(а) из комнаты: Disconnected: closed
[16:19:01] ForNeVeR вошёл(а) в комнату
[17:53:01] ForNeVeR вышел(а) из комнаты
[17:53:04] ForNeVeR вошёл(а) в комнату
[18:28:21] ForNeVeR вышел(а) из комнаты: Disconnected: No route to host
[23:30:08] irezvov вошёл(а) в комнату
[23:30:25] <irezvov> hi
[23:30:32] <irezvov> есть пережившие новый год?
[23:32:22] <irezvov> а то у меня есть подозрение, что я доказываю не так, как хотел бы автор
[23:35:35] <gds> irezvov: где-то вроде есть, поищи в интернетах.
но на деле не обязательно доказывать так, как хочет автор.
[23:36:22] <irezvov> ну я понимаю, что не обязательно
[23:36:44] <irezvov> просто он объяснил только rewrite
[23:37:09] <irezvov> и нигде не показывал как его с with использовать
[23:37:26] <irezvov> а у меня без rewrite with не получается упражнение доказать
[23:37:44] <irezvov> вот интересно
[23:38:09] <irezvov> он подразумевал что читатель уже умеет в rewrite with из другого источника(что врядли)
[23:38:32] <irezvov> или существует другой способ доказательства, который я не вижу, потому что что-то не понял
[23:40:20] <gds> вроде всё можно сделать.  Покажи суть проблемы и скажи, какие тактики (и подобное) можно использовать, я попробую помочь.
[23:41:20] <irezvov> второе упражнение
[23:41:44] <irezvov> ранее использовались только intros, destruct и rewrite без with
[23:42:04] <irezvov> я нашел на гитхабах 2 репозитория с решениями
[23:42:06] <irezvov> но не в одном его нет
[23:44:44] <irezvov> сейчас вот так доказал https://gist.github.com/SPY/8210862
[23:52:44] <gds> а всякое reflexivity было, ну или apply eq_refl?
[23:53:06] <irezvov> а, да reflexivity было
[23:53:31] <irezvov> вообще упражнения из решений на гитхабе сильно отличаются
[23:53:46] <irezvov> они были запосчены 3 года и года назад
[23:54:14] <irezvov> видимо в последней ревизии книги(в июле была) упражнения изменились
[23:56:08] <irezvov> ну и simple соответственно еще был
[23:56:32] <gds> критично: был ли "simpl in *"?
[23:56:52] ermine вышел(а) из комнаты
[23:57:18] <irezvov> нет, было тока simpl.
[23:57:39] <irezvov> а что делает simpl in *, если не секрет?
[23:57:51] <irezvov> я просто до этой книги Coq в глаза не видел :)
[23:57:54] <gds> делает simpl в цели и в гипотезах.
[23:58:59] <irezvov> понятно
[23:59:03] <gds> если чо, о задачке ещё думаю.  Интересно почувствовать себя инвалидом, чтобы научиться, например, ногой ухо чесать.
[23:59:34] <irezvov> меня еще смутило что у упражнения 2 звездочки
[23:59:45] <irezvov> это типа 3-5 минут, для неподготовленного читателя
Powered by ejabberd Powered by Erlang Valid XHTML 1.0 Transitional Valid CSS!