Skip to content

Commit

Permalink
Add multiplication cancelling to rationals
Browse files Browse the repository at this point in the history
  • Loading branch information
LuuBluum committed Oct 27, 2023
1 parent ca40e3e commit b10112f
Show file tree
Hide file tree
Showing 2 changed files with 139 additions and 17 deletions.
82 changes: 65 additions & 17 deletions Cubical/Data/Int/Order.agda
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,14 @@
module Cubical.Data.Int.Order where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Empty as ⊥ using (⊥)
open import Cubical.Data.Int.Base as ℤ
open import Cubical.Data.Int.Properties as ℤ
open import Cubical.Data.Nat as ℕ
open import Cubical.Data.NatPlusOne.Base as ℕ₊₁
open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary
Expand Down Expand Up @@ -53,6 +55,29 @@ isProp< = isProp≤
zero-≤pos : 0 ≤ pos l
zero-≤pos {l} = l , (sym (pos0+ (pos l)))

¬-pos<-zero : ¬ (pos k) < 0
¬-pos<-zero {k} (i , p) = snotz (injPos (pos+ (suc k) i ∙ p))

negsuc<-zero : negsuc k < 0
negsuc<-zero {k} = k ,
((sucℤ (negsuc k) +pos k) ≡⟨ sym (sucℤ+ (negsuc k) (pos k)) ⟩
sucℤ (negsuc k +pos k) ≡⟨ +sucℤ (negsuc k) (pos k) ⟩
neg (suc k) ℤ.+ pos (suc k) ≡⟨ -Cancel' (pos (suc k)) ⟩
pos zero ∎)

¬pos≤negsuc : ¬ (pos k) ≤ negsuc l
¬pos≤negsuc {k} {l} (i , p) = posNotnegsuc (k ℕ.+ i) l (pos+ k i ∙ p)

negsuc<pos : negsuc k < pos l
negsuc<pos {zero} {zero} = 0 , refl
negsuc<pos {zero} {suc l} = suc l , sym (pos0+ (pos (suc l)))
negsuc<pos {suc k} {zero} = suc k , -Cancel' (pos (suc k))
negsuc<pos {suc k} {suc l} = suc k ℕ.+ suc l
, cong (negsuc k ℤ.+_) (pos+ (suc k) (suc l)) ∙
+Assoc (negsuc k) (pos (suc k)) (pos (suc l)) ∙
cong (ℤ._+ pos (suc l)) (-Cancel' (pos (suc k))) ∙
sym (pos0+ (pos (suc l)))

suc-≤-suc : m ≤ n sucℤ m ≤ sucℤ n
suc-≤-suc {m} {n} (k , p) = k , (sym (sucℤ+pos k m) ∙ cong sucℤ p)

Expand Down Expand Up @@ -176,6 +201,10 @@ isAntisym≤ {m} {n} (i , p) (j , q)
(m +pos i) ℤ.· pos k ≡⟨ cong (ℤ._· pos k) p ⟩
n ℤ.· pos k ∎)

0≤o→≤-·o : 0 ≤ o m ≤ n m ℤ.· o ≤ n ℤ.· o
0≤o→≤-·o {pos o} 0≤o m≤n = ≤-·o {k = o} m≤n
0≤o→≤-·o {negsuc o} 0≤o _ = ⊥.rec (¬pos≤negsuc 0≤o)

