From 1cff95c652aaf5033ebab195c973a14a720f7d7f Mon Sep 17 00:00:00 2001
From: Patrick Stevens <patrick+github@patrickstevens.co.uk>
Date: Fri, 10 Apr 2020 09:24:53 +0100
Subject: [PATCH] UFD progress (#108)

---
 Everything/Safe.agda                          |  2 +-
 Rings/Divisible/Definition.agda               |  1 -
 Rings/Divisible/Lemmas.agda                   | 30 ++++++++++
 Rings/Irreducibles/Lemmas.agda                |  1 -
 .../Definition.agda                           | 51 +++++++++++++----
 Rings/UniqueFactorisationDomains/Lemmas.agda  | 57 +++++++++++++++++++
 Vectors.agda                                  | 23 ++++++++
 7 files changed, 152 insertions(+), 13 deletions(-)
 create mode 100644 Rings/Divisible/Lemmas.agda
 create mode 100644 Rings/UniqueFactorisationDomains/Lemmas.agda

diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 96da870..014ed6d 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -81,7 +81,7 @@ open import Rings.Subrings.Definition
 open import Rings.Ideals.Maximal.Lemmas
 open import Rings.Primes.Lemmas
 open import Rings.Irreducibles.Definition
-open import Rings.Divisible.Definition
+open import Rings.Divisible.Lemmas
 open import Rings.Associates.Lemmas
 open import Rings.InitialRing
 open import Rings.Homomorphisms.Lemmas
diff --git a/Rings/Divisible/Definition.agda b/Rings/Divisible/Definition.agda
index d6c1a1d..177488e 100644
--- a/Rings/Divisible/Definition.agda
+++ b/Rings/Divisible/Definition.agda
@@ -6,7 +6,6 @@ open import Functions
 open import Sets.EquivalenceRelations
 open import Rings.Definition
 
-
 module Rings.Divisible.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
 
 open Setoid S
diff --git a/Rings/Divisible/Lemmas.agda b/Rings/Divisible/Lemmas.agda
new file mode 100644
index 0000000..84c027d
--- /dev/null
+++ b/Rings/Divisible/Lemmas.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+
+module Rings.Divisible.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+open Setoid S
+open Equivalence eq
+open Ring R
+open import Rings.Divisible.Definition R
+open import Rings.Units.Definition R
+
+divisionTransitive : (x y z : A) → x ∣ y → y ∣ z → x ∣ z
+divisionTransitive x y z (a , pr) (b , pr2) = (a * b) , transitive (transitive *Associative (*WellDefined pr reflexive)) pr2
+
+divisionReflexive : (x : A) → x ∣ x
+divisionReflexive x = 1R , transitive *Commutative identIsIdent
+
+everythingDividesZero : (r : A) → r ∣ 0R
+everythingDividesZero r = 0R , timesZero
+
+nonzeroInherits : {x y : A} (nz : (x ∼ 0R) → False) → y ∣ x → (y ∼ 0R) → False
+nonzeroInherits {x} {y} nz (c , pr) y=0 = nz (transitive (symmetric pr) (transitive (*WellDefined y=0 reflexive) (transitive *Commutative timesZero)))
+
+nonunitInherits : {x y : A} (nonunit : Unit x → False) → x ∣ y → Unit y → False
+nonunitInherits nu (s , pr) (a , b) = nu ((s * a) , transitive (transitive *Associative (*WellDefined pr reflexive)) b)
diff --git a/Rings/Irreducibles/Lemmas.agda b/Rings/Irreducibles/Lemmas.agda
index eef3c5e..62dc11d 100644
--- a/Rings/Irreducibles/Lemmas.agda
+++ b/Rings/Irreducibles/Lemmas.agda
@@ -6,7 +6,6 @@ open import Sets.EquivalenceRelations
 open import Rings.IntegralDomains.Definition
 open import Rings.Definition
 
-
 module Rings.Irreducibles.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where
 
 open import Rings.Irreducibles.Definition intDom
diff --git a/Rings/UniqueFactorisationDomains/Definition.agda b/Rings/UniqueFactorisationDomains/Definition.agda
index 6a626b3..2048777 100644
--- a/Rings/UniqueFactorisationDomains/Definition.agda
+++ b/Rings/UniqueFactorisationDomains/Definition.agda
@@ -4,7 +4,10 @@ open import LogicalFormulae
 open import Setoids.Setoids
 open import Rings.Definition
 open import Rings.IntegralDomains.Definition
-open import Lists.Lists
+open import Vectors
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Order
+open import Numbers.Naturals.Definition
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
@@ -12,16 +15,44 @@ module Rings.UniqueFactorisationDomains.Definition {a b : _} {A : Set a} {S : Se
 
 open import Rings.Units.Definition R
 open import Rings.Irreducibles.Definition intDom
+open import Rings.Associates.Definition intDom
+open import Rings.Primes.Definition intDom
 open Ring R
 open Setoid S
 
-record Factorisation {r : A} (nonzero : (r ∼ 0R) → False) (nonunit : (Unit r) → False) : Set (a ⊔ b) where
-  field
-    factorise : List A
-    factoriseIsFactorisation : fold (_*_) 1R factorise ∼ r
-    factoriseIsIrreducibles : allTrue Irreducible factorise
+private
+  power : A → ℕ → A
+  power x zero = 1R
+  power x (succ n) = x * power x n
 
---record UFD : Set (a ⊔ b) where
---  field
---    factorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → Factorisation nonzero nonunit
---    uniqueFactorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → (f1 f2 : Factorisation nonzero nonunit) → {!Sg !}
+  allDistinct : {n : ℕ} → Vec A n → Set (a ⊔ b)
+  allDistinct [] = True'
+  allDistinct (x ,- xs) = (allDistinct xs) && vecAllTrue (λ n → (n ∼ x) → False) xs
+
+record Factorisation {r : A} .(nonzero : (r ∼ 0R) → False) .(nonunit : (Unit r) → False) : Set (a ⊔ b) where
+  field
+    len : ℕ
+    factorise : Vec (A && ℕ) len
+    factoriseIsFactorisation : vecFold (λ x y → y * power (_&&_.fst x) (succ (_&&_.snd x))) 1R factorise ∼ r
+    factoriseIsIrreducibles : vecAllTrue Irreducible (vecMap _&&_.fst factorise)
+    distinct : allDistinct (vecMap _&&_.fst factorise)
+
+private
+  equality : {n : ℕ} (v1 v2 : Vec (A && ℕ) n) → Set (a ⊔ b)
+  equality [] [] = True'
+  equality {succ n} ((a ,, an) ,- v1) v2 = Sg ℕ (λ index → Sg (index <N succ n) (λ i<n → (Associates (_&&_.fst (vecIndex v2 index i<n)) a) && ((_&&_.snd (vecIndex v2 index i<n) ≡ an) && equality v1 (vecDelete index i<n v2))))
+
+factorisationEquality : {r : A} → .{nonzero : (r ∼ 0R) → False} → .{nonunit : (Unit r) → False} → Factorisation nonzero nonunit → Factorisation nonzero nonunit → Set (a ⊔ b)
+factorisationEquality record { len = lenA ; factorise = factoriseA ; factoriseIsFactorisation = factoriseIsFactorisationA ; factoriseIsIrreducibles = factoriseIsIrreduciblesA ; distinct = distinctA } record { len = lenB ; factorise = factoriseB ; factoriseIsFactorisation = factoriseIsFactorisationB ; factoriseIsIrreducibles = factoriseIsIrreduciblesB ; distinct = distinctB } with ℕDecideEquality lenA lenB
+factorisationEquality record { len = a ; factorise = factoriseA } record { len = .a ; factorise = factoriseB } | inl refl = equality factoriseA factoriseB
+factorisationEquality record { len = a ; factorise = factoriseA } record { len = b ; factorise = factoriseB } | inr _ = False'
+
+record UFD : Set (a ⊔ b) where
+  field
+    factorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → Factorisation nonzero nonunit
+    uniqueFactorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → (f1 f2 : Factorisation nonzero nonunit) → factorisationEquality f1 f2
+
+record UFD' : Set (a ⊔ b) where
+  field
+    factorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → Factorisation nonzero nonunit
+    irreduciblesArePrime : {r : A} → Irreducible r → Prime r
diff --git a/Rings/UniqueFactorisationDomains/Lemmas.agda b/Rings/UniqueFactorisationDomains/Lemmas.agda
new file mode 100644
index 0000000..8aa6660
--- /dev/null
+++ b/Rings/UniqueFactorisationDomains/Lemmas.agda
@@ -0,0 +1,57 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.IntegralDomains.Definition
+open import Vectors
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Order
+open import Numbers.Naturals.Definition
+open import Sets.EquivalenceRelations
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.UniqueFactorisationDomains.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where
+
+open import Rings.Units.Definition R
+open import Rings.Irreducibles.Definition intDom
+open import Rings.Associates.Definition intDom
+open import Rings.Primes.Definition intDom
+open import Rings.Divisible.Definition R
+open import Rings.Divisible.Lemmas R
+open import Rings.UniqueFactorisationDomains.Definition intDom
+open Ring R
+open Setoid S
+open Equivalence eq
+
+ufdImpliesUfd' : UFD → UFD'
+UFD'.factorisation (ufdImpliesUfd' x) = UFD.factorisation x
+Prime.isPrime (UFD'.irreduciblesArePrime (ufdImpliesUfd' ufd) {r} irreducible) a b (s , ab=rs) rNotDivA = {!!}
+  where
+  -- we can't factorise a, it might be a unit :(
+    factA : Factorisation {a} (λ p → rNotDivA (divisibleWellDefined reflexive (symmetric p) (everythingDividesZero r))) {!!}
+    factA = UFD.factorisation ufd {a} {!!} {!!}
+    fact1 : Factorisation {r} {!!} {!!}
+    fact1 = {!!}
+    fact2 : Factorisation {r} {!!} {!!}
+    fact2 = {!!}
+Prime.nonzero (UFD'.irreduciblesArePrime (ufdImpliesUfd' x) irreducible) = Irreducible.nonzero irreducible
+Prime.nonunit (UFD'.irreduciblesArePrime (ufdImpliesUfd' x) irreducible) = Irreducible.nonunit irreducible
+
+private
+  lemma2 : UFD' → {r : A} → .(nonzero : (r ∼ 0R) → False) .(nonunit : (Unit r) → False) → (f1 f2 : Factorisation {r} nonzero nonunit) → factorisationEquality f1 f2
+  lemma2 x nonzero nonunit record { len = lenA ; factorise = factoriseA ; factoriseIsFactorisation = factoriseIsFactorisationA ; factoriseIsIrreducibles = factoriseIsIrreduciblesA ; distinct = distinctA } record { len = lenB ; factorise = factoriseB ; factoriseIsFactorisation = factoriseIsFactorisationB ; factoriseIsIrreducibles = factoriseIsIrreduciblesB ; distinct = distinctB } with ℕDecideEquality lenA lenB
+  lemma2 x nonzero nonunit record { len = zero ; factorise = [] ; factoriseIsFactorisation = factoriseIsFactorisationA ; factoriseIsIrreducibles = factoriseIsIrreduciblesA ; distinct = distinctA } record { len = .0 ; factorise = [] ; factoriseIsFactorisation = factoriseIsFactorisationB ; factoriseIsIrreducibles = factoriseIsIrreduciblesB ; distinct = distinctB } | inl refl = record {}
+  lemma2 ufd' {r} nonzero nonunit record { len = (succ len) ; factorise = (a1 ,, n1) ,- factoriseA ; factoriseIsFactorisation = factoriseIsFactorisationA ; factoriseIsIrreducibles = factoriseIsIrreduciblesA ; distinct = distinctA } record { len = .(succ len) ; factorise = factoriseB ; factoriseIsFactorisation = factoriseIsFactorisationB ; factoriseIsIrreducibles = factoriseIsIrreduciblesB ; distinct = distinctB } | inl refl = {!!}
+    where
+      a1Prime : Prime a1
+      a1Prime = UFD'.irreduciblesArePrime ufd' (_&&_.fst factoriseIsIrreduciblesA)
+      a1DivR : a1 ∣ r
+      a1DivR = {!!}
+
+  ... | inr neq = {!!}
+
+ufd'ImpliesUfd : UFD' → UFD
+UFD.factorisation (ufd'ImpliesUfd x) = UFD'.factorisation x
+UFD.uniqueFactorisation (ufd'ImpliesUfd x) {r} nonzero nonunit f1 f2 = lemma2 x nonzero nonunit f1 f2
diff --git a/Vectors.agda b/Vectors.agda
index cb7006f..8553769 100644
--- a/Vectors.agda
+++ b/Vectors.agda
@@ -3,6 +3,7 @@
 open import LogicalFormulae
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
+open import Numbers.Naturals.Order.Lemmas
 open import Semirings.Definition
 open import Orders.Total.Definition
 open import Lists.Lists
@@ -134,6 +135,28 @@ vecPure : {a : _} {X : Set a} → X → {n : ℕ} → Vec X n
 vecPure x {zero} = []
 vecPure x {succ n} = x ,- vecPure x {n}
 
+vecAllTrue : {a b : _} {X : Set a} (f : X → Set b) → {n : ℕ} (v : Vec X n) → Set b
+vecAllTrue f [] = True'
+vecAllTrue f (x ,- v) = f x && vecAllTrue f v
+
+vecFold : {a b : _} {X : Set a} {S : Set b} (f : X → S → S) (s : S) {n : ℕ} (v : Vec X n) → S
+vecFold f s [] = s
+vecFold f s (x ,- v) = vecFold f (f x s) v
+
+private
+  succLess1 : (i : ℕ) → .(succ i <N 1) → False
+  succLess1 zero pr with <NProp pr
+  ... | le zero ()
+  ... | le (succ x) ()
+  succLess1 (succ i) pr with <NProp pr
+  ... | le zero ()
+  ... | le (succ x) ()
+
+vecDelete : {a : _} {X : Set a} {n : ℕ} (index : ℕ) .(pr : index <N succ n) → Vec X (succ n) → Vec X n
+vecDelete zero _ (x ,- v) = v
+vecDelete (succ i) p (x ,- []) = exFalso (succLess1 i p)
+vecDelete (succ i) pr (x ,- (y ,- v)) = x ,- vecDelete i (canRemoveSuccFrom<N pr) (y ,- v)
+
 _$V_ : {a b : _} {X : Set a} {Y : Set b} {n : ℕ} → Vec (X → Y) n → Vec X n → Vec Y n
 [] $V [] = []
 (f ,- fs) $V (x ,- xs) = f x ,- (fs $V xs)