如何避免（不必要）重复使用公理在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

在阿格达你可以使用quoteGoal g in e来具体化，当前的目标类型和环境的价值。 g将被约束到具体目标，并将在e范围内。这两者都应该有类型Term

您可以将Term值转换回unquote的Agda语法。

所有这些都可以使用tactic关键字捆绑在一起。您可以在更新日志中阅读关于tactic的稍微过时的信息，并且可能更多地在Wiki上。 https://github.com/agda/agda/blob/master/CHANGELOG

Answer 2

通过查看所有可能的参数ope的对称性证明。在Agda中，您可以通过模式匹配来进行案例推理。