<-·o : m < n m ℤ.· (pos (suc k)) < n ℤ.· (pos (suc k))
<-·o {m} {n} {k} (i , p) = (i ℕ.· suc k ℕ.+ k) ,
((sucℤ (m ℤ.· pos (suc k)) +pos (i ℕ.· suc k ℕ.+ k)) ≡⟨ cong (sucℤ (m ℤ.· pos (suc k)) ℤ.+_)
Expand All @@ -199,18 +228,8 @@ isAntisym≤ {m} {n} (i , p) (j , q)
<-o+-cancel : o ℤ.+ m < o ℤ.+ n m < n
<-o+-cancel {o} {m} {n} = ≤-o+-cancel ∘ subst (_≤ o ℤ.+ n) (+sucℤ o m)

¬-pos<-zero : ¬ (pos k) < 0
¬-pos<-zero {k} (i , p) = snotz (injPos (pos+ (suc k) i ∙ p))

negsuc<-zero : negsuc k < 0
negsuc<-zero {k} = k ,
((sucℤ (negsuc k) +pos k) ≡⟨ sym (sucℤ+ (negsuc k) (pos k)) ⟩
sucℤ (negsuc k +pos k) ≡⟨ +sucℤ (negsuc k) (pos k) ⟩
neg (suc k) ℤ.+ pos (suc k) ≡⟨ -Cancel' (pos (suc k)) ⟩
pos zero ∎)

¬pos≤negsuc : ¬ (pos k) ≤ negsuc l
¬pos≤negsuc {k} {l} (i , p) = posNotnegsuc (k ℕ.+ i) l (pos+ k i ∙ p)
<-weaken : m < n m ≤ n
<-weaken {m} (i , p) = (suc i) , sucℤ+ m (pos i) ∙ p

isIrrefl< : ¬ m < m
isIrrefl< {pos zero} (i , p) = snotz (injPos (pos+ (suc zero) i ∙ p))
Expand All @@ -227,6 +246,11 @@ isIrrefl< {negsuc (suc n)} (i , p) = isIrrefl< {m = negsuc n} (i ,
sucℤ (negsuc n +pos i) ≡⟨ cong sucℤ p ⟩
negsuc n ∎))

0<o→<-·o : 0 < o m < n m ℤ.· o < n ℤ.· o
0<o→<-·o {pos zero} 0<o _ = ⊥.rec (isIrrefl< 0<o)
0<o→<-·o {pos (suc o)} 0<o m<n = <-·o {k = o} m<n
0<o→<-·o {negsuc o} 0<o _ = ⊥.rec (¬pos≤negsuc (<-weaken 0<o))

pos≤0→≡0 : pos k ≤ 0 pos k ≡ 0
pos≤0→≡0 {zero} _ = refl
pos≤0→≡0 {suc k} p = ⊥.rec (¬-pos<-zero {k = k} p)
Expand All @@ -240,9 +264,6 @@ predℤ-≤-predℤ {m} {n} (i , p) = i ,
¬m+posk<m : ¬ m ℤ.+ pos k < m
¬m+posk<m {m} {k} = ¬-pos<-zero ∘ <-o+-cancel {o = m} {m = pos k} {n = 0}

<-weaken : m < n m ≤ n
<-weaken {m} (i , p) = (suc i) , sucℤ+ m (pos i) ∙ p

≤<-trans : o ≤ m m < n o < n
≤<-trans p = isTrans≤ (suc-≤-suc p)

Expand Down Expand Up @@ -305,6 +326,11 @@ isAsym< m<n = isIrrefl< ∘ <≤-trans m<n
(-Cancel (n ℤ.· pos (suc k)))
(≤-+o {o = - (n ℤ.· pos (suc k))} mk≤nk))))

0<o→≤-·o-cancel : 0 < o m ℤ.· o ≤ n ℤ.· o m ≤ n
0<o→≤-·o-cancel {pos zero} 0<o _ = ⊥.rec (isIrrefl< 0<o)
0<o→≤-·o-cancel {pos (suc o)} 0<o mo≤no = ≤-·o-cancel {k = o} mo≤no
0<o→≤-·o-cancel {negsuc o} 0<o _ = ⊥.rec (¬pos≤negsuc 0<o)

≤-o·-cancel : (pos (suc k)) ℤ.· m ≤ (pos (suc k)) ℤ.· n m ≤ n
≤-o·-cancel {k} {m} {n} = ≤-·o-cancel ∘ (subst2 _≤_ (·Comm (pos (suc k)) m) (·Comm (pos (suc k)) n))

Expand All @@ -320,9 +346,31 @@ isAsym< m<n = isIrrefl< ∘ <≤-trans m<n
(-Cancel (n ℤ.· pos (suc k)))
(<-+o {o = - (n ℤ.· pos (suc k))} mk<nk))))

0<o→<-·o-cancel : 0 < o m ℤ.· o < n ℤ.· o m < n
0<o→<-·o-cancel {pos zero} 0<o _ = ⊥.rec (isIrrefl< 0<o)
0<o→<-·o-cancel {pos (suc o)} 0<o mo<no = <-·o-cancel {k = o} mo<no
0<o→<-·o-cancel {negsuc o} 0<o _ = ⊥.rec (¬pos≤negsuc 0<o)

