TN
но там может оказаться что упражнение не детское :-)
Size: a a a
2017 December 22
NK
@tonpa меня в первую очередь интересует, как применять ind_nat. Кубики из algstruct действительно выглядят страшновато
NK
Я так понимаю, это упражнение на механику применения ind_nat (что подтверждается тем, что соседние упражнения на механику применения rec_Nat). А полукольцо просто под руку продвернулось
TN
надо взять эти термы Coq и в Gallina их вывести :-)
NK
Нашёл на github.com проект HoTT, там рядом с книгой exercises сделанные на coq . На радостях полез туда, а все, что я ищу, там TODO :)
TN
стандартная фигня :-)
TN
Feel the cutting edge!
NK
Я сдался и пытаюсь доказать, что double n = n+n using only ind_nat
NK
Если я не хочу использовать Path, как это можно закодировать?
TN
кстати у теорем Nat есть своя страничка: http://groupoid.space/mltt/types/nat/
2017 December 23
NK
смотри какую книжку с картинками я нашёл http://www.mathematik.tu-darmstadt.de/~buchholtz/leanhott.pdf
NK
кубические конструкции == comp?
NK
comp <i> @
TN
double_n_is_add : (n:nat) -> Path nat (double n) (add n n) = split
zero -> <i> zero
suc x -> comp (<i> Path nat (suc (suc (double x))) (suc (add_suc x x @ -i)))
(<j> (suc (suc (double_n_is_add x @ j)))) []
zero -> <i> zero
suc x -> comp (<i> Path nat (suc (suc (double x))) (suc (add_suc x x @ -i)))
(<j> (suc (suc (double_n_is_add x @ j)))) []
TN
канонично так
NK
ага, если подставить все части в определение composition. Но с нуля такое имхо написать сложно (т.к. части в "обратном порядке" и [])
NK
— The first argument to comp is a path in the universe (i.e. an
— equality of types), as all of the paths in the example are in the
— same type this path is constantly A. The second argument is the
— bottom of the cube we are computing the composition of and the
— third argument is a list of the sides of the cube.
— equality of types), as all of the paths in the example are in the
— same type this path is constantly A. The second argument is the
— bottom of the cube we are computing the composition of and the
— third argument is a list of the sides of the cube.
NK
а тут у нас первый аргумент is not constantly A, и поэтому list of the sides is []