coq - Paramcoq:Coq 中的自由定理
问题描述
如何使用插件Paramcoq证明以下自由定理?
Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X), f X x = x.
如果不可能,那么这个插件的目的是什么?
解决方案
该插件可以为任何类型生成参数声明。您仍然需要将其声明为公理或假设才能实际使用它:
Declare ML Module "paramcoq".
Definition idt := forall A:Type, A -> A.
Parametricity idt arity 1.
(* ^^^ This command defines the constant idt_P. *)
Axiom param_idt : forall f, idt_P f.
Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X) : f X x = x.
Proof.
intros.
apply (param_idt f X (fun y => y = x) x).
reflexivity.
Qed.
推荐阅读
- css - 如何用css替换文本
- macos - 如何在 Mac 上删除对 Visual Studio 的钥匙串访问?
- python - 如何使用 youtube-dl 将“upload_date”标记为 m4a 文件的“年份”标签?
- python - Python PIL 图像裁剪增加文件大小
- java - 消费者数组中的 ArrayStoreException
- python - 我正在尝试在我的规范化函数中使用我在 getData 函数中创建的列表
- javascript - 如何将状态从一个功能组件传递到另一个由按钮组件呈现的功能组件?
- javascript - 加载第三方 javascript 库
- javascript - 使用 mysql2 async/await 时出现“发送到客户端后无法设置标头”错误
- javascript - 单击提交后无法自动清除输入字段(React)