<-o·-cancel : (pos (suc k)) ℤ.· m < (pos (suc k)) ℤ.· n m < n
<-o·-cancel {k} {m} {n} = <-·o-cancel ∘ (subst2 _<_ (·Comm (pos (suc k)) m) (·Comm (pos (suc k)) n))

-Dist≤ : m ≤ n (- n) ≤ (- m)
-Dist≤ {pos zero} {pos zero} _ = isRefl≤
-Dist≤ {pos zero} {pos (suc n)} _ = <-weaken negsuc<-zero
-Dist≤ {pos (suc m)} {pos zero} = ⊥.rec ∘ snotz ∘ injPos ∘ pos≤0→≡0
-Dist≤ {pos (suc m)} {pos (suc n)} = suc-≤-suc ∘ negsuc-≤-negsuc
-Dist≤ {pos m} {negsuc n} = ⊥.rec ∘ ¬pos≤negsuc
-Dist≤ {negsuc zero} {pos zero} = suc-≤-suc
-Dist≤ {negsuc zero} {pos (suc n)} = suc-≤-suc ∘ -Dist≤ ∘ suc-≤-suc
-Dist≤ {negsuc (suc m)} {pos zero} _ = zero-≤pos
-Dist≤ {negsuc (suc m)} {pos (suc n)} _ = negsuc<pos
-Dist≤ {negsuc m} {negsuc n} = suc-≤-suc ∘ pos-≤-pos

-Dist< : m < n (- n) < (- m)
-Dist< {m} {n} = subst (- n <_) (cong sucℤ (-sucℤ m) ∙ sucPred (- m))
∘ suc-≤-suc
∘ -Dist≤

≤max : m ≤ ℤ.max m n
≤max {pos zero} {pos m} = zero-≤pos
≤max {pos (suc m)} {pos zero} = isRefl≤
Expand All @@ -346,7 +394,7 @@ isAsym< m<n = isIrrefl< ∘ <≤-trans m<n
≤→max {negsuc m} {pos n} m≤n = refl
≤→max {negsuc zero} {negsuc zero} m≤n = refl
≤→max {negsuc zero} {negsuc (suc n)} m≤n
= rec (snotz (injPos (pos≤0→≡0 (pos-≤-pos m≤n))))
= ⊥.rec (snotz (injPos (pos≤0→≡0 (pos-≤-pos m≤n))))
≤→max {negsuc (suc m)} {negsuc zero} m≤n = refl
≤→max {negsuc (suc m)} {negsuc (suc n)} m≤n
= cong predℤ (≤→max {m = negsuc m} {n = negsuc n} (suc-≤-suc m≤n))
Expand Down
74 changes: 74 additions & 0 deletions Cubical/Data/Rationals/Order.agda
Original file line number Diff line number Diff line change
Expand Up @@ -436,6 +436,80 @@ isTrans≤< =
(subst (_ ℤ.<_) (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
(ℤ.<-·o {k = -1+ b} cf<ed)) )}

