NK
я застрял на упражнении 1.9 из HOTT :(
Size: a a a
2017 December 22
NK
Подскажите, откуда копать под упражнение 1.9 в хотт ака Fin type family + fmax
TN
дам подсказку оно есть в дереве priv ;-)
TN
но ты можешь не подсматривать, оно действительно не похоже как в остальных языках
NK
Вот на этом я похоже и застрял (пытаясь сделать "как в других языках")
NK
Ага
ЗП
у кока он чуть другой https://coq.inria.fr/library/Coq.Vectors.Fin.html
TN
Та такой же
NK
Pred! Вот я тормоз :(
NK
я продолжаю читать хотт, сделал упражнения 1.9 (Fin/fmax) и 1.10 (ackermann). Теперь застрял на 1.8, часть третья : показать только с помощью ind_nat, что nat это полукольцо. Покажите плиз пример кусочка доказательства?
TN
Checking: functor_idtype
Type checking failed: check conv:
U
/=
Unit
Type checking failed: check conv:
U
/=
Unit
TN
ну идея какая, тебе надо посмотреть как строить рекорды с теоремами
TN
вот пример в algstruct
TN
там должно быть полукольцо
TN
останется заполнить его инстансами nat, возьмешь умножение и сложение
TN
полукольца нет но можно собрать
TN
isring (R : SET) : U
= (mul : ismonoid R)
* (add : iscgroup R)
* (isDistributive R.1 add.1.1.1 mul.1)
ring : U
= (X : SET) * isring X
= (mul : ismonoid R)
* (add : iscgroup R)
* (isDistributive R.1 add.1.1.1 mul.1)
ring : U
= (X : SET) * isring X
ЗП
можно инетерсно полукольцо представить 2-мя сопряженными моноидами?) это будет near semiring