types - 如何避免(不必要的?)在 Agda 中重复使用公理?

标签 types pattern-matching agda

是否有一种方法可以在 Agda 中以编程方式构造(子)证明? 因为有些证明非常相似,最好简化它们......但我不知道该怎么做。例如考虑以下代码

{-
At first we reaname  Set to 𝓤 (as in Universe)
-}
𝓤 = Set

{-
  We define also a polymorphic idenity
-}
data _==_ {A : 𝓤} (a : A) : A → 𝓤 where
  definition-of-idenity : a == a
infix 30 _==_

{-
  The finite set Ω 
-}
data Ω : 𝓤 where
  A B : Ω

Operation = Ω → Ω → Ω

{-
 symmetry is a function that takes an Operation
 op and returns a proposition about this operation
-}

symmetry : Operation → 𝓤
symmetry op = ∀ x y → op x y == op y x

ope : Operation
ope A A = A
ope A B = B
ope B A = B
ope B B = B

proof-of-symmetry-of-operator-ope : symmetry ope
proof-of-symmetry-of-operator-ope A A = definition-of-idenity
proof-of-symmetry-of-operator-ope B B = definition-of-idenity
proof-of-symmetry-of-operator-ope A B = definition-of-idenity
proof-of-symmetry-of-operator-ope B A = definition-of-idenity

为什么我不能只使用以下简化的一行证明?

proof-of-symmetry-of-operator-ope _ _ = definition-of-idenity

看来模式匹配是造成这种行为的原因。但我不明白为什么。

最佳答案

您可以使用 Agda 的反射功能以编程方式生成证明。

这是使用可重用策略解决问题的示例。我把这个问题放在一起,所以我不保证这是最强大的策略。不过,它应该能让您了解如何在 Agda 中解决此类问题!

最重要的是,您可以编写如下实现:

proof-of-symmetry-of-operator-ope : symmetry ope
proof-of-symmetry-of-operator-ope = tactic exhaustive-tactic

http://www.galois.com/~emertens/exhaustive-tactic-example/Tactic.html

在 Agda 中,您可以使用 quoteGoal g in e 将当前目标类型和环境具体化为值。 g 将绑定(bind)到具体化的目标,并且将在 e 的范围内。这两个都应该有类型 Term

您可以使用unquoteTerm值转换回Agda语法。

所有这些都可以使用战术关键字捆绑在一起。您可以在变更日志中阅读一些关于战术的稍微过时的信息,并且可能在维基百科上的某个地方阅读更多信息。 https://github.com/agda/agda/blob/master/CHANGELOG

关于types - 如何避免(不必要的?)在 Agda 中重复使用公理?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/29976812/

相关文章:

c# - 如何在 C# 中检查一个字符串不是关键字或类型

swift - 有没有办法在函数中使用通用协议(protocol)作为数据类型?

rust - 如何编写宏来匹配略有不同的匹配语句?

正则表达式:如何匹配重复的字符或数字

agda - 列表合并的终止检查

sql - MS Access SQL,更改数据类型

c# - 为什么这段代码没有编译?

pattern-matching - Elixir:使用模式匹配捕获 map 的其余部分

agda - 如何使用身份消除(在 agda 中)来证明 Eckmann Hilton 在 HoTT 中的高维路径?

agda - 证明 Agda 中加法的交换律