≤-·o : m n o 0 ≤ o m ≤ n m ℚ.· o ≤ n ℚ.· o
≤-·o =
elimProp3 {P = λ a b c 0 ≤ c a ≤ b a ℚ.· c ≤ b ℚ.· c}
(λ x y z isPropΠ2 λ _ _ isProp≤ (x ℚ.· z) (y ℚ.· z))
λ { (a , b) (c , d) (e , f) 0≤e ad≤cb
subst2 ℤ._≤_ (cong (ℤ._· ℕ₊₁→ℤ f) (·CommR a (ℕ₊₁→ℤ d) e) ∙
sym (ℤ.·Assoc (a ℤ.· e) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
cong (a ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
(cong (ℤ._· ℕ₊₁→ℤ f) (·CommR c (ℕ₊₁→ℤ b) e) ∙
sym (ℤ.·Assoc (c ℤ.· e) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
cong (c ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
(ℤ.≤-·o {k = ℕ₊₁→ℕ f}
(ℤ.0≤o→≤-·o (subst (0 ℤ.≤_) (ℤ.·IdR e) 0≤e) ad≤cb)) }

≤-·o-cancel : m n o 0 < o m ℚ.· o ≤ n ℚ.· o m ≤ n
≤-·o-cancel =
elimProp3 {P = λ a b c 0 < c a ℚ.· c ≤ b ℚ.· c a ≤ b}
(λ x y _ isPropΠ2 λ _ _ isProp≤ x y)
λ { (a , b) (c , d) (e , f) 0<e aedf≤cebf
ℤ.0<o→≤-·o-cancel (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e)
(subst2 ℤ._≤_ (·CommR a e (ℕ₊₁→ℤ d)) (·CommR c e (ℕ₊₁→ℤ b))
(ℤ.≤-·o-cancel {k = -1+ f}
(subst2 ℤ._≤_ (sym (ℤ.·Assoc a e (ℕ₊₁→ℤ (d ·₊₁ f))) ∙
cong (λ x a ℤ.· (e ℤ.· x))
(ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)) ∙
assoc {a} {e})
(sym (ℤ.·Assoc c e (ℕ₊₁→ℤ (b ·₊₁ f))) ∙
cong (λ x c ℤ.· (e ℤ.· x))
(ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)) ∙
assoc {c} {e})
aedf≤cebf))) }

where assoc : {a b c d} a ℤ.· (b ℤ.· (c ℤ.· d)) ≡ a ℤ.· b ℤ.· c ℤ.· d
assoc {a} {b} {c} {d} = cong (a ℤ.·_) (ℤ.·Assoc b c d) ∙
ℤ.·Assoc a (b ℤ.· c) d ∙
cong (ℤ._· d) (ℤ.·Assoc a b c)

<-·o : m n o 0 < o m < n m ℚ.· o < n ℚ.· o
<-·o =
elimProp3 {P = λ a b c 0 < c a < b a ℚ.· c < b ℚ.· c}
(λ x y z isPropΠ2 λ _ _ isProp< (x ℚ.· z) (y ℚ.· z))
λ { (a , b) (c , d) (e , f) 0<e ad<cb
subst2 ℤ._<_ (cong (ℤ._· ℕ₊₁→ℤ f) (·CommR a (ℕ₊₁→ℤ d) e) ∙
sym (ℤ.·Assoc (a ℤ.· e) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
cong (a ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
(cong (ℤ._· ℕ₊₁→ℤ f) (·CommR c (ℕ₊₁→ℤ b) e) ∙
sym (ℤ.·Assoc (c ℤ.· e) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
cong (c ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
(ℤ.<-·o {k = -1+ f}
(ℤ.0<o→<-·o (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e) ad<cb)) }

<-·o-cancel : m n o 0 < o m ℚ.· o < n ℚ.· o m < n
<-·o-cancel =
elimProp3 {P = λ a b c 0 < c a ℚ.· c < b ℚ.· c a < b}
(λ x y _ isPropΠ2 λ _ _ isProp< x y)
λ { (a , b) (c , d) (e , f) 0<e aedf<cebf
ℤ.0<o→<-·o-cancel (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e)
(subst2 ℤ._<_ (·CommR a e (ℕ₊₁→ℤ d)) (·CommR c e (ℕ₊₁→ℤ b))
(ℤ.<-·o-cancel {k = -1+ f}
(subst2 ℤ._<_ (sym (ℤ.·Assoc a e (ℕ₊₁→ℤ (d ·₊₁ f))) ∙
cong (λ x a ℤ.· (e ℤ.· x))
(ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)) ∙
assoc {a} {e})
(sym (ℤ.·Assoc c e (ℕ₊₁→ℤ (b ·₊₁ f))) ∙
cong (λ x c ℤ.· (e ℤ.· x))
(ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)) ∙
assoc {c} {e})
aedf<cebf))) }

where assoc : {a b c d} a ℤ.· (b ℤ.· (c ℤ.· d)) ≡ a ℤ.· b ℤ.· c ℤ.· d
assoc {a} {b} {c} {d} = cong (a ℤ.·_) (ℤ.·Assoc b c d) ∙
ℤ.·Assoc a (b ℤ.· c) d ∙
cong (ℤ._· d) (ℤ.·Assoc a b c)

min≤ : m n ℚ.min m n ≤ m
min≤
= elimProp2 {P = λ a b ℚ.min a b ≤ a}
Expand Down

0 comments on commit b10112f

Please sign in to comment.