- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
- 67
- 68
- 69
- 70
- 71
- 72
- 73
- 74
- 75
- 76
- 77
- 78
- 79
- 80
- 81
- 82
- 83
- 84
- 85
- 86
- 87
- 88
Fixpoint mint_add0 {N} (i k : Fin.t N) te_i te' t0 vec
(Ht : MInt nonCommRel N k vec (te' :: t0))
(Hik : k < i)
(Hcomm0 : trace_elems_commute te_i te')
{struct Ht} :
exists t' : list TE,
MInt nonCommRel N k (vec_append i te_i vec) (te' :: t') /\
Permutation trace_elems_commute (te_i :: te' :: t0) (te' :: t').
Proof with eauto.
(* Welcome to the hell proof! *)
remember (te' :: t0) as t_.
destruct Ht as [k
|k j vec te_k t Hij Ht
|k j vec te_k te_j t Hij Hcomm Ht
];
[discriminate
|replace te' with te_k in * by congruence; clear Heqt_..
].
2:{ destruct (trace_elems_commute_dec te_i te_j).
- apply mint_add0 with (te_i := te_i) (i := i) in Ht; [|lia|assumption].
destruct Ht as [t' [Ht' Hperm']].
exists (te_j :: t'). split.
+ swap_vec_append.
eapply mint_cons2...
+ apply permut_cons with (a := te_k) in Hperm'.
eapply permut_trans...
now apply permut_head'.
- exists (te_i :: te_j :: t). split.
+ swap_vec_append.
apply mint_cons1 with (j0 := i); [lia|].
apply mint_cons2 with (j0 := j); [lia|auto..].
+ now apply permut_head'.
}
{ inversion_ Ht.
- exists [te_i]. split.
+ swap_vec_append.
apply mint_cons1 with (j0 := i); [lia|].
apply mint_cons1 with (j0 := i); [lia|].
constructor.
+ now apply permut_head'.
- rename te into te_j.
destruct (PeanoNat.Nat.lt_ge_cases j i).
2:{ exists (te_i :: te_j :: t1). split.
- swap_vec_append.
apply mint_cons1 with (j1 := i); [lia|].
apply mint_cons1 with (j1 := j); [lia|assumption].
- now apply permut_head'.
}
{ destruct (trace_elems_commute_dec te_i te_j) as [Hte_ij|Hte_ij].
- apply mint_add0 with (i := i) (te_i := te_i) in Ht; [|lia|assumption].
destruct Ht as [t' [Ht' Hperm']].
exists (te_j :: t'). split.
+ swap_vec_append.
eapply mint_cons1...
+ apply permut_cons with (a := te_k) in Hperm'.
now apply permut_head.
- exists (te_i :: te_j :: t1). split.
+ swap_vec_append.
apply mint_cons1 with (j1 := i); [lia|].
apply mint_cons2 with (j1 := j); [lia|assumption..].
+ apply permut_head; [assumption|constructor].
}
- rename j0 into i0. cbn in H0.
destruct (PeanoNat.Nat.lt_ge_cases j i).
2:{ exists (te_i :: te_i0 :: te_j :: t1). split.
+ swap_vec_append.
apply mint_cons1 with (j0 := i); [lia|].
apply mint_cons1 with (j0 := j); [lia|assumption].
+ now apply permut_head'.
}
{ destruct (trace_elems_commute_dec te_i te_i0).
- apply mint_add0 with (i := i) (te_i := te_i) in Ht; [|lia|assumption].
destruct Ht as [t' [Ht' Hperm']].
exists (te_i0 :: t'). split.
+ swap_vec_append.
eapply mint_cons1...
+ apply permut_cons with (a := te_k) in Hperm'.
now apply permut_head.
- exists (te_i :: te_i0 :: te_j :: t1). split.
+ swap_vec_append.
apply mint_cons1 with (j0 := i); [lia|].
apply mint_cons2 with (j0 := j); [lia|assumption..].
+ apply permut_head.
* assumption.
* constructor.
}
}
Qed.
Мой magnum opus. Часть доказательства про выкидывание из рассмотрения коммутирующих системных вызовов.
Follow us!
Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.
Теорему про раскраску графа вообще чуть ли не брутфорсом доказывали...
З.Ы. Ня, привет.
Что интересно, это не потому, что мне было лень эту функцию на леммы разбивать, а именно чтобы получить в итоге нужный тип. Такая вот злая лемма. Всё-то криво в этом вашем программировании, никаких красивых симметрий.
т.е. есть генератор стратегий, ему дают теорему, он выплевывает стратегию gen_strateg(theorem) -> strategy
и есть бесконечно генерирующая теоремы херня, допустим gen_theorem(0) - одна теорема, gen_theorem(1) - другая, и так далее.
А потом надо доказать что Так делают?
Вопрос я, конечно, не понял, но ответ на него скорее всего – нет. Дело в том, что стратегий в Coq нет, есть тактики, и они пишутся на совершенно другом метаязыке (Ltac), нежели теоремы (Gallina). (В Lean не так, кстати. Там по слухам гомоиконность) Поэтому написать теорему про тактику в Coq – это как написать функцию, принимающую как аргумент макрос, в C.
У `стратегии' тип это список правил, по которым некая питушня что-то набрасывает в качестве пруфа теоремы, пытаясь это доказать. Ну ок, пусть будет `тактики', а не `стратегии'. Почему б не доказывать, что такие-то тактики, генерируемые на основе конкретных теорем, всегда успешно доказывают теоремы, сгенеренные таким-то способом? Т.е. доказать что генератор тактик всегда для такого семейства теорем, генерируемых таким способом, генерит такие тактики, которые всегда доказывают соотв. теорему
А почему не сделать это одним языком? Чтобы можно было доказывать доказуемость некоего множества теорем такими-то генеренными из теорем тактиками.
Нянужно! Gallina имеет крайне строгую семантику, поскольку она является доверенной по принципу де Бройля. Поэтому в ней не может быть никаких свистелок и перделок, и всё крайне ограничено и консервативно. А Ltac – не доверенный язык, в нём можно сколько угодно фич пилить и ломать семантику как хочешь. Поэтому его используют для автоматизации, т.к. удобно.
Ну так почему б не написать транспилер из Ltac в Gallina? В самой Gallina сделать тьюринг-полноту с гомоиконами, и пусть само с собой там метушится, доказывая доказуемость.
Принципиально нявозможно. Ltac – Тьюринг полный, Gallina – нят.
Зачем? Зачем? Я могу описать функцию, принимающую стейт брейнфака возвращающую новый стейт брейнфака плюс номер шага, и через Ltac я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота. Ради чего это?
Во-первых, Ltac – логический язык, типа пролога. Формально описывать на Gallina шаг Ltac, и затем применять его с помощью Ltac – это как бутылку кваса провести через весь пищеварительный тракт наверх ко рту, чтобы вылить всё её содержимое в дыхательное горло.
> я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота
Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
Чтобы доказывать применимость таких-то стратегий (стратегий, построенных по определенному шаблону) к доказыванию таких-то теорем, построенных по определенному шаблону. Сделать еще какую-то алгебру стратегий, что такие-то стратегии можно упростить, сведя их к таким-то, а вот такие стратегии это частные случаи таких стратегий. Более высокий уровень абасракции короче.
> Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
Почему не будет? Так мы пробуем доказать небесконечность цикла, и раз мы так можем делать, это и есть тьюринг-полнота, мы интерпретируем брейнфак. Какая разница, зависнет ли у меня Ltac генерящий питушню для Gallina, или Gallina само себе питушню генерить будет и зависнет?
Огромная. [1] [2]
[1] https://govnokod.ru/26981#comment579147
[2] https://govnokod.ru/27333#comment620156
Поднимаю говно-Хирш
В переводе на петушиный: у меня есть функция F(n : nat), возвращающая термы в универсуме U + 1.
> Есть генератор тактик, тактика1 доказывает теорему1, тактика2 доказывает теорему2 и так далее.
В переводе на петушиный: у меня есть функция G от nat, которая возвращает терм типа F(n) в универсуме U.
> И надо доказать, что все такие генеретные тактики доказывают все такие генеренные теоремы.
В переводе на петушиный: надо найти определение G.
> Почему это не в рамках единого языка?
Просто переформулировав пробему как показано выше, ты и сделаешь это в рамках одного языка.
А тактики – это макроязык такой.
Переформулировать-то можно, это понятно. Но так не выйдет доказать что-то относительно неких свойств стратегий, применимости определенных стратегий к доказыванию определенных типов теорем и так далее. Окажись стратегий частью самого языка для описания теорем, это можно было бы делать.
В этом вроде и идея ltac. Нет никакого смысла доказывать, что он правильно работает в общем случае или для каких-то классов теорем. Достаточно просто проверять сгенерённые им пруфы для конкретных теорем которые тебе и нужно доказать.
А технически и питон и даже пхп сойдут, конечно.
Причина: ты что, пёс, я Computer Scientist.
Ну а на деле: люди бы ебанулись на LISP паттерн-матчинг типов пилить. Да в нём и нету нормального паттерн-матчинга.
Тогда еще больше причин делать всю петушню в рамках одного языка, а не разграничивать на две хрени, которые там еще как-то перепихиваются в процессе.
Я ведь тогда не могу в Coq доказать что Coq(Coq(x)) проверяет x и считает этот пруф верным или не верным тогда же, когда, когда это делает Coq(Coq(Coq(x))), даже не смогу это объявить как аксиому(если это недоказуемо из-за какой-то там неполноты), да? И что в этом хорошего?
Это копипаста, которую я хуй знает когда написал.
Это вореции?
Нет. Это одна моя старая идея метаязыка для конструирования языков, который будет сам на себе написан, и чтоб всё через частичные вычисления, проекции Футамуры и формальные доказательства там работало, и чтобы это был один единый язык с Тьюринг-полнотой, самомодифицирующийся в процессе исполнения (система переписывающих правил чтоб, грубо говоря запуск языка это самопереписывание графа, полученного из AST с чтением из STDIN выплевыванием чего-то из STDOUT). И на этой алгебре самопереписывания уже б вводились всякие теории типов.
Если б мне кто-то профинансировал запиливания хрени, которую я расписал, я б ее очень даже охотно писал.
Раз у Gallina нет тьюринг-полноты и в нем нельзя написать Gallina-интерпретатор, в рамках Gallina нельзя что-то доказывать о том, как что-либо делается самой Gallina для доказывания чего-либо, верно? И нельзя делать эти проекции Футамуры, о которых я выше написал.
Т.к. Gallina не Тьюринг-полна, в теории может и можно написать её интерпретатор на не-Тьюринг полном языке. Напиши, проверишь.
На сишных макросах? Они как раз не тьюринг полны.
https://github.com/orangeduck/CPP_COMPLETE
https://github.com/pfultz2/Cloak/wiki/Is-the-C-preprocessor-Turing-complete%3F
>Now this example is limited to 10 repeats, because of limitations of the counter. Just like a repeat counter in a computer would be limited by the finite memory. Multiple repeat counters could be combined together to workaround this limitation, just like in a computer. Furthermore, we could define a FOREVER macro:
>This will try to output ? forever, but will eventually stop because there are no more scans being applied. Now the question is, if we gave it an infinite number of scans would this algorithm complete? This is known as the halting problem, and Turing completeness is necessary to prove the undecidability of the halting problem. So as you can see, the preprocessor can act as a Turing complete language, but instead of being limited to the finite memory of a computer it is instead limited by the finite number of scans applied.
Т.е. это явно более узкий класс программ чем в типичном "тьюринг-полном" языке, который ограничен только памятью.
Ну как бы смотря как ты определяешь"класс программ". Если "тьюринг-полный" язык органичен конечной памятью, доказательство зависания для него можно всегда доказать через https://ru.wikipedia.org/wiki/Нахождение_цикла
Рассмотрим функцию "шаг интерпретатора"
Если state это некая хуита, занимающая конечный кусок в оперативной памяти (нет никаких указателей и выделений памяти) то если бесконечный вызов хуйни в хуйню
То значение `st' обязательно будет повторяться т.к. количество состояний конечно.
И если такая программа выводит что-то в stdout допустим(но ничего не получает извне), то она сводима к:
или принимает бесконечную периодическую строку, такую строку тоже можно в код вшить.
Некий условный 1 шаг интерпретатора Gallina однозначно можно написать на Gallina т.к. 1 шаг брейнфака написать там точно можно. А вот "вызывать" интерпретатор бесконечное количество раз в Gallina нельзя, и это может сделать только некая внешняя хрень, которая что-то доказывает в терминах Gallina. Как-то так
https://archive.jlongster.com/Lisp--It-s-Not-About-Macros,-It-s-About-Read
А я все ломал голову, как человек может так ненавидеть будущее, так привязаться к прошлому, что пишет на лиспе? Но для лиспопетушка-контрамота лисп - это и есть будущее. А дальше ВВ2, индустриальная контрреволюция, религиозные войны, рабовладельческий строй, отрастание хвостов и подъем на деревья. Скай из зе лимит!
На самом деле в Lisp и Scheme всё очень печально с pattern-matching'ом, и всякие CSшни в современном мире без него пилить никому не охота.
В чем именно заключается печальность? Что мешает сделать DSL для pattern-matching'а?
Его там нет. (Ну может в современных диалектах появился)
> Что мешает сделать DSL для pattern-matching'а?
Так сделали, само собой. Но когда я открываю доки по pcase, я плачу, настолько он уродливый.
https://docs.racket-lang.org/reference/match.html такой паттерн матчинг норм? Покажи реальный пример хорошего паттерн-матчинга в каком-то язычке.
Более того, с его помощью легко запилить что-то неправильное. Ключевые слова Qed. и Defined. потом всё перепроверяют.
Особенный багор, когда ты ltac'ом запилил огромный fixpoint, а он оказался не структурным, т.к. auto где-то подхватило рекуррентный вызов ))) Приходится во избежание этого гипотезы чистить вилкой.