如何避免（不必要）重複使用公理在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中，您可以通過模式匹配來進行案例推理。