Skip to content

Instantly share code, notes, and snippets.

@msakai
Last active October 22, 2024 14:40
Show Gist options
  • Save msakai/42a4ff7ea7be32781ad646502f42765f to your computer and use it in GitHub Desktop.
Save msakai/42a4ff7ea7be32781ad646502f42765f to your computer and use it in GitHub Desktop.
体 F が x + y = 1 かつ x y = 1 を満たすような元を持たない時、F ∪ {∞} は演算 x ⊛ y := (x y - 1) / (x + y - 1) に関して群になる
{-
体 F が x + y = 1 かつ x y = 1 を満たすような元を持たない時、F ∪ {∞} は
∞ ⊛ y = y
x ⊛ ∞ = x
x ⊛ y = (x y - 1) / (x + y - 1) if x + y ≠ 1
x ⊛ y = ∞ otherwise
で定義される演算によって群となる。
Checked with Agda version 2.7.0.1 and agda-stdlib-2.1.1
参考:
* https://x.com/MurakamiMath/status/1837434653634187342
-}
open import Algebra.Apartness.Bundles using (HeytingField)
open import Algebra.Core using (Op₁; Op₂)
open import Data.Product using (_×_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary using (¬_)
module ExtendedGroup
{c ℓ₁ ℓ₂}
(HF : HeytingField c ℓ₁ ℓ₂)
(#-dec : Decidable (HeytingField._#_ HF))
where
open import Algebra.Apartness.Structures using (IsHeytingField)
open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
open import Algebra.Definitions
open import Algebra.Solver.Ring.AlmostCommutativeRing using (AlmostCommutativeRing; fromCommutativeRing)
open import Algebra.Structures
open import Algebra.Bundles
open import Data.Empty
open import Data.List
open import Data.Product
open import Data.Sum
open import Function using (_$_)
open import Level using (_⊔_; suc)
open import Relation.Binary
open import Relation.Nullary
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import Algebra.Solver.Ring.NaturalCoefficients.Default
module Utils where
open HeytingField HF hiding (refl; sym; trans)
open IsEquivalence isEquivalence
open import Algebra.Properties.Ring (CommutativeRing.ring (HeytingCommutativeRing.commutativeRing heytingCommutativeRing)) using (-1*x≈-x) public
module Solver = Algebra.Solver.Ring.NaturalCoefficients.Default
(CommutativeRing.commutativeSemiring (HeytingCommutativeRing.commutativeRing heytingCommutativeRing))
open ≈-Reasoning setoid
unique-inverse
: ∀ {x₁ x₂} → (x₁≈x₂ : x₁ ≈ x₂)
→ ((x₁⁻¹ , _ , _) : Invertible _≈_ 1# _*_ x₁)
→ ((x₂⁻¹ , _ , _) : Invertible _≈_ 1# _*_ x₂)
→ x₁⁻¹ ≈ x₂⁻¹
unique-inverse {x₁} {x₂} x₁≈x₂ (x₁⁻¹ , x₁⁻¹x₁≈1 , x₁x₁⁻¹≈1) (x₂⁻¹ , x₂⁻¹x₂≈1 , x₂x₂⁻¹≈1) = begin
x₁⁻¹ ≈⟨ sym (*-identityʳ x₁⁻¹) ⟩
x₁⁻¹ * 1# ≈⟨ *-cong refl (sym x₂x₂⁻¹≈1) ⟩
x₁⁻¹ * (x₂ * x₂⁻¹) ≈⟨ sym (*-assoc x₁⁻¹ x₂ x₂⁻¹) ⟩
(x₁⁻¹ * x₂) * x₂⁻¹ ≈⟨ *-cong (*-cong refl (sym x₁≈x₂)) refl ⟩
(x₁⁻¹ * x₁) * x₂⁻¹ ≈⟨ *-cong x₁⁻¹x₁≈1 refl ⟩
1# * x₂⁻¹ ≈⟨ *-identityˡ x₂⁻¹ ⟩
x₂⁻¹
invert-right : ∀ {x y z} → x * y ≈ z → ((y⁻¹ , _ , _) : Invertible _≈_ 1# _*_ y) → x ≈ z * y⁻¹
invert-right {x} {y} {z} x*y≈z (y⁻¹ , _ , y*y⁻¹≈1) = begin
x ≈⟨ sym (*-identityʳ x) ⟩
x * 1# ≈⟨ *-cong refl (sym y*y⁻¹≈1) ⟩
x * (y * y⁻¹) ≈⟨ sym (*-assoc x y y⁻¹) ⟩
(x * y) * y⁻¹ ≈⟨ *-cong x*y≈z refl ⟩
z * y⁻¹
invert-left : ∀ {x y z} → x * y ≈ z → ((x⁻¹ , _ , _) : Invertible _≈_ 1# _*_ x) → y ≈ z * x⁻¹
invert-left {x} {y} {z} x*y≈z = invert-right y*x≈z
where
y*x≈z : y * x ≈ z
y*x≈z = trans (*-comm y x) x*y≈z
invert-both
: ∀ {x₁ y₁ x₂ y₂} → x₁ * y₁ ≈ x₂ * y₂
→ ((y₁⁻¹ , _ , _) : Invertible _≈_ 1# _*_ y₁)
→ ((y₂⁻¹ , _ , _) : Invertible _≈_ 1# _*_ y₂)
→ x₁ * y₂⁻¹ ≈ x₂ * y₁⁻¹
invert-both {x₁} {y₁} {x₂} {y₂} x₁*y₁≈x₂*y₂ inv-y₁@(y₁⁻¹ , _ , _) inv-y₂@(y₂⁻¹ , _ , _) = sym x₂*y₁⁻¹≈x₁*y₂⁻¹
where
x₁≈x₂*y₂*y₁⁻¹ : x₁ ≈ (x₂ * y₂) * y₁⁻¹
x₁≈x₂*y₂*y₁⁻¹ = invert-right x₁*y₁≈x₂*y₂ inv-y₁
x₁≈x₂*y₁⁻¹*y₂ : x₁ ≈ (x₂ * y₁⁻¹) * y₂
x₁≈x₂*y₁⁻¹*y₂ = begin
x₁ ≈⟨ x₁≈x₂*y₂*y₁⁻¹ ⟩
(x₂ * y₂) * y₁⁻¹ ≈⟨ *-assoc x₂ y₂ y₁⁻¹ ⟩
x₂ * (y₂ * y₁⁻¹) ≈⟨ *-cong refl (*-comm y₂ y₁⁻¹) ⟩
x₂ * (y₁⁻¹ * y₂) ≈⟨ sym (*-assoc x₂ y₁⁻¹ y₂) ⟩
(x₂ * y₁⁻¹) * y₂
x₂*y₁⁻¹≈x₁*y₂⁻¹ : x₂ * y₁⁻¹ ≈ x₁ * y₂⁻¹
x₂*y₁⁻¹≈x₁*y₂⁻¹ = invert-right (sym x₁≈x₂*y₁⁻¹*y₂) inv-y₂
*-cancelʳ : ∀ a {x₁ x₂} → (Invertible _≈_ 1# _*_ a) → (x₁ * a ≈ x₂ * a) → x₁ ≈ x₂
*-cancelʳ a {x₁} {x₂} (a⁻¹ , _ , a*a⁻¹≈1) x₁*a≈x₂*a = begin
x₁ ≈⟨ sym (*-identityʳ x₁) ⟩
x₁ * 1# ≈⟨ *-cong refl (sym a*a⁻¹≈1) ⟩
x₁ * (a * a⁻¹) ≈⟨ sym (*-assoc x₁ a a⁻¹) ⟩
(x₁ * a) * a⁻¹ ≈⟨ *-cong x₁*a≈x₂*a refl ⟩
(x₂ * a) * a⁻¹ ≈⟨ *-assoc x₂ a a⁻¹ ⟩
x₂ * (a * a⁻¹) ≈⟨ *-cong refl a*a⁻¹≈1 ⟩
x₂ * 1# ≈⟨ *-identityʳ x₂ ⟩
x₂
-‿-1≈1 : - (- 1#) ≈ 1#
-‿-1≈1 = begin
- (- 1#) ≈⟨ sym (+-identityˡ _) ⟩
0# - (- 1#) ≈⟨ +-cong (sym (-‿inverseʳ 1#)) refl ⟩
(1# + (- 1#)) - (- 1#) ≈⟨ +-assoc _ _ _ ⟩
1# + ((- 1#) - (- 1#)) ≈⟨ +-cong refl (-‿inverseʳ (- 1#)) ⟩
1# + 0# ≈⟨ +-identityʳ _ ⟩
1#
-1*-1≈1 : (- 1#) * (- 1#) ≈ 1#
-1*-1≈1 = begin
(- 1#) * (- 1#) ≈⟨ -1*x≈-x (- 1#) ⟩
- (- 1#) ≈⟨ -‿-1≈1 ⟩
1#
-0≈0 : - 0# ≈ 0#
-0≈0 = begin
- 0# ≈⟨ sym (+-identityˡ (- 0#)) ⟩
0# - 0# ≈⟨ -‿inverseʳ _ ⟩
0#
x≈y⇒x-y≈0 : ∀ {x y} → x ≈ y → x - y ≈ 0#
x≈y⇒x-y≈0 {x} {y} x≈y = begin
x - y ≈⟨ +-cong x≈y refl ⟩
y + (- y) ≈⟨ -‿inverseʳ y ⟩
0#
x-y≈0⇒x≈y : ∀ {x y} → x - y ≈ 0# → x ≈ y
x-y≈0⇒x≈y {x} {y} x-y≈0 = begin
x ≈⟨ sym (+-identityʳ x) ⟩
x + 0# ≈⟨ +-cong refl (sym (-‿inverseˡ y)) ⟩
x + (- y + y) ≈⟨ sym (+-assoc x (- y) y) ⟩
(x - y) + y ≈⟨ +-cong x-y≈0 refl ⟩
0# + y ≈⟨ +-identityˡ y ⟩
y
x+y≈1∧xy≈1⇒x²-x+1≈0 : ∀ {x y} → (x + y ≈ 1#) × (x * y ≈ 1#) → (x * x - x + 1# ≈ 0#)
x+y≈1∧xy≈1⇒x²-x+1≈0 {x} {y} (x+y≈1 , x*y≈1) = begin
x * x - x + 1# ≈⟨ +-cong (+-cong (sym (*-identityˡ (x * x))) (sym (-1*x≈-x x))) refl ⟩
1# * (x * x) + (- 1#) * x + 1# ≈⟨ +-cong (+-cong (*-cong (sym -1*-1≈1) refl) refl) refl ⟩
(- 1#) * (- 1#) * (x * x) + (- 1#) * x + 1# ≈⟨ solve 2 (λ x m → m :* m :* (x :* x) :+ m :* x :+ con 1 := m :* ((con 1 :+ m :* x) :* x) :+ con 1) refl x (- 1#) ⟩
(- 1#) * ((1# + (- 1#) * x) * x) + 1# ≈⟨ +-cong (*-cong refl (*-cong (+-cong refl (-1*x≈-x x)) refl)) refl ⟩
(- 1#) * ((1# - x) * x) + 1# ≈⟨ +-cong (-1*x≈-x _) refl ⟩
- ((1# - x) * x) + 1# ≈⟨ +-cong (-‿cong (*-cong (sym y≈1-x) refl)) refl ⟩
- (y * x) + 1# ≈⟨ +-cong (-‿cong (*-comm y x)) refl ⟩
- (x * y) + 1# ≈⟨ +-cong (-‿cong x*y≈1) refl ⟩
- 1# + 1# ≈⟨ -‿inverseˡ 1# ⟩
0#
where
open Solver
y≈1-x : y ≈ 1# - x
y≈1-x = begin
y ≈⟨ sym (+-identityʳ _) ⟩
y + 0# ≈⟨ +-cong refl (sym (-‿inverseʳ x)) ⟩
y + (x - x) ≈⟨ sym (+-assoc _ _ _) ⟩
(y + x) - x ≈⟨ +-cong (+-comm y x) refl ⟩
(x + y) - x ≈⟨ +-cong x+y≈1 refl ⟩
1# - x
x²-x+1≈0⇒x+y≈1∧xy≈1 : ∀ {x} → (x * x - x + 1# ≈ 0#) → ∃[ y ] ((x + y ≈ 1#) × (x * y ≈ 1#))
x²-x+1≈0⇒x+y≈1∧xy≈1 {x} x²-x+1≈0 = (y , (x+y≈1 , x*y≈1))
where
open Solver
y = 1# - x
x+y≈1 : x + y ≈ 1#
x+y≈1 = begin
x + y ≈⟨ refl ⟩
x + (1# - x) ≈⟨ +-cong refl (+-comm _ _) ⟩
x + (- x + 1#) ≈⟨ sym (+-assoc _ _ _) ⟩
(x - x) + 1# ≈⟨ +-cong (-‿inverseʳ _) refl ⟩
0# + 1# ≈⟨ +-identityˡ 1# ⟩
1#
x*y-1≈0 : x * y - 1# ≈ 0#
x*y-1≈0 = begin
x * y - 1# ≈⟨ refl ⟩
x * (1# - x) - 1# ≈⟨ +-cong (*-cong refl (+-cong (sym -1*-1≈1) (sym (-1*x≈-x x)))) refl ⟩
x * ((- 1#) * (- 1#) + (- 1#) * x) - 1# ≈⟨ solve 2 (\x m → x :* (m :* m :+ m :* x) :+ m := m :* (x :* x :+ m :* x :+ con 1)) refl x (- 1#) ⟩
(- 1#) * (x * x + (- 1#) * x + 1#) ≈⟨ *-cong refl (+-cong (+-cong (refl {x * x}) (-1*x≈-x x)) refl) ⟩
(- 1#) * (x * x - x + 1#) ≈⟨ -1*x≈-x _ ⟩
- (x * x - x + 1#) ≈⟨ -‿cong x²-x+1≈0 ⟩
- 0# ≈⟨ -0≈0 ⟩
0#
x*y≈1 : x * y ≈ 1#
x*y≈1 = x-y≈0⇒x≈y x*y-1≈0
-- 後で定義する _⊛_ の「発散しない場合」の定義
-- func x y = (xy - 1) / (x + y - 1)
func : (x y : Carrier) → (x+y#1 : x + y # 1#) → Carrier
func x y x+y#1 = (x * y - 1#) * proj₁ (#⇒invertible x+y#1)
func-cong
: ∀ {x₁ x₂ y₁ y₂} → (x₁+y₁#1 : x₁ + y₁ # 1#) → (x₂+y₂#1 : x₂ + y₂ # 1#)
→ x₁ ≈ x₂ → y₁ ≈ y₂
→ func x₁ y₁ x₁+y₁#1 ≈ func x₂ y₂ x₂+y₂#1
func-cong {x₁} {x₂} {y₁} {y₂} x₁+y₁#1 x₂+y₂#1 x₁≈x₂ y₁≈y₂ =
*-cong (+-cong (*-cong x₁≈x₂ y₁≈y₂) refl)
(unique-inverse (+-cong (+-cong x₁≈x₂ y₁≈y₂) refl) (#⇒invertible x₁+y₁#1) (#⇒invertible x₂+y₂#1))
func-comm : ∀ x y → (x+y#1 : x + y # 1#) → (y+x#1 : y + x # 1#) → func x y x+y#1 ≈ func y x y+x#1
func-comm x y x+y#1 y+x#1 = *-cong
(+-cong (*-comm x y) refl)
(unique-inverse (+-cong (+-comm x y) refl) (#⇒invertible x+y#1) (#⇒invertible y+x#1))
[x+y⊛z-1][y+z-1]≈xy+xz+yz-x-y-z
: ∀ x {y z} → (y+z#1 : y + z # 1#)
→ (x + func y z y+z#1 - 1#) * (y + z - 1#) ≈ x * y + x * z + y * z - x - y - z
[x+y⊛z-1][y+z-1]≈xy+xz+yz-x-y-z x {y} {z} y+z#1 =
begin
(x + (y * z - 1#) * proj₁ (#⇒invertible y+z#1) - 1#) * (y + z - 1#)
≈⟨ solve 5 (λ a b c d e → (a :+ b :* c :+ d) :* e := a :* e :+ b :* (c :* e) :+ d :* e) refl _ _ _ _ _ ⟩
x * (y + z - 1#) + (y * z - 1#) * (proj₁ (#⇒invertible y+z#1) * (y + z - 1#)) + (- 1#) * (y + z - 1#)
≈⟨ +-cong (+-cong refl (*-cong refl ((proj₁ (proj₂ (#⇒invertible y+z#1)))))) refl ⟩
x * (y + z - 1#) + (y * z - 1#) * 1# + (- 1#) * (y + z - 1#)
≈⟨ solve 4 (λ x y z m →
x :* (y :+ z :+ m) :+ (y :* z :+ m) :* con 1 :+ m :* (y :+ z :+ m)
:= x :* y :+ x :* z :+ y :* z :+ m :* x :+ m :* y :+ m :* z :+ (m :* m :+ m)
) refl x y z (- 1#) ⟩
x * y + x * z + y * z + (- 1#) * x + (- 1#) * y + (- 1#) * z + ((- 1#) * (- 1#) + (- 1#))
≈⟨ +-cong refl (+-cong -1*-1≈1 refl) ⟩
x * y + x * z + y * z + (- 1#) * x + (- 1#) * y + (- 1#) * z + (1# + (- 1#))
≈⟨ +-cong (+-cong (+-cong (+-cong refl (-1*x≈-x x)) (-1*x≈-x y)) (-1*x≈-x z)) (-‿inverseʳ 1#) ⟩
x * y + x * z + y * z - x - y - z + 0#
≈⟨ +-identityʳ _ ⟩
x * y + x * z + y * z - x - y - z
where
open Solver
[x⊛y+z-1][x+y-1]≈xy+xz+yz-x-y-z
: ∀ {x y} → (x+y#1 : x + y # 1#) → ∀ z
→ (func x y x+y#1 + z - 1#) * (x + y - 1#) ≈ x * y + x * z + y * z - x - y - z
[x⊛y+z-1][x+y-1]≈xy+xz+yz-x-y-z {x} {y} x+y#1 z =
begin
(func x y x+y#1 + z - 1#) * (x + y - 1#)
≈⟨ *-cong (+-cong (+-comm _ _) refl) refl ⟩
(z + func x y x+y#1 - 1#) * (x + y - 1#)
≈⟨ [x+y⊛z-1][y+z-1]≈xy+xz+yz-x-y-z z x+y#1 ⟩
z * x + z * y + x * y - z - x - y
≈⟨ solve 6 (λ x y z mx my mz →
z :* x :+ z :* y :+ x :* y :+ mz :+ mx :+ my
:=
x :* y :+ x :* z :+ y :* z :+ mx :+ my :+ mz
) refl x y z (- x) (- y) (- z) ⟩
x * y + x * z + y * z - x - y - z
where
open Solver
[[x⊛y]z-1][x+y-1#]≈xyz-x-y-z+1
: ∀ {x y} → (x+y#1 : x + y # 1#) → ∀ z
→ (func x y x+y#1 * z - 1#) * (x + y - 1#) ≈ x * y * z - x - y - z + 1#
[[x⊛y]z-1][x+y-1#]≈xyz-x-y-z+1 {x} {y} x+y#1 z =
begin
((x * y - 1#) * proj₁ (#⇒invertible x+y#1) * z - 1#) * (x + y - 1#)
≈⟨ solve 5 (λ p s s⁻¹ z c → (p :* s⁻¹ :* z :+ c) :* s := p :* (s⁻¹ :* s) :* z :+ c :* s)
refl
(x * y - 1#) (x + y - 1#) (proj₁ (#⇒invertible x+y#1)) z (- 1#) ⟩
((x * y - 1#) * (proj₁ (#⇒invertible x+y#1) * (x + y - 1#)) * z + (- 1#) * (x + y - 1#))
≈⟨ +-cong (*-cong (*-cong refl (proj₁ (proj₂ (#⇒invertible x+y#1)))) refl) refl ⟩
((x * y - 1#) * 1# * z + (- 1#) * (x + y - 1#))
≈⟨ solve 4 (λ x y z m → ((x :* y :+ m) :* con 1 :* z :+ m :* (x :+ y :+ m)) := x :* y :* z :+ m :* x :+ m :* y :+ m :* z :+ m :* m)
refl x y z (- 1#) ⟩
x * y * z + (- 1#) * x + (- 1#) * y + (- 1#) * z + (- 1#) * (- 1#)
≈⟨ +-cong (+-cong (+-cong (+-cong refl (-1*x≈-x x)) (-1*x≈-x y)) (-1*x≈-x z)) -1*-1≈1 ⟩
x * y * z - x - y - z + 1#
where
open Solver
[x[y⊛z]-1][y+z-1]≈xyz-x-y-z+1
: ∀ x {y z} → (y+z#1 : y + z # 1#)
→ (x * func y z y+z#1 - 1#) * (y + z - 1#) ≈ x * y * z - x - y - z + 1#
[x[y⊛z]-1][y+z-1]≈xyz-x-y-z+1 x {y} {z} y+z#1 =
begin
(x * func y z y+z#1 - 1#) * (y + z - 1#)
≈⟨ *-cong (+-cong (*-comm _ _) refl) refl ⟩
((func y z y+z#1 * x - 1#) * (y + z - 1#))
≈⟨ [[x⊛y]z-1][x+y-1#]≈xyz-x-y-z+1 y+z#1 x ⟩
y * z * x - y - z - x + 1#
≈⟨ solve 6 (λ x y z mx my mz → y :* z :* x :+ my :+ mz :+ mx :+ con 1 := x :* y :* z :+ mx :+ my :+ mz :+ con 1) refl x y z (- x) (- y) (- z) ⟩
x * y * z - x - y - z + 1#
where
open Solver
func-assoc
: ∀ x y z
→ (x+y#1 : (x + y # 1#))
→ (y+z#1 : (y + z # 1#))
→ (x⊛y+z#1 : func x y x+y#1 + z # 1#)
→ (x+y⊛z#1 : x + func y z y+z#1 # 1#)
→ func (func x y x+y#1) z x⊛y+z#1 ≈ func x (func y z y+z#1) x+y⊛z#1
func-assoc x y z x+y#1 y+z#1 x⊛y+z#1 x+y⊛z#1 = invert-both lem (#⇒invertible x+y⊛z#1) (#⇒invertible x⊛y+z#1)
where
open Solver
lem : (func x y x+y#1 * z - 1#) * (x + func y z y+z#1 - 1#) ≈ (x * func y z y+z#1 - 1#) * (func x y x+y#1 + z - 1#)
lem = *-cancelʳ (y + z - 1#) (#⇒invertible y+z#1) $ *-cancelʳ (x + y - 1#) (#⇒invertible x+y#1) $
begin
(func x y x+y#1 * z - 1#) * (x + func y z y+z#1 - 1#) * (y + z - 1#) * (x + y - 1#)
≈⟨ solve 4 (λ a b c d → a :* b :* c :* d := (a :* d) :* (b :* c)) refl _ _ _ _ ⟩
(func x y x+y#1 * z - 1#) * (x + y - 1#) * ((x + func y z y+z#1 - 1#) * (y + z - 1#))
≈⟨ *-cong ([[x⊛y]z-1][x+y-1#]≈xyz-x-y-z+1 x+y#1 z) ([x+y⊛z-1][y+z-1]≈xy+xz+yz-x-y-z x y+z#1) ⟩
(x * y * z - x - y - z + 1#) * (x * y + x * z + y * z - x - y - z)
≈⟨ *-cong (sym ([x[y⊛z]-1][y+z-1]≈xyz-x-y-z+1 x y+z#1)) (sym ([x⊛y+z-1][x+y-1]≈xy+xz+yz-x-y-z x+y#1 z)) ⟩
(x * func y z y+z#1 - 1#) * (y + z - 1#) * ((func x y x+y#1 + z - 1#) * (x + y - 1#))
≈⟨ solve 4 (λ a b c d → (a :* c) :* (b :* d) := a :* b :* c :* d) refl _ _ _ _ ⟩
(x * func y z y+z#1 - 1#) * (func x y x+y#1 + z - 1#) * (y + z - 1#) * (x + y - 1#)
lemma-1 : ∀ {x y z} → (x+y#1 : x + y # 1#) → ¬ (y + z # 1#) → ¬ (func x y x+y#1 + z # 1#) → ((y + z ≈ 1#) × (y * z ≈ 1#))
lemma-1 {x} {y} {z} x+y#1 ¬y+z#1 ¬x⊛y+z#1 = (y+z≈1 , y*z≈1)
where
open Solver
y+z≈1 : y + z ≈ 1#
y+z≈1 = proj₁ (tight _ _) ¬y+z#1
x⊛y+z≈1 : func x y x+y#1 + z ≈ 1#
x⊛y+z≈1 = proj₁ (tight _ _) ¬x⊛y+z#1
lem1 : (x * y - 1#) + z * (x + y - 1#) ≈ x + y - 1#
lem1 =
begin
(x * y - 1#) + z * (x + y - 1#)
≈⟨ +-cong (sym (*-identityʳ _)) refl ⟩
(x * y - 1#) * 1# + z * (x + y - 1#)
≈⟨ +-cong (*-cong refl (sym (proj₁ (proj₂ (#⇒invertible x+y#1))))) refl ⟩
(x * y - 1#) * (proj₁ (#⇒invertible x+y#1) * (x + y - 1#)) + z * (x + y - 1#)
≈⟨ +-cong (sym (*-assoc _ _ _)) refl ⟩
(x * y - 1#) * proj₁ (#⇒invertible x+y#1) * (x + y - 1#) + z * (x + y - 1#)
≈⟨ refl ⟩
func x y x+y#1 * (x + y - 1#) + z * (x + y - 1#)
≈⟨ sym (distribʳ (x + y - 1#) _ _) ⟩
(func x y x+y#1 + z) * (x + y - 1#)
≈⟨ *-cong x⊛y+z≈1 refl ⟩
1# * (x + y - 1#)
≈⟨ *-identityˡ _ ⟩
x + y - 1#
lem2 : (x * y - 1#) + z * (x + y - 1#) - (x + y - 1#) ≈ 0#
lem2 = x≈y⇒x-y≈0 lem1
lem3 : (x * y - 1#) + z * (x + y - 1#) - (x + y - 1#) ≈ y * z - 1#
lem3 =
begin
(x * y - 1#) + z * (x + y - 1#) - (x + y - 1#)
≈⟨ refl ⟩
(x * y + (- 1#)) + z * (x + y + (- 1#)) - (x + y + (- 1#))
≈⟨ +-cong refl (sym (-1*x≈-x _)) ⟩
(x * y + (- 1#)) + z * (x + y + (- 1#)) + (- 1#) * (x + y + (- 1#))
≈⟨ solve 4 (λ x y z m →
(x :* y :+ m) :+ z :* (x :+ y :+ m) :+ m :* (x :+ y :+ m)
:= y :* z :+ m :+ ((x :+ m) :* (y :+ z) :+ m :* x :+ m :* m))
refl x y z (- 1#) ⟩
y * z + (- 1#) + ((x - 1#) * (y + z) + (- 1#) * x + (- 1#) * (- 1#))
≈⟨ +-cong refl (+-cong (+-cong (*-cong refl y+z≈1) refl) -1*-1≈1) ⟩
y * z - 1# + ((x - 1#) * 1# + (- 1#) * x + 1#)
≈⟨ solve 4 (λ x y z m → y :* z :+ m :+ ((x :+ m) :* con 1 :+ m :* x :+ con 1) := y :* z :+ m :+ (x :+ m :* x) :+ (con 1 :+ m)) refl x y z (- 1#) ⟩
y * z - 1# + (x + (- 1#) * x) + (1# - 1#)
≈⟨ +-cong (+-cong refl (+-cong refl (-1*x≈-x x))) refl ⟩
y * z - 1# + (x - x) + (1# - 1#)
≈⟨ +-cong (+-cong refl (-‿inverseʳ _)) (-‿inverseʳ _) ⟩
y * z - 1# + 0# + 0#
≈⟨ +-identityʳ _ ⟩
y * z - 1# + 0#
≈⟨ +-identityʳ _ ⟩
y * z - 1#
lem4 : y * z - 1# ≈ 0#
lem4 = trans (sym lem3) lem2
y*z≈1 : y * z ≈ 1#
y*z≈1 = x-y≈0⇒x≈y lem4
lemma-2 : ∀ {x y z} → (x+y#1 : x + y # 1#) → ¬ (y + z # 1#) → (x⊛y+z#1 : func x y x+y#1 + z # 1#) → func (func x y x+y#1) z x⊛y+z#1 ≈ x
lemma-2 {x} {y} {z} x+y#1 ¬y+z#1 x⊛y+z#1 =
*-cancelʳ (func x y x+y#1 + z - 1#) (#⇒invertible x⊛y+z#1) $
*-cancelʳ (x + y - 1#) (#⇒invertible x+y#1) $ lem2
where
open Solver
y+z≈1 : y + z ≈ 1#
y+z≈1 = proj₁ (tight _ _) ¬y+z#1
[x⊛y+z-1][x+y-1]≈yz-1 : (func x y x+y#1 + z - 1#) * (x + y - 1#) ≈ y * z - 1#
[x⊛y+z-1][x+y-1]≈yz-1 =
begin
(func x y x+y#1 + z - 1#) * (x + y - 1#)
≈⟨ [x⊛y+z-1][x+y-1]≈xy+xz+yz-x-y-z x+y#1 z ⟩
x * y + x * z + y * z - x - y - z
≈⟨ sym (+-cong (+-cong (+-cong refl (-1*x≈-x x)) (-1*x≈-x y)) (-1*x≈-x z)) ⟩
x * y + x * z + y * z + (- 1#) * x + (- 1#) * y + (- 1#) * z
≈⟨ solve 4 (λ x y z m → x :* y :+ x :* z :+ y :* z :+ m :* x :+ m :* y :+ m :* z := y :* z :+ m :* (y :+ z) :+ (x :* (y :+ z) :+ m :* x)) refl x y z (- 1#) ⟩
y * z + (- 1#) * (y + z) + (x * (y + z) + (- 1#) * x)
≈⟨ +-cong (+-cong refl (*-cong refl y+z≈1)) (+-cong (*-cong refl y+z≈1) (-1*x≈-x x)) ⟩
y * z + (- 1#) * 1# + (x * 1# - x)
≈⟨ +-cong refl (+-cong (*-identityʳ x) refl) ⟩
y * z + (- 1#) * 1# + (x - x)
≈⟨ +-cong refl (-‿inverseʳ x) ⟩
y * z + (- 1#) * 1# + 0#
≈⟨ +-identityʳ _ ⟩
y * z + (- 1#) * 1#
≈⟨ +-cong refl (-1*x≈-x 1#) ⟩
y * z - 1#
lem1 : 1# + (- 1#) * (y + z) ≈ 0#
lem1 =
begin
1# + (- 1#) * (y + z)
≈⟨ +-cong refl (*-cong refl y+z≈1) ⟩
1# + (- 1#) * 1#
≈⟨ +-cong refl (-1*x≈-x 1#) ⟩
1# - 1#
≈⟨ -‿inverseʳ 1# ⟩
0#
lem2 : func (func x y x+y#1) z x⊛y+z#1 * (func x y x+y#1 + z - 1#) * (x + y - 1#) ≈ x * (func x y x+y#1 + z - 1#) * (x + y - 1#)
lem2 =
begin
func (func x y x+y#1) z x⊛y+z#1 * (func x y x+y#1 + z - 1#) * (x + y - 1#)
≈⟨ refl ⟩
(func x y x+y#1 * z - 1#) * proj₁ (#⇒invertible x⊛y+z#1) * (func x y x+y#1 + z - 1#) * (x + y - 1#)
≈⟨ *-cong (*-assoc _ _ _) refl ⟩
(func x y x+y#1 * z - 1#) * (proj₁ (#⇒invertible x⊛y+z#1) * (func x y x+y#1 + z - 1#)) * (x + y - 1#)
≈⟨ *-cong (*-cong refl (proj₁ (proj₂ (#⇒invertible x⊛y+z#1)))) refl ⟩
(func x y x+y#1 * z - 1#) * 1# * (x + y - 1#)
≈⟨ *-cong (*-identityʳ _) refl ⟩
(func x y x+y#1 * z - 1#) * (x + y - 1#)
≈⟨ [[x⊛y]z-1][x+y-1#]≈xyz-x-y-z+1 x+y#1 z ⟩
x * y * z - x - y - z + 1#
≈⟨ +-cong (+-cong (+-cong (+-cong refl (sym (-1*x≈-x x))) (sym (-1*x≈-x y))) (sym (-1*x≈-x z))) refl ⟩
x * y * z + (- 1#) * x + (- 1#) * y + (- 1#) * z + 1#
≈⟨ solve 4 (λ x y z m → x :* y :* z :+ m :* x :+ m :* y :+ m :* z :+ con 1 := x :* (y :* z :+ m) :+ (con 1 :+ m :* (y :+ z))) refl x y z (- 1#) ⟩
x * (y * z - 1#) + (1# + (- 1#) * (y + z))
≈⟨ +-cong refl lem1 ⟩
x * (y * z - 1#) + 0#
≈⟨ +-identityʳ _ ⟩
x * (y * z - 1#)
≈⟨ *-cong refl (sym [x⊛y+z-1][x+y-1]≈yz-1) ⟩
x * ((func x y x+y#1 + z - 1#) * (x + y - 1#))
≈⟨ sym (*-assoc _ _ _) ⟩
x * (func x y x+y#1 + z - 1#) * (x + y - 1#)
lemma-3
: ∀ x y z → (x+y#1 : x + y # 1#)
→ func x y x+y#1 + z ≈ 1#
→ x * y + x * z + y * z - x - y - z ≈ 0#
lemma-3 x y z x+y#1 x⊛y+z≈1 =
begin
x * y + x * z + y * z - x - y - z
≈⟨ sym ([x⊛y+z-1][x+y-1]≈xy+xz+yz-x-y-z x+y#1 z) ⟩
(func x y x+y#1 + z - 1#) * (x + y - 1#)
≈⟨ *-cong (x≈y⇒x-y≈0 x⊛y+z≈1) refl ⟩
0# * (x + y - 1#)
≈⟨ zeroˡ _ ⟩
0#
lemma-3'
: ∀ x y z → (y+z#1 : y + z # 1#)
→ x + func y z y+z#1 ≈ 1#
→ x * y + x * z + y * z - x - y - z ≈ 0#
lemma-3' x y z y+z#1 x+y⊛z≈1 =
begin
x * y + x * z + y * z - x - y - z
≈⟨ sym ([x+y⊛z-1][y+z-1]≈xy+xz+yz-x-y-z x y+z#1) ⟩
(x + func y z y+z#1 - 1#) * (y + z - 1#)
≈⟨ *-cong (x≈y⇒x-y≈0 x+y⊛z≈1) refl ⟩
0# * (y + z - 1#)
≈⟨ zeroˡ _ ⟩
0#
lemma-4
: ∀ x y z → (x+y#1 : x + y # 1#)
→ x * y + x * z + y * z - x - y - z ≈ 0#
→ func x y x+y#1 + z ≈ 1#
lemma-4 x y z x+y#1 xy+xz+yz-x-y-z≈0 = x-y≈0⇒x≈y $
begin
func x y x+y#1 + z - 1#
≈⟨ sym (*-identityʳ _) ⟩
(func x y x+y#1 + z - 1#) * 1#
≈⟨ *-cong refl (sym (proj₂ (proj₂ (#⇒invertible x+y#1)))) ⟩
(func x y x+y#1 + z - 1#) * ((x + y - 1#) * proj₁ (#⇒invertible x+y#1))
≈⟨ sym (*-assoc _ _ _) ⟩
(func x y x+y#1 + z - 1#) * (x + y - 1#) * proj₁ (#⇒invertible x+y#1)
≈⟨ *-cong ([x⊛y+z-1][x+y-1]≈xy+xz+yz-x-y-z x+y#1 z) refl ⟩
(x * y + x * z + y * z - x - y - z) * proj₁ (#⇒invertible x+y#1)
≈⟨ *-cong xy+xz+yz-x-y-z≈0 refl ⟩
0# * proj₁ (#⇒invertible x+y#1)
≈⟨ zeroˡ _ ⟩
0#
lemma-4'
: ∀ x y z → (y+z#1 : y + z # 1#)
→ x * y + x * z + y * z - x - y - z ≈ 0#
→ x + func y z y+z#1 ≈ 1#
lemma-4' x y z y+z#1 xy+xz+yz-x-y-z≈0 = x-y≈0⇒x≈y $
begin
x + func y z y+z#1 - 1#
≈⟨ sym (*-identityʳ _) ⟩
(x + func y z y+z#1 - 1#) * 1#
≈⟨ *-cong refl (sym (proj₂ (proj₂ (#⇒invertible y+z#1)))) ⟩
(x + func y z y+z#1 - 1#) * ((y + z - 1#) * proj₁ (#⇒invertible y+z#1))
≈⟨ sym (*-assoc _ _ _) ⟩
(x + func y z y+z#1 - 1#) * (y + z - 1#) * proj₁ (#⇒invertible y+z#1)
≈⟨ *-cong ([x+y⊛z-1][y+z-1]≈xy+xz+yz-x-y-z x y+z#1) refl ⟩
(x * y + x * z + y * z - x - y - z) * proj₁ (#⇒invertible y+z#1)
≈⟨ *-cong xy+xz+yz-x-y-z≈0 refl ⟩
0# * proj₁ (#⇒invertible y+z#1)
≈⟨ zeroˡ _ ⟩
0#
open Utils
open HeytingField HF
renaming
( Carrier to F
; _≈_ to _≈F_
; isEquivalence to F-isEquivalence
; setoid to F-setoid
)
open IsEquivalence F-isEquivalence
renaming
( refl to F-refl
; sym to F-sym
; trans to F-trans
)
open import Algebra.Apartness.Properties.HeytingCommutativeRing (heytingCommutativeRing)
module F-Solver = Algebra.Solver.Ring.NaturalCoefficients.Default
(CommutativeRing.commutativeSemiring (HeytingCommutativeRing.commutativeRing heytingCommutativeRing))
data E : Set c where
fin : F → E
∞ : E
infix 4 _≈_
data _≈_ : Rel E (c ⊔ ℓ₁) where
∞≈∞ : ∞ ≈ ∞
fin-cong : {x y : F} → x ≈F y → fin x ≈ fin y
≈-refl : Reflexive _≈_
≈-refl {∞} = ∞≈∞
≈-refl {fin x} = fin-cong F-refl
≈-sym : Symmetric _≈_
≈-sym ∞≈∞ = ∞≈∞
≈-sym (fin-cong x≈y) = fin-cong (F-sym x≈y)
≈-trans : Transitive _≈_
≈-trans ∞≈∞ ∞≈∞ = ∞≈∞
≈-trans (fin-cong x≈y) (fin-cong y≈z) = fin-cong (F-trans x≈y y≈z)
≈-isEquivalence : IsEquivalence (_≈_)
≈-isEquivalence = record
{ refl = ≈-refl
; sym = ≈-sym
; trans = ≈-trans
}
setoid : Setoid c (c ⊔ ℓ₁)
setoid = record
{ Carrier = E
; _≈_ = _≈_
; isEquivalence = ≈-isEquivalence
}
infixl 7 _⊛_
-- x ⊛ y = (xy - 1) / (x + y - 1)
_⊛_ : E → E → E
∞ ⊛ y = y
x ⊛ ∞ = x
fin x ⊛ fin y with #-dec (x + y) 1#
... | yes x+y#1 = fin (func x y x+y#1)
... | no _ = ∞
⊛-identityˡ : LeftIdentity (_≈_) ∞ _⊛_
⊛-identityˡ x = ≈-refl
⊛-identityʳ : RightIdentity (_≈_) ∞ _⊛_
⊛-identityʳ ∞ = ≈-refl
⊛-identityʳ (fin x) = ≈-refl
⊛-comm : Commutative (_≈_) _⊛_
⊛-comm ∞ y = begin
∞ ⊛ y ≈⟨ ⊛-identityˡ y ⟩
y ≈⟨ ≈-sym (⊛-identityʳ y) ⟩
y ⊛ ∞
where open ≈-Reasoning setoid
⊛-comm x ∞ = begin
x ⊛ ∞ ≈⟨ ⊛-identityʳ x ⟩
x ≈⟨ ≈-sym (⊛-identityˡ x) ⟩
∞ ⊛ x
where open ≈-Reasoning setoid
⊛-comm (fin x) (fin y) with #-dec (x + y) 1# | #-dec (y + x) 1#
... | yes x+y#1 | yes y+x#1 = fin-cong $ func-comm x y x+y#1 y+x#1
... | yes x+y#1 | no ¬y+x#1 = ⊥-elim (¬y+x#1 (#-congʳ (+-comm x y) x+y#1))
... | no ¬x+y#1 | yes y+x#1 = ⊥-elim (¬x+y#1 (#-congʳ (+-comm y x) y+x#1))
... | no ¬x+y#1 | no ¬y+x#1 = ∞≈∞
⊛-cong : Congruent₂ (_≈_) _⊛_
⊛-cong ∞≈∞ y₁≈y₂ = y₁≈y₂
⊛-cong {x₁} {x₂} x₁≈x₂ ∞≈∞ = begin
x₁ ⊛ ∞ ≈⟨ ⊛-identityʳ x₁ ⟩
x₁ ≈⟨ x₁≈x₂ ⟩
x₂ ≈⟨ ≈-sym (⊛-identityʳ x₂) ⟩
x₂ ⊛ ∞
where open ≈-Reasoning setoid
⊛-cong (fin-cong {x₁} {x₂} x₁≈x₂) (fin-cong {y₁} {y₂} y₁≈y₂) with #-dec (x₁ + y₁) 1# | #-dec (x₂ + y₂) 1#
... | yes x₁+y₁#1 | yes x₂+y₂#1 = fin-cong $ *-cong
(+-cong (*-cong x₁≈x₂ y₁≈y₂) F-refl)
(unique-inverse r (#⇒invertible x₁+y₁#1) ((#⇒invertible x₂+y₂#1)))
where
r : (x₁ + y₁) - 1# ≈F (x₂ + y₂) - 1#
r = +-cong (+-cong x₁≈x₂ y₁≈y₂) F-refl
... | yes x₁+y₁#1 | no ¬x₂+y₂#1 = ⊥-elim (¬x₂+y₂#1 (#-congʳ (+-cong x₁≈x₂ y₁≈y₂) x₁+y₁#1))
... | no ¬x₁+y₁#1 | yes x₂+y₂#1 = ⊥-elim (¬x₁+y₁#1 (#-congʳ (+-cong (F-sym x₁≈x₂) (F-sym y₁≈y₂)) x₂+y₂#1))
... | no ¬x₁+y₁#1 | no ¬x₂+y₂#1 = ∞≈∞
isMagma : IsMagma _≈_ _⊛_
isMagma = record
{ isEquivalence = ≈-isEquivalence
; ∙-cong = ⊛-cong
}
_⁻¹ : E → E
∞ ⁻¹ = ∞
(fin x) ⁻¹ = fin (1# - x)
isLeftInverse : LeftInverse _≈_ ∞ (_⁻¹) _⊛_
isLeftInverse ∞ = ∞≈∞
isLeftInverse (fin x) with #-dec ((1# - x) + x) 1#
... | yes 1-x+x#1 = ⊥-elim (lem3 lem2)
where
lem1 : 1# - x + x ≈F 1#
lem1 = begin
(1# - x) + x ≈⟨ +-assoc 1# (- x) x ⟩
1# + (- x + x) ≈⟨ +-cong F-refl (-‿inverseˡ x) ⟩
1# + 0# ≈⟨ +-identityʳ 1# ⟩
1#
where open ≈-Reasoning F-setoid
lem2 : 1# # 1#
lem2 = #-congʳ lem1 1-x+x#1
lem3 : ¬ (1# # 1#)
lem3 = proj₂ (tight 1# 1#) F-refl
... | no ¬1-x+x#1 = ∞≈∞
isRightInverse : RightInverse _≈_ ∞ (_⁻¹) _⊛_
isRightInverse x = begin
x ⊛ (x ⁻¹) ≈⟨ ⊛-comm x (x ⁻¹) ⟩
(x ⁻¹) ⊛ x ≈⟨ isLeftInverse x ⟩
where open ≈-Reasoning setoid
⁻¹-cong : Congruent₁ _≈_ _⁻¹
⁻¹-cong {.∞} {.∞} (∞≈∞) = ∞≈∞
⁻¹-cong {.fin x} {.fin y} (fin-cong {x} {y} x≈y) = fin-cong (+-cong F-refl (-‿cong x≈y))
module Main (condition : ∀ {x y} → ¬ ((x + y ≈F 1#) × (x * y ≈F 1#))) where
⊛-fin-assoc : (x y z : F) → (fin x ⊛ fin y) ⊛ fin z ≈ fin x ⊛ (fin y ⊛ fin z)
⊛-fin-assoc x y z with #-dec (x + y) 1# | #-dec (y + z) 1#
⊛-fin-assoc x y z | yes x+y#1 | yes y+z#1 with #-dec (func x y x+y#1 + z) 1# | #-dec (x + func y z y+z#1) 1#
⊛-fin-assoc x y z | yes x+y#1 | yes y+z#1 | yes x⊛y+z#1 | yes x+y⊛z#1 = fin-cong (func-assoc x y z x+y#1 y+z#1 x⊛y+z#1 x+y⊛z#1)
⊛-fin-assoc x y z | yes x+y#1 | yes y+z#1 | yes x⊛y+z#1 | no ¬x+y⊛z#1 = ⊥-elim ((¬x⊛y+z#1 x⊛y+z#1))
where
tmp : x * y + x * z + y * z - x - y - z ≈F 0#
tmp = lemma-3' x y z y+z#1 (proj₁ (tight _ _) (¬x+y⊛z#1))
x⊛y+z≈1 : func x y x+y#1 + z ≈F 1#
x⊛y+z≈1 = lemma-4 x y z x+y#1 tmp
¬x⊛y+z#1 : ¬ (func x y x+y#1 + z # 1#)
¬x⊛y+z#1 = proj₂ (tight _ _) x⊛y+z≈1
⊛-fin-assoc x y z | yes x+y#1 | yes y+z#1 | no ¬x⊛y+z#1 | yes x+y⊛z#1 = ⊥-elim (¬x+y⊛z#1 x+y⊛z#1)
where
tmp : x * y + x * z + y * z - x - y - z ≈F 0#
tmp = lemma-3 x y z x+y#1 (proj₁ (tight _ _) (¬x⊛y+z#1))
x+y⊛z≈1 : x + func y z y+z#1 ≈F 1#
x+y⊛z≈1 = lemma-4' x y z y+z#1 tmp
¬x+y⊛z#1 : ¬ (x + func y z y+z#1 # 1#)
¬x+y⊛z#1 = proj₂ (tight _ _) x+y⊛z≈1
⊛-fin-assoc x y z | yes x+y#1 | yes y+z#1 | no ¬x⊛y+z#1 | no ¬x+y⊛z#1 = ∞≈∞
⊛-fin-assoc x y z | yes x+y#1 | no ¬y+z#1 with #-dec (func x y x+y#1 + z) 1#
⊛-fin-assoc x y z | yes x+y#1 | no ¬y+z#1 | yes x⊛y+z#1 = fin-cong (lemma-2 x+y#1 ¬y+z#1 x⊛y+z#1)
⊛-fin-assoc x y z | yes x+y#1 | no ¬y+z#1 | no ¬x⊛y+z#1 = ⊥-elim (condition (lemma-1 x+y#1 ¬y+z#1 ¬x⊛y+z#1))
⊛-fin-assoc x y z | no ¬x+y#1 | yes y+z#1 with #-dec (x + func y z y+z#1) 1#
⊛-fin-assoc x y z | no ¬x+y#1 | yes y+z#1 | yes x+y⊛z#1 = fin-cong (F-sym lem)
where
open ≈-Reasoning F-setoid
z+y#1 : z + y # 1#
z+y#1 = #-congʳ (+-comm _ _) y+z#1
¬y+x#1 : ¬ (y + x # 1#)
¬y+x#1 y+x#1 = ¬x+y#1 (#-congʳ (+-comm _ _) y+x#1)
y⊛z+x#1 : func y z y+z#1 + x # 1#
y⊛z+x#1 = #-congʳ (+-comm _ _) x+y⊛z#1
z⊛y+x#1 : func z y z+y#1 + x # 1#
z⊛y+x#1 = #-congʳ (+-cong (func-comm y z y+z#1 z+y#1) (refl {x})) y⊛z+x#1
lem : func x (func y z y+z#1) x+y⊛z#1 ≈F z
lem = begin
func x (func y z y+z#1) x+y⊛z#1 ≈⟨ func-comm x ((func y z y+z#1)) x+y⊛z#1 y⊛z+x#1 ⟩
func (func y z y+z#1) x y⊛z+x#1 ≈⟨ func-cong y⊛z+x#1 z⊛y+x#1 (func-comm y z y+z#1 z+y#1) refl ⟩
func (func z y z+y#1) x z⊛y+x#1 ≈⟨ lemma-2 z+y#1 ¬y+x#1 z⊛y+x#1 ⟩
z
⊛-fin-assoc x y z | no ¬x+y#1 | yes y+z#1 | no ¬x+y⊛z#1 = ⊥-elim (condition (lemma-1 z+y#1 ¬y+x#1 ¬z⊛y+x#1))
where
open ≈-Reasoning F-setoid
z+y#1 : z + y # 1#
z+y#1 = #-congʳ (+-comm _ _) y+z#1
¬y+x#1 : ¬ (y + x # 1#)
¬y+x#1 y+x#1 = ¬x+y#1 (#-congʳ (+-comm _ _) y+x#1)
z⊛y+x≈x+y⊛z : func z y z+y#1 + x ≈F x + func y z y+z#1
z⊛y+x≈x+y⊛z = begin
func z y z+y#1 + x ≈⟨ +-comm (func z y z+y#1) x ⟩
x + func z y z+y#1 ≈⟨ +-cong (refl {x}) (func-comm z y z+y#1 y+z#1) ⟩
x + func y z y+z#1
¬z⊛y+x#1 : ¬ (func z y z+y#1 + x # 1#)
¬z⊛y+x#1 z⊛y+x#1 = ¬x+y⊛z#1 (#-congʳ z⊛y+x≈x+y⊛z z⊛y+x#1)
⊛-fin-assoc x y z | no ¬x+y#1 | no ¬y+z#1 = fin-cong z≈x
where
open ≈-Reasoning F-setoid
y+z≈y+x : y + z ≈F y + x
y+z≈y+x = begin
y + z ≈⟨ proj₁ (tight _ _) ¬y+z#1 ⟩
1# ≈⟨ F-sym (proj₁ (tight _ _) ¬x+y#1 ) ⟩
x + y ≈⟨ +-comm x y ⟩
y + x
z≈x : z ≈F x
z≈x = begin
z ≈⟨ F-sym (+-identityˡ z) ⟩
0# + z ≈⟨ +-cong (F-sym (-‿inverseˡ y)) F-refl ⟩
(- y + y) + z ≈⟨ +-assoc (- y) y z ⟩
- y + (y + z) ≈⟨ +-cong F-refl y+z≈y+x ⟩
- y + (y + x) ≈⟨ F-sym (+-assoc (- y) y x) ⟩
(- y + y) + x ≈⟨ +-cong (-‿inverseˡ y) F-refl ⟩
0# + x ≈⟨ +-identityˡ x ⟩
x
⊛-assoc : Associative _≈_ _⊛_
⊛-assoc ∞ y z = ≈-refl
⊛-assoc x ∞ z = ⊛-cong (⊛-identityʳ x) ≈-refl
⊛-assoc x y ∞ = begin
((x ⊛ y) ⊛ ∞) ≈⟨ ⊛-identityʳ (x ⊛ y) ⟩
x ⊛ y ≈⟨ ⊛-cong (≈-refl {x}) (≈-sym (⊛-identityʳ y)) ⟩
x ⊛ (y ⊛ ∞)
where open ≈-Reasoning setoid
⊛-assoc (fin x) (fin y) (fin z) = ⊛-fin-assoc x y z
isSemigroup : IsSemigroup _≈_ _⊛_
isSemigroup = record
{ isMagma = isMagma
; assoc = ⊛-assoc
}
isMonoid : IsMonoid _≈_ _⊛_ ∞
isMonoid = record
{ isSemigroup = isSemigroup
; identity = (⊛-identityˡ , ⊛-identityʳ)
}
isGroup : IsGroup _≈_ _⊛_ ∞ (_⁻¹)
isGroup = record
{ isMonoid = isMonoid
; inverse = (isLeftInverse , isRightInverse)
; ⁻¹-cong = ⁻¹-cong
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment