lol.agda

module Chapter2 where

open import Agda.Builtin.FromNat
open import Data.Nat using (ℕ; zero; suc)
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.Core using (Decidable)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- postulate
  -- trustMe : ∀ {A : Set} {x y : A} -> x ≡ y

negsym : ∀ {A : Set} {x y : A} -> x ≢ y -> y ≢ x
negsym x≢y = λ x≡y → x≢y (sym x≡y)

Op : Set -> Set
Op A = A -> A

Op₂ : Set -> Set
Op₂ A = A -> A -> A

record Identity {A : Set} (_·_ : Op₂ A) (e : A) : Set where
  field
    left-identity : ∀ (x : A) -> e · x ≡ x
    right-identity : ∀ (x : A) -> x · e ≡ x

uniquness-of-identities : ∀ {A : Set} {_·_ : Op₂ A} {e f : A} -> Identity _·_ e -> Identity _·_ f -> e ≡ f
uniquness-of-identities {A} {_·_} {e} {f} identity1 identity2 =
  e ≡⟨ sym (right-identity identity2 e) ⟩
  e · f ≡⟨ left-identity identity1 f ⟩
  f ∎
  where open Identity

record Inverse {A : Set} (_·_ : Op₂ A) (P : A -> Set) (_⁻¹ : ∃ P -> ∃ P) (e : A) : Set where
  field
    left-inverse : ∀ (x : ∃ P) -> proj₁ x · proj₁ (x ⁻¹) ≡ e
    right-inverse : ∀ (x : ∃ P) -> proj₁ (x ⁻¹) · proj₁ x ≡ e

Associative : ∀ {A : Set} (_·_ : Op₂ A) -> Set
Associative {A} _·_ = (a b c : A) -> a · (b · c) ≡ (a · b) · c

module Inverse-Theorems
  {A : Set} {_·_ : Op₂ A} {P : A -> Set} {_⁻¹ : ∃ P -> ∃ P} {e : A}
  (assoc : Associative _·_) (identity : Identity _·_ e) (inverse : Inverse _·_ P _⁻¹ e)
  where
  open Identity identity
  open Inverse inverse

  double-inverse : ∀ (x : ∃ P) -> proj₁ ((x ⁻¹) ⁻¹) ≡ proj₁ x
  double-inverse x =
    proj₁ ((x ⁻¹) ⁻¹) ≡⟨ sym (right-identity _) ⟩
    proj₁ ((x ⁻¹) ⁻¹) · e ≡⟨ cong (λ t → _ · t) (sym (right-inverse _)) ⟩
    proj₁ ((x ⁻¹) ⁻¹) · (proj₁ (x ⁻¹) · proj₁ x) ≡⟨ assoc _ _ _ ⟩
    (proj₁ ((x ⁻¹) ⁻¹) · proj₁ (x ⁻¹)) · proj₁ x ≡⟨ cong (λ t → t · _) (right-inverse _) ⟩
    e · proj₁ x ≡⟨ left-identity _ ⟩
    proj₁ x ∎

  right-cancellation : ∀ (x y : A) (v : ∃ P) -> x · proj₁ v ≡ y · proj₁ v -> x ≡ y
  right-cancellation x y v x·v≡y·v =
    x ≡⟨ sym (right-identity _) ⟩
    x · e ≡⟨ cong (λ t → _ · t) (sym (left-inverse _)) ⟩
    x · (proj₁ v · proj₁ (v ⁻¹)) ≡⟨ assoc _ _ _ ⟩
    (x · proj₁ v) · proj₁ (v ⁻¹) ≡⟨ cong (λ t → t · _) x·v≡y·v ⟩
    (y · proj₁ v) · proj₁ (v ⁻¹) ≡⟨ sym (assoc _ _ _) ⟩
    y · (proj₁ v · proj₁ (v ⁻¹)) ≡⟨ cong (λ t → _ · t) (left-inverse _) ⟩
    y · e ≡⟨ right-identity _ ⟩
    y ∎

  left-cancellation : ∀ (x y : A) (v : ∃ P) -> proj₁ v · x ≡ proj₁ v · y -> x ≡ y
  left-cancellation x y v v·x≡v·y =
    x ≡⟨ sym (left-identity _) ⟩
    e · x ≡⟨ cong (λ t → t · _) (sym (right-inverse _)) ⟩
    (proj₁ (v ⁻¹) · proj₁ v) · x ≡⟨ sym (assoc _ _ _) ⟩
    proj₁ (v ⁻¹) · (proj₁ v · x) ≡⟨ cong (λ t → _ · t) v·x≡v·y ⟩
    proj₁ (v ⁻¹) · (proj₁ v · y) ≡⟨ assoc _ _ _ ⟩
    (proj₁ (v ⁻¹) · proj₁ v) · y ≡⟨ cong (λ t → t · _) (right-inverse _) ⟩
    e · y ≡⟨ left-identity _ ⟩
    y ∎

  identity-inverse : (identity-proof : P e) -> proj₁ ((e , identity-proof)  ⁻¹) ≡ e
  identity-inverse identity-proof =
    proj₁ ((e , identity-proof)  ⁻¹) ≡⟨ sym (right-identity _) ⟩
    proj₁ ((e , identity-proof)  ⁻¹) · e ≡⟨ right-inverse _ ⟩
    e ∎

