coq - HoTT 的 Coq:证明 || P-> X || -> (P-> ||X||)
问题描述
我需要在 Coq 中证明对于任何类型 X 和任何命题 P(尽管我认为即使 P 是一种类型它也应该有效)存在
截断实现:|| P-> X || -> (P-> ||X||)
在哪里 ||_|| 是HoTT书中用来表示命题截断的符号。
我证明了类型论中的陈述:一个人通过使用命题截断的归纳原理得到论文,假设从 H :|| P-> X || 和 ap: P 即 H=|H'|,其中 H': P->X ,然后定义 trunc_impl(p):= |H'(p)|。(|-| 表示 trucation 的构造函数,即 |_| : A -> ||A||)。
顺便说一句,我不能用 Coq 写它!任何帮助将不胜感激。
我正在使用 GitHub 上提供的 HoTT 库。
解决方案
您需要这样做,Require Import Basics.
因为 coq 不知道 Trunc.TruncType 可以强制转换为 Type 否则。您要了解的策略是apply Trunc_ind
针对诸如forall (x : Tr _ _), _
.
intros x y
并将revert x
派上用场将目标转化为您要申请的表格trunc_ind
。
您还具有(自定义)策略strip_truncations
,它将在上下文中搜索任何被截断的术语,并尝试对它们进行归纳以删除它们。这要求目标被截断,但这在这里不应该是一个问题。
最后,截断的构造函数是tr
,所以你可以apply
在那里使用。
推荐阅读
- python - Kivy 无法更新操作按钮图标
- java - 如何要求多部分文件的虚假列表?
- html - 如何使导航链接居中
- apache-spark-sql - Spark中Group_Concat函数的替代
- javascript - 如何从类内部调用的函数返回值
- docker - 在 Windows 容器重新启动之间保留对 Windows 注册表的更改
- javascript - 如何使用javascript或jquery检查嵌套gridview中的取消选中复选框
- php - 由于密码字段而导致注册失败错误?
- string - 打字稿类型'字符串| string[]' 不能分配给类型'string',什么是'string | 字符串[]' 类型?如何将它们转换为字符串?
- apache - 为什么我的 mod_proxy 标志在 htaccess 中停止工作?