mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-13 07:38:40 +00:00
Primes and mod-n into the fold (#47)
This commit is contained in:
Patrick Stevens
GitHub
704
Numbers/Modulo/IntegersModN.agda
Normal file
704
Numbers/Modulo/IntegersModN.agda
Normal file
@@ -0,0 +1,704 @@
|
||||
{-# OPTIONS --safe --warning=error #-}
|
||||
-- These are explicitly with-K, because we currently encode an element of Zn as
|
||||
-- a natural together with a proof that it is small.
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Definition
|
||||
open import Groups.Groups
|
||||
open import Numbers.Naturals.Naturals
|
||||
open import Numbers.Naturals.Addition -- TODO remove this dependency
|
||||
open import Numbers.Primes.PrimeNumbers
|
||||
open import Setoids.Setoids
|
||||
open import Sets.FinSet
|
||||
open import Sets.FinSetWithK
|
||||
open import Functions
|
||||
open import Numbers.Naturals.WithK
|
||||
open import Semirings.Definition
|
||||
open import Orders
|
||||
|
||||
module Numbers.Modulo.IntegersModN where
|
||||
record ℤn (n : ℕ) (pr : 0 <N n) : Set where
|
||||
field
|
||||
x : ℕ
|
||||
xLess : x <N n
|
||||
|
||||
equalityZn : {n : ℕ} {pr : 0 <N n} → (a b : ℤn n pr) → (ℤn.x a ≡ ℤn.x b) → a ≡ b
|
||||
equalityZn record { x = a ; xLess = aLess } record { x = .a ; xLess = bLess } refl rewrite <NRefl aLess bLess = refl
|
||||
|
||||
cancelSumFromInequality : {a b c : ℕ} → a +N b <N a +N c → b <N c
|
||||
cancelSumFromInequality {a} {b} {c} (le x proof) = le x help
|
||||
where
|
||||
help : succ x +N b ≡ c
|
||||
help rewrite Semiring.+Associative ℕSemiring (succ x) a b | Semiring.commutative ℕSemiring x a | equalityCommutative (Semiring.+Associative ℕSemiring (succ a) x b) | Semiring.commutative ℕSemiring a (x +N b) | Semiring.commutative ℕSemiring (succ (x +N b)) a = canSubtractFromEqualityLeft {a} proof
|
||||
|
||||
_+n_ : {n : ℕ} {pr : 0 <N n} → ℤn n pr → ℤn n pr → ℤn n pr
|
||||
_+n_ {0} {le x ()} a b
|
||||
_+n_ {succ n} {pr} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } with orderIsTotal (a +N b) (succ n)
|
||||
_+n_ {succ n} {pr} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inl (a+b<n)) = record { x = a +N b ; xLess = a+b<n }
|
||||
_+n_ {succ n} {pr} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inr (n<a+b)) = record { x = subtractionNResult.result sub ; xLess = pr2 }
|
||||
where
|
||||
sub : subtractionNResult (succ n) (a +N b) (inl n<a+b)
|
||||
sub = -N (inl n<a+b)
|
||||
pr1 : a +N b <N succ n +N succ n
|
||||
pr1 = addStrongInequalities aLess bLess
|
||||
pr1' : succ n +N (subtractionNResult.result sub) <N succ n +N succ n
|
||||
pr1' rewrite subtractionNResult.pr sub = pr1
|
||||
pr2 : subtractionNResult.result sub <N succ n
|
||||
pr2 = cancelSumFromInequality pr1'
|
||||
_+n_ {succ n} {pr} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inr (a+b=n) = record { x = 0 ; xLess = succIsPositive n }
|
||||
|
||||
plusZnIdentityRight : {n : ℕ} → {pr : 0 <N n} → (a : ℤn n pr) → (a +n record { x = 0 ; xLess = pr }) ≡ a
|
||||
plusZnIdentityRight {zero} {()} a
|
||||
plusZnIdentityRight {succ x} {_} record { x = a ; xLess = aLess } with orderIsTotal (a +N 0) (succ x)
|
||||
plusZnIdentityRight {succ x} {_} record { x = a ; xLess = aLess } | inl (inl a<sx) = equalityZn _ _ (Semiring.commutative ℕSemiring a 0)
|
||||
plusZnIdentityRight {succ x} {_} record { x = a ; xLess = aLess } | inl (inr sx<a) = exFalso (f aLess sx<a)
|
||||
where
|
||||
f : (aL : a <N succ x) → (sx<a : succ x <N a +N 0) → False
|
||||
f aL sx<a rewrite Semiring.commutative ℕSemiring a 0 = orderIsIrreflexive aL sx<a
|
||||
plusZnIdentityRight {succ x} {_} record { x = a ; xLess = aLess } | inr a=sx = exFalso (f aLess a=sx)
|
||||
where
|
||||
f : (aL : a <N succ x) → (a=sx : a +N 0 ≡ succ x) → False
|
||||
f aL a=sx rewrite Semiring.commutative ℕSemiring a 0 | a=sx = TotalOrder.irreflexive ℕTotalOrder aL
|
||||
|
||||
|
||||
plusZnIdentityLeft : {n : ℕ} → {pr : 0 <N n} → (a : ℤn n pr) → (record { x = 0 ; xLess = pr }) +n a ≡ a
|
||||
plusZnIdentityLeft {zero} {()}
|
||||
plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } with orderIsTotal x (succ n)
|
||||
plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } | inl (inl x<succn) rewrite <NRefl x<succn xLess = refl
|
||||
plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } | inl (inr succn<x) = exFalso (cannotBeLeqAndG {x} {succ n} (inl xLess) succn<x)
|
||||
plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } | inr x=succn rewrite x=succn = exFalso (TotalOrder.irreflexive ℕTotalOrder xLess)
|
||||
|
||||
subLemma : {a b c : ℕ} → (pr1 : a <N b) → (pr2 : a <N c) → (pr : b ≡ c) → (subtractionNResult.result (-N (inl pr1))) ≡ (subtractionNResult.result (-N (inl pr2)))
|
||||
subLemma {a} {b} {c} a<b a<c b=c rewrite b=c | <NRefl a<b a<c = refl
|
||||
|
||||
plusZnCommutative : {n : ℕ} → {pr : 0 <N n} → (a b : ℤn n pr) → (a +n b) ≡ b +n a
|
||||
plusZnCommutative {zero} {()} a b
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } with orderIsTotal (a +N b) (succ n)
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inl a+b<sn) with orderIsTotal (b +N a) (succ n)
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inl a+b<sn) | inl (inl b+a<sn) = equalityZn _ _ (Semiring.commutative ℕSemiring a b)
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inl a+b<sn) | inl (inr sn<b+a) = exFalso (f a+b<sn sn<b+a)
|
||||
where
|
||||
f : (a +N b) <N succ n → succ n <N b +N a → False
|
||||
f pr1 pr2 rewrite Semiring.commutative ℕSemiring b a = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr2 pr1)
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inl a+b<sn) | inr b+a=sn = exFalso (f a+b<sn b+a=sn)
|
||||
where
|
||||
f : (a +N b) <N succ n → b +N a ≡ succ n → False
|
||||
f pr1 eq rewrite Semiring.commutative ℕSemiring b a | eq = TotalOrder.irreflexive ℕTotalOrder pr1
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inr sn<a+b) with orderIsTotal (b +N a) (succ n)
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inr sn<a+b) | inl (inl b+a<sn) = exFalso (f sn<a+b b+a<sn)
|
||||
where
|
||||
f : succ n <N a +N b → b +N a <N succ n → False
|
||||
f pr1 pr2 rewrite Semiring.commutative ℕSemiring b a = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive sn<a+b b+a<sn)
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inr sn<a+b) | inl (inr sn<b+a) = equalityZn _ _ (subLemma sn<a+b sn<b+a (Semiring.commutative ℕSemiring a b))
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inl (inr sn<a+b) | inr sn=b+a = exFalso (f sn<a+b sn=b+a)
|
||||
where
|
||||
f : succ n <N a +N b → b +N a ≡ succ n → False
|
||||
f pr eq rewrite Semiring.commutative ℕSemiring b a | eq = TotalOrder.irreflexive ℕTotalOrder pr
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inr sn=a+b with orderIsTotal (b +N a) (succ n)
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inr sn=a+b | inl (inl b+a<sn) = exFalso f
|
||||
where
|
||||
f : False
|
||||
f rewrite Semiring.commutative ℕSemiring b a | sn=a+b = TotalOrder.irreflexive ℕTotalOrder b+a<sn
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inr sn=a+b | inl (inr sn<b+a) = exFalso f
|
||||
where
|
||||
f : False
|
||||
f rewrite Semiring.commutative ℕSemiring b a | sn=a+b = TotalOrder.irreflexive ℕTotalOrder sn<b+a
|
||||
plusZnCommutative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } | inr sn=a+b | inr sn=b+a = equalityZn _ _ refl
|
||||
|
||||
help30 : {a b c n : ℕ} → (c <N n) → (a +N b ≡ n) → (n<b+c : n <N b +N c) → (n <N a +N subtractionNResult.result (-N (inl n<b+c))) → False
|
||||
help30 {a} {b} {c} {n} c<n a+b=n n<b+c x = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr5 c<n)
|
||||
where
|
||||
pr : n +N n <N a +N (subtractionNResult.result (-N (inl n<b+c)) +N n)
|
||||
pr = identityOfIndiscernablesRight _ _ _ _<N_ (additionPreservesInequality n x) (equalityCommutative (Semiring.+Associative ℕSemiring a _ n))
|
||||
pr2 : n +N n <N a +N (b +N c)
|
||||
pr2 = identityOfIndiscernablesRight _ _ _ _<N_ pr (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
pr3 : n +N n <N (a +N b) +N c
|
||||
pr3 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = pr2
|
||||
pr4 : n +N n <N c +N n
|
||||
pr4 rewrite Semiring.commutative ℕSemiring c n = identityOfIndiscernablesRight _ _ _ _<N_ pr3 (applyEquality (_+N c) a+b=n)
|
||||
pr5 : n <N c
|
||||
pr5 = subtractionPreservesInequality n pr4
|
||||
|
||||
help31 : {a b c n : ℕ} → (a +N b ≡ n) → (n<b+c : n <N b +N c) → (a +N subtractionNResult.result (-N (inl n<b+c))) ≡ c
|
||||
help31 {a} {b} {c} {n} a+b=n n<b+c = canSubtractFromEqualityLeft pr2
|
||||
where
|
||||
pr1 : a +N (n +N subtractionNResult.result (-N (inl n<b+c))) ≡ n +N c
|
||||
pr1 rewrite addMinus' (inl n<b+c) | Semiring.+Associative ℕSemiring a b c | a+b=n = refl
|
||||
pr2 : n +N (a +N subtractionNResult.result (-N (inl n<b+c))) ≡ n +N c
|
||||
pr2 = identityOfIndiscernablesLeft _ _ _ _≡_ pr1 (lemm a n (subtractionNResult.result (-N (inl n<b+c))))
|
||||
where
|
||||
lemm : (a b c : ℕ) → a +N (b +N c) ≡ b +N (a +N c)
|
||||
lemm a b c rewrite Semiring.+Associative ℕSemiring a b c | Semiring.commutative ℕSemiring a b | equalityCommutative (Semiring.+Associative ℕSemiring b a c) = refl
|
||||
|
||||
help7 : {a b c n : ℕ} → b +N c ≡ n → a <N n → (n<a+b : n <N a +N b) → (subtractionNResult.result (-N (inl n<a+b)) +N c ≡ n) → False
|
||||
help7 {a} {b} {c} {n} b+c=n a<n n<a+b x = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesLeft _ _ _ _<N_ a<n pr5)
|
||||
where
|
||||
pr : (n +N subtractionNResult.result (-N (inl n<a+b))) +N c ≡ n +N n
|
||||
pr = identityOfIndiscernablesLeft _ _ _ _≡_ (applyEquality (n +N_) x) (Semiring.+Associative ℕSemiring n _ c)
|
||||
pr2 : (a +N b) +N c ≡ n +N n
|
||||
pr2 = identityOfIndiscernablesLeft _ _ _ _≡_ pr (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
pr3 : a +N (b +N c) ≡ n +N n
|
||||
pr3 rewrite Semiring.+Associative ℕSemiring a b c = pr2
|
||||
pr4 : a +N n ≡ n +N n
|
||||
pr4 = identityOfIndiscernablesLeft _ _ _ _≡_ pr3 (applyEquality (a +N_) b+c=n)
|
||||
pr5 : a ≡ n
|
||||
pr5 = canSubtractFromEqualityRight pr4
|
||||
|
||||
help29 : {a b c n : ℕ} → (c <N n) → (n<b+c : n <N b +N c) → (a +N subtractionNResult.result (-N (inl n<b+c))) ≡ n → a +N b ≡ n → False
|
||||
help29 {a} {b} {c} {n} c<n n<b+c pr a+b=n = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesLeft _ _ _ _<N_ c<n p4)
|
||||
where
|
||||
p1 : a +N (subtractionNResult.result (-N (inl n<b+c)) +N n) ≡ n +N n
|
||||
p1 = identityOfIndiscernablesLeft _ _ _ _≡_ (applyEquality (_+N n) pr) (equalityCommutative (Semiring.+Associative ℕSemiring a _ n))
|
||||
p2 : (a +N b) +N c ≡ n +N n
|
||||
p2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = identityOfIndiscernablesLeft _ _ _ _≡_ p1 (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
p3 : n +N c ≡ n +N n
|
||||
p3 = identityOfIndiscernablesLeft _ _ _ _≡_ p2 (applyEquality (_+N c) a+b=n)
|
||||
p4 : c ≡ n
|
||||
p4 = canSubtractFromEqualityLeft p3
|
||||
|
||||
help28 : {a b c n : ℕ} → (n<a+'b+c : n <N a +N (b +N c)) → (a +N b ≡ n) → subtractionNResult.result (-N (inl n<a+'b+c)) ≡ c
|
||||
help28 {a} {b} {c} {n} pr a+b=n = canSubtractFromEqualityLeft p2
|
||||
where
|
||||
p1 : a +N (b +N c) ≡ n +N c
|
||||
p1 rewrite Semiring.+Associative ℕSemiring a b c | a+b=n = refl
|
||||
p2 : n +N subtractionNResult.result (-N (inl pr)) ≡ n +N c
|
||||
p2 = identityOfIndiscernablesLeft _ _ _ _≡_ p1 (equalityCommutative (addMinus' (inl pr)))
|
||||
|
||||
help27 : {a b c n : ℕ} → (a +N b ≡ succ n) → (a +N (b +N c) <N succ n) → a +N (b +N c) ≡ c
|
||||
help27 {a} {b} {zero} {n} a+b=sn a+b+c<sn rewrite Semiring.commutative ℕSemiring b 0 | a+b=sn = exFalso (TotalOrder.irreflexive ℕTotalOrder a+b+c<sn)
|
||||
help27 {a} {b} {succ c} {n} a+b=sn a+b+c<sn rewrite Semiring.+Associative ℕSemiring a b (succ c) | a+b=sn = exFalso (cannotAddAndEnlarge' a+b+c<sn)
|
||||
|
||||
help26 : {a b c n : ℕ} → (a +N b ≡ n) → (a +N (b +N c) ≡ n) → 0 ≡ c
|
||||
help26 {a} {b} {c} {n} a+b=n a+b+c=n rewrite Semiring.+Associative ℕSemiring a b c | a+b=n | Semiring.commutative ℕSemiring n c = equalityCommutative (canSubtractFromEqualityRight a+b+c=n)
|
||||
|
||||
help25 : {a b c n : ℕ} → (a +N b ≡ n) → (b +N c ≡ n) → (a +N 0 ≡ c)
|
||||
help25 {a} {b} {c} {n} a+b=n b+c=n rewrite Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring a b | equalityCommutative a+b=n = equalityCommutative (canSubtractFromEqualityLeft b+c=n)
|
||||
|
||||
help24 : {a n : ℕ} → (a <N n) → (n <N a +N 0) → False
|
||||
help24 {a} {n} a<n n<a+0 rewrite Semiring.commutative ℕSemiring a 0 = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive a<n n<a+0)
|
||||
|
||||
help23 : {a n : ℕ} → (a <N n) → (a +N 0 ≡ n) → False
|
||||
help23 {a} {n} a<n a+0=n rewrite Semiring.commutative ℕSemiring a 0 | a+0=n = TotalOrder.irreflexive ℕTotalOrder a<n
|
||||
|
||||
help22 : {a b c n : ℕ} → (a +N b ≡ n) → (c ≡ n) → (n<b+c : n <N b +N c) → (n <N a +N subtractionNResult.result (-N (inl n<b+c))) → False
|
||||
help22 {a} {b} {c} {.c} a+b=n refl n<b+c pr = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _ _ _ _<N_ pr4 a+b=n)
|
||||
where
|
||||
pr1 : c +N c <N a +N (subtractionNResult.result (-N (inl n<b+c)) +N c)
|
||||
pr1 = identityOfIndiscernablesRight _ _ _ _<N_ (additionPreservesInequality c pr) (equalityCommutative (Semiring.+Associative ℕSemiring a _ c))
|
||||
pr2 : c +N c <N a +N (b +N c)
|
||||
pr2 = identityOfIndiscernablesRight _ _ _ _<N_ pr1 (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
pr3 : c +N c <N (a +N b) +N c
|
||||
pr3 = identityOfIndiscernablesRight _ _ _ _<N_ pr2 (Semiring.+Associative ℕSemiring a b c)
|
||||
pr4 : c <N a +N b
|
||||
pr4 = subtractionPreservesInequality c pr3
|
||||
|
||||
help21 : {a b c n : ℕ} → (a +N b ≡ n) → (b +N c ≡ n) → (c ≡ n) → (a <N n) → False
|
||||
help21 {a} {b} {c} {.c} a+b=n b+c=n refl a<n = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesLeft _ _ _ _<N_ a<n a=c)
|
||||
where
|
||||
b=0 : b ≡ 0
|
||||
a=c : a ≡ c
|
||||
a=c = identityOfIndiscernablesLeft _ _ _ _≡_ a+b=n lemm
|
||||
where
|
||||
lemm : a +N b ≡ a
|
||||
lemm rewrite b=0 | Semiring.commutative ℕSemiring a 0 = refl
|
||||
b=0' : (b c : ℕ) → (b +N c ≡ c) → b ≡ 0
|
||||
b=0' zero c b+c=c = refl
|
||||
b=0' (succ b) zero b+c=c = naughtE (equalityCommutative b+c=c)
|
||||
b=0' (succ b) (succ c) b+c=c = b=0' (succ b) c bl2
|
||||
where
|
||||
bl2 : succ b +N c ≡ c
|
||||
bl2 rewrite Semiring.commutative ℕSemiring b c | Semiring.commutative ℕSemiring (succ c) b = succInjective b+c=c
|
||||
b=0 = b=0' b c b+c=n
|
||||
|
||||
help20 : {a b c n : ℕ} → (c ≡ n) → (a +N b ≡ n) → (n<b+c : n <N b +N c) → (a +N subtractionNResult.result (-N (inl n<b+c)) <N n) → False
|
||||
help20 {a} {b} {c} {n} c=n a+b=n n<b+c pr = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesLeft _ _ _ _<N_ pr5 c=n)
|
||||
where
|
||||
pr1 : a +N (subtractionNResult.result (-N (inl n<b+c)) +N n) <N n +N n
|
||||
pr1 = identityOfIndiscernablesLeft _ _ _ _<N_ (additionPreservesInequality n pr) (equalityCommutative (Semiring.+Associative ℕSemiring a _ n))
|
||||
pr2 : a +N (b +N c) <N n +N n
|
||||
pr2 = identityOfIndiscernablesLeft _ _ _ _<N_ pr1 (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
pr3 : (a +N b) +N c <N n +N n
|
||||
pr3 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = pr2
|
||||
pr4 : c +N n <N n +N n
|
||||
pr4 = identityOfIndiscernablesLeft _ _ _ _<N_ pr3 (transitivity (applyEquality (_+N c) a+b=n) (Semiring.commutative ℕSemiring n c))
|
||||
pr5 : c <N n
|
||||
pr5 = subtractionPreservesInequality n pr4
|
||||
|
||||
help19 : {a b c n : ℕ} → (b+c<n : b +N c <N n) → (n<a+b : n <N a +N b) → (a <N n) → (subtractionNResult.result (-N (inl n<a+b)) +N c ≡ n) → False
|
||||
help19 {a} {b} {c} {n} b+c<n n<a+b a<n pr = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesLeft _ _ _ _<N_ r q')
|
||||
where
|
||||
p : (n +N subtractionNResult.result (-N (inl n<a+b))) +N c ≡ n +N n
|
||||
p = identityOfIndiscernablesLeft _ _ _ _≡_ (applyEquality (n +N_ ) pr) (Semiring.+Associative ℕSemiring n _ c)
|
||||
q : (a +N b) +N c ≡ n +N n
|
||||
q = identityOfIndiscernablesLeft _ _ _ _≡_ p (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
q' : a +N (b +N c) ≡ n +N n
|
||||
q' = identityOfIndiscernablesLeft _ _ _ _≡_ q (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
|
||||
r : a +N (b +N c) <N n +N n
|
||||
r = addStrongInequalities a<n b+c<n
|
||||
|
||||
help18 : {a b c n : ℕ} → (b+c<n : b +N c <N n) → (n<a+b : n <N a +N b) → (a <N n) → (n <N subtractionNResult.result (-N (inl n<a+b)) +N c) → False
|
||||
help18 {a} {b} {c} {n} b+c<n n<a+b a<n pr = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive p4 a<n)
|
||||
where
|
||||
p : n +N n <N (n +N subtractionNResult.result (-N (inl n<a+b))) +N c
|
||||
p = identityOfIndiscernablesRight _ _ _ _<N_ (additionPreservesInequalityOnLeft n pr) (Semiring.+Associative ℕSemiring n _ c)
|
||||
p' : n +N n <N (a +N b) +N c
|
||||
p' = identityOfIndiscernablesRight _ _ _ _<N_ p (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
p2 : n +N n <N a +N (b +N c)
|
||||
p2 = identityOfIndiscernablesRight _ _ _ _<N_ p' (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
|
||||
p3 : n +N n <N a +N n
|
||||
p3 = orderIsTransitive p2 (additionPreservesInequalityOnLeft a b+c<n)
|
||||
p4 : n <N a
|
||||
p4 = subtractionPreservesInequality n p3
|
||||
|
||||
help17 : {a b c n : ℕ} → (n<b+c : n <N b +N c) → (n<a+b : n <N a +N b) → (a +N subtractionNResult.result (-N (inl n<b+c)) <N n) → (subtractionNResult.result (-N (inl n<a+b)) +N c) ≡ n → False
|
||||
help17 {a} {b} {c} {n} n<b+c n<a+b p1 p2 = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesLeft _ _ _ _<N_ pr1'' pr3)
|
||||
where
|
||||
pr1' : a +N (subtractionNResult.result (-N (inl n<b+c)) +N n) <N n +N n
|
||||
pr1' = identityOfIndiscernablesLeft _ _ _ _<N_ (additionPreservesInequality n p1) (equalityCommutative (Semiring.+Associative ℕSemiring a _ n))
|
||||
pr1'' : a +N (b +N c) <N n +N n
|
||||
pr1'' = identityOfIndiscernablesLeft _ _ _ _<N_ pr1' (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
pr2' : (n +N subtractionNResult.result (-N (inl n<a+b))) +N c ≡ n +N n
|
||||
pr2' = identityOfIndiscernablesLeft _ _ _ _≡_ (applyEquality (n +N_) p2) (Semiring.+Associative ℕSemiring n _ c)
|
||||
pr2'' : (a +N b) +N c ≡ n +N n
|
||||
pr2'' = identityOfIndiscernablesLeft _ _ _ _≡_ pr2' (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
pr3 : a +N (b +N c) ≡ n +N n
|
||||
pr3 = identityOfIndiscernablesLeft _ _ _ _≡_ pr2'' (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
|
||||
|
||||
help16 : {a b c n : ℕ} → (n<b+c : n <N b +N c) → (n<a+b : n <N a +N b) → (a +N subtractionNResult.result (-N (inl n<b+c))) <N n → (pr : n <N subtractionNResult.result (-N (inl n<a+b)) +N c) → a +N subtractionNResult.result (-N (inl n<b+c)) ≡ subtractionNResult.result (-N (inl pr))
|
||||
help16 {a} {b} {c} {n} n<b+c n<a+b pr1 pr2 = exFalso (TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr3 pr1''))
|
||||
where
|
||||
pr1' : a +N (subtractionNResult.result (-N (inl n<b+c)) +N n) <N n +N n
|
||||
pr1' = identityOfIndiscernablesLeft _ _ _ _<N_ (additionPreservesInequality n pr1) (equalityCommutative (Semiring.+Associative ℕSemiring a _ n))
|
||||
pr1'' : a +N (b +N c) <N n +N n
|
||||
pr1'' = identityOfIndiscernablesLeft _ _ _ _<N_ pr1' (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
pr2' : n +N n <N (n +N subtractionNResult.result (-N (inl n<a+b))) +N c
|
||||
pr2' = identityOfIndiscernablesRight _ _ _ _<N_ (additionPreservesInequalityOnLeft n pr2) (Semiring.+Associative ℕSemiring n _ c)
|
||||
pr2'' : n +N n <N (a +N b) +N c
|
||||
pr2'' = identityOfIndiscernablesRight _ _ _ _<N_ pr2' (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
pr3 : n +N n <N a +N (b +N c)
|
||||
pr3 = identityOfIndiscernablesRight _ _ _ _<N_ pr2'' (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
|
||||
|
||||
help15 : {a b c n : ℕ} → (n<b+c : n <N b +N c) → (n<a+b : n <N a +N b) → (n <N a +N subtractionNResult.result (-N (inl n<b+c))) → (subtractionNResult.result (-N (inl n<a+b)) +N c) <N n → False
|
||||
help15 {a} {b} {c} {n} n<b+c n<a+b pr1 pr2 = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive p2'' p1')
|
||||
where
|
||||
p1 : (n +N subtractionNResult.result (-N (inl n<a+b))) +N c <N n +N n
|
||||
p1 = identityOfIndiscernablesLeft _ _ _ _<N_ (additionPreservesInequalityOnLeft n pr2) (Semiring.+Associative ℕSemiring n _ c)
|
||||
p1' : (a +N b) +N c <N n +N n
|
||||
p1' = identityOfIndiscernablesLeft _ _ _ _<N_ p1 (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
p2 : n +N n <N a +N (subtractionNResult.result (-N (inl n<b+c)) +N n)
|
||||
p2 = identityOfIndiscernablesRight _ _ _ _<N_ (additionPreservesInequality n pr1) (equalityCommutative (Semiring.+Associative ℕSemiring a _ n))
|
||||
p2' : n +N n <N a +N (b +N c)
|
||||
p2' = identityOfIndiscernablesRight _ _ _ _<N_ p2 (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
p2'' : n +N n <N (a +N b) +N c
|
||||
p2'' = identityOfIndiscernablesRight _ _ _ _<N_ p2' (Semiring.+Associative ℕSemiring a b c)
|
||||
|
||||
help14 : {a b c n : ℕ} → (n<b+c : n <N b +N c) → (n<a+b : n <N a +N b) → (pr1 : n <N a +N subtractionNResult.result (-N (inl n<b+c))) → (pr2 : n <N subtractionNResult.result (-N (inl n<a+b)) +N c) → subtractionNResult.result (-N (inl pr1)) ≡ subtractionNResult.result (-N (inl pr2))
|
||||
help14 {a} {b} {c} {n} n<b+c n<a+b pr1 pr2 = equivalentSubtraction _ _ _ _ pr1 pr2 (transitivity (Semiring.+Associative ℕSemiring n _ c) (transitivity (applyEquality (_+N c) (addMinus' (inl n<a+b))) (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring a b c)) (equalityCommutative p2))))
|
||||
where
|
||||
p1 : (a +N subtractionNResult.result (-N (inl n<b+c))) +N n ≡ a +N (subtractionNResult.result (-N (inl n<b+c)) +N n)
|
||||
p1 = equalityCommutative (Semiring.+Associative ℕSemiring a _ n)
|
||||
p2 : (a +N subtractionNResult.result (-N (inl n<b+c))) +N n ≡ a +N (b +N c)
|
||||
p2 = identityOfIndiscernablesRight _ _ _ _≡_ p1 (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
|
||||
help13 : {a b c n : ℕ} → (n<b+c : n <N b +N c) → (n<a+b : n <N a +N b) → (n <N a +N subtractionNResult.result (-N (inl n<b+c))) → (subtractionNResult.result (-N (inl n<a+b)) +N c ≡ n) → False
|
||||
help13 {a} {b} {c} {n} n<b+c n<a+b pr1 pr2 = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _ _ _ _<N_ lemm1' lemm3)
|
||||
where
|
||||
lemm1 : n +N n <N a +N (subtractionNResult.result (-N (inl n<b+c)) +N n)
|
||||
lemm1 = identityOfIndiscernablesRight _ _ _ _<N_ (additionPreservesInequality n pr1) (equalityCommutative (Semiring.+Associative ℕSemiring a _ n))
|
||||
lemm1' : n +N n <N a +N (b +N c)
|
||||
lemm1' = identityOfIndiscernablesRight _ _ _ _<N_ lemm1 (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
lemm2 : (n +N subtractionNResult.result (-N (inl n<a+b))) +N c ≡ n +N n
|
||||
lemm2 = identityOfIndiscernablesLeft _ _ _ _≡_ (applyEquality (n +N_) pr2) (Semiring.+Associative ℕSemiring n _ c)
|
||||
lemm2' : (a +N b) +N c ≡ n +N n
|
||||
lemm2' = identityOfIndiscernablesLeft _ _ _ _≡_ lemm2 (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
lemm3 : a +N (b +N c) ≡ n +N n
|
||||
lemm3 rewrite Semiring.+Associative ℕSemiring a b c = lemm2'
|
||||
|
||||
help12 : {a b c n : ℕ} → (n<b+c : n <N b +N c) → (n<a+b : n <N a +N b) → (a +N subtractionNResult.result (-N (inl n<b+c))) ≡ n → subtractionNResult.result (-N (inl n<a+b)) +N c <N n → False
|
||||
help12 {a} {b} {c} {n} n<b+c n<a+b pr1 pr2 = TotalOrder.irreflexive ℕTotalOrder lemm4
|
||||
where
|
||||
pr : {a b c : ℕ} → a +N (b +N c) ≡ b +N (a +N c)
|
||||
pr {a} {b} {c} rewrite Semiring.+Associative ℕSemiring a b c | Semiring.commutative ℕSemiring a b | equalityCommutative (Semiring.+Associative ℕSemiring b a c) = refl
|
||||
lemm1 : (n +N subtractionNResult.result (-N (inl n<a+b))) +N c <N n +N n
|
||||
lemm1 = identityOfIndiscernablesLeft _ _ _ _<N_ (additionPreservesInequalityOnLeft n pr2) (Semiring.+Associative ℕSemiring n _ c)
|
||||
lemm2 : (a +N b) +N c <N n +N n
|
||||
lemm2 = identityOfIndiscernablesLeft _ _ _ _<N_ lemm1 (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
lemm1' : a +N (subtractionNResult.result (-N (inl n<b+c)) +N n) ≡ n +N n
|
||||
lemm1' = identityOfIndiscernablesLeft _ _ _ _≡_ (applyEquality (_+N n) pr1) (equalityCommutative (Semiring.+Associative ℕSemiring a _ n))
|
||||
lemm2' : a +N (b +N c) ≡ n +N n
|
||||
lemm2' = identityOfIndiscernablesLeft _ _ _ _≡_ lemm1' (applyEquality (a +N_) (addMinus (inl n<b+c)))
|
||||
lemm3 : (a +N b) +N c ≡ n +N n
|
||||
lemm3 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = lemm2'
|
||||
lemm4 : (a +N b) +N c <N (a +N b) +N c
|
||||
lemm4 = identityOfIndiscernablesRight _ _ _ _<N_ lemm2 (equalityCommutative lemm3)
|
||||
|
||||
help11 : {a b c n : ℕ} → (a <N n) → (b +N c ≡ n) → (n<a+b : n <N a +N b) → (n <N subtractionNResult.result (-N (inl n<a+b)) +N c) → False
|
||||
help11 {a} {b} {c} {n} a<n b+c=n n<a+b pr1 = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive a<n lemm5)
|
||||
where
|
||||
pr : {a b c : ℕ} → a +N (b +N c) ≡ b +N (a +N c)
|
||||
pr {a} {b} {c} rewrite Semiring.+Associative ℕSemiring a b c | Semiring.commutative ℕSemiring a b | equalityCommutative (Semiring.+Associative ℕSemiring b a c) = refl
|
||||
lemm : n +N n <N (n +N subtractionNResult.result (-N (inl n<a+b))) +N c
|
||||
lemm = identityOfIndiscernablesRight _ _ _ _<N_ (additionPreservesInequalityOnLeft n pr1) (Semiring.+Associative ℕSemiring n _ c)
|
||||
lemm2 : n +N n <N (a +N b) +N c
|
||||
lemm2 = identityOfIndiscernablesRight _ _ _ _<N_ lemm (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
lemm3 : n +N n <N a +N (b +N c)
|
||||
lemm3 = identityOfIndiscernablesRight _ _ _ _<N_ lemm2 (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
|
||||
lemm4 : n +N n <N a +N n
|
||||
lemm4 = identityOfIndiscernablesRight _ _ _ _<N_ lemm3 (applyEquality (a +N_) b+c=n)
|
||||
lemm5 : n <N a
|
||||
lemm5 = subtractionPreservesInequality n lemm4
|
||||
|
||||
help10 : {a b c n : ℕ} → (n<b+c : n <N b +N c) → (n<a+b : n <N a +N b) → (a +N subtractionNResult.result (-N (inl n<b+c)) ≡ n) → (n <N subtractionNResult.result (-N (inl n<a+b)) +N c) → False
|
||||
help10 {a} {b} {c} {n} n<b+c n<a+b pr1 pr2 = TotalOrder.irreflexive ℕTotalOrder lemm6
|
||||
where
|
||||
pr : {a b c : ℕ} → a +N (b +N c) ≡ b +N (a +N c)
|
||||
pr {a} {b} {c} rewrite Semiring.+Associative ℕSemiring a b c | Semiring.commutative ℕSemiring a b | equalityCommutative (Semiring.+Associative ℕSemiring b a c) = refl
|
||||
lemm : a +N (n +N subtractionNResult.result (-N (inl n<b+c))) ≡ n +N n
|
||||
lemm = identityOfIndiscernablesLeft _ _ _ _≡_ (applyEquality (n +N_) pr1) (pr {n} {a})
|
||||
lemm2 : a +N (b +N c) ≡ n +N n
|
||||
lemm2 = identityOfIndiscernablesLeft _ _ _ _≡_ lemm (applyEquality (a +N_) (addMinus' (inl n<b+c)))
|
||||
lemm3 : n +N n <N (n +N subtractionNResult.result (-N (inl n<a+b))) +N c
|
||||
lemm3 = identityOfIndiscernablesRight _ _ _ _<N_ (additionPreservesInequalityOnLeft n pr2) (Semiring.+Associative ℕSemiring n _ c)
|
||||
lemm4 : n +N n <N (a +N b) +N c
|
||||
lemm4 = identityOfIndiscernablesRight _ _ _ _<N_ lemm3 (applyEquality (_+N c) (addMinus' (inl n<a+b)))
|
||||
lemm5 : n +N n <N a +N (b +N c)
|
||||
lemm5 = identityOfIndiscernablesRight _ _ _ _<N_ lemm4 (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
|
||||
lemm6 : a +N (b +N c) <N a +N (b +N c)
|
||||
lemm6 = identityOfIndiscernablesLeft _ _ _ _<N_ lemm5 (equalityCommutative lemm2)
|
||||
|
||||
help9 : {a n : ℕ} → (a +N 0 ≡ n) → (a <N n) → False
|
||||
help9 {a} {n} n=a+0 a<n rewrite Semiring.commutative ℕSemiring a 0 | n=a+0 = TotalOrder.irreflexive ℕTotalOrder a<n
|
||||
|
||||
help8 : {a n : ℕ} → (n <N a +N 0) → (a <N n) → False
|
||||
help8 {a} {n} n<a+0 a<n rewrite Semiring.commutative ℕSemiring a 0 = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive a<n n<a+0)
|
||||
|
||||
help6 : {a b c n : ℕ} → (b +N c ≡ n) → (n<a+b : n <N a +N b) → (a +N 0 ≡ subtractionNResult.result (-N (inl n<a+b)) +N c)
|
||||
help6 {a} {b} {c} {n} b+c=n n<a+b rewrite Semiring.commutative ℕSemiring a 0 = canSubtractFromEqualityLeft {n} lem'
|
||||
where
|
||||
lem : n +N a ≡ (n +N subtractionNResult.result (-N (inl n<a+b))) +N c
|
||||
lem rewrite addMinus' (inl n<a+b) | equalityCommutative (Semiring.+Associative ℕSemiring a b c) | b+c=n = Semiring.commutative ℕSemiring n a
|
||||
lem' : n +N a ≡ n +N (subtractionNResult.result (-N (inl n<a+b)) +N c)
|
||||
lem' = identityOfIndiscernablesRight _ _ _ _≡_ lem (equalityCommutative (Semiring.+Associative ℕSemiring n _ c))
|
||||
|
||||
help5 : {a b c n : ℕ} → (n<b+c : n <N b +N c) → (n<a+b : n <N a +N b) → a +N subtractionNResult.result (-N (inl n<b+c)) ≡ subtractionNResult.result (-N (inl n<a+b)) +N c
|
||||
help5 {a} {b} {c} {n} n<b+c n<a+b = canSubtractFromEqualityLeft {n} lemma''
|
||||
where
|
||||
lemma : a +N (n +N subtractionNResult.result (-N (inl n<b+c))) ≡ (n +N subtractionNResult.result (-N (inl n<a+b))) +N c
|
||||
lemma rewrite addMinus' (inl n<b+c) | addMinus' (inl n<a+b) = Semiring.+Associative ℕSemiring a b c
|
||||
lemma' : a +N (n +N subtractionNResult.result (-N (inl n<b+c))) ≡ n +N (subtractionNResult.result (-N (inl n<a+b)) +N c)
|
||||
lemma' = identityOfIndiscernablesRight _ _ _ _≡_ lemma (equalityCommutative (Semiring.+Associative ℕSemiring n _ c))
|
||||
lemma'' : n +N (a +N subtractionNResult.result (-N (inl n<b+c))) ≡ n +N (subtractionNResult.result (-N (inl n<a+b)) +N c)
|
||||
lemma'' = identityOfIndiscernablesLeft _ _ _ _≡_ lemma' (pr {a} {n} {subtractionNResult.result (-N (inl n<b+c))})
|
||||
where
|
||||
pr : {a b c : ℕ} → a +N (b +N c) ≡ b +N (a +N c)
|
||||
pr {a} {b} {c} rewrite Semiring.+Associative ℕSemiring a b c | Semiring.commutative ℕSemiring a b | equalityCommutative (Semiring.+Associative ℕSemiring b a c) = refl
|
||||
|
||||
help4 : {a b c n : ℕ} → (n<a+'b+c : n <N a +N (b +N c)) → (n<a+b : n <N a +N b) → (subtractionNResult.result (-N (inl n<a+'b+c)) ≡ subtractionNResult.result (-N (inl n<a+b)) +N c)
|
||||
help4 {a} {b} {c} {n} n<a+'b+c n<a+b = canSubtractFromEqualityLeft lemma'
|
||||
where
|
||||
lemma : (n +N subtractionNResult.result (-N (inl n<a+'b+c))) ≡ (n +N subtractionNResult.result (-N (inl n<a+b))) +N c
|
||||
lemma rewrite addMinus' (inl n<a+'b+c) | addMinus' (inl n<a+b) = Semiring.+Associative ℕSemiring a b c
|
||||
lemma' : n +N subtractionNResult.result (-N (inl n<a+'b+c)) ≡ n +N (subtractionNResult.result (-N (inl n<a+b)) +N c)
|
||||
lemma' = identityOfIndiscernablesRight _ _ _ _≡_ lemma (equalityCommutative (Semiring.+Associative ℕSemiring n (subtractionNResult.result (-N (inl n<a+b))) c))
|
||||
|
||||
help3 : {a b c n : ℕ} → (a <N n) → (b <N n) → (c <N n) → (a +N b <N n) → (pr : n <N b +N c) → a +N subtractionNResult.result (-N (inl pr)) ≡ n → False
|
||||
help3 {a} {b} {c} {n} a<n b<n c<n a+b<n n<b+c pr = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive (inter4 inter3) c<n)
|
||||
where
|
||||
inter : a +N (n +N subtractionNResult.result (-N (inl n<b+c))) ≡ n +N n
|
||||
inter = identityOfIndiscernablesLeft _ _ _ _≡_ (applyEquality (n +N_) pr) (lemma n a (subtractionNResult.result (-N (inl n<b+c))))
|
||||
where
|
||||
lemma : (a b c : ℕ) → a +N (b +N c) ≡ b +N (a +N c)
|
||||
lemma a b c rewrite Semiring.+Associative ℕSemiring a b c | Semiring.+Associative ℕSemiring b a c = applyEquality (_+N c) (Semiring.commutative ℕSemiring a b)
|
||||
inter2 : n +N n ≡ a +N (b +N c)
|
||||
inter2 = equalityCommutative (identityOfIndiscernablesLeft _ _ _ _≡_ inter (applyEquality (a +N_) (addMinus' (inl n<b+c))))
|
||||
inter3 : n +N n <N n +N c
|
||||
inter3 rewrite inter2 | Semiring.+Associative ℕSemiring a b c = additionPreservesInequality c a+b<n
|
||||
inter4 : (n +N n <N n +N c) → n <N c
|
||||
inter4 pr rewrite Semiring.commutative ℕSemiring n c = subtractionPreservesInequality n pr
|
||||
|
||||
help2 : {a b c n : ℕ} → (sn<b+c : succ n <N b +N c) → (sn<a+b+c : succ n <N (a +N b) +N c) → a +N subtractionNResult.result (-N (inl sn<b+c)) ≡ subtractionNResult.result (-N (inl sn<a+b+c))
|
||||
help2 {a} {b} {c} {n} sn<b+c sn<a+b+c = res inter
|
||||
where
|
||||
inter : a +N (subtractionNResult.result (-N (inl sn<b+c)) +N succ n) ≡ subtractionNResult.result (-N (inl sn<a+b+c)) +N succ n
|
||||
inter rewrite addMinus (inl sn<b+c) | addMinus (inl sn<a+b+c) = Semiring.+Associative ℕSemiring a b c
|
||||
res : (a +N (subtractionNResult.result (-N (inl sn<b+c)) +N succ n) ≡ subtractionNResult.result (-N (inl sn<a+b+c)) +N succ n) → a +N subtractionNResult.result (-N (inl sn<b+c)) ≡ subtractionNResult.result (-N (inl sn<a+b+c))
|
||||
res pr = canSubtractFromEqualityRight {_} {succ n} (identityOfIndiscernablesLeft _ _ _ _≡_ pr (Semiring.+Associative ℕSemiring a (subtractionNResult.result (-N (inl sn<b+c))) (succ n)))
|
||||
|
||||
help1 : {a b c n : ℕ} → (sn<b+c : succ n <N b +N c) → (pr1 : succ n <N a +N subtractionNResult.result (-N (inl sn<b+c))) → (a +N b <N succ n) → (a <N succ n) → (b <N succ n) → (c <N succ n) → False
|
||||
help1 {a} {b} {c} {n} sn<b+c pr1 a+b<sn a<sn b<sn c<sn with -N (inl sn<b+c)
|
||||
help1 {a} {b} {c} {n} sn<b+c pr1 a+b<sn a<sn b<sn c<sn | record { result = b+c-sn ; pr = Prb+c-sn } = ans
|
||||
where
|
||||
b+c-nNonzero : b+c-sn ≡ 0 → False
|
||||
b+c-nNonzero pr rewrite (equalityCommutative Prb+c-sn) | pr | Semiring.commutative ℕSemiring n 0 = TotalOrder.irreflexive ℕTotalOrder sn<b+c
|
||||
2sn<a+b+c' : succ n +N succ n <N succ n +N (a +N b+c-sn)
|
||||
2sn<a+b+c' = additionPreservesInequalityOnLeft (succ n) pr1
|
||||
2sn<a+b+c'' : succ n +N succ n <N a +N (succ n +N b+c-sn)
|
||||
2sn<a+b+c'' rewrite Semiring.+Associative ℕSemiring a (succ n) b+c-sn | Semiring.commutative ℕSemiring a (succ n) | equalityCommutative (Semiring.+Associative ℕSemiring (succ n) a b+c-sn) = 2sn<a+b+c'
|
||||
eep : succ n +N succ n <N a +N (b +N c)
|
||||
eep rewrite equalityCommutative Prb+c-sn = 2sn<a+b+c''
|
||||
eep2 : a +N (b +N c) <N succ n +N c
|
||||
eep2 rewrite Semiring.+Associative ℕSemiring a b c = additionPreservesInequality c a+b<sn
|
||||
eep2' : a +N (b +N c) <N succ n +N succ n
|
||||
eep2' = orderIsTransitive eep2 (additionPreservesInequalityOnLeft (succ n) c<sn)
|
||||
ans : False
|
||||
ans = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive eep eep2')
|
||||
|
||||
plusZnAssociative : {n : ℕ} → {pr : 0 <N n} → (a b c : ℤn n pr) → a +n (b +n c) ≡ ((a +n b) +n c)
|
||||
plusZnAssociative {zero} {()}
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess} record { x = c ; xLess = cLess } with orderIsTotal (a +N b) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) with orderIsTotal ((a +N b) +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) with orderIsTotal (b +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inl b+c<sn) with orderIsTotal (a +N (b +N c)) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inl b+c<sn) | inl (inl a+'b+c<sn) = equalityZn _ _ (Semiring.+Associative ℕSemiring a b c)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inl b+c<sn) | inl (inr sn<a+'b+c) = exFalso (false {succ n} a+b+c<sn sn<a+'b+c)
|
||||
where
|
||||
false : {x : ℕ} → (a +N b) +N c <N succ n → succ n <N a +N (b +N c) → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr1 pr2)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inl b+c<sn) | inr sn=a+b+c = exFalso (false a+b+c<sn sn=a+b+c)
|
||||
where
|
||||
false : {x : ℕ} → (a +N b) +N c <N x → (a +N (b +N c)) ≡ x → False
|
||||
false p1 p2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | p2 = TotalOrder.irreflexive ℕTotalOrder p1
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) with orderIsTotal (a +N (b +N c)) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inl (inl _) with orderIsTotal (a +N subtractionNResult.result (-N (inl sn<b+c))) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inl (inl _) | inl (inl x) with -N (inl sn<b+c)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inl (inl a+'b+c<sn) | inl (inl x) | record { result = result ; pr = pr } = exFalso (false a+'b+c<sn pr)
|
||||
where
|
||||
false : a +N (b +N c) <N succ n → succ n +N result ≡ b +N c → False
|
||||
false pr1 pr2 rewrite equalityCommutative pr2 | Semiring.+Associative ℕSemiring a (succ n) result | Semiring.commutative ℕSemiring a (succ n) | equalityCommutative (Semiring.+Associative ℕSemiring (succ n) a result) = cannotAddAndEnlarge' pr1
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inl (inl _) | inl (inr x) with -N (inl sn<b+c)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inl (inl a+'b+c<sn) | inl (inr x) | record { result = result ; pr = pr } = exFalso false
|
||||
where
|
||||
lemma : a +N (succ n +N result) ≡ a +N (b +N c)
|
||||
lemma' : a +N (succ n +N result) <N succ n
|
||||
lemma'' : succ n +N (a +N result) <N succ n
|
||||
lemma'' = identityOfIndiscernablesLeft _ _ _ _<N_ lemma' (transitivity (Semiring.+Associative ℕSemiring a (succ n) result) (transitivity (applyEquality (λ t → t +N result) (Semiring.commutative ℕSemiring a (succ n))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ n) a result))))
|
||||
lemma = applyEquality (λ i → a +N i) pr
|
||||
lemma' rewrite lemma = a+'b+c<sn
|
||||
false : False
|
||||
false = cannotAddAndEnlarge' lemma''
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inl (inl _) | inr x with -N (inl sn<b+c)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inl (inl a+'b+c<sn) | inr x | record { result = result ; pr = pr } = exFalso false
|
||||
where
|
||||
lemma : a +N (succ n +N result) <N succ n
|
||||
lemma rewrite pr = a+'b+c<sn
|
||||
lemma' : succ n +N (a +N result) <N succ n
|
||||
lemma' = identityOfIndiscernablesLeft _ _ _ _<N_ lemma (transitivity (Semiring.+Associative ℕSemiring a (succ n) result) (transitivity (applyEquality (λ t → t +N result) (Semiring.commutative ℕSemiring a (succ n))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ n) a result))))
|
||||
false : False
|
||||
false = cannotAddAndEnlarge' lemma'
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inl (inr x) = equalityZn _ _ (exFalso (false {succ n} a+b+c<sn x))
|
||||
where
|
||||
false : {x : ℕ} → (a +N b) +N c <N succ n → succ n <N a +N (b +N c) → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr1 pr2)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inl (inr sn<b+c) | inr x = exFalso (false a+b+c<sn x)
|
||||
where
|
||||
false : (a +N b) +N c <N succ n → a +N (b +N c) ≡ succ n → False
|
||||
false pr1 pr2 rewrite equalityCommutative pr2 | equalityCommutative (Semiring.+Associative ℕSemiring a b c) = TotalOrder.irreflexive ℕTotalOrder pr1
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inl a+b+c<sn) | inr sn=b+c = exFalso (false a+b+c<sn sn=b+c)
|
||||
where
|
||||
false : (a +N b) +N c <N succ n → b +N c ≡ succ n → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr2 | Semiring.commutative ℕSemiring a (succ n) = cannotAddAndEnlarge' a+b+c<sn
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) with orderIsTotal (b +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inl b+c<sn) with orderIsTotal (a +N (b +N c)) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inl b+c<sn) | inl (inl a+'b+c<sn) = exFalso (false sn<a+b+c a+'b+c<sn)
|
||||
where
|
||||
false : (succ n <N (a +N b) +N c) → a +N (b +N c) <N succ n → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr1 pr2)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inl b+c<sn) | inl (inr sn<a+'b+c) = equalityZn _ _ ans
|
||||
where
|
||||
lemma : succ n +N ((a +N b) +N c) ≡ (a +N (b +N c)) +N succ n
|
||||
lemma rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = Semiring.commutative ℕSemiring (succ n) _
|
||||
ans : subtractionNResult.result (-N (inl sn<a+'b+c)) ≡ subtractionNResult.result (-N (inl sn<a+b+c))
|
||||
ans = equivalentSubtraction _ _ _ _ sn<a+'b+c sn<a+b+c lemma
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inl b+c<sn) | inr x = exFalso (false sn<a+b+c x)
|
||||
where
|
||||
false : succ n <N (a +N b) +N c → (a +N (b +N c)) ≡ succ n → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr2 = TotalOrder.irreflexive ℕTotalOrder sn<a+b+c
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inr sn<b+c) with orderIsTotal (a +N (b +N c)) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inr sn<b+c) | inl (inl a+b+c<sn) = exFalso (false sn<a+b+c a+b+c<sn)
|
||||
where
|
||||
false : succ n <N (a +N b) +N c → (a +N (b +N c)) <N succ n → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr1 pr2)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inr sn<b+c) | inl (inr _) with orderIsTotal (a +N subtractionNResult.result (-N (inl sn<b+c))) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inr sn<b+c) | inl (inr _) | inl (inl x) = equalityZn _ _ (help2 {a} {b} {c} {n} sn<b+c sn<a+b+c)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inr sn<b+c) | inl (inr _) | inl (inr x) = equalityZn _ _ (exFalso (help1 sn<b+c x a+b<sn aLess bLess cLess))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inr sn<b+c) | inl (inr _) | inr x = exFalso (help3 aLess bLess cLess a+b<sn sn<b+c x)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inl (inr sn<b+c) | inr a+b+c=sn = exFalso (false sn<a+b+c a+b+c=sn)
|
||||
where
|
||||
false : (succ n <N (a +N b) +N c) → (a +N (b +N c) ≡ succ n) → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr2 = TotalOrder.irreflexive ℕTotalOrder pr1
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inr sn=b+c with orderIsTotal (a +N (b +N c)) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inr sn=b+c | inl (inl x) = exFalso (false sn<a+b+c x)
|
||||
where
|
||||
false : succ n <N (a +N b) +N c → a +N (b +N c) <N succ n → False
|
||||
false p1 p2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive p1 p2)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inr sn=b+c | inl (inr _) with orderIsTotal (a +N 0) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inr sn=b+c | inl (inr _) | inl (inl x) = equalityZn _ _ (ans sn=b+c)
|
||||
where
|
||||
ans : b +N c ≡ succ n → a +N 0 ≡ subtractionNResult.result (-N (inl sn<a+b+c))
|
||||
ans pr with -N (inl sn<a+b+c)
|
||||
ans b+c=sn | record { result = result ; pr = pr1 } rewrite Semiring.commutative ℕSemiring a 0 | equalityCommutative (Semiring.+Associative ℕSemiring a b c) | b+c=sn | Semiring.commutative ℕSemiring (succ n) result = equalityCommutative (canSubtractFromEqualityRight pr1)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inr sn=b+c | inl (inr _) | inl (inr x) = exFalso (false b a+b<sn x)
|
||||
where
|
||||
false : (b : ℕ) → a +N b <N succ n → succ n <N a +N 0 → False
|
||||
false zero pr1 pr2 rewrite Semiring.commutative ℕSemiring a 0 = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr1 pr2)
|
||||
false (succ b) pr1 pr2 rewrite Semiring.commutative ℕSemiring a 0 = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr2 (orderIsTransitive (le b (Semiring.commutative ℕSemiring (succ b) a)) pr1))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inr sn=b+c | inl (inr _) | inr x = exFalso (false b a+b<sn x)
|
||||
where
|
||||
false : (b : ℕ) → a +N b <N succ n → a +N 0 ≡ succ n → False
|
||||
false zero pr1 pr2 rewrite pr2 = TotalOrder.irreflexive ℕTotalOrder pr1
|
||||
false (succ b) pr1 pr2 rewrite Semiring.commutative ℕSemiring a 0 | pr2 = cannotAddAndEnlarge' pr1
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inl (inr sn<a+b+c) | inr sn=b+c | inr x = exFalso (false sn<a+b+c x)
|
||||
where
|
||||
false : succ n <N (a +N b) +N c → a +N (b +N c) ≡ succ n → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr2 = TotalOrder.irreflexive ℕTotalOrder pr1
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c with orderIsTotal (b +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inl (inl b+c<sn) with orderIsTotal (a +N (b +N c)) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inl (inl b+c<sn) | inl (inl a+'b+c<sn) = exFalso (false sn=a+b+c a+'b+c<sn)
|
||||
where
|
||||
false : (a +N b) +N c ≡ succ n → a +N (b +N c) <N succ n → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr1 = TotalOrder.irreflexive ℕTotalOrder pr2
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inl (inl b+c<sn) | inl (inr sn<a+'b+c) = exFalso (false sn=a+b+c sn<a+'b+c)
|
||||
where
|
||||
false : (a +N b) +N c ≡ succ n → succ n <N a +N (b +N c) → False
|
||||
false pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr1 = TotalOrder.irreflexive ℕTotalOrder pr2
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inl (inl b+c<sn) | inr _ = equalityZn _ _ refl
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inl (inr sn<b+c) = exFalso (false a sn=a+b+c sn<b+c)
|
||||
where
|
||||
false : (a : ℕ) → (a +N b) +N c ≡ succ n → succ n <N b +N c → False
|
||||
false zero pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | equalityCommutative pr1 = TotalOrder.irreflexive ℕTotalOrder pr2
|
||||
false (succ a) pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | equalityCommutative pr1 = TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive pr2 (le a refl))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inr b+c=sn with orderIsTotal (a +N 0) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inr b+c=sn | inl (inl a+0<sn) = equalityZn _ _ ans
|
||||
where
|
||||
a=0 : (a : ℕ) → (a +N b) +N c ≡ succ n → b +N c ≡ succ n → a ≡ 0
|
||||
a=0 zero pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr2 = refl
|
||||
a=0 (succ a) pr1 pr2 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr2 = canSubtractFromEqualityRight pr1
|
||||
ans : a +N 0 ≡ 0
|
||||
ans rewrite Semiring.commutative ℕSemiring a 0 = a=0 a sn=a+b+c b+c=sn
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inr b+c=sn | inl (inr sn<a+0) = exFalso (false sn<a+0 sn=a+b+c b+c=sn)
|
||||
where
|
||||
false : succ n <N a +N 0 → (a +N b) +N c ≡ succ n → b +N c ≡ succ n → False
|
||||
false pr1 pr2 pr3 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr3 | Semiring.commutative ℕSemiring a 0 = zeroNeverGreater {succ n} (identityOfIndiscernablesRight _ _ _ _<N_ pr1 (a=0 a pr2))
|
||||
where
|
||||
a=0 : (a : ℕ) → (a +N succ n ≡ succ n) → a ≡ 0
|
||||
a=0 zero pr = refl
|
||||
a=0 (succ a) pr = canSubtractFromEqualityRight pr
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inl a+b<sn) | inr sn=a+b+c | inr b+c=sn | inr sn=a+0 = exFalso (false sn=a+b+c b+c=sn sn=a+0)
|
||||
where
|
||||
false : (a +N b) +N c ≡ succ n → b +N c ≡ succ n → a +N 0 ≡ succ n → False
|
||||
false pr1 pr2 pr3 rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | pr2 | equalityCommutative pr3 | Semiring.commutative ℕSemiring a 0 = naughtE (identityOfIndiscernablesLeft _ _ _ _≡_ pr3 (a=0 a pr1))
|
||||
where
|
||||
a=0 : (a : ℕ) → (a +N a ≡ a) → a ≡ 0
|
||||
a=0 zero pr = refl
|
||||
a=0 (succ a) pr = naughtE {_} {a} (equalityCommutative (canSubtractFromEqualityRight pr))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) with orderIsTotal (b +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inl b+c<sn) with orderIsTotal (a +N (b +N c)) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inl b+c<sn) | inl (inl a+'b+c<sn) = exFalso (false sn<a+b a+'b+c<sn)
|
||||
where
|
||||
false : succ n <N a +N b → a +N (b +N c) <N succ n → False
|
||||
false pr1 pr2 rewrite Semiring.+Associative ℕSemiring a b c = cannotAddAndEnlarge' (orderIsTransitive pr2 pr1)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inl b+c<sn) | inl (inr sn<a+'b+c) with orderIsTotal (subtractionNResult.result (-N (inl sn<a+b)) +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inl b+c<sn) | inl (inr sn<a+'b+c) | inl (inl x) = equalityZn _ _ (help4 {a} {b} {c} {succ n} sn<a+'b+c sn<a+b)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inl b+c<sn) | inl (inr sn<a+'b+c) | inl (inr x) = exFalso (help18 {a} {b} {c} {succ n} b+c<sn sn<a+b aLess x)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inl b+c<sn) | inl (inr sn<a+'b+c) | inr x = exFalso (help19 {a} {b} {c} {succ n} b+c<sn sn<a+b aLess x)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inl b+c<sn) | inr a+'b+c=sn = exFalso (false sn<a+b a+'b+c=sn)
|
||||
where
|
||||
false : (succ n <N a +N b) → a +N (b +N c) ≡ succ n → False
|
||||
false pr1 pr2 rewrite Semiring.+Associative ℕSemiring a b c | equalityCommutative pr2 = cannotAddAndEnlarge' pr1
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) with orderIsTotal (a +N subtractionNResult.result (-N (inl sn<b+c))) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inl (inl x) with orderIsTotal (subtractionNResult.result (-N (inl sn<a+b)) +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inl (inl x) | inl (inl x₁) = equalityZn _ _ (help5 {a} {b} {c} {succ n} sn<b+c sn<a+b)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inl (inl x) | inl (inr x1) = equalityZn _ _ (help16 {a} {b} {c} {succ n} sn<b+c sn<a+b x x1)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inl (inl x) | inr x1 = exFalso (help17 {a} {b} {c} {succ n} sn<b+c sn<a+b x x1)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inl (inr x) with orderIsTotal (subtractionNResult.result (-N (inl sn<a+b)) +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inl (inr x) | inl (inl x1) = equalityZn _ _ (exFalso (help15 {a} {b} {c} {succ n} sn<b+c sn<a+b x x1))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inl (inr x) | inl (inr x1) = equalityZn _ _ (help14 {a} {b} {c} {succ n} sn<b+c sn<a+b x x1)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inl (inr x) | inr x1 = equalityZn _ _ (exFalso (help13 {a} {b} {c} {succ n} sn<b+c sn<a+b x x1))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inr x with orderIsTotal (subtractionNResult.result (-N (inl sn<a+b)) +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inr x | inl (inl x1) = equalityZn _ _ (exFalso (help12 {a} {b} {c} {succ n} sn<b+c sn<a+b x x1))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inr x | inl (inr x1) = equalityZn _ _ (exFalso (help10 {a} {b} {c} {succ n} sn<b+c sn<a+b x x1))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inl (inr sn<b+c) | inr x | inr x₁ = equalityZn _ _ refl
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inr b+c=sn with orderIsTotal (a +N 0) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inr b+c=sn | inl (inl a+0<sn) with orderIsTotal (subtractionNResult.result (-N (inl sn<a+b)) +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inr b+c=sn | inl (inl a+0<sn) | inl (inl x) = equalityZn _ _ (help6 {a} {b} {c} {succ n} b+c=sn sn<a+b)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inr b+c=sn | inl (inl _) | inl (inr x) = equalityZn _ _ (exFalso (help11 {a} {b} {c} {succ n} aLess b+c=sn sn<a+b x))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inr b+c=sn | inl (inl a+0<sn) | inr x = equalityZn _ _ (exFalso (help7 {a} {b} {c} {succ n} b+c=sn aLess sn<a+b x))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inr b+c=sn | inl (inr sn<a+0) = exFalso (help8 {a} {succ n} sn<a+0 aLess)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inl (inr sn<a+b) | inr b+c=sn | inr a+0=sn = exFalso (help9 {a} {succ n} a+0=sn aLess)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b with orderIsTotal c (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) with orderIsTotal (b +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inl (inl b+c<sn) with orderIsTotal (a +N (b +N c)) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inl (inl b+c<sn) | inl (inl a+'b+c<sn) = equalityZn _ _ (help27 {a} {b} {c} {n} sn=a+b a+'b+c<sn)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inl (inl b+c<sn) | inl (inr sn<a+'b+c) = equalityZn _ _ (help28 {a} {b} {c} {succ n} sn<a+'b+c sn=a+b)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inl (inl b+c<sn) | inr a+'b+c=sn = equalityZn _ _ (help26 {a} {b} {c} {succ n} sn=a+b a+'b+c=sn)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inl (inr sn<b+c) with orderIsTotal (a +N subtractionNResult.result (-N (inl sn<b+c))) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inl (inr sn<b+c) | inl (inl x) = equalityZn _ _ (help31 {a} {b} {c} {succ n} sn=a+b sn<b+c)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inl (inr sn<b+c) | inl (inr x) = exFalso (help30 {a} {b} {c} {succ n} cLess sn=a+b sn<b+c x)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inl (inr sn<b+c) | inr x = exFalso (help29 {a} {b} {c} {succ n} cLess sn<b+c x sn=a+b)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inr b+c=sn with orderIsTotal (a +N 0) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inr b+c=sn | inl (inl a+0<sn) = equalityZn _ _ (help25 {a} {b} {c} {succ n} sn=a+b b+c=sn)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inr b+c=sn | inl (inr sn<a+0) = exFalso (help24 {a} {succ n} aLess sn<a+0)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inl c<sn) | inr b+c=sn | inr a+0=sn = exFalso (help23 {a} {succ n} aLess a+0=sn)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inl (inr sn<c) = exFalso (TotalOrder.irreflexive ℕTotalOrder (orderIsTransitive sn<c cLess))
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inr c=sn with orderIsTotal (b +N c) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inr c=sn | inl (inl b+c<sn) = exFalso (help b+c<sn)
|
||||
where
|
||||
help : (b +N c <N succ n) → False
|
||||
help b+c<sn rewrite equalityCommutative c=sn | Semiring.commutative ℕSemiring b c = cannotAddAndEnlarge' b+c<sn
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inr c=sn | inl (inr sn<b+c) with orderIsTotal (a +N subtractionNResult.result (-N (inl sn<b+c))) (succ n)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inr c=sn | inl (inr sn<b+c) | inl (inl x) = exFalso (help20 {a} {b} {c} {succ n} c=sn sn=a+b sn<b+c x)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inr c=sn | inl (inr sn<b+c) | inl (inr x) = exFalso (help22 {a} {b} {c} {succ n} sn=a+b c=sn sn<b+c x)
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inr c=sn | inl (inr sn<b+c) | inr x = equalityZn _ _ refl
|
||||
plusZnAssociative {succ n} {_} record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } | inr sn=a+b | inr c=sn | inr b+c=sn = exFalso (help21 {a} {b} {c} {succ n} sn=a+b b+c=sn c=sn aLess)
|
||||
|
||||
subLess : {a b : ℕ} → (0<a : 0 <N a) → (a<b : a <N b) → subtractionNResult.result (-N (inl a<b)) <N b
|
||||
subLess {zero} {b} 0<a a<b = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
|
||||
subLess {succ a} {b} _ a<b with -N (inl a<b)
|
||||
... | record { result = b-a ; pr = pr } = record { x = a ; proof = pr }
|
||||
|
||||
inverseZn : {n : ℕ} → {pr : 0 <N n} → (a : ℤn n pr) → Sg (ℤn n pr) (λ i → i +n a ≡ record { x = 0 ; xLess = pr } )
|
||||
inverseZn {zero} {()}
|
||||
inverseZn {succ n} {0<n} record { x = zero ; xLess = zeroLess } = record { x = zero ; xLess = zeroLess } , plusZnIdentityLeft _
|
||||
inverseZn {succ n} {0<n} record { x = (succ a) ; xLess = aLess } = ans , pr
|
||||
where
|
||||
ans = record { x = subtractionNResult.result (-N (inl (subtractOneFromInequality aLess))) ; xLess = subLess (succIsPositive a) aLess }
|
||||
pr : ans +n record { x = (succ a) ; xLess = aLess } ≡ record { x = 0 ; xLess = 0<n }
|
||||
pr with orderIsTotal (subtractionNResult.result (-N (inl (subtractOneFromInequality aLess))) +N (succ a)) (succ n)
|
||||
... | inl (inl x) = exFalso f
|
||||
where
|
||||
h : subtractionNResult.result (-N (inl (le (_<N_.x aLess) (transitivity (equalityCommutative (succExtracts (_<N_.x aLess) a)) (succInjective (_<N_.proof aLess)))))) +N succ a ≡ succ n
|
||||
h = addMinus {succ a} {succ n} (inl aLess)
|
||||
f : False
|
||||
f rewrite h = TotalOrder.irreflexive ℕTotalOrder x
|
||||
... | inl (inr x) = exFalso f
|
||||
where
|
||||
h : subtractionNResult.result (-N (inl (subtractOneFromInequality aLess))) +N succ a ≡ succ n
|
||||
h = addMinus {succ a} {succ n} (inl aLess)
|
||||
f : False
|
||||
f rewrite h = TotalOrder.irreflexive ℕTotalOrder x
|
||||
... | (inr n-a+sa=sn) = equalityZn _ _ refl
|
||||
|
||||
ℤnGroup : (n : ℕ) → (pr : 0 <N n) → Group (reflSetoid (ℤn n pr)) _+n_
|
||||
ℤnGroup n pr = record { identity = record { x = 0 ; xLess = pr } ; inverse = λ a → underlying (inverseZn a) ; multAssoc = λ {a} {b} {c} → plusZnAssociative a b c ; multIdentRight = λ {a} → plusZnIdentityRight a ; multIdentLeft = λ {a} → plusZnIdentityLeft a ; invLeft = λ {a} → helpInvLeft a ; invRight = λ {a} → helpInvRight a ; wellDefined = reflGroupWellDefined }
|
||||
where
|
||||
helpInvLeft : (a : ℤn n pr) → underlying (inverseZn a) +n a ≡ record { x = 0 ; xLess = pr }
|
||||
helpInvLeft a with inverseZn a
|
||||
... | -a , pr-a = pr-a
|
||||
helpInvRight : (a : ℤn n pr) → a +n underlying (inverseZn a) ≡ record { x = 0 ; xLess = pr }
|
||||
helpInvRight a rewrite plusZnCommutative a (underlying (inverseZn a)) = helpInvLeft a
|
||||
|
||||
ℤnAbGroup : (n : ℕ) → (pr : 0 <N n) → AbelianGroup (ℤnGroup n pr)
|
||||
AbelianGroup.commutative (ℤnAbGroup n pr) {a} {b} = plusZnCommutative a b
|
||||
|
||||
ℤnFinite : (n : ℕ) → (pr : 0 <N n) → FiniteGroup (ℤnGroup n pr) (FinSet n)
|
||||
SetoidToSet.project (FiniteGroup.toSet (ℤnFinite n pr)) record { x = x ; xLess = xLess } = ofNat x xLess
|
||||
SetoidToSet.wellDefined (FiniteGroup.toSet (ℤnFinite n pr)) x y x=y rewrite x=y = refl
|
||||
Surjection.property (SetoidToSet.surj (FiniteGroup.toSet (ℤnFinite n pr))) b = record { x = toNat b ; xLess = toNatSmaller b } , ofNatToNat b
|
||||
SetoidToSet.inj (FiniteGroup.toSet (ℤnFinite zero ())) x y x=y
|
||||
SetoidToSet.inj (FiniteGroup.toSet (ℤnFinite (succ n) pr)) record { x = x ; xLess = xLess } record { x = y ; xLess = yLess } x=y = equalityZn _ _ b
|
||||
where
|
||||
b : x ≡ y
|
||||
b = ofNatInjective x y xLess yLess x=y
|
||||
FiniteSet.size (FiniteGroup.finite (ℤnFinite n pr)) = n
|
||||
FiniteSet.mapping (FiniteGroup.finite (ℤnFinite n pr)) = id
|
||||
FiniteSet.bij (FiniteGroup.finite (ℤnFinite n pr)) = idIsBijective
|
||||
268
Numbers/Primes/IntegerFactorisation.agda
Normal file
268
Numbers/Primes/IntegerFactorisation.agda
Normal file
@@ -0,0 +1,268 @@
|
||||
{-# OPTIONS --warning=error --safe #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Numbers.Naturals.Naturals
|
||||
open import Numbers.Naturals.Addition
|
||||
open import Numbers.Naturals.Order
|
||||
open import Numbers.Primes.PrimeNumbers
|
||||
open import WellFoundedInduction
|
||||
open import Semirings.Definition
|
||||
open import Orders
|
||||
|
||||
module Numbers.Primes.IntegerFactorisation where
|
||||
|
||||
-- Represent a factorisation into increasing factors
|
||||
-- Note that 0 cannot be expressed this way.
|
||||
record factorisationNonunit (minFactor : ℕ) (a : ℕ) : Set where
|
||||
inductive
|
||||
field
|
||||
1<a : 1 <N a
|
||||
firstFactor : ℕ
|
||||
firstFactorNontrivial : 1 <N firstFactor
|
||||
firstFactorBiggerMin : minFactor ≤N firstFactor
|
||||
firstFactorDivision : divisionAlgResult firstFactor a
|
||||
firstFactorDivides : divisionAlgResult.rem firstFactorDivision ≡ 0
|
||||
firstFactorPrime : Prime firstFactor
|
||||
otherFactorsNumber : ℕ
|
||||
otherFactors : ((divisionAlgResult.quot firstFactorDivision ≡ 1) && (otherFactorsNumber ≡ 0)) || (((1 <N divisionAlgResult.quot firstFactorDivision) && (factorisationNonunit firstFactor (divisionAlgResult.quot firstFactorDivision))))
|
||||
|
||||
lemma : (p : ℕ) → p *N 1 +N 0 ≡ p
|
||||
lemma p rewrite Semiring.sumZeroRight ℕSemiring (p *N 1) | Semiring.productOneRight ℕSemiring p = refl
|
||||
|
||||
lemma' : {a b : ℕ} → a *N zero +N 0 ≡ b → b ≡ zero
|
||||
lemma' {a} {b} pr rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | Semiring.productZeroRight ℕSemiring a = equalityCommutative pr
|
||||
|
||||
primeFactorisation : {p : ℕ} → (pr : Prime p) → factorisationNonunit 1 p
|
||||
primeFactorisation {p} record { p>1 = p>1 ; pr = pr } = record {1<a = p>1 ; firstFactor = p ; firstFactorNontrivial = p>1 ; firstFactorBiggerMin = inl p>1 ; firstFactorDivision = record { quot = 1 ; rem = 0 ; pr = lemma p ; remIsSmall = zeroIsValidRem p ; quotSmall = inl (TotalOrder.transitive ℕTotalOrder (le zero refl) p>1) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = p>1 ; pr = pr} ; otherFactors = inl record { fst = refl ; snd = refl } ; otherFactorsNumber = 0 }
|
||||
where
|
||||
proof : (s : ℕ) → s *N 1 +N 0 ≡ s
|
||||
proof s rewrite Semiring.sumZeroRight ℕSemiring (s *N 1) | multiplicationNIsCommutative s 1 | Semiring.sumZeroRight ℕSemiring s = refl
|
||||
|
||||
twoAsFact : factorisationNonunit 2 2
|
||||
factorisationNonunit.1<a twoAsFact = succPreservesInequality (succIsPositive 0)
|
||||
factorisationNonunit.firstFactor twoAsFact = 2
|
||||
factorisationNonunit.firstFactorNontrivial twoAsFact = succPreservesInequality (succIsPositive 0)
|
||||
factorisationNonunit.firstFactorBiggerMin twoAsFact = inr refl
|
||||
factorisationNonunit.firstFactorDivision twoAsFact = record { quot = 1 ; rem = 0 ; remIsSmall = zeroIsValidRem 2 ; pr = refl ; quotSmall = inl (le 1 refl) }
|
||||
factorisationNonunit.firstFactorDivides twoAsFact = refl
|
||||
factorisationNonunit.firstFactorPrime twoAsFact = twoIsPrime
|
||||
factorisationNonunit.otherFactorsNumber twoAsFact = 0
|
||||
factorisationNonunit.otherFactors twoAsFact = inl record { fst = refl ; snd = refl }
|
||||
|
||||
fourFact : factorisationNonunit 1 4
|
||||
factorisationNonunit.1<a fourFact = succPreservesInequality (succIsPositive 2)
|
||||
factorisationNonunit.firstFactor fourFact = 2
|
||||
factorisationNonunit.firstFactorNontrivial fourFact = succPreservesInequality (succIsPositive 0)
|
||||
factorisationNonunit.firstFactorBiggerMin fourFact = inl (succPreservesInequality (succIsPositive 0))
|
||||
factorisationNonunit.firstFactorDivision fourFact = record { quot = 2 ; rem = 0 ; remIsSmall = zeroIsValidRem 2 ; pr = refl ; quotSmall = inl (le 1 refl) }
|
||||
factorisationNonunit.firstFactorDivides fourFact = refl
|
||||
factorisationNonunit.firstFactorPrime fourFact = twoIsPrime
|
||||
factorisationNonunit.otherFactorsNumber fourFact = 1
|
||||
factorisationNonunit.otherFactors fourFact = inr record { fst = succPreservesInequality (succIsPositive 0) ; snd = twoAsFact }
|
||||
|
||||
lessLemma : {y : ℕ} → (1 <N y) → (zero <N y)
|
||||
lessLemma {.(succ (x +N 1))} (le x refl) = succIsPositive (x +N 1)
|
||||
|
||||
canReduceFactorBound : {a i j : ℕ} → factorisationNonunit i a → j <N i → factorisationNonunit j a
|
||||
canReduceFactorBound {a} {i} {j} record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = inl ff<i ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors } j<i = record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = inl (lessTransitive j<i ff<i) ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors }
|
||||
canReduceFactorBound {a} {i} {j} record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = inr ff=i ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors } j<i = record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = inl (identityOfIndiscernablesRight j i firstFactor _<N_ j<i ff=i) ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors }
|
||||
|
||||
canReduceFactorBound' : {a i j : ℕ} → factorisationNonunit i a → j ≤N i → factorisationNonunit j a
|
||||
canReduceFactorBound' {a} {i} {j} factA (inl x) = canReduceFactorBound factA x
|
||||
canReduceFactorBound' {a} {i} {.i} factA (inr refl) = factA
|
||||
|
||||
canIncreaseFactorBound : {a i : ℕ} → (fact : factorisationNonunit 1 a) → (∀ x → 1 <N x → x <N i → x ∣ a → False) → (i ≤N factorisationNonunit.firstFactor fact) → factorisationNonunit i a
|
||||
canIncreaseFactorBound {a} {i} record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors } noSmaller iSmallEnough = record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = Prime.p>1 firstFactorPrime ; firstFactorBiggerMin = iSmallEnough ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors }
|
||||
|
||||
-- Get the smallest prime factor of the number
|
||||
everyNumberHasAPrimeFactor : {a : ℕ} → (1 <N a) → Sg ℕ (λ i → ((i ∣ a) && (1 <N i)) && ((Prime i) && (∀ x → x <N i → 1 <N x → x ∣ a → False)))
|
||||
everyNumberHasAPrimeFactor {a} 1<a with compositeOrPrime a 1<a
|
||||
everyNumberHasAPrimeFactor {a} 1<a | inl record { n>1 = n>1 ; divisor = divisor ; dividesN = dividesN ; divisorLessN = divisorLessN ; divisorNot1 = divisorNot1 ; divisorPrime = divisorPrime ; noSmallerDivisors = noSmallerDivisors } = ( divisor , record { fst = record { fst = dividesN ; snd = divisorNot1 } ; snd = record { fst = divisorPrime ; snd = noSmallerDivisors } } )
|
||||
everyNumberHasAPrimeFactor {a} 1<a | inr x = (a , record { fst = record { fst = aDivA a ; snd = 1<a } ; snd = record { fst = x ; snd = λ y y<a 1<y y|a → lessImpliesNotEqual 1<y (equalityCommutative (Prime.pr x y|a y<a (lessLemma 1<y))) }} )
|
||||
|
||||
lemma2 : {a b c : ℕ} → 1 <N a → 0 <N b → a *N b +N 0 ≡ c → b <N c
|
||||
lemma2 {zero} {b} {c} 1<a _ pr = exFalso (zeroNeverGreater 1<a)
|
||||
lemma2 {succ zero} {b} {c} 1<a _ pr = exFalso (lessIrreflexive 1<a)
|
||||
lemma2 {succ (succ a)} {zero} {zero} 1<a t pr = exFalso (lessIrreflexive t)
|
||||
lemma2 {succ (succ a)} {zero} {succ c} 1<a t pr = succIsPositive c
|
||||
lemma2 {succ (succ a)} {succ b} {c} 1<a t pr = le (b +N (a *N succ b)) go
|
||||
where
|
||||
assocLemm : (a b c : ℕ) → (a +N b) +N c ≡ (a +N c) +N b
|
||||
assocLemm a b c rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | Semiring.commutative ℕSemiring b c | Semiring.+Associative ℕSemiring a c b = refl
|
||||
go : succ ((b +N a *N succ b) +N succ b) ≡ c
|
||||
go rewrite Semiring.sumZeroRight ℕSemiring (succ (b +N succ (b +N a *N succ b))) | equalityCommutative (assocLemm b (succ b) (a *N succ b)) | Semiring.+Associative ℕSemiring b (succ b) (a *N succ b) = pr
|
||||
|
||||
factorIntegerLemma : (x : ℕ) (indHyp : (y : ℕ) (y<x : y <N x) → ((y <N 2) || (factorisationNonunit 1 y))) → ((x <N 2) || (factorisationNonunit 1 x))
|
||||
factorIntegerLemma zero indHyp = inl (succIsPositive 1)
|
||||
factorIntegerLemma (succ zero) indHyp = inl (succPreservesInequality (succIsPositive 0))
|
||||
factorIntegerLemma (succ (succ x)) indHyp with everyNumberHasAPrimeFactor {succ (succ x)} (succPreservesInequality (succIsPositive x))
|
||||
factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = zero ; rem = .0 ; pr = ssxDivA ; remIsSmall = r } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | multiplicationNIsCommutative a 0 = naughtE ssxDivA
|
||||
factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = succ zero ; rem = .0 ; pr = ssxDivA ; remIsSmall = r } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } = inr record { 1<a = succPreservesInequality (succIsPositive x) ; firstFactor = a ; firstFactorNontrivial = Prime.p>1 primeA ; firstFactorBiggerMin = inl (Prime.p>1 primeA) ; firstFactorDivision = record { quot = 1 ; rem = 0 ; pr = ssxDivA ; remIsSmall = r ; quotSmall = inl (TotalOrder.transitive ℕTotalOrder (le zero refl) 1<a) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = Prime.p>1 primeA ; pr = Prime.pr primeA } ; otherFactors = inl record { fst = refl ; snd = refl } ; otherFactorsNumber = 0 }
|
||||
|
||||
factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = succ (succ qu) ; rem = .0 ; pr = ssxDivA ; remIsSmall = remSmall } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } = inr record { 1<a = succPreservesInequality (succIsPositive x) ; firstFactor = a ; firstFactorNontrivial = Prime.p>1 primeA ; firstFactorBiggerMin = inl (Prime.p>1 primeA) ; firstFactorDivision = record { quot = succ (succ qu) ; rem = 0 ; pr = ssxDivA ; remIsSmall = remSmall ; quotSmall = inl (TotalOrder.transitive ℕTotalOrder (le zero refl) 1<a) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = Prime.p>1 primeA ; pr = Prime.pr primeA } ; otherFactors = inr record {fst = succPreservesInequality (succIsPositive qu) ; snd = factNonunit} ; otherFactorsNumber = succ (factorisationNonunit.otherFactorsNumber indHypRes') }
|
||||
where
|
||||
indHypRes : ((succ (succ qu)) <N 2) || factorisationNonunit 1 (succ (succ qu))
|
||||
indHypRes = indHyp (succ (succ qu)) (lemma2 {a} {succ (succ qu)} {succ (succ x)} 1<a (succIsPositive (succ qu)) ssxDivA)
|
||||
indHypRes' : factorisationNonunit 1 (succ (succ qu))
|
||||
indHypRes' with indHypRes
|
||||
indHypRes' | inl y = exFalso (zeroNeverGreater (canRemoveSuccFrom<N (canRemoveSuccFrom<N y)))
|
||||
indHypRes' | inr y = y
|
||||
z|ssx : (z : ℕ) → z ∣ succ (succ qu) → z ∣ succ (succ x)
|
||||
z|ssx z z|ssq = (divisibilityTransitive z|ssq (divides (record { quot = a ; rem = 0 ; pr = identityOfIndiscernablesLeft (a *N succ (succ qu) +N 0) (succ (succ x)) (succ (succ qu) *N a +N 0) _≡_ ssxDivA (applyEquality (λ t → t +N 0) (multiplicationNIsCommutative a (succ (succ qu)))) ; remIsSmall = zeroIsValidRem (succ (succ qu)) ; quotSmall = inl (succIsPositive _) }) refl))
|
||||
factNonunit : factorisationNonunit a (succ (succ qu))
|
||||
factNonunit with orderIsTotal a (factorisationNonunit.firstFactor indHypRes')
|
||||
factNonunit | inl (inl a<ff) = canIncreaseFactorBound indHypRes' (λ z 1<z z<a z|ssq → smallerFactors z z<a 1<z (z|ssx z z|ssq)) (inl a<ff)
|
||||
factNonunit | inl (inr ff<a) = exFalso (smallerFactors (factorisationNonunit.firstFactor indHypRes') ff<a (factorisationNonunit.firstFactorNontrivial indHypRes') (z|ssx (factorisationNonunit.firstFactor indHypRes') (divides (factorisationNonunit.firstFactorDivision indHypRes') (factorisationNonunit.firstFactorDivides indHypRes'))))
|
||||
factNonunit | inr ff=a = canIncreaseFactorBound indHypRes' (λ z 1<z z<a z|ssq → smallerFactors z z<a 1<z (divisibilityTransitive z|ssq (divides (record { quot = a ; rem = 0 ; pr = identityOfIndiscernablesLeft (a *N succ (succ qu) +N 0) (succ (succ x)) (succ (succ qu) *N a +N 0) _≡_ ssxDivA (applyEquality (λ t → t +N 0) (multiplicationNIsCommutative a (succ (succ qu)))) ; remIsSmall = zeroIsValidRem (succ (succ qu)) ; quotSmall = inl (succIsPositive _) }) refl))) (inr ff=a)
|
||||
|
||||
factorInteger : (a : ℕ) → (1 <N a) → factorisationNonunit 1 a
|
||||
factorInteger a 1<a with (rec <NWellfounded (λ n → (n <N 2) || (factorisationNonunit 1 n))) factorIntegerLemma
|
||||
... | bl with bl a
|
||||
factorInteger a 1<a | bl | inl x = exFalso (noIntegersBetweenXAndSuccX 1 1<a x)
|
||||
factorInteger a 1<a | bl | inr x = x
|
||||
|
||||
lessTransLemma : {p i j : ℕ} → p <N i → i ≤N j → p <N j
|
||||
lessTransLemma {p} {i} {j} p<i (inl x) = orderIsTransitive p<i x
|
||||
lessTransLemma {p} {i} {j} p<i (inr x) rewrite x = p<i
|
||||
|
||||
lemma4' : {quot rem b : ℕ} → (quot +N quot) +N rem ≡ succ b → quot <N succ b
|
||||
lemma4' {zero} {rem} {b} pr = succIsPositive b
|
||||
lemma4' {succ quot} {rem} {b} pr rewrite equalityCommutative (Semiring.+Associative ℕSemiring quot (succ quot) rem) = succPreservesInequality (le (quot +N rem) (succInjective (transitivity (applyEquality succ (Semiring.commutative ℕSemiring _ quot)) pr)))
|
||||
|
||||
lemma4 : {quot a rem b : ℕ} → (a *N quot +N rem ≡ succ b) → (1 <N a) → (quot <N succ b)
|
||||
lemma4 {quot} {zero} {rem} {b} pr 1<a = exFalso (zeroNeverGreater 1<a)
|
||||
lemma4 {quot} {succ zero} {rem} {b} pr 1<a = exFalso (lessIrreflexive 1<a)
|
||||
lemma4 {quot} {succ (succ zero)} {rem} {b} pr 1<a rewrite Semiring.sumZeroRight ℕSemiring quot = lemma4' pr
|
||||
lemma4 {quot} {succ (succ (succ a))} {rem} {b} pr 1<a = lemma4 {quot} {succ (succ a)} {quot +N rem} {b} p' (succPreservesInequality (succIsPositive a))
|
||||
where
|
||||
p' : (quot +N (quot +N a *N quot)) +N (quot +N rem) ≡ succ b
|
||||
p' rewrite Semiring.commutative ℕSemiring quot (quot +N (quot +N a *N quot)) | Semiring.+Associative ℕSemiring (quot +N (quot +N a *N quot)) quot rem = pr
|
||||
|
||||
noSmallerFactors : {a i p : ℕ} → (factorisationNonunit i a) → (Prime p) → (p <N i) → (p ∣ a) → False
|
||||
noSmallerFactors {a} {i} {p} factA pPrime p<i p|a with rec <NWellfounded (λ b → (factorisationNonunit i b) → p ∣ b → False)
|
||||
... | indHyp = (indHyp prf) a factA p|a
|
||||
where
|
||||
prf : (x : ℕ) (ind : (y : ℕ) (y<x : y <N x) (factY : factorisationNonunit i y) (p|y : p ∣ y) → False) (factX : factorisationNonunit i x) (p|x : p ∣ x) → False
|
||||
prf x ind record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = (inl record { fst = quotFirstfact=1 ; snd = otherFactorsNumber }) } p|x = cannotBeLeqAndG i<=firstFactor p<i
|
||||
where
|
||||
x=firstFact : firstFactor *N 1 +N 0 ≡ x
|
||||
x=firstFact rewrite equalityCommutative firstFactorDivides | equalityCommutative quotFirstfact=1 = divisionAlgResult.pr firstFactorDivision
|
||||
x=firstFact' : firstFactor ≡ x
|
||||
x=firstFact' = transitivity (equalityCommutative (lemma firstFactor)) x=firstFact
|
||||
p|firstFact : p ∣ firstFactor
|
||||
p|firstFact rewrite x=firstFact' = p|x
|
||||
p=firstFact : p ≡ firstFactor
|
||||
p=firstFact = primeDivPrimeImpliesEqual pPrime firstFactorPrime p|firstFact
|
||||
i<=firstFactor : i ≤N p
|
||||
i<=firstFactor rewrite p=firstFact = firstFactorBiggerMin
|
||||
prf zero ind record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = (inr otherFact) } p|x = zeroNeverGreater 1<a
|
||||
prf (succ x) ind record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = (inr otherFact) } p|x = ind (divisionAlgResult.quot firstFactorDivision) (lemma4 {divisionAlgResult.quot firstFactorDivision} {firstFactor} {divisionAlgResult.rem firstFactorDivision} {x} (divisionAlgResult.pr (firstFactorDivision)) (primesAreBiggerThanOne firstFactorPrime)) (canReduceFactorBound' (_&&_.snd otherFact) firstFactorBiggerMin) (p|q p|ffOrQ)
|
||||
where
|
||||
succXNotSmaller : succ x <N firstFactor → False
|
||||
succXNotSmaller = divisorIsSmaller {firstFactor} {x} (divides firstFactorDivision firstFactorDivides)
|
||||
succXNotSmaller' : firstFactor ≤N succ x
|
||||
succXNotSmaller' = notSmallerMeansGE succXNotSmaller
|
||||
inter : firstFactor *N (divisionAlgResult.quot firstFactorDivision) +N divisionAlgResult.rem firstFactorDivision ≡ (succ x)
|
||||
inter = divisionAlgResult.pr firstFactorDivision
|
||||
inter' : firstFactor *N (divisionAlgResult.quot firstFactorDivision) +N 0 ≡ (succ x)
|
||||
inter' rewrite equalityCommutative firstFactorDivides = inter
|
||||
inter'' : firstFactor *N (divisionAlgResult.quot firstFactorDivision) ≡ (succ x)
|
||||
inter'' rewrite equalityCommutative (Semiring.sumZeroRight ℕSemiring (firstFactor *N (divisionAlgResult.quot firstFactorDivision))) = inter'
|
||||
p|ff*q : p ∣ firstFactor *N (divisionAlgResult.quot firstFactorDivision)
|
||||
p|ff*q rewrite inter'' = p|x
|
||||
p|ffOrQ : (p ∣ firstFactor) || (p ∣ divisionAlgResult.quot firstFactorDivision)
|
||||
p|ffOrQ = primesArePrime pPrime p|ff*q
|
||||
p|ffIsFalse : (p ∣ firstFactor) → False
|
||||
p|ffIsFalse p|ff = lessIrreflexive (lessTransLemma p<i i<=p)
|
||||
where
|
||||
p=ff : p ≡ firstFactor
|
||||
p=ff = primeDivPrimeImpliesEqual pPrime firstFactorPrime p|ff
|
||||
i<=p : i ≤N p
|
||||
i<=p rewrite p=ff = firstFactorBiggerMin
|
||||
p|q : ((p ∣ firstFactor) || (p ∣ divisionAlgResult.quot firstFactorDivision)) → (p ∣ divisionAlgResult.quot firstFactorDivision)
|
||||
p|q (inl fls) = exFalso (p|ffIsFalse fls)
|
||||
p|q (inr res) = res
|
||||
|
||||
lemma3 : {a : ℕ} → a ≡ 0 → 1 <N a → False
|
||||
lemma3 {a} a=0 pr rewrite a=0 = zeroNeverGreater pr
|
||||
|
||||
firstFactorUniqueLemma : {i : ℕ} → (a : ℕ) → (1 <N a) → (f1 : factorisationNonunit i a) → (f2 : factorisationNonunit i a) → (factorisationNonunit.firstFactor f1 <N factorisationNonunit.firstFactor f2) → False
|
||||
firstFactorUniqueLemma {i} a 1<a f1 f2 ff1<ff2 = go
|
||||
where
|
||||
p1 = factorisationNonunit.firstFactor f1
|
||||
rem1 = divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f1)
|
||||
p2 = factorisationNonunit.firstFactor f2
|
||||
rem2 = divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f2)
|
||||
p1<p2 : p1 <N p2
|
||||
p1<p2 = ff1<ff2
|
||||
a=p2rem2 : a ≡ p2 *N rem2
|
||||
a=p2rem2 with divisionAlgResult.pr (factorisationNonunit.firstFactorDivision f2)
|
||||
... | ff rewrite factorisationNonunit.firstFactorDivides f2 | Semiring.sumZeroRight ℕSemiring (factorisationNonunit.firstFactor f2 *N divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f2)) = equalityCommutative ff
|
||||
p1|second : (p1 ∣ p2) || (p1 ∣ rem2)
|
||||
p1|second = primesArePrime {p1} {p2} {rem2} (factorisationNonunit.firstFactorPrime f1) lem
|
||||
where
|
||||
lem : p1 ∣ (p2 *N rem2)
|
||||
lem = identityOfIndiscernablesRight p1 a (p2 *N rem2) _∣_ (divides (factorisationNonunit.firstFactorDivision f1) (factorisationNonunit.firstFactorDivides f1)) a=p2rem2
|
||||
p1|second' : ((p1 ∣ p2) || (p1 ∣ rem2)) → ((p1 ≡ p2) || (p1 ∣ rem2))
|
||||
p1|second' (inl x) = inl (primeDivPrimeImpliesEqual (factorisationNonunit.firstFactorPrime f1) (factorisationNonunit.firstFactorPrime f2) x)
|
||||
p1|second' (inr x) = inr x
|
||||
p1|second'' : (p1 ≡ p2) || (p1 ∣ rem2)
|
||||
p1|second'' = p1|second' p1|second
|
||||
go : False
|
||||
go with p1|second''
|
||||
go | inl x = lessImpliesNotEqual ff1<ff2 x
|
||||
go | inr x with factorisationNonunit.otherFactors f2
|
||||
go | inr x | inl record { fst = rem2=1 ; snd = _ } rewrite rem2=1 = exFalso (oneIsNotPrime res)
|
||||
where
|
||||
1prime' : Prime p1 ≡ Prime 1
|
||||
1prime' = applyEquality Prime (oneHasNoDivisors x)
|
||||
res : Prime 1
|
||||
res rewrite equalityCommutative 1prime' = (factorisationNonunit.firstFactorPrime f1)
|
||||
go | inr x | inr p1|rem2 with factorisationNonunit.otherFactors f2
|
||||
go | inr x | inr p1|rem2 | inl record { fst = rem2=1 ; snd = _ } rewrite rem2=1 = exFalso (oneIsNotPrime res)
|
||||
where
|
||||
1prime' : Prime p1 ≡ Prime 1
|
||||
1prime' = applyEquality Prime (oneHasNoDivisors x)
|
||||
res : Prime 1
|
||||
res rewrite equalityCommutative 1prime' = (factorisationNonunit.firstFactorPrime f1)
|
||||
go | inr x | inr p1|rem2 | inr factorRem2 = noSmallerFactors (_&&_.snd factorRem2) (factorisationNonunit.firstFactorPrime f1) p1<p2 x
|
||||
|
||||
firstFactorUnique : {i : ℕ} → (a : ℕ) → (1 <N a) → (f1 : factorisationNonunit i a) → (f2 : factorisationNonunit i a) → (factorisationNonunit.firstFactor f1 ≡ factorisationNonunit.firstFactor f2)
|
||||
firstFactorUnique {i} a 1<a f1 f2 with orderIsTotal (factorisationNonunit.firstFactor f1) (factorisationNonunit.firstFactor f2)
|
||||
firstFactorUnique {i} a 1<a f1 f2 | inl (inl f1<f2) = exFalso (firstFactorUniqueLemma a 1<a f1 f2 f1<f2)
|
||||
firstFactorUnique {i} a 1<a f1 f2 | inl (inr f2<f1) = exFalso (firstFactorUniqueLemma a 1<a f2 f1 f2<f1)
|
||||
firstFactorUnique {i} a 1<a f1 f2 | inr x = x
|
||||
|
||||
factorListLemma : {i : ℕ} → (a : ℕ) → (1 <N a) → (f1 : factorisationNonunit i a) → (f2 : factorisationNonunit i a) → (divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f2)) ≡ (divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f1))
|
||||
factorListLemma {i} a 1<a f1 f2 with firstFactorUnique {i} a 1<a f1 f2
|
||||
... | firstFactEqual = res
|
||||
where
|
||||
div1 : divisionAlgResult (factorisationNonunit.firstFactor f1) a
|
||||
div1 = factorisationNonunit.firstFactorDivision f1
|
||||
rem1=0 : divisionAlgResult.rem div1 ≡ 0
|
||||
rem1=0 = factorisationNonunit.firstFactorDivides f1
|
||||
pr1 : (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1) +N 0 ≡ a
|
||||
pr1 rewrite equalityCommutative rem1=0 = divisionAlgResult.pr div1
|
||||
pr1' : (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1) ≡ a
|
||||
pr1' rewrite equalityCommutative (Semiring.sumZeroRight ℕSemiring ((factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1))) = pr1
|
||||
div2 : divisionAlgResult (factorisationNonunit.firstFactor f2) a
|
||||
div2 = factorisationNonunit.firstFactorDivision f2
|
||||
rem2=0 : divisionAlgResult.rem div2 ≡ 0
|
||||
rem2=0 = factorisationNonunit.firstFactorDivides f2
|
||||
pr2 : (factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2) +N 0 ≡ a
|
||||
pr2 rewrite equalityCommutative rem2=0 = divisionAlgResult.pr div2
|
||||
pr2' : (factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2) ≡ a
|
||||
pr2' rewrite equalityCommutative (Semiring.sumZeroRight ℕSemiring ((factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2))) = pr2
|
||||
pr : (factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2) ≡ (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1)
|
||||
pr = transitivity pr2' (equalityCommutative pr1')
|
||||
pr' : (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div2) ≡ (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1)
|
||||
pr' = identityOfIndiscernablesLeft ((factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2)) ((factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1)) ((factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div2)) _≡_ pr (applyEquality (λ t → t *N divisionAlgResult.quot div2) (equalityCommutative firstFactEqual))
|
||||
positive : zero <N factorisationNonunit.firstFactor f1
|
||||
positive = lessTransitive (succIsPositive 0) (factorisationNonunit.firstFactorNontrivial f1)
|
||||
res : divisionAlgResult.quot div2 ≡ divisionAlgResult.quot div1
|
||||
res = productCancelsLeft (factorisationNonunit.firstFactor f1) (divisionAlgResult.quot div2) (divisionAlgResult.quot div1) positive pr'
|
||||
|
||||
factorListSameLength : {i : ℕ} → (a : ℕ) → (1 <N a) → (f1 : factorisationNonunit i a) → (f2 : factorisationNonunit i a) → (divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f1) ≡ 1) → divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f2) ≡ 1
|
||||
factorListSameLength {i} a 1<a f1 f2 quot=1 with firstFactorUnique {i} a 1<a f1 f2
|
||||
... | firstFactEqual with factorListLemma {i} a 1<a f1 f2
|
||||
... | eq = transitivity eq quot=1
|
||||
782
Numbers/Primes/PrimeNumbers.agda
Normal file
782
Numbers/Primes/PrimeNumbers.agda
Normal file
@@ -0,0 +1,782 @@
|
||||
{-# OPTIONS --warning=error --safe #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Numbers.Naturals.Naturals
|
||||
open import Numbers.Naturals.Addition -- TODO - remove this dependency
|
||||
open import Numbers.Naturals.Multiplication -- TODO - remove this dependency
|
||||
open import Numbers.Naturals.Order -- TODO - remove this dependency
|
||||
open import Numbers.Naturals.WithK
|
||||
open import WellFoundedInduction
|
||||
open import KeyValue.KeyValue
|
||||
open import Orders
|
||||
open import Vectors
|
||||
open import Maybe
|
||||
open import WithK
|
||||
open import Semirings.Definition
|
||||
|
||||
module Numbers.Primes.PrimeNumbers where
|
||||
|
||||
record divisionAlgResult (a : ℕ) (b : ℕ) : Set where
|
||||
field
|
||||
quot : ℕ
|
||||
rem : ℕ
|
||||
pr : a *N quot +N rem ≡ b
|
||||
remIsSmall : (rem <N a) || (a ≡ 0)
|
||||
quotSmall : (0 <N a) || ((0 ≡ a) && (quot ≡ 0))
|
||||
|
||||
divAlgLessLemma : (a b : ℕ) → (0 <N a) → (r : divisionAlgResult a b) → (divisionAlgResult.quot r ≡ 0) || (divisionAlgResult.rem r <N b)
|
||||
divAlgLessLemma zero b pr _ = exFalso (TotalOrder.irreflexive ℕTotalOrder pr)
|
||||
divAlgLessLemma (succ a) b _ record { quot = zero ; rem = a%b ; pr = pr ; remIsSmall = remIsSmall } = inl refl
|
||||
divAlgLessLemma (succ a) b _ record { quot = (succ a/b) ; rem = a%b ; pr = pr ; remIsSmall = remIsSmall } = inr record { x = a/b +N a *N succ (a/b) ; proof = pr }
|
||||
|
||||
modUniqueLemma : {rem1 rem2 a : ℕ} → (quot1 quot2 : ℕ) → rem1 <N a → rem2 <N a → a *N quot1 +N rem1 ≡ a *N quot2 +N rem2 → rem1 ≡ rem2
|
||||
modUniqueLemma {rem1} {rem2} {a} zero zero rem1<a rem2<a pr rewrite Semiring.productZeroRight ℕSemiring a = pr
|
||||
modUniqueLemma {rem1} {rem2} {a} zero (succ quot2) rem1<a rem2<a pr rewrite Semiring.productZeroRight ℕSemiring a | pr | multiplicationNIsCommutative a (succ quot2) | equalityCommutative (Semiring.+Associative ℕSemiring a (quot2 *N a) rem2) = exFalso (cannotAddAndEnlarge' {a} {quot2 *N a +N rem2} rem1<a)
|
||||
modUniqueLemma {rem1} {rem2} {a} (succ quot1) zero rem1<a rem2<a pr rewrite Semiring.productZeroRight ℕSemiring a | equalityCommutative pr | multiplicationNIsCommutative a (succ quot1) | equalityCommutative (Semiring.+Associative ℕSemiring a (quot1 *N a) rem1) = exFalso (cannotAddAndEnlarge' {a} {quot1 *N a +N rem1} rem2<a)
|
||||
modUniqueLemma {rem1} {rem2} {a} (succ quot1) (succ quot2) rem1<a rem2<a pr rewrite multiplicationNIsCommutative a (succ quot1) | multiplicationNIsCommutative a (succ quot2) | equalityCommutative (Semiring.+Associative ℕSemiring a (quot1 *N a) rem1) | equalityCommutative (Semiring.+Associative ℕSemiring a (quot2 *N a) rem2) = modUniqueLemma {rem1} {rem2} {a} quot1 quot2 rem1<a rem2<a (go {a}{quot1}{rem1}{quot2}{rem2} pr)
|
||||
where
|
||||
go : {a quot1 rem1 quot2 rem2 : ℕ} → (a +N (quot1 *N a +N rem1) ≡ a +N (quot2 *N a +N rem2)) → a *N quot1 +N rem1 ≡ a *N quot2 +N rem2
|
||||
go {a} {quot1} {rem1} {quot2} {rem2} pr rewrite multiplicationNIsCommutative quot1 a | multiplicationNIsCommutative quot2 a = canSubtractFromEqualityLeft {a} pr
|
||||
|
||||
modIsUnique : {a b : ℕ} → (div1 div2 : divisionAlgResult a b) → divisionAlgResult.rem div1 ≡ divisionAlgResult.rem div2
|
||||
modIsUnique {zero} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = remIsSmall1 } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = remIsSmall } = transitivity pr1 (equalityCommutative pr)
|
||||
modIsUnique {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inl y) } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) } = modUniqueLemma {rem1} {rem} {succ a} quot1 quot y x (transitivity pr1 (equalityCommutative pr))
|
||||
modIsUnique {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inr ()) } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) }
|
||||
modIsUnique {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = remIsSmall1 } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr ()) }
|
||||
|
||||
transferAddition : (a b c : ℕ) → (a +N b) +N c ≡ (a +N c) +N b
|
||||
transferAddition a b c rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = p a b c
|
||||
where
|
||||
p : (a b c : ℕ) → a +N (b +N c) ≡ (a +N c) +N b
|
||||
p a b c = transitivity (applyEquality (a +N_) (Semiring.commutative ℕSemiring b c)) (Semiring.+Associative ℕSemiring a c b)
|
||||
|
||||
divisionAlgLemma : (x b : ℕ) → x *N zero +N b ≡ b
|
||||
divisionAlgLemma x b rewrite (Semiring.productZeroRight ℕSemiring x) = refl
|
||||
|
||||
divisionAlgLemma2 : (x b : ℕ) → (x ≡ b) → x *N succ zero +N zero ≡ b
|
||||
divisionAlgLemma2 x b pr rewrite (Semiring.productOneRight ℕSemiring x) = equalityCommutative (transitivity (equalityCommutative pr) (equalityCommutative (Semiring.sumZeroRight ℕSemiring x)))
|
||||
|
||||
divisionAlgLemma3 : {a x : ℕ} → (p : succ a <N succ x) → (subtractionNResult.result (-N (inl p))) <N (succ x)
|
||||
divisionAlgLemma3 {a} {x} p = -NIsDecreasing {a} {succ x} p
|
||||
|
||||
divisionAlgLemma4 : (p a q : ℕ) → ((p +N a *N p) +N q) +N succ a ≡ succ ((p +N a *N succ p) +N q)
|
||||
divisionAlgLemma4 p a q = ans
|
||||
where
|
||||
r : ((p +N a *N p) +N q) +N succ a ≡ succ (((p +N a *N p) +N q) +N a)
|
||||
ans : ((p +N a *N p) +N q) +N succ a ≡ succ ((p +N a *N succ p) +N q)
|
||||
s : ((p +N a *N p) +N q) +N a ≡ (p +N a *N succ p) +N q
|
||||
t : (p +N a *N p) +N a ≡ p +N a *N succ p
|
||||
s = transitivity (transferAddition (p +N a *N p) q a) (applyEquality (λ i → i +N q) t)
|
||||
ans = identityOfIndiscernablesRight (((p +N a *N p) +N q) +N succ a) (succ (((p +N a *N p) +N q) +N a)) (succ ((p +N a *N succ p) +N q)) _≡_ r (applyEquality succ s)
|
||||
r = succExtracts ((p +N a *N p) +N q) a
|
||||
t = transitivity (additionNIsAssociative p (a *N p) a) (applyEquality (λ n → p +N n) (equalityCommutative (aSucB a p)))
|
||||
|
||||
divisionAlg : (a : ℕ) → (b : ℕ) → divisionAlgResult a b
|
||||
divisionAlg zero = λ b → record { quot = zero ; rem = b ; pr = refl ; remIsSmall = inr refl ; quotSmall = inr (record { fst = refl ; snd = refl }) }
|
||||
divisionAlg (succ a) = rec <NWellfounded (λ n → divisionAlgResult (succ a) n) go
|
||||
where
|
||||
go : (x : ℕ) (indHyp : (y : ℕ) (y<x : y <N x) → divisionAlgResult (succ a) y) →
|
||||
divisionAlgResult (succ a) x
|
||||
go zero prop = record { quot = zero ; rem = zero ; pr = divisionAlgLemma (succ a) zero ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }
|
||||
go (succ x) indHyp with orderIsTotal (succ a) (succ x)
|
||||
go (succ x) indHyp | inl (inl sa<sx) with indHyp (subtractionNResult.result (-N (inl sa<sx))) (divisionAlgLemma3 sa<sx)
|
||||
... | record { quot = prevQuot ; rem = prevRem ; pr = prevPr ; remIsSmall = smallRem } = p
|
||||
where
|
||||
p : divisionAlgResult (succ a) (succ x)
|
||||
addedA : (succ a *N prevQuot +N prevRem) +N (succ a) ≡ subtractionNResult.result (-N (inl sa<sx)) +N (succ a)
|
||||
addedA' : (succ a *N prevQuot +N prevRem) +N succ a ≡ succ x
|
||||
addedA'' : (succ a *N succ prevQuot) +N prevRem ≡ succ x
|
||||
addedA''' : succ ((prevQuot +N a *N succ prevQuot) +N prevRem) ≡ succ x
|
||||
addedA''' = identityOfIndiscernablesLeft ((succ a *N succ prevQuot) +N prevRem) (succ x) (succ ((prevQuot +N a *N succ prevQuot) +N prevRem)) _≡_ addedA'' refl
|
||||
p = record { quot = succ prevQuot ; rem = prevRem ; pr = addedA''' ; remIsSmall = smallRem ; quotSmall = inl (succIsPositive a) }
|
||||
addedA = applyEquality (λ n → n +N succ a) prevPr
|
||||
addedA' = identityOfIndiscernablesRight ((succ a *N prevQuot +N prevRem) +N succ a) (subtractionNResult.result (-N (inl sa<sx)) +N (succ a)) (succ x) _≡_ addedA (addMinus {succ a} {succ x} (inl sa<sx))
|
||||
addedA'' = identityOfIndiscernablesLeft ((succ a *N prevQuot +N prevRem) +N succ a) (succ x) ((succ a *N succ prevQuot) +N prevRem) _≡_ addedA' (divisionAlgLemma4 prevQuot a prevRem)
|
||||
go (succ x) indHyp | inr (sa=sx) = record { quot = succ zero ; rem = zero ; pr = divisionAlgLemma2 (succ a) (succ x) sa=sx ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }
|
||||
go (succ x) indHyp | inl (inr (sx<sa)) = record { quot = zero ; rem = succ x ; pr = divisionAlgLemma (succ a) (succ x) ; remIsSmall = inl sx<sa ; quotSmall = inl (succIsPositive a) }
|
||||
|
||||
data _∣_ : ℕ → ℕ → Set where
|
||||
divides : {a b : ℕ} → (res : divisionAlgResult a b) → divisionAlgResult.rem res ≡ zero → a ∣ b
|
||||
|
||||
dividesEqualityLemma'' : {a b : ℕ} → (quot1 quot2 : ℕ) → (quot1 ≡ quot2) → (rem : ℕ) → (pr1 : (quot1 +N a *N quot1) +N rem ≡ b) → (pr2 : (quot2 +N a *N quot2) +N rem ≡ b) → (y : rem <N succ a) → (x1 : zero <N succ a) → record { quot = quot1 ; rem = rem ; pr = pr1 ; remIsSmall = inl y ; quotSmall = inl x1 } ≡ record { quot = quot2 ; rem = rem ; pr = pr2 ; remIsSmall = inl y ; quotSmall = inl x1}
|
||||
dividesEqualityLemma'' {a} {b} q1 .q1 refl rem pr1 pr2 y x1 rewrite reflRefl pr1 pr2 = refl
|
||||
|
||||
dividesEqualityLemma' : {a b : ℕ} → (quot1 quot2 : ℕ) → (rem : ℕ) → (pr1 : (quot1 +N a *N quot1) +N rem ≡ b) → (pr2 : (quot2 +N a *N quot2) +N rem ≡ b) → (y : rem <N succ a) → (y2 : rem <N succ a) → (x1 : zero <N succ a) → record { quot = quot1 ; rem = rem ; pr = pr1 ; remIsSmall = inl y ; quotSmall = inl x1 } ≡ record { quot = quot2 ; rem = rem ; pr = pr2 ; remIsSmall = inl y2 ; quotSmall = inl x1}
|
||||
dividesEqualityLemma' {a} {b} quot1 quot2 rem pr1 pr2 y y2 x1 rewrite <NRefl y2 y = dividesEqualityLemma'' quot1 quot2 (equalityCommutative lemm'') rem pr1 pr2 y x1
|
||||
where
|
||||
lemm : (succ a) *N quot2 +N rem ≡ (succ a) *N quot1 +N rem
|
||||
lemm rewrite equalityCommutative pr1 = pr2
|
||||
lemm' : (succ a) *N quot2 ≡ (succ a) *N quot1
|
||||
lemm' = canSubtractFromEqualityRight lemm
|
||||
lemm'' : quot2 ≡ quot1
|
||||
lemm'' = productCancelsLeft (succ a) quot2 quot1 (succIsPositive a) lemm'
|
||||
|
||||
dividesEqualityLemma : {a b : ℕ} → (quot1 quot2 : ℕ) → (rem1 rem2 : ℕ) → (pr1 : (quot1 +N a *N quot1) +N rem1 ≡ b) → (pr2 : (quot2 +N a *N quot2) +N rem2 ≡ b) → (rem1 ≡ rem2) → (y : rem1 <N succ a) → (y2 : rem2 <N succ a) → (x1 : zero <N succ a) → record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = inl y ; quotSmall = inl x1 } ≡ record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = inl y2 ; quotSmall = inl x1}
|
||||
dividesEqualityLemma {a} {b} quot1 quot2 rem1 rem2 pr1 pr2 remEq y y2 x1 rewrite remEq = dividesEqualityLemma' quot1 quot2 rem2 pr1 pr2 y y2 x1
|
||||
|
||||
dividesEqualityPr : {a b : ℕ} → (res1 res2 : divisionAlgResult a b) → res1 ≡ res2
|
||||
dividesEqualityPr {zero} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = remIsSmall1 ; quotSmall = (inl (le x ())) } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = remIsSmall2 ; quotSmall = quotSmall2 }
|
||||
dividesEqualityPr {zero} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = remIsSmall1 ; quotSmall = (inr (fst ,, snd)) } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = remIsSmall2 ; quotSmall = (inl (le x ())) }
|
||||
dividesEqualityPr {zero} {b} record { quot = .0 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inl (le x ())) ; quotSmall = (inr (refl ,, refl)) } record { quot = .0 ; rem = rem2 ; pr = pr2 ; remIsSmall = remIsSmall2 ; quotSmall = (inr (refl ,, refl)) }
|
||||
dividesEqualityPr {zero} {b} record { quot = .0 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inr refl) ; quotSmall = (inr (refl ,, refl)) } record { quot = .0 ; rem = rem2 ; pr = pr2 ; remIsSmall = (inl (le x ())) ; quotSmall = (inr (refl ,, refl)) }
|
||||
dividesEqualityPr {zero} {.rem1} record { quot = .0 ; rem = rem1 ; pr = refl ; remIsSmall = (inr refl) ; quotSmall = (inr (refl ,, refl)) } record { quot = .0 ; rem = .rem1 ; pr = refl ; remIsSmall = (inr refl) ; quotSmall = (inr (refl ,, refl)) } = refl
|
||||
|
||||
dividesEqualityPr {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inl y) ; quotSmall = (inl x) } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = (inl y2) ; quotSmall = (inl x1) } rewrite <NRefl x x1 = dividesEqualityLemma quot1 quot2 rem1 rem2 pr1 pr2 remsEqual y y2 x1
|
||||
where
|
||||
remsEqual : rem1 ≡ rem2
|
||||
remsEqual = modIsUnique (record { quot = quot1 ; rem = rem1 ; pr = pr1 ; quotSmall = (inl x) ; remIsSmall = (inl y) }) (record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = (inl y2) ; quotSmall = (inl x1) })
|
||||
dividesEqualityPr {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inl y) ; quotSmall = (inl x) } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = (inr ()) ; quotSmall = (inl x1) }
|
||||
dividesEqualityPr {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inr ()) ; quotSmall = (inl x) } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = remIsSmall2 ; quotSmall = (inl x1) }
|
||||
dividesEqualityPr {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = remIsSmall1 ; quotSmall = (inl x) } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = remIsSmall2 ; quotSmall = (inr (() ,, snd)) }
|
||||
dividesEqualityPr {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = remIsSmall1 ; quotSmall = (inr (() ,, snd)) } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = remIsSmall2 ; quotSmall = quotSmall2 }
|
||||
|
||||
dividesEquality : {a b : ℕ} → (res1 res2 : a ∣ b) → res1 ≡ res2
|
||||
dividesEquality (divides res1 x1) (divides res2 x2) rewrite dividesEqualityPr res1 res2 = applyEquality (λ i → divides res2 i) (reflRefl x1 x2)
|
||||
|
||||
data notDiv : ℕ → ℕ → Set where
|
||||
doesNotDivide : {a b : ℕ} → (res : divisionAlgResult a b) → 0 <N divisionAlgResult.rem res → notDiv a b
|
||||
|
||||
zeroDividesNothing : (a : ℕ) → zero ∣ succ a → False
|
||||
zeroDividesNothing a (divides record { quot = quot ; rem = rem ; pr = pr } x) = naughtE p
|
||||
where
|
||||
p : zero ≡ succ a
|
||||
p = transitivity (equalityCommutative x) pr
|
||||
|
||||
twoDividesFour : succ (succ zero) ∣ succ (succ (succ (succ zero)))
|
||||
twoDividesFour = divides {(succ (succ zero))} {succ (succ (succ (succ zero)))} (record { quot = succ (succ zero) ; rem = zero ; pr = refl ; remIsSmall = inl (succIsPositive 1) ; quotSmall = inl (succIsPositive 1) }) refl
|
||||
|
||||
record Prime (p : ℕ) : Set where
|
||||
field
|
||||
p>1 : 1 <N p
|
||||
pr : forall {i : ℕ} → i ∣ p → i <N p → zero <N i → i ≡ (succ zero)
|
||||
|
||||
record Composite (n : ℕ) : Set where
|
||||
field
|
||||
n>1 : 1 <N n
|
||||
divisor : ℕ
|
||||
dividesN : divisor ∣ n
|
||||
divisorLessN : divisor <N n
|
||||
divisorNot1 : 1 <N divisor
|
||||
divisorPrime : Prime divisor
|
||||
noSmallerDivisors : ∀ i → i <N divisor → 1 <N i → i ∣ n → False
|
||||
|
||||
notBothPrimeAndComposite : {n : ℕ} → Composite n → Prime n → False
|
||||
notBothPrimeAndComposite {n} record { n>1 = n>1 ; divisor = divisor ; dividesN = dividesN ; divisorLessN = divisorLessN ; divisorNot1 = divisorNot1 } record { p>1 = p>1 ; pr = pr } = lessImpliesNotEqual divisorNot1 (equalityCommutative div=1)
|
||||
where
|
||||
div=1 : divisor ≡ 1
|
||||
div=1 = pr {divisor} dividesN divisorLessN (orderIsTransitive (succIsPositive 0) divisorNot1)
|
||||
|
||||
zeroIsNotPrime : Prime 0 → False
|
||||
zeroIsNotPrime record { p>1 = p>1 ; pr = pr } = zeroNeverGreater p>1
|
||||
|
||||
oneIsNotPrime : Prime 1 → False
|
||||
oneIsNotPrime record { p>1 = (le x proof) ; pr = pr } = naughtE (equalityCommutative absurd')
|
||||
where
|
||||
absurd : x +N 1 ≡ 0
|
||||
absurd = succInjective proof
|
||||
absurd' : succ x ≡ 0
|
||||
absurd' rewrite additionNIsCommutative 1 x = absurd
|
||||
|
||||
twoIsPrime : Prime 2
|
||||
Prime.p>1 twoIsPrime = succPreservesInequality (succIsPositive 0)
|
||||
Prime.pr twoIsPrime {i} i|2 i<2 0<i with orderIsTotal i (succ (succ zero))
|
||||
Prime.pr twoIsPrime {zero} i|2 i<2 (le x ()) | order
|
||||
Prime.pr twoIsPrime {succ zero} i|2 i<2 0<i | order = refl
|
||||
Prime.pr twoIsPrime {succ (succ zero)} i|2 i<2 0<i | order = exFalso (lessImpliesNotEqual {2} i<2 refl)
|
||||
Prime.pr twoIsPrime {succ (succ (succ i))} i|2 i<2 0<i | inl (inl x) = exFalso (orderIsIrreflexive i<2 (succPreservesInequality (succPreservesInequality (succIsPositive i))))
|
||||
Prime.pr twoIsPrime {succ (succ (succ i))} i|2 i<2 0<i | inl (inr twoLessThree) = exFalso (orderIsIrreflexive twoLessThree i<2)
|
||||
Prime.pr twoIsPrime {succ (succ (succ i))} i|2 i<2 0<i | inr ()
|
||||
|
||||
compositeImpliesNotPrime : (m p : ℕ) → (succ zero <N m) → (m <N p) → (m ∣ p) → Prime p → False
|
||||
compositeImpliesNotPrime zero p (le x ()) _ mDivP pPrime
|
||||
compositeImpliesNotPrime (succ zero) p mLarge _ mDivP pPrime = lessImpliesNotEqual {succ zero} {succ zero} mLarge refl
|
||||
compositeImpliesNotPrime (succ (succ m)) zero _ _ mDivP ()
|
||||
compositeImpliesNotPrime (succ (succ m)) (succ zero) _ _ mDivP primeP = exFalso (oneIsNotPrime primeP)
|
||||
compositeImpliesNotPrime (succ (succ m)) (succ (succ p)) _ mLessP mDivP pPrime = false
|
||||
where
|
||||
r = succ (succ m)
|
||||
q = succ (succ p)
|
||||
rEqOne : r ≡ succ zero
|
||||
rEqOne = (Prime.pr pPrime) {r} mDivP mLessP (succIsPositive (succ m))
|
||||
false : False
|
||||
false = succIsNonzero (succInjective rEqOne)
|
||||
|
||||
fourIsNotPrime : Prime 4 → False
|
||||
fourIsNotPrime = compositeImpliesNotPrime (succ (succ zero)) (succ (succ (succ (succ zero)))) (le zero refl) (le (succ zero) refl) twoDividesFour
|
||||
|
||||
record hcfData (a b : ℕ) : Set where
|
||||
field
|
||||
c : ℕ
|
||||
c|a : c ∣ a
|
||||
c|b : c ∣ b
|
||||
hcf : ∀ x → x ∣ a → x ∣ b → x ∣ c
|
||||
|
||||
record Coprime (a : ℕ) (b : ℕ) : Set where
|
||||
field
|
||||
hcf : hcfData a b
|
||||
hcfNot1 : 1 <N hcfData.c hcf
|
||||
|
||||
record numberLessThan (n : ℕ) : Set where
|
||||
field
|
||||
a : ℕ
|
||||
a<n : a <N n
|
||||
upper : ℕ
|
||||
upper = n
|
||||
|
||||
numberLessThanEquality : {n : ℕ} → (a b : numberLessThan n) → (numberLessThan.a a ≡ numberLessThan.a b) → a ≡ b
|
||||
numberLessThanEquality record { a = a ; a<n = a<n } record { a = b ; a<n = b<n } pr rewrite pr | <NRefl b<n a<n = refl
|
||||
|
||||
numberLessThanOrder : (n : ℕ) → TotalOrder (numberLessThan n)
|
||||
PartialOrder._<_ (TotalOrder.order (numberLessThanOrder n)) = λ a b → (numberLessThan.a a) <N numberLessThan.a b
|
||||
PartialOrder.irreflexive (TotalOrder.order (numberLessThanOrder n)) pr = TotalOrder.irreflexive ℕTotalOrder pr
|
||||
PartialOrder.transitive (TotalOrder.order (numberLessThanOrder n)) pr1 pr2 = orderIsTransitive pr1 pr2
|
||||
TotalOrder.totality (numberLessThanOrder n) a b with TotalOrder.totality ℕTotalOrder (numberLessThan.a a) (numberLessThan.a b)
|
||||
TotalOrder.totality (numberLessThanOrder n) a b | inl (inl x) = inl (inl x)
|
||||
TotalOrder.totality (numberLessThanOrder n) a b | inl (inr x) = inl (inr x)
|
||||
TotalOrder.totality (numberLessThanOrder n) a b | inr x rewrite x = inr (numberLessThanEquality a b x)
|
||||
|
||||
numberLessThanInject : {newMax : ℕ} → (max : ℕ) → (n : numberLessThan max) → (max <N newMax) → (numberLessThan newMax)
|
||||
numberLessThanInject max record { a = n ; a<n = n<max } max<newMax = record { a = n ; a<n = PartialOrder.transitive (TotalOrder.order ℕTotalOrder) n<max max<newMax }
|
||||
|
||||
numberLessThanInjectComp : {max : ℕ} (a b : ℕ) → (i : numberLessThan b) → (pr : b <N a) → (pr2 : a <N max) → numberLessThanInject {max} a (numberLessThanInject {a} b i pr) pr2 ≡ numberLessThanInject {max} b i (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) pr pr2)
|
||||
numberLessThanInjectComp {max} a b record { a = i ; a<n = i<max } b<a a<max = numberLessThanEquality _ _ refl
|
||||
|
||||
allNumbersLessThanDescending : (n : ℕ) → Vec (numberLessThan n) n
|
||||
allNumbersLessThanDescending zero = []
|
||||
allNumbersLessThanDescending (succ n) = record { a = n ; a<n = le zero refl } ,- vecMap (λ i → numberLessThanInject {succ n} (numberLessThan.upper i) i (le zero refl)) (allNumbersLessThanDescending n)
|
||||
|
||||
allNumbersLessThan : (n : ℕ) → Vec (numberLessThan n) n
|
||||
allNumbersLessThan n = vecRev (allNumbersLessThanDescending n)
|
||||
|
||||
positiveTimes : {a b : ℕ} → (succ a *N succ b <N succ a) → False
|
||||
positiveTimes {a} {b} pr = zeroNeverGreater f'
|
||||
where
|
||||
g : succ a *N succ b <N succ a *N succ 0
|
||||
g rewrite multiplicationNIsCommutative a 1 | additionNIsCommutative a 0 = pr
|
||||
f : succ b <N succ 0
|
||||
f = cancelInequalityLeft {succ a} {succ b} g
|
||||
f' : b <N 0
|
||||
f' = canRemoveSuccFrom<N f
|
||||
|
||||
biggerThanCantDivideLemma : {a b : ℕ} → (a <N b) → (b ∣ a) → a ≡ 0
|
||||
biggerThanCantDivideLemma {zero} {b} a<b b|a = refl
|
||||
biggerThanCantDivideLemma {succ a} {zero} a<b (divides record { quot = quot ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = (inl (le x ())) } refl)
|
||||
biggerThanCantDivideLemma {succ a} {zero} a<b (divides record { quot = quot ; rem = .0 ; pr = () ; remIsSmall = remIsSmall ; quotSmall = (inr x) } refl)
|
||||
biggerThanCantDivideLemma {succ a} {succ b} a<b (divides record { quot = zero ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } refl) rewrite additionNIsCommutative (b *N zero) 0 | multiplicationNIsCommutative b 0 = naughtE pr
|
||||
biggerThanCantDivideLemma {succ a} {succ b} a<b (divides record { quot = (succ quot) ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } refl) rewrite additionNIsCommutative (quot +N b *N succ quot) 0 | equalityCommutative pr = exFalso (positiveTimes {b} {quot} a<b)
|
||||
|
||||
biggerThanCantDivide : {a b : ℕ} → (x : ℕ) → (TotalOrder.max ℕTotalOrder a b) <N x → (x ∣ a) → (x ∣ b) → (a ≡ 0) && (b ≡ 0)
|
||||
biggerThanCantDivide {a} {b} x pr x|a x|b with TotalOrder.totality ℕTotalOrder a b
|
||||
biggerThanCantDivide {a} {b} x pr x|a x|b | inl (inl a<b) = exFalso (zeroNeverGreater f')
|
||||
where
|
||||
f : b ≡ 0
|
||||
f = biggerThanCantDivideLemma pr x|b
|
||||
f' : a <N 0
|
||||
f' rewrite equalityCommutative f = a<b
|
||||
biggerThanCantDivide {a} {b} x pr x|a x|b | inl (inr b<a) = exFalso (zeroNeverGreater f')
|
||||
where
|
||||
f : a ≡ 0
|
||||
f = biggerThanCantDivideLemma pr x|a
|
||||
f' : b <N 0
|
||||
f' rewrite equalityCommutative f = b<a
|
||||
biggerThanCantDivide {a} {b} x pr x|a x|b | inr a=b = (transitivity a=b f ,, f)
|
||||
where
|
||||
f : b ≡ 0
|
||||
f = biggerThanCantDivideLemma pr x|b
|
||||
|
||||
aDivA : (a : ℕ) → a ∣ a
|
||||
aDivA zero = divides (record { quot = 0 ; rem = 0 ; pr = equalityCommutative (oneTimesPlusZero zero) ; remIsSmall = inr refl ; quotSmall = inr (refl ,, refl) }) refl
|
||||
aDivA (succ a) = divides (record { quot = 1 ; rem = 0 ; pr = equalityCommutative (oneTimesPlusZero (succ a)) ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }) refl
|
||||
|
||||
aDivZero : (a : ℕ) → a ∣ zero
|
||||
aDivZero zero = aDivA zero
|
||||
aDivZero (succ a) = divides (record { quot = zero ; rem = zero ; pr = lemma (succ a) ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }) refl
|
||||
where
|
||||
lemma : (b : ℕ) → b *N zero +N zero ≡ zero
|
||||
lemma b rewrite (addZeroRight (b *N zero)) = productZeroIsZeroRight b
|
||||
|
||||
maxDivides : (a b : ℕ) → ((TotalOrder.max ℕTotalOrder a b) ∣ a) → (TotalOrder.max ℕTotalOrder a b) ∣ b → (((a ≡ 0) && (0 <N b)) || ((b ≡ 0) && (0 <N a))) || (a ≡ b)
|
||||
maxDivides a b max|a max|b with TotalOrder.totality ℕTotalOrder a b
|
||||
maxDivides a b max|a max|b | inl (inl a<b) = inl (inl (record { fst = gg ; snd = identityOfIndiscernablesLeft _ _ _ _<N_ a<b gg}))
|
||||
where
|
||||
gg : a ≡ 0
|
||||
gg = biggerThanCantDivideLemma {a} {b} a<b max|a
|
||||
maxDivides a b max|a max|b | inl (inr b<a) = inl (inr (record { fst = gg ; snd = identityOfIndiscernablesLeft _ _ _ _<N_ b<a gg }))
|
||||
where
|
||||
gg : b ≡ 0
|
||||
gg = biggerThanCantDivideLemma b<a max|b
|
||||
maxDivides a .a a|max b|max | inr refl = inr refl
|
||||
|
||||
{-
|
||||
hcfsEquivalent' : {a b : ℕ} → extensionalHCF a b → hcfData a b
|
||||
hcfData.c (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcfExtension = hcfExtension }) = c
|
||||
hcfData.c|a (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcfExtension = hcfExtension }) = c|a
|
||||
hcfData.c|b (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcfExtension = hcfExtension }) = c|b
|
||||
hcfData.hcf (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcfExtension = hcfExtension }) x x|a x|b with orderIsTotal x c
|
||||
hcfData.hcf (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; zeroCase = zeroCase ; hcfExtension = hcfExtension ; hcfExtensionIsRightLength = hIRL }) x x|a x|b | inl (inl x<c) = {!!}
|
||||
where
|
||||
xLess : numberLessThan c
|
||||
xLess = record { a = x ; a<n = x<c }
|
||||
pair : Set
|
||||
pair = Sg (numberLessThan c) (λ i → (notDiv (numberLessThan.a i) a || notDiv (numberLessThan.a i) b) || (numberLessThan.a i ∣ a) & numberLessThan.a i ∣ b & (numberLessThan.a i ∣ c))
|
||||
pr : Sg pair λ p → (lookup (MapWithDomain.map hcfExtension) xLess ≡ {!!})
|
||||
pr = MapWithDomain.lookup' hcfExtension xLess (hcfsContains {a} {b} {x} (record { c = c ; c|a = c|a ; c|b = c|b ; zeroCase = zeroCase ; hcfExtension = hcfExtension ; hcfExtensionIsRightLength = hIRL }) x<c)
|
||||
hcfData.hcf (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; zeroCase = _ ; hcfExtension = hcfExtension ; hcfExtensionIsRightLength = _ }) x x|a x|b | inl (inr c<x) = {!!}
|
||||
hcfData.hcf (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; zeroCase = _ ; hcfExtension = hcfExtension ; hcfExtensionIsRightLength = _ }) x x|a x|b | inr x=c rewrite x=c = aDivA c
|
||||
|
||||
extensionalHCFEquality : {a b : ℕ} → {h1 h2 : extensionalHCF a b} → (extensionalHCF.c h1 ≡ extensionalHCF.c h2) → h1 ≡ h2
|
||||
extensionalHCFEquality {a} {b} {record { c = c1 ; c|a = c|a1 ; c|b = c|b1 ; hcfExtension = hcfExtension1 }} {record { c = c2 ; c|a = c|a2 ; c|b = c|b2 ; hcfExtension = hcfExtension2 }} pr rewrite pr = {!!}
|
||||
-}
|
||||
|
||||
record extendedHcf (a b : ℕ) : Set where
|
||||
field
|
||||
hcf : hcfData a b
|
||||
c : ℕ
|
||||
c = hcfData.c hcf
|
||||
field
|
||||
extended1 : ℕ
|
||||
extended2 : ℕ
|
||||
extendedProof : (a *N extended1 ≡ b *N extended2 +N c) || (a *N extended1 +N c ≡ b *N extended2)
|
||||
|
||||
divEqualityLemma1 : {a b c : ℕ} → b ≡ zero → b *N c +N 0 ≡ a → a ≡ b
|
||||
divEqualityLemma1 {a} {.0} {c} refl pr = equalityCommutative pr
|
||||
|
||||
divEquality : {a b : ℕ} → a ∣ b → b ∣ a → a ≡ b
|
||||
divEquality {a} {b} (divides record { quot = quotAB ; rem = .0 ; pr = prAB ; remIsSmall = _ ; quotSmall = quotSmallAB } refl) (divides record { quot = quot ; rem = .0 ; pr = pr ; remIsSmall = _ ; quotSmall = (inl x) } refl) rewrite additionNIsCommutative (b *N quot) 0 | additionNIsCommutative (a *N quotAB) 0 | equalityCommutative pr | equalityCommutative (multiplicationNIsAssociative b quot quotAB) = res
|
||||
where
|
||||
lem : {b r : ℕ} → b *N r ≡ b → (0 <N b) → r ≡ 1
|
||||
lem {zero} {r} pr ()
|
||||
lem {succ b} {zero} pr _ rewrite multiplicationNIsCommutative b 0 = naughtE pr
|
||||
lem {succ b} {succ zero} pr _ = refl
|
||||
lem {succ b} {succ (succ r)} pr _ rewrite multiplicationNIsCommutative b (succ (succ r)) | additionNIsCommutative (succ r) (b +N (b +N r *N b)) | additionNIsAssociative b (b +N r *N b) (succ r) | additionNIsCommutative (b +N r *N b) (succ r) = exFalso (cannotAddAndEnlarge'' {succ b} pr)
|
||||
p : quot *N quotAB ≡ 1
|
||||
p = lem prAB x
|
||||
q : quot ≡ 1
|
||||
q = _&&_.fst (productOneImpliesOperandsOne p)
|
||||
res : b *N quot ≡ b
|
||||
res rewrite q | multiplicationNIsCommutative b 1 | additionNIsCommutative b 0 = refl
|
||||
divEquality {.0} {.0} (divides record { quot = quotAB ; rem = .0 ; pr = prAB ; remIsSmall = _ ; quotSmall = quotSmallAB } refl) (divides record { quot = quot ; rem = .0 ; pr = refl ; remIsSmall = _ ; quotSmall = (inr (refl ,, snd)) } refl) = refl
|
||||
|
||||
hcfWelldefined : {a b : ℕ} → (ab : hcfData a b) → (ab' : hcfData a b) → (hcfData.c ab ≡ hcfData.c ab')
|
||||
hcfWelldefined {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } record { c = c' ; c|a = c|a' ; c|b = c|b' ; hcf = hcf' } with hcf c' c|a' c|b'
|
||||
... | c'DivC with hcf' c c|a c|b
|
||||
... | cDivC' = divEquality cDivC' c'DivC
|
||||
|
||||
reverseHCF : {a b : ℕ} → (ab : extendedHcf a b) → extendedHcf b a
|
||||
reverseHCF {a} {b} record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = (inl x) } = record { hcf = record { c = c ; c|a = c|b ; c|b = c|a ; hcf = λ x z z₁ → hcf x z₁ z } ; extended1 = extended2 ; extended2 = extended1 ; extendedProof = inr (equalityCommutative x) }
|
||||
reverseHCF {a} {b} record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = (inr x) } = record { hcf = record { c = c ; c|a = c|b ; c|b = c|a ; hcf = λ x z z₁ → hcf x z₁ z } ; extended1 = extended2 ; extended2 = extended1 ; extendedProof = inl (equalityCommutative x) }
|
||||
|
||||
|
||||
oneDivN : (a : ℕ) → 1 ∣ a
|
||||
oneDivN a = divides (record { quot = a ; rem = zero ; pr = pr ; remIsSmall = inl (succIsPositive zero) ; quotSmall = inl (le zero refl) }) refl
|
||||
where
|
||||
pr : (a +N zero) +N zero ≡ a
|
||||
pr rewrite addZeroRight (a +N zero) = addZeroRight a
|
||||
|
||||
hcfZero : (a : ℕ) → extendedHcf zero a
|
||||
hcfZero a = record { hcf = record { c = a ; c|a = aDivZero a ; c|b = aDivA a ; hcf = λ _ _ p → p } ; extended1 = 0 ; extended2 = 1 ; extendedProof = inr (equalityCommutative (productWithOneRight a))}
|
||||
|
||||
hcfOne : (a : ℕ) → extendedHcf 1 a
|
||||
hcfOne a = record { hcf = record { c = 1 ; c|a = aDivA 1 ; c|b = oneDivN a ; hcf = λ _ z _ → z } ; extended1 = 1 ; extended2 = 0 ; extendedProof = inl g }
|
||||
where
|
||||
g : 1 ≡ a *N 0 +N 1
|
||||
g rewrite multiplicationNIsCommutative a 0 = refl
|
||||
|
||||
zeroIsValidRem : (a : ℕ) → (0 <N a) || (a ≡ 0)
|
||||
zeroIsValidRem zero = inr refl
|
||||
zeroIsValidRem (succ a) = inl (succIsPositive a)
|
||||
|
||||
dividesBothImpliesDividesSum : {a x y : ℕ} → a ∣ x → a ∣ y → a ∣ (x +N y)
|
||||
dividesBothImpliesDividesSum {a} {x} {y} (divides record { quot = xDivA ; rem = .0 ; pr = prA ; quotSmall = qsm1 } refl) (divides record { quot = quot ; rem = .0 ; pr = pr ; quotSmall = qsm2 } refl) = divides (record { quot = xDivA +N quot ; rem = 0 ; pr = go {a} {x} {y} {xDivA} {quot} pr prA ; remIsSmall = zeroIsValidRem a ; quotSmall = (quotSmall qsm1 qsm2) }) refl
|
||||
where
|
||||
go : {a x y quot quot2 : ℕ} → (a *N quot2 +N zero ≡ y) → (a *N quot +N zero ≡ x) → a *N (quot +N quot2) +N zero ≡ x +N y
|
||||
go {a} {x} {y} {quot} {quot2} pr1 pr2 rewrite addZeroRight (a *N quot) = identityOfIndiscernablesLeft (a *N (quot +N quot2)) (x +N y) (a *N (quot +N quot2) +N zero) _≡_ t (equalityCommutative (addZeroRight (a *N (quot +N quot2))))
|
||||
where
|
||||
t : a *N (quot +N quot2) ≡ x +N y
|
||||
t rewrite addZeroRight (a *N quot2) = transitivity (productDistributes a quot quot2) p
|
||||
where
|
||||
s : a *N quot +N a *N quot2 ≡ x +N a *N quot2
|
||||
s = applyEquality (λ n → n +N a *N quot2) pr2
|
||||
r : x +N a *N quot2 ≡ x +N y
|
||||
r = applyEquality (λ n → x +N n) pr1
|
||||
p : a *N quot +N a *N quot2 ≡ x +N y
|
||||
p = transitivity s r
|
||||
quotSmall : ((0 <N a) || ((0 ≡ a) && (xDivA ≡ 0))) → ((0 <N a) || ((0 ≡ a) && (quot ≡ 0))) → (0 <N a) || ((0 ≡ a) && (xDivA +N quot ≡ 0))
|
||||
quotSmall (inl x1) (inl x2) = inl x1
|
||||
quotSmall (inl x1) (inr x2) = inl x1
|
||||
quotSmall (inr x1) (inl x2) = inl x2
|
||||
quotSmall (inr (a=0 ,, bl)) (inr (_ ,, bl2)) = inr (a=0 ,, ans)
|
||||
where
|
||||
ans : xDivA +N quot ≡ 0
|
||||
ans rewrite bl | bl2 = refl
|
||||
|
||||
dividesBothImpliesDividesDifference : {a b c : ℕ} → a ∣ b → a ∣ c → (c<b : c <N b) → a ∣ (subtractionNResult.result (-N (inl c<b)))
|
||||
dividesBothImpliesDividesDifference {zero} {b} {.0} prab (divides record { quot = quot ; rem = .0 ; pr = refl } refl) c<b = prab
|
||||
dividesBothImpliesDividesDifference {succ a} {b} {c} (divides record { quot = bDivSA ; rem = .0 ; pr = pr } refl) (divides record { quot = cDivSA ; rem = .0 ; pr = pr2 } refl) c<b rewrite (addZeroRight (succ a *N cDivSA)) | (addZeroRight (succ a *N bDivSA)) = divides (record { quot = subtractionNResult.result bDivSA-cDivSA ; rem = 0 ; pr = identityOfIndiscernablesLeft (succ a *N (subtractionNResult.result bDivSA-cDivSA)) (subtractionNResult.result (-N (inl c<b))) (succ a *N (subtractionNResult.result bDivSA-cDivSA) +N zero) _≡_ (identityOfIndiscernablesLeft (la-ka) (subtractionNResult.result (-N (inl c<b))) (succ a *N (subtractionNResult.result bDivSA-cDivSA)) _≡_ s (equalityCommutative q)) (equalityCommutative (addZeroRight _)) ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }) refl
|
||||
where
|
||||
p : cDivSA <N bDivSA
|
||||
p rewrite (equalityCommutative pr2) | (equalityCommutative pr) = cancelInequalityLeft {succ a} {cDivSA} {bDivSA} c<b
|
||||
bDivSA-cDivSA : subtractionNResult cDivSA bDivSA (inl p)
|
||||
bDivSA-cDivSA = -N {cDivSA} {bDivSA} (inl p)
|
||||
la-ka = subtractionNResult.result (-N {succ a *N cDivSA} {succ a *N bDivSA} (inl (lessRespectsMultiplicationLeft cDivSA bDivSA (succ a) p (succIsPositive a))))
|
||||
q : (succ a *N (subtractionNResult.result bDivSA-cDivSA)) ≡ la-ka
|
||||
q = subtractProduct {succ a} {cDivSA} {bDivSA} (succIsPositive a) p
|
||||
s : la-ka ≡ subtractionNResult.result (-N {c} {b} (inl c<b))
|
||||
s = equivalentSubtraction (succ a *N cDivSA) b (succ a *N bDivSA) c (lessRespectsMultiplicationLeft cDivSA bDivSA (succ a) p (succIsPositive a)) c<b g
|
||||
where
|
||||
g : (succ a *N cDivSA) +N b ≡ (succ a *N bDivSA) +N c
|
||||
g rewrite equalityCommutative pr2 | equalityCommutative pr = additionNIsCommutative (cDivSA +N a *N cDivSA) (bDivSA +N a *N bDivSA)
|
||||
|
||||
euclidLemma1 : {a b : ℕ} → (a<b : a <N b) → (t : ℕ) → a +N b <N t → a +N (subtractionNResult.result (-N (inl a<b))) <N t
|
||||
euclidLemma1 {zero} {b} zero<b t b<t = b<t
|
||||
euclidLemma1 {succ a} {b} sa<b t sa+b<t = identityOfIndiscernablesLeft (subtractionNResult.result (-N (inl sa<b)) +N succ a) t (succ a +N (subtractionNResult.result (-N (inl sa<b)))) _<N_ q (additionNIsCommutative (subtractionNResult.result (-N (inl sa<b))) (succ a))
|
||||
where
|
||||
p : b <N t
|
||||
p = orderIsTransitive (le a refl) sa+b<t
|
||||
q : (subtractionNResult.result (-N (inl sa<b))) +N succ a <N t
|
||||
q = identityOfIndiscernablesLeft b t (subtractionNResult.result (-N (inl sa<b)) +N succ a) _<N_ p (equalityCommutative (addMinus (inl sa<b)))
|
||||
|
||||
euclidLemma2 : {a b max : ℕ} → (succ (a +N b) <N max) → b <N max
|
||||
euclidLemma2 {a} {b} {max} pr = lessTransitive {b} {succ (a +N b)} {max} (lemma a b) pr
|
||||
where
|
||||
lemma : (a b : ℕ) → b <N succ (a +N b)
|
||||
lemma a zero = succIsPositive (a +N zero)
|
||||
lemma a (succ b) = succPreservesInequality (collapseSuccOnRight {b} {a} {b} (lemma a b))
|
||||
|
||||
euclidLemma3 : {a b max : ℕ} → (succ (succ (a +N b)) <N max) → succ b <N max
|
||||
euclidLemma3 {a} {b} {max} pr = euclidLemma2 {a} {succ b} {max} (identityOfIndiscernablesLeft (succ (succ (a +N b))) max (succ (a +N succ b)) _<N_ pr (applyEquality succ (equalityCommutative (succExtracts a b))))
|
||||
|
||||
euclidLemma4 : (a b c d h : ℕ) → (sa<b : (succ a) <N b) → (pr : subtractionNResult.result (-N (inl sa<b)) *N c ≡ (succ a) *N d +N h) → b *N c ≡ (succ a) *N (d +N c) +N h
|
||||
euclidLemma4 a b zero d h sa<b pr rewrite addZeroRight d | productZeroIsZeroRight b | productZeroIsZeroRight (subtractionNResult.result (-N (inl sa<b))) = pr
|
||||
euclidLemma4 a b (succ c) d h sa<b pr rewrite subtractProduct' (succIsPositive c) sa<b = transitivity q' r'
|
||||
where
|
||||
q : (succ c) *N b ≡ succ (a +N c *N succ a) +N ((succ a) *N d +N h)
|
||||
q = moveOneSubtraction {succ (a +N c *N succ a)} {b +N c *N b} {(succ a) *N d +N h} {inl _} pr
|
||||
q' : b *N succ c ≡ succ (a +N c *N succ a) +N ((succ a) *N d +N h)
|
||||
q' rewrite multiplicationNIsCommutative b (succ c) = q
|
||||
r' : ((succ c) *N succ a) +N (((succ a) *N d) +N h) ≡ ((succ a) *N (d +N succ c)) +N h
|
||||
r' rewrite equalityCommutative (additionNIsAssociative ((succ c) *N succ a) ((succ a) *N d) h) = applyEquality (λ t → t +N h) {((succ c) *N succ a) +N ((succ a) *N d)} {(succ a) *N (d +N succ c)} (go (succ c) (succ a) d)
|
||||
where
|
||||
go' : (a b c : ℕ) → b *N a +N b *N c ≡ b *N (c +N a)
|
||||
go : (a b c : ℕ) → a *N b +N b *N c ≡ b *N (c +N a)
|
||||
go a b c rewrite multiplicationNIsCommutative a b = go' a b c
|
||||
go' a b c rewrite additionNIsCommutative (b *N a) (b *N c) = equalityCommutative (productDistributes b c a)
|
||||
|
||||
euclidLemma5 : (a b c d h : ℕ) → (sa<b : (succ a) <N b) → (pr : subtractionNResult.result (-N (inl sa<b)) *N c +N h ≡ (succ a) *N d) → (succ a) *N (d +N c) ≡ b *N c +N h
|
||||
euclidLemma5 a b c d h sa<b pr with (-N (inl sa<b))
|
||||
euclidLemma5 a b zero d h sa<b pr | record { result = result ; pr = sub } rewrite addZeroRight d | productZeroIsZeroRight b | productZeroIsZeroRight result = equalityCommutative pr
|
||||
euclidLemma5 a b (succ c) d h sa<b pr | record { result = result ; pr = sub } rewrite subtractProduct' (succIsPositive c) sa<b | equalityCommutative sub = pv''
|
||||
where
|
||||
p : succ a *N d ≡ result *N succ c +N h
|
||||
p = equalityCommutative pr
|
||||
p' : a *N succ c +N succ a *N d ≡ (a *N succ c) +N ((result *N succ c) +N h)
|
||||
p' = applyEquality (λ t → a *N succ c +N t) p
|
||||
p'' : a *N succ c +N succ a *N d ≡ (a *N succ c +N result *N succ c) +N h
|
||||
p'' rewrite (additionNIsAssociative (a *N succ c) (result *N succ c) h) = p'
|
||||
p''' : a *N succ c +N succ a *N d ≡ (a +N result) *N succ c +N h
|
||||
p''' rewrite productDistributes' a result (succ c) = p''
|
||||
pv : c +N (a *N succ c +N succ a *N d) ≡ (c +N (a +N result) *N succ c) +N h
|
||||
pv rewrite additionNIsAssociative c ((a +N result) *N succ c) h = applyEquality (λ t → c +N t) p'''
|
||||
pv' : (succ c) +N (a *N succ c +N succ a *N d) ≡ succ ((c +N (a +N result) *N succ c) +N h)
|
||||
pv' = applyEquality succ pv
|
||||
pv'' : (succ a) *N (d +N succ c) ≡ succ ((c +N (a +N result) *N succ c) +N h)
|
||||
pv'' = identityOfIndiscernablesLeft ((succ c) +N (a *N succ c +N succ a *N d)) _ ((succ a) *N (d +N succ c)) _≡_ pv' (go a c d)
|
||||
where
|
||||
go : (a c d : ℕ) → (succ c) +N (a *N succ c +N ((succ a) *N d)) ≡ (succ a) *N (d +N succ c)
|
||||
go a c d rewrite equalityCommutative (additionNIsAssociative (succ c) (a *N succ c) ((succ a) *N d)) = go'
|
||||
where
|
||||
go' : (succ a) *N (succ c) +N (succ a) *N d ≡ (succ a) *N (d +N succ c)
|
||||
go' rewrite additionNIsCommutative d (succ c) = equalityCommutative (productDistributes (succ a) (succ c) d)
|
||||
|
||||
euclid : (a b : ℕ) → extendedHcf a b
|
||||
euclid a b = inducted (succ a +N b) a b (a<SuccA (a +N b))
|
||||
where
|
||||
P : ℕ → Set
|
||||
P sum = ∀ (a b : ℕ) → a +N b <N sum → extendedHcf a b
|
||||
go'' : {a b : ℕ} → (maxsum : ℕ) → (a <N b) → (a +N b <N maxsum) → (∀ y → y <N maxsum → P y) → extendedHcf a b
|
||||
go'' {zero} {b} maxSum zero<b b<maxsum indHyp = hcfZero b
|
||||
go'' {1} {b} maxSum 1<b b<maxsum indHyp = hcfOne b
|
||||
go'' {succ (succ a)} {b} maxSum ssa<b ssa+b<maxsum indHyp with (indHyp (succ b) (euclidLemma3 {a} {b} {maxSum} ssa+b<maxsum)) (subtractionNResult.result (-N (inl ssa<b))) (succ (succ a)) (identityOfIndiscernablesLeft b (succ b) (subtractionNResult.result (-N (inl ssa<b)) +N succ (succ a)) _<N_ (a<SuccA b) (equalityCommutative (addMinus (inl ssa<b))))
|
||||
go'' {succ (succ a)} {b} maxSum ssa<b ssa+b<maxsum indHyp | record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = inl extendedProof } = record { hcf = record { c = c ; c|a = c|b ; c|b = hcfDivB'' ; hcf = λ div prDivSSA prDivB → hcf div (dividesBothImpliesDividesDifference prDivB prDivSSA ssa<b) prDivSSA } ; extended2 = extended1; extended1 = extended2 +N extended1 ; extendedProof = inr (equalityCommutative (euclidLemma4 (succ a) b extended1 extended2 c ssa<b extendedProof)) }
|
||||
where
|
||||
hcfDivB : c ∣ ((succ (succ a)) +N (subtractionNResult.result (-N (inl ssa<b))))
|
||||
hcfDivB = dividesBothImpliesDividesSum {c} {succ (succ a)} { subtractionNResult.result (-N (inl ssa<b))} c|b c|a
|
||||
hcfDivB' : c ∣ ((subtractionNResult.result (-N (inl ssa<b))) +N (succ (succ a)))
|
||||
hcfDivB' = identityOfIndiscernablesRight c ((succ (succ a)) +N (subtractionNResult.result (-N (inl ssa<b)))) ((subtractionNResult.result (-N (inl ssa<b))) +N (succ (succ a))) _∣_ hcfDivB (additionNIsCommutative (succ (succ a)) ( subtractionNResult.result (-N (inl ssa<b))))
|
||||
hcfDivB'' : c ∣ b
|
||||
hcfDivB'' = identityOfIndiscernablesRight c ((subtractionNResult.result (-N (inl ssa<b))) +N (succ (succ a))) b _∣_ hcfDivB' (addMinus (inl ssa<b))
|
||||
go'' {succ (succ a)} {b} maxSum ssa<b ssa+b<maxsum indHyp | record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = inr extendedProof } = record { hcf = record { c = c ; c|a = c|b ; c|b = hcfDivB'' ; hcf = λ div prDivSSA prDivB → hcf div (dividesBothImpliesDividesDifference prDivB prDivSSA ssa<b) prDivSSA } ; extended2 = extended1; extended1 = extended2 +N extended1 ; extendedProof = inl (euclidLemma5 (succ a) b extended1 extended2 c ssa<b extendedProof) }
|
||||
where
|
||||
hcfDivB : c ∣ ((succ (succ a)) +N (subtractionNResult.result (-N (inl ssa<b))))
|
||||
hcfDivB = dividesBothImpliesDividesSum {c} {succ (succ a)} { subtractionNResult.result (-N (inl ssa<b))} c|b c|a
|
||||
hcfDivB' : c ∣ ((subtractionNResult.result (-N (inl ssa<b))) +N (succ (succ a)))
|
||||
hcfDivB' = identityOfIndiscernablesRight c ((succ (succ a)) +N (subtractionNResult.result (-N (inl ssa<b)))) ((subtractionNResult.result (-N (inl ssa<b))) +N (succ (succ a))) _∣_ hcfDivB (additionNIsCommutative (succ (succ a)) ( subtractionNResult.result (-N (inl ssa<b))))
|
||||
hcfDivB'' : c ∣ b
|
||||
hcfDivB'' = identityOfIndiscernablesRight c ((subtractionNResult.result (-N (inl ssa<b))) +N (succ (succ a))) b _∣_ hcfDivB' (addMinus (inl ssa<b))
|
||||
go' : (maxSum a b : ℕ) → (a +N b <N maxSum) → (∀ y → y <N maxSum → P y) → extendedHcf a b
|
||||
go' maxSum a b a+b<maxsum indHyp with orderIsTotal a b
|
||||
go' maxSum a b a+b<maxsum indHyp | inl (inl a<b) = go'' maxSum a<b a+b<maxsum indHyp
|
||||
go' maxSum a b a+b<maxsum indHyp | inl (inr b<a) = reverseHCF (go'' maxSum b<a (identityOfIndiscernablesLeft (a +N b) maxSum (b +N a) _<N_ a+b<maxsum (additionNIsCommutative a b)) indHyp)
|
||||
go' maxSum a .a _ indHyp | inr refl = record { hcf = record { c = a ; c|a = aDivA a ; c|b = aDivA a ; hcf = λ _ _ z → z } ; extended1 = 0 ; extended2 = 1 ; extendedProof = inr s}
|
||||
where
|
||||
s : a *N zero +N a ≡ a *N 1
|
||||
s rewrite multiplicationNIsCommutative a zero | productWithOneRight a = refl
|
||||
go : ∀ x → (∀ y → y <N x → P y) → P x
|
||||
go maxSum indHyp = λ a b a+b<maxSum → go' maxSum a b a+b<maxSum indHyp
|
||||
inducted : ∀ x → P x
|
||||
inducted = rec <NWellfounded P go
|
||||
|
||||
divisorIsSmaller : {a b : ℕ} → a ∣ succ b → succ b <N a → False
|
||||
divisorIsSmaller {a} {b} (divides record { quot = zero ; rem = .0 ; pr = pr } refl) sb<a rewrite addZeroRight (a *N zero) = go
|
||||
where
|
||||
go : False
|
||||
go rewrite productZeroIsZeroRight a = naughtE pr
|
||||
divisorIsSmaller {a} {b} (divides record { quot = (succ quot) ; rem = .0 ; pr = pr } refl) sb<a rewrite addZeroRight (a *N succ quot) = go
|
||||
where
|
||||
go : False
|
||||
go rewrite equalityCommutative pr = go'
|
||||
where
|
||||
go' : False
|
||||
go' rewrite multiplicationNIsCommutative a (succ quot) = cannotAddAndEnlarge' sb<a
|
||||
|
||||
primeDivisorIs1OrP : {a p : ℕ} → (prime : Prime p) → (a ∣ p) → (a ≡ 1) || (a ≡ p)
|
||||
primeDivisorIs1OrP {zero} {zero} prime a|p = inr refl
|
||||
primeDivisorIs1OrP {zero} {succ p} prime a|p = exFalso (zeroDividesNothing p a|p)
|
||||
primeDivisorIs1OrP {succ zero} {p} prime a|p = inl refl
|
||||
primeDivisorIs1OrP {succ (succ a)} {p} prime a|p with orderIsTotal (succ (succ a)) p
|
||||
primeDivisorIs1OrP {succ (succ a)} {p} prime a|p | inl (inl ssa<p) = go p prime a|p ssa<p
|
||||
where
|
||||
go : (n : ℕ) → Prime n → succ (succ a) ∣ n → succ (succ a) <N n → (succ (succ a) ≡ 1) || (succ (succ a) ≡ p)
|
||||
go zero pr x|n n<n = exFalso (zeroIsNotPrime pr)
|
||||
go (succ zero) pr x|n n<n = exFalso (oneIsNotPrime pr)
|
||||
go (succ (succ n)) pr x|n n<n = inl ((Prime.pr pr) {succ (succ a)} x|n n<n (succIsPositive (succ a)))
|
||||
primeDivisorIs1OrP {succ (succ a)} {zero} prime a|p | inl (inr x) = exFalso (zeroIsNotPrime prime)
|
||||
primeDivisorIs1OrP {succ (succ a)} {succ p} prime a|p | inl (inr x) = exFalso (divisorIsSmaller {succ (succ a)} {p} a|p x)
|
||||
primeDivisorIs1OrP {succ (succ a)} {p} prime a|p | inr x = inr x
|
||||
|
||||
hcfPrimeIsOne' : {p : ℕ} → {a : ℕ} → (Prime p) → (0 <N divisionAlgResult.rem (divisionAlg p a)) → (extendedHcf.c (euclid a p) ≡ 1) || (extendedHcf.c (euclid a p) ≡ p)
|
||||
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA with euclid a p
|
||||
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA | record { hcf = record { c = hcf ; c|a = hcf|a ; c|b = hcf|p ; hcf = hcfPr } } with divisionAlg p a
|
||||
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA | record { hcf = record { c = hcf ; c|a = hcf|a ; c|b = hcf|p ; hcf = hcfPr } } | record { quot = quot ; rem = rem ; pr = prPDivA } with primeDivisorIs1OrP pPrime hcf|p
|
||||
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA | record { hcf = record { c = hcf ; c|a = hcf|a ; c|b = hcf|p ; hcf = hcfPr } } | record { quot = quot ; rem = rem ; pr = prPDivA } | inl x = inl x
|
||||
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA | record { hcf = record { c = hcf ; c|a = hcf|a ; c|b = hcf|p ; hcf = hcfPr } } | record { quot = quot ; rem = rem ; pr = prPDivA } | inr x = inr x
|
||||
|
||||
divisionDecidable : (a b : ℕ) → (a ∣ b) || ((a ∣ b) → False)
|
||||
divisionDecidable zero zero = inl (aDivA zero)
|
||||
divisionDecidable zero (succ b) = inr f
|
||||
where
|
||||
f : zero ∣ succ b → False
|
||||
f (divides record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = remIsSmall } x) rewrite x = naughtE pr
|
||||
divisionDecidable (succ a) b with divisionAlg (succ a) b
|
||||
divisionDecidable (succ a) b | record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remSmall } = inl (divides (record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remSmall ; quotSmall = inl (succIsPositive a) }) refl)
|
||||
divisionDecidable (succ a) b | record { quot = b/a ; rem = succ rem ; pr = prANotDivB ; remIsSmall = inr p } = naughtE (equalityCommutative p)
|
||||
divisionDecidable (succ a) b | record { quot = b/a ; rem = succ rem ; pr = prANotDivB ; remIsSmall = inl p } = inr f
|
||||
where
|
||||
f : (succ a) ∣ b → False
|
||||
f (divides record { quot = b/a' ; rem = .0 ; pr = pr } refl) rewrite addZeroRight ((succ a) *N b/a') = naughtE (modUniqueLemma {zero} {succ rem} {succ a} b/a' b/a (succIsPositive a) p comp')
|
||||
where
|
||||
comp : (succ a) *N b/a' ≡ (succ a) *N b/a +N succ rem
|
||||
comp = transitivity pr (equalityCommutative prANotDivB)
|
||||
comp' : (succ a) *N b/a' +N zero ≡ (succ a) *N b/a +N succ rem
|
||||
comp' rewrite addZeroRight (succ a *N b/a') = comp
|
||||
|
||||
doesNotDivideImpliesNonzeroRem : (a b : ℕ) → ((a ∣ b) → False) → 0 <N divisionAlgResult.rem (divisionAlg a b)
|
||||
doesNotDivideImpliesNonzeroRem a b pr with divisionAlg a b
|
||||
doesNotDivideImpliesNonzeroRem a b pr | record { quot = quot ; rem = rem ; pr = divAlgPr ; remIsSmall = remIsSmall } with zeroIsValidRem rem
|
||||
doesNotDivideImpliesNonzeroRem a b pr | record { quot = quot ; rem = rem ; pr = divAlgPr ; remIsSmall = remIsSmall } | inl x = x
|
||||
doesNotDivideImpliesNonzeroRem a b pr | record { quot = quot ; rem = rem ; pr = divAlgPr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } | inr x = exFalso (pr aDivB)
|
||||
where
|
||||
aDivB : a ∣ b
|
||||
aDivB = divides (record { quot = quot ; rem = rem ; pr = divAlgPr ; remIsSmall = remIsSmall ; quotSmall = quotSmall }) x
|
||||
|
||||
hcfPrimeIsOne : {p : ℕ} → {a : ℕ} → (Prime p) → ((p ∣ a) → False) → extendedHcf.c (euclid a p) ≡ 1
|
||||
hcfPrimeIsOne {p} {a} pPrime pr with hcfPrimeIsOne' {p} {a} pPrime (doesNotDivideImpliesNonzeroRem p a pr)
|
||||
hcfPrimeIsOne {p} {a} pPrime pr | inl x = x
|
||||
hcfPrimeIsOne {p} {a} pPrime pr | inr x with euclid a p
|
||||
hcfPrimeIsOne {p} {a} pPrime pr | inr x | record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = extendedProof } rewrite x = exFalso (pr c|a)
|
||||
|
||||
reduceEquationMod : {a b c : ℕ} → (d : ℕ) → (a ∣ b) → (a ∣ c) → b ≡ c +N d → a ∣ d
|
||||
reduceEquationMod {a} {b} {c} 0 a|b a|c pr = aDivZero a
|
||||
reduceEquationMod {a} {b} {c} (succ d) (divides record { quot = b/a ; rem = .0 ; pr = prb/a ; remIsSmall = r1 ; quotSmall = qSm1 } refl) (divides record { quot = c/a ; rem = .0 ; pr = prc/a ; remIsSmall = r2 ; quotSmall = qSm2 } refl) b=c+d = identityOfIndiscernablesRight a (subtractionNResult.result (-N (inl c<b))) (succ d) _∣_ a|b-c ex'
|
||||
where
|
||||
c<b : c <N b
|
||||
c<b rewrite succExtracts c d | additionNIsCommutative c d = le d (equalityCommutative b=c+d)
|
||||
a|b-c : a ∣ subtractionNResult.result (-N (inl c<b))
|
||||
a|b-c = dividesBothImpliesDividesDifference (divides record { quot = b/a ; rem = 0 ; pr = prb/a ; remIsSmall = r1 ; quotSmall = qSm1 } refl) (divides record { quot = c/a ; rem = 0 ; pr = prc/a ; remIsSmall = r2 ; quotSmall = qSm2 } refl) c<b
|
||||
ex : subtractionNResult.result (-N {c} {b} (inl c<b)) ≡ subtractionNResult.result (-N {0} {succ d} (inl (succIsPositive d)))
|
||||
ex = equivalentSubtraction c (succ d) b 0 (c<b) (succIsPositive d) (equalityCommutative (identityOfIndiscernablesLeft b (c +N succ d) (b +N 0) _≡_ b=c+d (equalityCommutative (addZeroRight b))))
|
||||
ex' : subtractionNResult.result (-N {c} {b} (inl c<b)) ≡ succ d
|
||||
ex' = identityOfIndiscernablesRight (subtractionNResult.result (-N (inl c<b))) (subtractionNResult.result (-N (inl (succIsPositive d)))) (succ d) _≡_ ex refl
|
||||
|
||||
primesArePrime : {p : ℕ} → {a b : ℕ} → (Prime p) → p ∣ (a *N b) → (p ∣ a) || (p ∣ b)
|
||||
primesArePrime {p} {a} {b} pPrime pr with divisionDecidable p a
|
||||
primesArePrime {p} {a} {b} pPrime pr | inl p|a = inl p|a
|
||||
primesArePrime {p} {a} {b} pPrime (divides record {quot = ab/p ; rem = .0 ; pr = p|ab ; remIsSmall = _ ; quotSmall = quotSmall } refl) | inr notp|a = inr (answer ex'')
|
||||
where
|
||||
euc : extendedHcf a p
|
||||
euc = euclid a p
|
||||
h : extendedHcf.c euc ≡ 1
|
||||
h = hcfPrimeIsOne {p} {a} pPrime notp|a
|
||||
x = extendedHcf.extended1 euc
|
||||
y = extendedHcf.extended2 euc
|
||||
extended : ((a *N x) ≡ p *N y +N extendedHcf.c euc) || (a *N x +N extendedHcf.c euc ≡ p *N y)
|
||||
extended = extendedHcf.extendedProof euc
|
||||
extended' : (a *N x ≡ p *N y +N 1) || (a *N x +N 1 ≡ p *N y)
|
||||
extended' rewrite equalityCommutative h = extended
|
||||
extended'' : ((a *N x ≡ p *N y +N 1) || (a *N x +N 1 ≡ p *N y)) → (b *N (a *N x) ≡ b *N (p *N y +N 1)) || (b *N (a *N x +N 1) ≡ b *N (p *N y))
|
||||
extended'' (inl z) = inl (applyEquality (λ t → b *N t) z)
|
||||
extended'' (inr z) = inr (applyEquality (λ t → b *N t) z)
|
||||
ex : (b *N (a *N x) ≡ b *N (p *N y +N 1)) || (b *N (a *N x +N 1) ≡ b *N (p *N y)) → ((b *N a) *N x ≡ (b *N (p *N y) +N b)) || (((b *N a) *N x +N b) ≡ b *N (p *N y))
|
||||
ex (inl z) rewrite multiplicationNIsAssociative b a x | productDistributes b (p *N y) 1 | productWithOneRight b = inl z
|
||||
ex (inr z) rewrite productDistributes b (a *N x) 1 | multiplicationNIsAssociative b a x | productWithOneRight b = inr z
|
||||
ex' : ((a *N b) *N x ≡ ((p *N y) *N b +N b)) || (((a *N b) *N x +N b) ≡ (p *N y) *N b)
|
||||
ex' rewrite multiplicationNIsCommutative a b | multiplicationNIsCommutative (p *N y) b = ex (extended'' extended')
|
||||
ex'' : ((a *N b) *N x ≡ (p *N (y *N b) +N b)) || (((a *N b) *N x +N b) ≡ p *N (y *N b))
|
||||
ex'' rewrite multiplicationNIsAssociative (p) y b = ex'
|
||||
inter1 : p ∣ (a *N b) *N x
|
||||
inter1 = divides (record {quot = ab/p *N x ; rem = 0 ; pr = g ; remIsSmall = zeroIsValidRem p ; quotSmall = qsm quotSmall}) refl
|
||||
where
|
||||
g' : p *N ab/p ≡ a *N b
|
||||
g' rewrite addZeroRight (p *N ab/p) = p|ab
|
||||
g'' : p *N (ab/p *N x) ≡ (a *N b) *N x
|
||||
g'' rewrite multiplicationNIsAssociative (p) ab/p x = applyEquality (λ t → t *N x) g'
|
||||
g : p *N (ab/p *N x) +N 0 ≡ (a *N b) *N x
|
||||
g rewrite addZeroRight (p *N (ab/p *N x)) = g''
|
||||
qsm : ((0 <N p) || ((0 ≡ p) && (ab/p ≡ 0))) → (0 <N p) || ((0 ≡ p) && (ab/p *N x ≡ 0))
|
||||
qsm (inl pr) = inl pr
|
||||
qsm (inr (pr1 ,, pr2)) = inr (pr1 ,, blah)
|
||||
where
|
||||
blah : ab/p *N x ≡ 0
|
||||
blah rewrite pr2 = refl
|
||||
inter2 : ((0 <N p) || ((0 ≡ p) && (ab/p ≡ 0))) → p ∣ (p *N (y *N b))
|
||||
inter2 (inl 0<p) = divides (record {quot = y *N b ; rem = 0 ; pr = addZeroRight (p *N (y *N b)) ; remIsSmall = zeroIsValidRem p ; quotSmall = inl 0<p }) refl
|
||||
inter2 (inr (0=p ,, ab/p=0)) = divides (record {quot = y *N b ; rem = 0 ; pr = addZeroRight (p *N (y *N b)) ; remIsSmall = zeroIsValidRem p ; quotSmall = inr (0=p ,, blah) }) refl
|
||||
where
|
||||
oneZero : (a ≡ 0) || (b ≡ 0)
|
||||
oneZero rewrite additionNIsCommutative (p *N ab/p) 0 | ab/p=0 | equalityCommutative 0=p = productZeroImpliesOperandZero (equalityCommutative p|ab)
|
||||
blah : y *N b ≡ 0
|
||||
blah with oneZero
|
||||
blah | inl x1 = exFalso (notp|a p|a)
|
||||
where
|
||||
p|a : p ∣ a
|
||||
p|a rewrite x1 = aDivZero p
|
||||
blah | inr x1 rewrite x1 = productZeroIsZeroRight y
|
||||
answer : ((a *N b) *N x ≡ (p *N (y *N b) +N b)) || (((a *N b) *N x +N b) ≡ p *N (y *N b)) → (p ∣ b)
|
||||
answer (inl z) = reduceEquationMod {p} b inter1 (inter2 quotSmall) z
|
||||
answer (inr z) = reduceEquationMod {p} b (inter2 quotSmall) inter1 (equalityCommutative z)
|
||||
|
||||
primesAreBiggerThanOne : {p : ℕ} → Prime p → (1 <N p)
|
||||
primesAreBiggerThanOne {zero} record { p>1 = (le x ()) ; pr = pr }
|
||||
primesAreBiggerThanOne {succ zero} pr = exFalso (oneIsNotPrime pr)
|
||||
primesAreBiggerThanOne {succ (succ p)} pr = succPreservesInequality (succIsPositive p)
|
||||
|
||||
primesAreBiggerThanZero : {p : ℕ} → Prime p → 0 <N p
|
||||
primesAreBiggerThanZero {p} pr = orderIsTransitive (succIsPositive 0) (primesAreBiggerThanOne pr)
|
||||
|
||||
record notDividedByLessThan (a : ℕ) (firstPossibleDivisor : ℕ) : Set where
|
||||
field
|
||||
previousDoNotDivide : ∀ x → 1 <N x → x <N firstPossibleDivisor → x ∣ a → False
|
||||
|
||||
alternativePrime : {a : ℕ} → 1 <N a → notDividedByLessThan a a → Prime a
|
||||
alternativePrime {a} 1<a record { previousDoNotDivide = previousDoNotDivide } = record { pr = pr ; p>1 = 1<a}
|
||||
where
|
||||
pr : {x : ℕ} → (x|a : x ∣ a) (x<a : x <N a) (0<x : zero <N x) → x ≡ 1
|
||||
pr {zero} _ _ (le x ())
|
||||
pr {succ zero} _ _ _ = refl
|
||||
pr {succ (succ x)} x|a x<a 0<x = exFalso (previousDoNotDivide (succ (succ x)) (succPreservesInequality (succIsPositive x)) x<a x|a)
|
||||
|
||||
divisibilityTransitive : {a b c : ℕ} → a ∣ b → b ∣ c → a ∣ c
|
||||
divisibilityTransitive {a} {b} {c} (divides record { quot = b/a ; rem = .0 ; pr = prDivAB ; remIsSmall = remIsSmallAB ; quotSmall = quotSmall } refl) (divides record { quot = c/b ; rem = .0 ; pr = prDivBC ; remIsSmall = remIsSmallBC } refl) = divides record { quot = b/a *N c/b ; rem = 0 ; pr = p ; remIsSmall = zeroIsValidRem a ; quotSmall = qsm quotSmall } refl
|
||||
where
|
||||
p : a *N (b/a *N c/b) +N 0 ≡ c
|
||||
p rewrite addZeroRight (a *N (b/a *N c/b)) | addZeroRight (b *N c/b) | addZeroRight (a *N b/a) | multiplicationNIsAssociative a b/a c/b | prDivAB | prDivBC = refl
|
||||
qsm : ((0 <N a) || (0 ≡ a) && (b/a ≡ 0)) → ((0 <N a) || (0 ≡ a) && (b/a *N c/b ≡ 0))
|
||||
qsm (inl x) = inl x
|
||||
qsm (inr (p1 ,, p2)) = inr (p1 ,, blah)
|
||||
where
|
||||
blah : b/a *N c/b ≡ 0
|
||||
blah rewrite p2 = refl
|
||||
|
||||
compositeOrPrimeLemma : {a b : ℕ} → notDividedByLessThan b a → a ∣ b → {i : ℕ} → (i ∣ a) → (i <N a) → (0 <N i) → i ≡ 1
|
||||
compositeOrPrimeLemma {a} {b} record { previousDoNotDivide = previousDoNotDivide } a|b {zero} i|a i<a 0<i = exFalso (lessIrreflexive 0<i)
|
||||
compositeOrPrimeLemma {a} {b} record { previousDoNotDivide = previousDoNotDivide } a|b {succ zero} i|a i<a 0<i = refl
|
||||
compositeOrPrimeLemma {a} {b} record { previousDoNotDivide = previousDoNotDivide } a|b {succ (succ i)} i|a i<a 0<i = exFalso (previousDoNotDivide (succ (succ i)) (succPreservesInequality (succIsPositive i)) i<a (divisibilityTransitive i|a a|b) )
|
||||
|
||||
compositeOrPrime : (a : ℕ) → (1 <N a) → (Composite a) || (Prime a)
|
||||
compositeOrPrime a pr = go''' go''
|
||||
where
|
||||
base : notDividedByLessThan a 2
|
||||
base = record { previousDoNotDivide = λ x 1<x x<2 _ → noIntegersBetweenXAndSuccX 1 1<x x<2 }
|
||||
go : {firstPoss : ℕ} → notDividedByLessThan a firstPoss → ((notDividedByLessThan a (succ firstPoss)) || ((firstPoss ∣ a) && (firstPoss <N a))) || (firstPoss ≡ a)
|
||||
go' : (firstPoss : ℕ) → (((notDividedByLessThan a firstPoss) || (Composite a))) || (notDividedByLessThan a a)
|
||||
go'' : (notDividedByLessThan a a) || (Composite a)
|
||||
go'' with go' a
|
||||
... | inr x = inl x
|
||||
... | inl x = x
|
||||
go''' : ((notDividedByLessThan a a) || (Composite a)) → ((Composite a) || (Prime a))
|
||||
go''' (inl x) = inr (alternativePrime pr x)
|
||||
go''' (inr x) = inl x
|
||||
go' (zero) = inl (inl (record { previousDoNotDivide = λ x 1<x x<0 _ → zeroNeverGreater x<0 }))
|
||||
go' (succ 0) = inl (inl (record { previousDoNotDivide = λ x 1<x x<1 _ → orderIsIrreflexive x<1 1<x }))
|
||||
go' (succ (succ zero)) = inl (inl base)
|
||||
go' (succ (succ (succ firstPoss))) with go' (succ (succ firstPoss))
|
||||
go' (succ (succ (succ firstPoss))) | inl (inl x) with go {succ (succ firstPoss)} x
|
||||
go' (succ (succ (succ firstPoss))) | inl (inl x) | inl (inl x1) = inl (inl x1)
|
||||
go' (succ (succ (succ firstPoss))) | inl (inl x) | inl (inr x1) = inl (inr record { noSmallerDivisors = λ i i<ssFP 1<i i|a → notDividedByLessThan.previousDoNotDivide x i 1<i i<ssFP i|a ; n>1 = pr ; divisor = succ (succ firstPoss) ; dividesN = _&&_.fst x1 ; divisorLessN = _&&_.snd x1 ; divisorNot1 = succPreservesInequality (succIsPositive firstPoss) ; divisorPrime = record { p>1 = succPreservesInequality (succIsPositive firstPoss) ; pr = compositeOrPrimeLemma {succ (succ firstPoss)} {a} x (_&&_.fst x1) } })
|
||||
go' (succ (succ (succ firstPoss))) | inl (inl x) | inr y rewrite y = inr x
|
||||
go' (succ (succ (succ firstPoss))) | inl (inr x) = inl (inr x)
|
||||
go' (succ (succ (succ firstPoss))) | inr x = inr x
|
||||
|
||||
go {zero} pr = inl (inl (record { previousDoNotDivide = λ x 1<x x<1 _ → orderIsIrreflexive x<1 1<x}))
|
||||
go {succ firstPoss} knownCoprime with orderIsTotal (succ firstPoss) a
|
||||
go {succ firstPoss} knownCoprime | inr x = inr x
|
||||
go {succ firstPoss} knownCoprime | inl (inl sFP<a) with divisionAlg (succ firstPoss) a
|
||||
go {succ firstPoss} knownCoprime | inl (inl sFP<a) | record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remIsSmall } = inl (inr record { fst = (divides (record { quot = quot ; rem = zero ; remIsSmall = remIsSmall ; pr = pr ; quotSmall = inl (succIsPositive firstPoss) }) refl) ; snd = sFP<a })
|
||||
go {succ firstPoss} knownCoprime | inl (inl sFP<a) | record { quot = quot ; rem = succ rem ; pr = pr ; remIsSmall = remIsSmall } = inl next
|
||||
where
|
||||
previous : ∀ x → 1 <N x → x <N succ firstPoss → x ∣ a → False
|
||||
previous = notDividedByLessThan.previousDoNotDivide knownCoprime
|
||||
next : notDividedByLessThan a (succ (succ firstPoss)) || (((succ firstPoss) ∣ a) && (succ firstPoss <N a))
|
||||
next with divisionAlg (succ firstPoss) a
|
||||
next | record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remIsSmall } = inr (record { fst = divides record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = inl (succIsPositive firstPoss) } refl ; snd = sFP<a } )
|
||||
next | record { quot = quot ; rem = succ rem ; pr = pr ; remIsSmall = remIsSmall } = inl record { previousDoNotDivide = (next' record { quot = quot ; rem = succ rem ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = inl (succIsPositive firstPoss) } (succIsPositive rem)) }
|
||||
where
|
||||
next' : (res : divisionAlgResult (succ firstPoss) a) → (pr : 0 <N divisionAlgResult.rem res) → (x : ℕ) → 1 <N x → x <N succ (succ firstPoss) → x ∣ a → False
|
||||
next' (res) (prDiv) x 1<x x<ssFirstposs x|a with orderIsTotal x (succ firstPoss)
|
||||
next' (res) (prDiv) x 1<x x<ssFirstposs x|a | inl (inl x<sFirstPoss) = previous x 1<x x<sFirstPoss x|a
|
||||
next' (res) (prDiv) x 1<x x<ssFirstposs x|a | inl (inr sFirstPoss<x) = noIntegersBetweenXAndSuccX (succ firstPoss) sFirstPoss<x x<ssFirstposs
|
||||
next' res prDiv x 1<x x<ssFirstposs (divides res1 x1) | inr x=sFirstPoss rewrite equalityCommutative x=sFirstPoss = g
|
||||
where
|
||||
g : False
|
||||
g with modIsUnique res res1
|
||||
... | r rewrite r = lessImpliesNotEqual prDiv (equalityCommutative x1)
|
||||
go {succ firstPoss} record { previousDoNotDivide = previousDoNotDivide } | inl (inr a<sFP) = exFalso (previousDoNotDivide a pr a<sFP (aDivA a))
|
||||
|
||||
primeDivPrimeImpliesEqual : {p1 p2 : ℕ} → Prime p1 → Prime p2 → p1 ∣ p2 → p1 ≡ p2
|
||||
primeDivPrimeImpliesEqual {p1} {p2} pr1 pr2 p1|p2 with orderIsTotal p1 p2
|
||||
primeDivPrimeImpliesEqual {p1} {p2} pr1 record { p>1 = p>1 ; pr = pr } p1|p2 | inl (inl p1<p2) with pr p1|p2 p1<p2 (primesAreBiggerThanZero {p1} pr1)
|
||||
... | p1=1 = exFalso (oneIsNotPrime contr)
|
||||
where
|
||||
contr : Prime 1
|
||||
contr rewrite p1=1 = pr1
|
||||
primeDivPrimeImpliesEqual {p1} {zero} pr1 pr2 p1|p2 | inl (inr p1>p2) = exFalso (zeroIsNotPrime pr2)
|
||||
primeDivPrimeImpliesEqual {p1} {succ p2} pr1 pr2 p1|p2 | inl (inr p1>p2) = exFalso (divisorIsSmaller p1|p2 p1>p2)
|
||||
primeDivPrimeImpliesEqual {p1} {p2} pr1 pr2 p1|p2 | inr p1=p2 = p1=p2
|
||||
|
||||
mult1Lemma : {a b : ℕ} → a *N succ b ≡ 1 → (a ≡ 1) && (b ≡ 0)
|
||||
mult1Lemma {a} {b} pr = record { fst = _&&_.fst p ; snd = q}
|
||||
where
|
||||
p : (a ≡ 1) && (succ b ≡ 1)
|
||||
p = productOneImpliesOperandsOne pr
|
||||
q : b ≡ zero
|
||||
q = succInjective (_&&_.snd p)
|
||||
|
||||
oneHasNoDivisors : {a : ℕ} → a ∣ 1 → a ≡ 1
|
||||
oneHasNoDivisors {a} (divides record { quot = zero ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall } refl) rewrite addZeroRight (a *N zero) | multiplicationNIsCommutative a zero | addZeroRight a = naughtE pr
|
||||
oneHasNoDivisors {a} (divides record { quot = (succ quot) ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall } refl) rewrite addZeroRight (a *N succ quot) = _&&_.fst (mult1Lemma pr)
|
||||
|
||||
notSmallerMeansGE : {a b : ℕ} → (a <N b → False) → b ≤N a
|
||||
notSmallerMeansGE {a} {b} notA<b with orderIsTotal a b
|
||||
notSmallerMeansGE {a} {b} notA<b | inl (inl x) = exFalso (notA<b x)
|
||||
notSmallerMeansGE {a} {b} notA<b | inl (inr x) = inl x
|
||||
notSmallerMeansGE {a} {b} notA<b | inr x = inr (equalityCommutative x)
|
||||
@@ -7,7 +7,7 @@ open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Rings.Definition
|
||||
open import Fields.Fields
|
||||
open import PrimeNumbers
|
||||
open import Numbers.Primes.PrimeNumbers
|
||||
open import Setoids.Setoids
|
||||
open import Setoids.Orders
|
||||
open import Functions
|
||||
|
||||
@@ -9,7 +9,7 @@ open import Groups.Lemmas
|
||||
open import Groups.Definition
|
||||
open import Rings.Definition
|
||||
open import Fields.Fields
|
||||
open import PrimeNumbers
|
||||
open import Numbers.Primes.PrimeNumbers
|
||||
open import Setoids.Setoids
|
||||
open import Setoids.Orders
|
||||
open import Functions
|
||||
|
||||
Reference in New Issue
Block a user