Commutative : ∀ {A : Set} (_·_ : Op₂ A) -> Set
Commutative {A} (_·_) = ∀ (x y : A) -> x · y ≡ y · x

always : ∀ {A : Set} -> A -> Set
always _ = ⊤

record Field {F : Set} : Set where
  infixl 6 _+_
  infixl 7 _·_
  infix 8 -_
  infix 8 _⁻¹
  field
    _+_ : Op₂ F
    +-assoc : Associative _+_
    0# : F
    +-identity : Identity _+_ 0#
    -_ : ∃ always -> ∃ always
    +-inverse : Inverse _+_ always -_ 0#
    _·_ : Op₂ F
    ·-comm : Commutative _·_
    ·-assoc : Associative _·_
    1# : F
    ·-identity : Identity _·_ 1#
    _⁻¹ : ∃ (λ x -> x ≢ 0#) -> ∃ (λ x -> x ≢ 0#)
    ·-inverse : Inverse _·_ (λ x -> x ≢ 0#) _⁻¹ 1#
    ·-+-dist : ∀ (x y z : F) -> x · (y + z) ≡ (x · y) + (x · z)
    0≢1 : 0# ≢ 1#

module Field-Theorems {F : Set} (f : Field {F}) where
  open Field f hiding (-_)
  open Identity +-identity
    renaming ( left-identity to +-left-identity ; right-identity to +-right-identity )
  open Identity ·-identity
    renaming ( left-identity to ·-left-identity ; right-identity to ·-right-identity )

  instance
    FieldNumber : Number F
    FieldNumber =
      record
      { Constraint = λ _ → ⊤
      ; fromNat = natToField }
      where
      natToField : ℕ → {{_ : ⊤}} → F
      natToField 0 = 0#
      natToField 1 = 1#
      natToField 2 = 1# + 1#
      natToField (suc (suc n)) = (natToField n + 1#) + 1#

  +-right-cancellation : ∀ {x y z : F} -> x + z ≡ y + z -> x ≡ y
  +-right-cancellation {x} {y} {z} x+z≡y+z = right-cancellation x y (z , tt) x+z≡y+z
    where open Inverse-Theorems +-assoc +-identity +-inverse

  +-left-cancellation : ∀ {x y z : F} -> z + x ≡ z + y -> x ≡ y
  +-left-cancellation {x} {y} {z} z+x≡z+y = left-cancellation x y (z , tt) z+x≡z+y
    where open Inverse-Theorems +-assoc +-identity +-inverse

  NonZero : Set
  NonZero = ∃ (λ x -> x ≢ 0#)

  ·-right-cancellation : ∀ {x y : F} (z : NonZero) -> x · proj₁ z ≡ y · proj₁ z -> x ≡ y
  ·-right-cancellation {x} {y} = right-cancellation x y
    where open Inverse-Theorems ·-assoc ·-identity ·-inverse

  ·-left-cancellation : ∀ {x y : F} (z : NonZero) -> proj₁ z · x ≡ proj₁ z · y -> x ≡ y
  ·-left-cancellation {x} {y} = left-cancellation x y
    where open Inverse-Theorems ·-assoc ·-identity ·-inverse

  -_ : F -> F
  - x = proj₁ (Field.-_ f (x , tt))

  0-inverse : - 0 ≡ 0
  0-inverse = identity-inverse _
    where open Inverse-Theorems +-assoc +-identity +-inverse

  1-inverse : proj₁ ((1 , negsym 0≢1) ⁻¹) ≡ 1
  1-inverse = identity-inverse (negsym 0≢1)
    where open Inverse-Theorems ·-assoc ·-identity ·-inverse

  +-double-inverse : ∀ (x : F) -> - (- x) ≡ x
  +-double-inverse x = double-inverse (x , tt)
    where open Inverse-Theorems +-assoc +-identity +-inverse

  ·-double-inverse : ∀ (x : NonZero) -> proj₁ ((x ⁻¹) ⁻¹) ≡ proj₁ x
  ·-double-inverse = double-inverse
    where open Inverse-Theorems ·-assoc ·-identity ·-inverse

  ·-zero : ∀ (x : F) -> x · 0 ≡ 0
  ·-zero x = +-left-cancellation lemma
    where
    lemma : x · 0 + x · 0 ≡ x · 0 + 0
    lemma =
      x · 0 + x · 0 ≡⟨ sym (·-+-dist _ _ _) ⟩
      x · (0 + 0) ≡⟨ cong (λ t → _ · t) (+-left-identity _) ⟩
      x · 0 ≡⟨ sym (+-right-identity _) ⟩
      x · 0 + 0 ∎

  -- This is not constructive
  2-68 : Decidable {A = F} _≡_ -> ∀ (x y : F) -> x · y ≡ 0 -> x ≡ 0 ⊎ y ≡ 0
  2-68 decEq x y x·y≡0 with decEq x 0
  ...                  | yes x≡0 = inj₁ x≡0
  ...                  | no x≢0 = inj₂ (·-left-cancellation (x , x≢0) lemma)
    where
    lemma : x · y ≡ x · 0
    lemma =
      x · y ≡⟨ x·y≡0 ⟩
      0 ≡⟨ sym (·-zero _) ⟩
      x · 0 ∎

  foil : ∀ (a b c d : F) -> (a + b) · (c + d) ≡ a · c + a · d + b · c + b · d
  foil a b c d =
    (a + b) · (c + d) ≡⟨ ·-comm _ _ ⟩
    (c + d) · (a + b) ≡⟨ ·-+-dist _ _ _ ⟩
    (c + d) · a + (c + d) · b ≡⟨  cong (λ x → x + (c + d) · b) (lemma c d a) ⟩
    a · c + a · d + (c + d) · b ≡⟨ cong (λ x → a · c + a · d + x) (lemma c d b) ⟩
    a · c + a · d + (b · c + b · d) ≡⟨ +-assoc _ _ _ ⟩
    a · c + a · d + b · c + b · d ∎
    where
    lemma : ∀ (x y z : F) -> (x + y) · z ≡ z · x + z · y
    lemma x y z =
      (x + y) · z ≡⟨ ·-comm _ _ ⟩
      z · (x + y) ≡⟨ ·-+-dist _ _ _ ⟩
      z · x + z · y ∎

  +-comm : ∀ (x y : F) -> x + y ≡ y + x
  +-comm x y = cancel (+-right-cancellation lemma)
    where
    cancel : 1 + x + y ≡ 1 + y + x -> x + y ≡ y + x
    cancel eq = +-left-cancellation (
      1 + (x + y) ≡⟨ +-assoc _ _ _ ⟩
      1 + x + y ≡⟨ eq ⟩
      1 + y + x ≡⟨ sym (+-assoc _ _ _) ⟩
      1 + (y + x) ∎ )
    lemma : 1 + x + y + x · y ≡ 1 + y + x + x · y
    lemma =
      1 + x + y + x · y ≡⟨ cong (λ t -> t + x + y + x · y) (sym (·-left-identity _)) ⟩
      1 · 1 + x + y + x · y ≡⟨ cong (λ t -> 1 · 1 + t + y + x · y ) (sym (·-left-identity _)) ⟩
      1 · 1 + 1 · x + y + x · y ≡⟨  cong (λ t -> 1 · 1 + 1 · x + t + x · y) (sym (·-right-identity _)) ⟩
      1 · 1 + 1 · x + y · 1 + x · y ≡⟨  cong (λ t -> 1 · 1 + 1 · x + y · 1 + t) (·-comm _ _) ⟩
      1 · 1 + 1 · x + y · 1 + y · x ≡⟨ sym (foil 1 y 1 x) ⟩
      (1 + y) · (1 + x) ≡⟨ ·-comm _ _ ⟩
      (1 + x) · (1 + y) ≡⟨ foil 1 x 1 y ⟩
      1 · 1 + 1 · y + x · 1 + x · y ≡⟨  cong (λ t -> 1 · 1 + 1 · y + t + x · y) (·-right-identity _) ⟩
      1 · 1 + 1 · y + x + x · y ≡⟨ cong (λ t -> 1 · 1 + t + x + x · y) (·-left-identity _) ⟩
      1 · 1 + y + x + x · y ≡⟨ cong (λ t -> t + y + x + x · y) (·-left-identity _) ⟩
      1 + y + x + x · y ∎