agda - 在 Agda 中应用规则

Question

我是 Agda 的新手，我认为我在那个范式中仍然有问题需要思考。这是我的问题..我有一个类型 monoid 和一个类型 Group 实现如下:

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 = ?

如果我在纸上这样做，我将应用关联性然后留下身份..但我不知道如何告诉 agda 应用这些规则..我有将我的想法转化为 Agda 范式的问题..

非常感谢任何帮助..

Answer 1

当您在纸上进行证明时，应用关联性并然后留下身份使用身份关系的唯一关键属性 - 传递性。也就是说，当您有 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