- 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. Часть доказательства про выкидывание из рассмотрения коммутирующих системных вызовов.
CHayT 17.11.2020 01:44 # 0
j123123 17.11.2020 02:22 # 0
bormand 17.11.2020 02:32 # 0
Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.
Теорему про раскраску графа вообще чуть ли не брутфорсом доказывали...
З.Ы. Ня, привет.
CHayT 17.11.2020 02:56 # +1
Что интересно, это не потому, что мне было лень эту функцию на леммы разбивать, а именно чтобы получить в итоге нужный тип. Такая вот злая лемма. Всё-то криво в этом вашем программировании, никаких красивых симметрий.
j123123 15.04.2021 01:15 # 0
т.е. есть генератор стратегий, ему дают теорему, он выплевывает стратегию gen_strateg(theorem) -> strategy
и есть бесконечно генерирующая теоремы херня, допустим gen_theorem(0) - одна теорема, gen_theorem(1) - другая, и так далее.
А потом надо доказать что Так делают?
CHayT 15.04.2021 01:40 # +1
Вопрос я, конечно, не понял, но ответ на него скорее всего – нет. Дело в том, что стратегий в Coq нет, есть тактики, и они пишутся на совершенно другом метаязыке (Ltac), нежели теоремы (Gallina). (В Lean не так, кстати. Там по слухам гомоиконность) Поэтому написать теорему про тактику в Coq – это как написать функцию, принимающую как аргумент макрос, в C.
MAKAKA 15.04.2021 01:41 # +1
CHayT 15.04.2021 01:42 # 0
j123123 15.04.2021 01:59 # 0
У `стратегии' тип это список правил, по которым некая питушня что-то набрасывает в качестве пруфа теоремы, пытаясь это доказать. Ну ок, пусть будет `тактики', а не `стратегии'. Почему б не доказывать, что такие-то тактики, генерируемые на основе конкретных теорем, всегда успешно доказывают теоремы, сгенеренные таким-то способом? Т.е. доказать что генератор тактик всегда для такого семейства теорем, генерируемых таким способом, генерит такие тактики, которые всегда доказывают соотв. теорему
CHayT 15.04.2021 02:08 # 0
j123123 15.04.2021 02:04 # 0
А почему не сделать это одним языком? Чтобы можно было доказывать доказуемость некоего множества теорем такими-то генеренными из теорем тактиками.
CHayT 15.04.2021 02:14 # 0
Нянужно! Gallina имеет крайне строгую семантику, поскольку она является доверенной по принципу де Бройля. Поэтому в ней не может быть никаких свистелок и перделок, и всё крайне ограничено и консервативно. А Ltac – не доверенный язык, в нём можно сколько угодно фич пилить и ломать семантику как хочешь. Поэтому его используют для автоматизации, т.к. удобно.
j123123 15.04.2021 02:21 # 0
Ну так почему б не написать транспилер из Ltac в Gallina? В самой Gallina сделать тьюринг-полноту с гомоиконами, и пусть само с собой там метушится, доказывая доказуемость.
CHayT 15.04.2021 02:28 # 0
Принципиально нявозможно. Ltac – Тьюринг полный, Gallina – нят.
j123123 15.04.2021 02:47 # 0
Зачем? Зачем? Я могу описать функцию, принимающую стейт брейнфака возвращающую новый стейт брейнфака плюс номер шага, и через Ltac я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота. Ради чего это?
CHayT 15.04.2021 03:00 # +1
Во-первых, Ltac – логический язык, типа пролога. Формально описывать на Gallina шаг Ltac, и затем применять его с помощью Ltac – это как бутылку кваса провести через весь пищеварительный тракт наверх ко рту, чтобы вылить всё её содержимое в дыхательное горло.
> я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота
Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
j123123 15.04.2021 03:28 # 0
Чтобы доказывать применимость таких-то стратегий (стратегий, построенных по определенному шаблону) к доказыванию таких-то теорем, построенных по определенному шаблону. Сделать еще какую-то алгебру стратегий, что такие-то стратегии можно упростить, сведя их к таким-то, а вот такие стратегии это частные случаи таких стратегий. Более высокий уровень абасракции короче.
> Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
Почему не будет? Так мы пробуем доказать небесконечность цикла, и раз мы так можем делать, это и есть тьюринг-полнота, мы интерпретируем брейнфак. Какая разница, зависнет ли у меня Ltac генерящий питушню для Gallina, или Gallina само себе питушню генерить будет и зависнет?
CHayT 15.04.2021 03:50 # 0
Огромная. [1] [2]
[1] https://govnokod.ru/26981#comment579147
[2] https://govnokod.ru/27333#comment620156
Поднимаю говно-Хирш
j123123 15.04.2021 02:17 # 0
CHayT 15.04.2021 02:27 # 0
В переводе на петушиный: у меня есть функция F(n : nat), возвращающая термы в универсуме U + 1.
> Есть генератор тактик, тактика1 доказывает теорему1, тактика2 доказывает теорему2 и так далее.
В переводе на петушиный: у меня есть функция G от nat, которая возвращает терм типа F(n) в универсуме U.
> И надо доказать, что все такие генеретные тактики доказывают все такие генеренные теоремы.
В переводе на петушиный: надо найти определение G.
> Почему это не в рамках единого языка?
Просто переформулировав пробему как показано выше, ты и сделаешь это в рамках одного языка.
CHayT 15.04.2021 02:35 # 0
А тактики – это макроязык такой.
j123123 15.04.2021 04:18 # 0
Переформулировать-то можно, это понятно. Но так не выйдет доказать что-то относительно неких свойств стратегий, применимости определенных стратегий к доказыванию определенных типов теорем и так далее. Окажись стратегий частью самого языка для описания теорем, это можно было бы делать.
CHayT 15.04.2021 10:49 # 0
j123123 16.04.2021 18:42 # 0
bormand 16.04.2021 18:49 # +1
В этом вроде и идея ltac. Нет никакого смысла доказывать, что он правильно работает в общем случае или для каких-то классов теорем. Достаточно просто проверять сгенерённые им пруфы для конкретных теорем которые тебе и нужно доказать.
j123123 16.04.2021 18:58 # 0
bormand 16.04.2021 19:01 # 0
А технически и питон и даже пхп сойдут, конечно.
j123123 16.04.2021 19:08 # 0
bormand 16.04.2021 19:09 # +1
DypHuu_niBEHb 16.04.2021 19:10 # 0
j123123 16.04.2021 19:11 # 0
CHayT 16.04.2021 19:15 # 0
Причина: ты что, пёс, я Computer Scientist.
Ну а на деле: люди бы ебанулись на LISP паттерн-матчинг типов пилить. Да в нём и нету нормального паттерн-матчинга.
CHayT 16.04.2021 19:10 # +1
j123123 16.04.2021 19:18 # 0
CHayT 16.04.2021 19:22 # 0
CHayT 16.04.2021 19:34 # 0
j123123 16.04.2021 19:40 # 0
Тогда еще больше причин делать всю петушню в рамках одного языка, а не разграничивать на две хрени, которые там еще как-то перепихиваются в процессе.
CHayT 16.04.2021 19:43 # 0
j123123 16.04.2021 19:46 # 0
Я ведь тогда не могу в Coq доказать что Coq(Coq(x)) проверяет x и считает этот пруф верным или не верным тогда же, когда, когда это делает Coq(Coq(Coq(x))), даже не смогу это объявить как аксиому(если это недоказуемо из-за какой-то там неполноты), да? И что в этом хорошего?
j123123 16.04.2021 19:58 # 0
j123123 16.04.2021 20:22 # 0
j123123 16.04.2021 20:22 # 0
CHayT 16.04.2021 20:30 # +1
j123123 16.04.2021 20:31 # 0
Это копипаста, которую я хуй знает когда написал.
CHayT 16.04.2021 20:40 # 0
Это вореции?
j123123 16.04.2021 20:47 # 0
Нет. Это одна моя старая идея метаязыка для конструирования языков, который будет сам на себе написан, и чтоб всё через частичные вычисления, проекции Футамуры и формальные доказательства там работало, и чтобы это был один единый язык с Тьюринг-полнотой, самомодифицирующийся в процессе исполнения (система переписывающих правил чтоб, грубо говоря запуск языка это самопереписывание графа, полученного из AST с чтением из STDIN выплевыванием чего-то из STDOUT). И на этой алгебре самопереписывания уже б вводились всякие теории типов.
bormand 16.04.2021 22:51 # +1
j123123 17.04.2021 04:57 # +1
Если б мне кто-то профинансировал запиливания хрени, которую я расписал, я б ее очень даже охотно писал.
j123123 16.04.2021 20:30 # 0
Раз у Gallina нет тьюринг-полноты и в нем нельзя написать Gallina-интерпретатор, в рамках Gallina нельзя что-то доказывать о том, как что-либо делается самой Gallina для доказывания чего-либо, верно? И нельзя делать эти проекции Футамуры, о которых я выше написал.
CHayT 16.04.2021 20:45 # 0
Т.к. Gallina не Тьюринг-полна, в теории может и можно написать её интерпретатор на не-Тьюринг полном языке. Напиши, проверишь.
bormand 16.04.2021 22:57 # 0
На сишных макросах? Они как раз не тьюринг полны.
j123123 17.04.2021 04:55 # 0
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.
bormand 17.04.2021 05:50 # 0
Т.е. это явно более узкий класс программ чем в типичном "тьюринг-полном" языке, который ограничен только памятью.
j123123 17.04.2021 06:11 # +1
Ну как бы смотря как ты определяешь"класс программ". Если "тьюринг-полный" язык органичен конечной памятью, доказательство зависания для него можно всегда доказать через https://ru.wikipedia.org/wiki/Нахождение_цикла
Рассмотрим функцию "шаг интерпретатора"
Если state это некая хуита, занимающая конечный кусок в оперативной памяти (нет никаких указателей и выделений памяти) то если бесконечный вызов хуйни в хуйню
То значение `st' обязательно будет повторяться т.к. количество состояний конечно.
И если такая программа выводит что-то в stdout допустим(но ничего не получает извне), то она сводима к:
j123123 17.04.2021 06:34 # 0
j123123 17.04.2021 06:48 # 0
или принимает бесконечную периодическую строку, такую строку тоже можно в код вшить.
j123123 17.04.2021 05:02 # 0
Некий условный 1 шаг интерпретатора Gallina однозначно можно написать на Gallina т.к. 1 шаг брейнфака написать там точно можно. А вот "вызывать" интерпретатор бесконечное количество раз в Gallina нельзя, и это может сделать только некая внешняя хрень, которая что-то доказывает в терминах Gallina. Как-то так
j123123 16.04.2021 19:44 # 0
https://archive.jlongster.com/Lisp--It-s-Not-About-Macros,-It-s-About-Read
CHayT 16.04.2021 19:53 # +1
А я все ломал голову, как человек может так ненавидеть будущее, так привязаться к прошлому, что пишет на лиспе? Но для лиспопетушка-контрамота лисп - это и есть будущее. А дальше ВВ2, индустриальная контрреволюция, религиозные войны, рабовладельческий строй, отрастание хвостов и подъем на деревья. Скай из зе лимит!
На самом деле в Lisp и Scheme всё очень печально с pattern-matching'ом, и всякие CSшни в современном мире без него пилить никому не охота.
j123123 16.04.2021 20:01 # 0
В чем именно заключается печальность? Что мешает сделать DSL для pattern-matching'а?
CHayT 16.04.2021 20:04 # 0
Его там нет. (Ну может в современных диалектах появился)
> Что мешает сделать DSL для pattern-matching'а?
Так сделали, само собой. Но когда я открываю доки по pcase, я плачу, настолько он уродливый.
j123123 17.04.2021 05:44 # 0
https://docs.racket-lang.org/reference/match.html такой паттерн матчинг норм? Покажи реальный пример хорошего паттерн-матчинга в каком-то язычке.
CHayT 16.04.2021 19:28 # 0
Более того, с его помощью легко запилить что-то неправильное. Ключевые слова Qed. и Defined. потом всё перепроверяют.
Особенный багор, когда ты ltac'ом запилил огромный fixpoint, а он оказался не структурным, т.к. auto где-то подхватило рекуррентный вызов ))) Приходится во избежание этого гипотезы чистить вилкой.
CHayT 15.04.2021 02:03 # 0
j123123 15.04.2021 02:05 # 0
CHayT 15.04.2021 02:19 # 0
TOPT 15.04.2021 04:26 # 0
j123123 15.04.2021 04:40 # 0
JloJle4Ka 15.04.2021 05:45 # +1
rotoeb 17.11.2020 02:29 # −4
nihau 17.11.2020 11:34 # +2
CHayT 17.11.2020 12:33 # +7
Xepyc_DJIuHyc 17.11.2020 12:49 # 0
CHayT 17.11.2020 12:59 # +5
OCETuHCKuu_nemyx 17.11.2020 17:17 # +2
CHayT 18.11.2020 02:20 # 0
BY3 17.11.2020 23:12 # 0
j123123 17.11.2020 13:12 # 0
CHayT 17.11.2020 13:25 # 0
CHayT 17.11.2020 15:27 # 0
bormand 17.11.2020 15:35 # 0
CHayT 17.11.2020 15:39 # 0
bormand 18.11.2020 02:49 # +3
CHayT 22.12.2020 12:47 # +1
bormand 22.12.2020 13:03 # 0
CHayT 22.12.2020 15:52 # +4
OCETuHCKuu_nemyx 17.11.2020 17:18 # +7