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

논문에서 증명을 할 때, 연관성과 을 누른 다음 왼쪽 신원은 신원 관계의 과대 키 속성을 사용합니다 - 전이성. 즉, p : x ≡ y과 q : y ≡ z의 증명이있는 경우이를 trans p q : x ≡ z의 단일 증명으로 결합 할 수 있습니다. trans 기능은 이미 표준 라이브러리 (Relation.Binary.PropositionalEquality 모듈)의 일부이지만, 그 구현은 어쨌든 매우 간단하다 : 나는 monoids 및 그룹의 약간 다른 프리젠 테이션을 사용하고

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 기록의 일부로서 기록된다). 이 목표 (x ⁻¹ ∙ x) ∙ y ≡ y 우리 잎, 즉 assoc (x ⁻¹) x y입니다

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

첫 번째 단계는 연관성을 사용하는 것입니다 - 우리가 증명되면 우리가 함께 trans를 사용하여이 두 부분을 병합 할 수 있습니다 : 우리는 것을 증명하고 싶습니다 :

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

오른쪽 역 특성을 적용해야하지만 유형이 적합하지 않은 것 같습니다. 우리는 left-inv x : x ⁻¹ ∙ x ≡ ε이 있고 여분의 것을 어떻게 처리해야합니까? y. 이것은 정체성의 또 다른 속성이 작용할 때입니다.

일반 기능은 신원을 보존합니다. f 함수와 p : x ≡ y 증명이있는 경우 x 및 y에 f을 적용 할 수 있으며 증명은 여전히 ​​유효해야합니다 즉 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