将 Coq 定义翻译成 agda？答案

【问题标题】：Translating Coq Definitions to agda?将 Coq 定义翻译成 agda？
【发布时间】：2020-07-22 17:50:39
【问题描述】：

我想知道是否有系统的方法可以将 Coq 定义解释为 agda 程序。我正在翻译部分编程基础，但无法让 tUpdate 函数在下面工作。为什么这会失败。 coq代码被注释掉了。

--Definition total_map (A : Type) := string -> A.

totalMap : Set → Set
totalMap A = String → A

-- Definition t_empty {A : Type} (v : A) : total_map A :=
-- (fun _ => v).

tEmpty : {A : Set} (v : A) → totalMap A
tEmpty = λ v x → v

-- Definition t_update {A : Type} (m : total_map A)
-- (x : string) (v : A) :=
-- fun x' => if eqb_string x x' then v else m x'.

tUpdate : {A : Set} (m : totalMap A) (x : String) (v : A) → Set 
tUpdate m x v = λ x' → (if (x == x') then v else m x')

lambda 项产生以下错误

(x' : String) → A !=< Set of type Set
when checking that the expression
λ x' → if x == x' then v else m x' has type Set

这是否是进行此翻译的正确通用模式，例如，此翻译是否合理且完整？

编辑：

我意识到 update 应该返回一个地图，但我很困惑，因为它 coq 似乎可以推断出这一点，而 agda 不能？我仍然欢迎对后一个问题提供更一般的答案。

tUpdate : {A : Set} (m : totalMap A) (x : String) (v : A) → totalMap A
tUpdate m x v = λ x' → (if (x == x') then v else m x')

【问题讨论】：

标签： compilation coq translate agda

【解决方案1】：

Coq 和 Agda 都基于非常粗略相同的依赖类型理论，因此理论上可以将 Coq 脚本生成的证明项转换为 Agda 程序。但是，有许多小的（而且不是那么小的）差异，例如Coq 的隐含性 Prop、累积性、终止检查器的差异等，会使这样的翻译变得困难或不可能。

但是，您在这里要求的并不是真正的自动翻译器，而是手动将 Coq 翻译成 Agda 的一套规则。由于许多基本特征可以一对一地映射，所以这个过程要简单得多。但是，在 Coq 代码中使用任何策略都必须在 Agda 中转换为显式证明术语，或者编写自己的 Agda 反射宏（因为目前还没有完整的 Agda 策略库）。

回答您在这里遇到的具体问题：Agda 没有尝试推断tUpdate 函数的返回类型，因为您已经将其指定为Set。如果您希望 Agda 为您推断，您可以简单地将返回类型替换为下划线 _（在这种情况下可以正常工作）：

tUpdate : {A : Set} (m : totalMap A) (x : String) (v : A) → _
tUpdate m x v = λ x' → (if (x == x') then v else m x')

【讨论】：