将 Coq 定义转化为现实？

Question

我想知道是否有系统的方法将 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

这是进行此翻译的正确通用架构吗，例如，此翻译是否可靠且完整？

编辑：

我意识到更新应该 return 一张地图，但我很困惑，因为 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')

Answer 1

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

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

回答你在这里遇到的具体问题：Agda 没有尝试推断 tUpdate 函数的 return 类型，因为你自己已经指定它是 Set 。如果你想让 Agda 为你推断它，你可以简单地用下划线 _ 替换 return 类型（在这种情况下工作正常）：

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

将 Coq 定义转化为现实？

Translating Coq Definitions to agda?

compilation

translate

coq

agda