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

Question

在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

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

Answer 1

您可以使用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将被绑定到具体化的目标上，并将在e中发挥作用。这两者都应该具有Term类型。

您可以使用Term将Term值转换为Agda语法。

所有这些都可以使用tactic关键字捆绑起来。您可以在changelog中阅读一些关于tactic的稍微过时的信息，大概在wiki的某个地方读到更多的信息。https://github.com/agda/agda/blob/master/CHANGELOG

Answer 2

对称性的证明是通过研究ope的所有可能的情况来证明的。在Agda中，通过模式匹配进行案例推理。