标签: agda

我想证明

\xe2\x88\x80 {\xe2\x84\x93} {A B C D : Set \xe2\x84\x93} \xe2\x86\x92 (A \xe2\x86\x92 B) \xe2\x89\xa1 (C \xe2\x86\x92 D) \xe2\x86\x92 A \xe2\x89\xa1 C\n

（与密码域类似）。

如果我有一个函数domain返回函数类型域的函数，我可以将证明写为

cong domain\n

但我认为不可能编写这样的函数。

有什么办法可以做到这一点吗？

在Agda中,通常有两种方法来改进集合.一种是简单地编写一个函数来检查属性是否成立,并提升.例如:

has_true : List Bool -> Bool 
has_true (true ? xs) = true
has_true (false ? xs) = has_true xs
has_true [] = false

Truthy : List Bool -> Set
Truthy list = T (has_true list)

这里Truthy list证明了布尔列表至少有一个真元素.另一种方法是直接编码该属性,作为归纳类型:

data Truthy : List Bool -> Set where
  Here  : (x : Bool) -> (x ? true) -> (xs : List Bool) -> Truthy (x ? xs)
  There : (x : Bool) -> (xs : List Bool) -> Truthy xs …

我尝试使用Agda 2.6.1.3和Agda stdlib 1.5编译hello-world示例。下面是代码：

module hello-world where

open import IO

main = run (putStrLn "Hello, World!")

用Agda( agda --compile hello-world.agda)编译时，报如下错误：

Unsolved metas at the following locations:
  $HOME/hello-world.agda:5,8-11

报告的位置 ( 5,8-11) 对应于 token run。

我在 Agda 和 Agda-stdlib Issues 中都没有找到任何相关信息，在 SO 或其他网站上也没有找到任何相关信息。文档是否已过时，或者我是否犯了任何错误？

笔记：

• Agda 编译器是通过stack install Agda解析器安装的lts-17.5。
• 我还尝试从 GitHub 源（分支）手动编译release-2.6.1.3。
• 在$HOME/.agda/libraries我有：

  $HOME/agda-stdlib/standard-library.agda-lib
  

  Run Code Online (Sandbox Code Playgroud)
• 在$HOME/.agda/defaults我有：

  standard-library
  

  Run Code Online (Sandbox Code Playgroud)

在 Haskell 中寻找一个可以将任意深度嵌套列表展平的函数时，即一个concat递归应用并在最后一次迭代（使用非嵌套列表）时停止的函数，我注意到这需要有一个更灵活的类型系统，因为列表深度不同，输入类型也不同。事实上，有几个 stackoverflow 问题——比如这个问题——其中的回答指出“不存在一个函数可以‘查看’不同深度的不同嵌套列表”。

编辑：一些答案提供哈斯克尔的解决方法，无论是对自定义数据类型或具有帮助TypeFamilies或MultiParamTypeClasses（如在由Noughtmare下面的答案，或者通过“Landei”在回答上述职位或由“约翰·L”回答这个职位）。然而，这些家族和类似乎也是因为缺少/替代haskell 中的依赖类型而引入的（例如，haskell wiki声明“类型家族 [...] 很像依赖类型”。

我现在的问题是，如果这是真的，哈斯克尔的确originially没有定义此类功能（即如扁平化不同深度的列表），而且，如果这些问题就会消失，一旦一个移动到语言实现由依赖类型？（例如 Idris、Agda、Coq 等）我没有使用这些语言的经验，这就是我问的原因。

例如，在 Idris 网站上，据说“类型可以作为参数传递给函数”，因此，我认为，在列表扁平化的情况下，可以简单地将列表的类型作为参数传递并实现以直接的方式获得所需的功能。这可能吗？

一个后续问题也将是：在haskell 中解决这个问题的那些族和类是否在haskell 中提供了依赖类型理论的完整实现，或者如果没有，有什么重要区别？

当我写下以下函数是agda时,

f : (A : Set) ? (a : A) ? ?
f ? n = n

我希望错误说我没有指定所有情况.

相反,我收到此错误:

Type mismatch:
expected: ?
actual: ?
when checking that the expression n
has type ?

这里发生了什么？

我在看下面的定义cong:

cong : ? {a b} {A : Set a} {B : Set b} (f : A ? B) {x y} ? x ? y ? f x ? f y
cong f refl = refl

我无法理解为什么它的打字很好.特别是,似乎隐含的论点refl必须是f x和f y.为了使事情更清楚,我写了一个非隐式的相等版本,并试图复制证明:

data Eq : (A : Set) -> A -> A -> Set where
  refl : (A : Set) -> (x : A) -> Eq A x x

cong : (A : Set) -> …

一段代码在这里：

-- transitivity
trans : {A : Set} {x y z : A} -> x == y -> y == z -> x == z
trans refl refl = refl

union-pair' : {A : Set} -> (m n : S {A}) -> (x : A) ->
                           (ismember (set-union (set-pair m n)) x) == (ismember (union m n) x)
union-pair' m n x with ismember m x | ismember n x | ismember (set-union (set-pair m n)) x
union-pair' : {A …