mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-15 08:28:39 +00:00
UFD progress (#108)
This commit is contained in:
Patrick Stevens
GitHub
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
30
Rings/Divisible/Lemmas.agda
Normal file
30
Rings/Divisible/Lemmas.agda
Normal file
@@ -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)
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
57
Rings/UniqueFactorisationDomains/Lemmas.agda
Normal file
57
Rings/UniqueFactorisationDomains/Lemmas.agda
Normal file
@@ -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
|
||||
23
Vectors.agda
23
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)
|
||||
|
||||
Reference in New Issue
Block a user