在Agda中应用规则

Question

我是Agda的新手，我认为在这种范例中我仍然有一个问题需要思考。这里是我的问题.. 我有一种独异和实施的类型组如下：

record Monoid : Set₁ where 
    constructor monoid 
    field Carrier : Set 
     _⊙_  : Carrier → Carrier → Carrier 
     e  : Carrier 
     leftId : ∀ {x : Carrier} → (e ⊙ x) ≡ x 
     rightId : ∀ {x : Carrier} → (x ⊙ e) ≡ x 
     assoc : ∀ {x y z : Carrier} → (x ⊙ (y ⊙ z)) ≡ ((x ⊙ y) ⊙ z) 

record Group : Set₁ where 
    constructor group 
    field m  : Monoid 
      inv  : Carrier → Carrier 
      inverse1 : {x y : Carrier} → x ⊙ (inv x) ≡ e 
      inverse2 : {x y : Carrier} → (inv x) ⊙ x ≡ e 

现在，我要证明下面的引理：

lemma1 : (x y : Carrier) → (inv x) ⊙ (x ⊙ y) ≡ y 
lemma1 x y = ? 

如果我写在纸上，我会申请associativity然后离开身份..但我不知道如何告诉agda应用这些规则..我有我的想法转化为Agda范式的问题..

任何帮助是高度赞赏..

Answer 1

当你在纸上做证明时，应用关联性和，然后左边的身份使用ony关键性质的关系 - 传递性。也就是说，当您有一个p : x ≡ y和q : y ≡ z的证明时，您可以将它们合并为一个trans p q : x ≡ z的单个证明。该trans功能已经是标准库（Relation.Binary.PropositionalEquality模块）的一部分，但它的实现是相当简单的，反正：

trans : {A : Set} {i j k : A} → i ≡ j → j ≡ k → i ≡ k 
trans refl eq = eq 

我正在使用幺和团体的有点不同表现，但你可以轻松适应证明到你的场景。

open import Function 
open import Relation.Binary.PropositionalEquality 

Op₁ : Set → Set 
Op₁ A = A → A 

Op₂ : Set → Set 
Op₂ A = A → A → A 

record IsMonoid {A : Set} 
     (_∙_ : Op₂ A) (ε : A) : Set where 
    field 
    right-id : ∀ x → x ∙ ε ≡ x 
    left-id : ∀ x → ε ∙ x ≡ x 
    assoc : ∀ x y z → x ∙ (y ∙ z) ≡ (x ∙ y) ∙ z 

record IsGroup {A : Set} 
     (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set where 
    field 
    monoid : IsMonoid _∙_ ε 
    right-inv : ∀ x → x ∙ x ⁻¹ ≡ ε 
    left-inv : ∀ x → x ⁻¹ ∙ x ≡ ε 

    open IsMonoid monoid public 

（为简便起见，缩进代码写为IsGroup记录的一部分）。我们想证明：

lemma : ∀ x y → x ⁻¹ ∙ (x ∙ y) ≡ y 
    lemma x y = ? 

的第一步是使用相关性，即assoc (x ⁻¹) x y，这给我们留下了一个目标(x ⁻¹ ∙ x) ∙ y ≡ y - 一旦我们证明，我们可以合并这两个部分共同使用trans：

lemma x y = 
    trans (assoc (x ⁻¹) x y) ? 

现在，我们需要应用正确的反转属性，但类型似乎不适合。我们有left-inv x : x ⁻¹ ∙ x ≡ ε，我们需要以某种方式处理额外的y。这是身份的另一个属性起作用的时候。

普通函数保存身份;如果我们有功能f和证明p : x ≡ y我们可以将f应用于x和y并且证明应该仍然有效，即cong f p : f x ≡ f y。再次，实施已经在标准库中，但在这里它是反正：

cong : {A : Set} {B : Set} 
     (f : A → B) {x y} → x ≡ y → f x ≡ f y 
cong f refl = refl 

我们应该使用什么函数？好的候选人似乎是λ z → z ∙ y，它增加了缺失的y部分。因此，我们有：

cong (λ z → z ∙ y) (left-inv x) : (x ⁻¹ ∙ x) ∙ y ≡ ε ∙ y 

再次，我们只需要证明ε ∙ y ≡ y，然后我们可以使用trans拼凑那些在一起。但是这最后一个属性很简单，只是left-id y。全部放在一起，我们得到：

lemma : ∀ x y → x ⁻¹ ∙ (x ∙ y) ≡ y 
    lemma x y = 
    trans (assoc (x ⁻¹) x y) $ 
    trans (cong (λ z → z ∙ y) (left-inv x)) $ 
      (left-id y) 

---

标准库还为我们提供了一些不错的语法糖这样的：

open ≡-Reasoning 

    lemma′ : ∀ x y → x ⁻¹ ∙ (x ∙ y) ≡ y 
    lemma′ x y = begin 
    x ⁻¹ ∙ (x ∙ y) ≡⟨ assoc (x ⁻¹) x y ⟩ 
    (x ⁻¹ ∙ x) ∙ y ≡⟨ cong (λ z → z ∙ y) (left-inv x) ⟩ 
    ε ∙ y   ≡⟨ left-id y ⟩ 
    y    ∎ 

在幕后，≡⟨ ⟩使用精确trans合并这些证据。这些类型是可选的（证明本身带有足够的关于它们的信息），但它们在这里是为了可读性。

---

为了让您的原始Group记录，我们可以这样做：

record Group : Set₁ where 
    field 
    Carrier : Set 
    _∙_  : Op₂ Carrier 
    ε  :  Carrier 
    _⁻¹  : Op₁ Carrier 

    isGroup : IsGroup _∙_ ε _⁻¹ 

    open IsGroup isGroup public