Objective Caml - Понедельник, 1 апреля 2013

Objective Caml

ocaml@conference.jabber.ru

Понедельник, 1 апреля 2013< ^ >

Конфигурация комнаты

Участники комнаты

GMT+4
[00:17:53] Kakadu вышел(а) из комнаты
[00:26:55] komar вышел(а) из комнаты: Logged out
[00:27:02] komar вошёл(а) в комнату
[00:28:20] komar вышел(а) из комнаты: Logged out
[01:30:51] f[x] вошёл(а) в комнату
[01:39:33] Sun][ вышел(а) из комнаты
[02:06:57] f[x] вышел(а) из комнаты
[02:39:57] strobegen вышел(а) из комнаты
[04:46:28] zinid вошёл(а) в комнату
[07:29:18] ermine вошёл(а) в комнату
[08:31:24] strobegen вошёл(а) в комнату
[08:53:54] Sun][ вошёл(а) в комнату
[09:08:04] komar вошёл(а) в комнату
[09:24:57] Sun][ вышел(а) из комнаты
[10:31:15] komar вышел(а) из комнаты
[11:43:11] komar вошёл(а) в комнату
[11:43:33] f[x] вошёл(а) в комнату
[11:50:35] komar вышел(а) из комнаты: Replaced by new connection
[11:50:35] komar вошёл(а) в комнату
[11:53:11] komar вышел(а) из комнаты: Logged out
[11:53:14] komar вошёл(а) в комнату
[12:05:34] Kakadu вошёл(а) в комнату
[12:24:25] komar вышел(а) из комнаты: Logged out
[12:24:27] komar вошёл(а) в комнату
[12:24:32] komar вышел(а) из комнаты: Logged out
[12:32:10] komar вошёл(а) в комнату
[12:34:00] komar вышел(а) из комнаты: Logged out
[12:46:26] <aleksey> gds: я на выходных поигрался, вместо маркера сделал нумерацию всех переменных как в cpdt, и уже по номерам сортировку
[12:50:59] Typhon вошёл(а) в комнату
[12:53:28] komar вошёл(а) в комнату
[13:05:58] komar вышел(а) из комнаты
[13:19:41] komar вошёл(а) в комнату
[13:20:40] komar вышел(а) из комнаты: Logged out
[13:51:27] komar вошёл(а) в комнату
[13:57:00] f[x] вышел(а) из комнаты
[14:02:36] ermine вчера успешно доказала коммутативность умножения
[14:39:36] <gds> aleksey: а как ты сделал нумерацию переменных?
[14:40:19] <gds> ermine: так таки шо, действительно коммутативно?  во дают...
[14:41:16] <aleksey> gds: скопипстил из cpdt из главы про proof by reflection
[14:42:04] <aleksey> ну ещё переделал немного чтоб из гипотез тоже брало, а не только из цели
[14:50:23] <ermine> gds: в общем прониклась этой кокятиной, только с сообразительностью иногда не всё ладно, пачками идут Restartы, чтобы попробовать ту или иную идейку и параллельно всякой лабуды в леммах узаконить
[14:51:02] <ermine> выучила еще пару команд - assert и replace, ниче так, если можно механически узаконить
[14:51:45] <ermine> задалбывает пока лишь то, что надо в assert или replace выделить нужный кусок теоремы, а то ревайт не то сжует
[14:53:24] <ermine> и пока неясно как с этим букетом доказываются монады и прочие любимые погремушки хаскеллистов
[14:56:36] <gds> ermine: вот потому coqide/proofgeneral и хороши, что не надо restart, а достаточно, например, ctrl+alt+up пару раз.
кроме того, лемму можно объявить прямо в proof mode.
replace -- мутная тактика, set/assert -- чоткие.
куски выделять -- иногда нужно, факт.
как монады -- просто, только лучше сразу трансформеры.  Доказываешь 5 законов -- имеешь манатку и трансформер.  Более того, в #coq посоны просят, чтобы я зарелизил "практически-полезные манатки", и вот, сегодня-завтра кину ссылку и сюда.  А как пример я им кинул https://gist.github.com/gdsfh/971a5db696ada4933dec , ну и тебе может интересно будет.
[14:59:47] <ermine> gds: чем это repalce мунтая? relpace (t) wtih (u), и u стоавнится суеблцью, а полсе асреста обчыно ндао еще реравйт упоетрбить
[15:00:41] <gds> ну, если тебе так нравится -- значит не мутная.
[15:01:33] <gds> только не сразу понял слово "суеблць" -- какое-то ругательство, подумал изначально.
[15:02:28] <ermine> именно
[15:02:45] <ermine> все subgoals - те еще ругательство, с которым придецца возиться
[15:03:29] <ermine> например в индукции все самые простые цели сначала идут, а потом - хоть плачь :)
[15:04:00] <ermine> еще надо не промахнуться мимо верного столба, которое надо спилить
[15:05:08] <gds> иногда, чтобы не плакать, надо admit, попробовать доказать сложное, и, если получится, перейти к простому.
[15:06:14] <ermine> проще подергаться и и подергать Undo, если не тот столб спилил
[15:18:19] <ermine> gds: а вот попалось первый намек на трансформации: теорема о том, что forall f bool->bool b:bool, f (f (f b) = f b и читаю длинное описание доказательства
[15:26:35] <gds> aleksey: понял я тот подход.  Вообще, достаточно просто составить список всех переменных и написать функцию "входит ли A в список раньше, чем B".  И ещё что не очень нравится, что нужно явно описывать, какие выражения нужно разбирать (типа как у адама, /\ \/ -> True False).  Но может это не такая уж проблема.
[15:46:08] UncleVasya вошёл(а) в комнату
[15:58:59] <gds> aleksey: ещё интересно, получится ли запихивать подвыражения в тот списочек, чтобы через коммутативность плюса и умножения доказывалось (a+b)*(c+d) = (d+c)*(b+a).  Вроде получится.
[16:00:47] <aleksey> coq от этих перестановок создаёт ненужные выражения типа let H2 = blabla H1 in H, хотя можно было бы просто H оставить
[16:03:57] f[x] вошёл(а) в комнату
[16:06:14] <gds> ну конечно, если было a+b, то для получения b+a будет что-то типа eq_ind (plus_comm a b (a+b)).  То есть, со ссылкой на то, что изначально было a+b, что мы взяли plus_comm, получили утверждение a+b = b+a, и далее через eq_*, имея a+b, получили b+a.  А по-другому как?
[16:06:42] <gds> и чем это создаёт проблемы?
[16:08:09] <aleksey> если в доказательстве это a+b не участвует, то coq всё равно оставляет соответствующие преобразования
[16:08:12] <gds> ну, от let in избавиться можно, я думаю, записав через change.
[16:08:35] <aleksey> так это уже в том что он генерит после Qed
[16:09:38] <gds> ну пусть себе генерит.  Да, пруф терм получается большим при этом.  И при Eval compute скорее всего останутся следы rewrite'ов.  Но бывают случаи, где это не важно.
[16:36:46] komar вышел(а) из комнаты: Logged out
[17:58:05] tilarids вошёл(а) в комнату
[18:07:43] f[x] вышел(а) из комнаты
[18:29:48] Zbroyar вошёл(а) в комнату
[18:34:08] zinid вышел(а) из комнаты
[18:52:57] Typhon вышел(а) из комнаты
[18:55:22] Typhon вошёл(а) в комнату
[19:38:47] Typhon вышел(а) из комнаты
[19:48:18] kevin вошёл(а) в комнату
[19:51:07] kevin вышел(а) из комнаты
[19:52:32] tilarids вышел(а) из комнаты: Computer went to sleep
[20:10:50] Zbroyar вышел(а) из комнаты
[20:11:41] UncleVasya вышел(а) из комнаты
[20:14:04] tilarids вошёл(а) в комнату
[20:26:21] UncleVasya вошёл(а) в комнату
[20:30:54] tilarids вышел(а) из комнаты: Computer went to sleep
[20:49:01] Kakadu вышел(а) из комнаты
[21:19:31] tilarids вошёл(а) в комнату
[21:36:27] Kakadu вошёл(а) в комнату
[21:53:29] ermine вышел(а) из комнаты
[22:05:03] f[x] вошёл(а) в комнату
[22:05:29] Sun][ вошёл(а) в комнату
[22:20:27] f[x] вышел(а) из комнаты
[23:03:42] komar вошёл(а) в комнату
[23:13:17] komar вышел(а) из комнаты: Logged out
[23:13:48] Zbroyar вошёл(а) в комнату
[23:14:05] <Zbroyar> Обнаружил странное:
[23:15:01] <Zbroyar> Если задать вариант вида: type v = V1 | V2 | V3 | V4 ;;
[23:15:18] <Zbroyar> То работаю сравнения:
# V1 < V2 ;;
- : bool = true
# V2 < V1 ;;
- : bool = false
[23:15:25] <Zbroyar> работают*
[23:16:21] <gds> не странное.  Обычные полиморфные = < > <= >=.  Посмотри тип let lt a b = a < b, например.
[23:16:21] <Zbroyar> Это баг или фича?
[23:16:33] <gds> фича, но порой хочется, чтобы был баг.
[23:17:15] <Zbroyar> Странная фича, блин.
[23:18:56] <gds> ну а полиморфное "=" как работает -- примерно по такому же механизму.  Ну и маршаллинг туда же.  Такая фича, вот.
[23:21:33] <Zbroyar> Я так понимаю, что если посмотреть во внутренности вариантов, то там окажутся union's с числовыми type codes?
[23:21:35] Sun][ вышел(а) из комнаты
[23:29:29] <gds> да.  Те, которые без аргументов -- int'ы внутренне, int зависит от конструктора.  С аргументами -- туплы, где тег определяется конструктором.
[23:38:11] komar вошёл(а) в комнату
[23:38:38] Sun][ вошёл(а) в комнату
[23:47:55] tilarids вышел(а) из комнаты: Computer went to sleep
[23:57:08] f[x] вошёл(а) в комнату