Book cauchy reals

Cubical/Data/Fin/Properties.agda

@@ -16,7 +16,7 @@ open import Cubical.HITs.PropositionalTruncation renaming (rec to ∥∥rec)
 
 open import Cubical.Data.Fin.Base as Fin
 open import Cubical.Data.Nat
-open import Cubical.Data.Nat.Order
+open import Cubical.Data.Nat.Order hiding (<-·sk-cancel)
 open import Cubical.Data.Empty as Empty
 open import Cubical.Data.Unit
 open import Cubical.Data.Sum

Cubical/Data/Int/Order.agda

@@ -9,6 +9,7 @@ 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 ℕ
+import Cubical.Data.Nat.Order as ℕ
 open import Cubical.Data.NatPlusOne.Base as ℕ₊₁
 open import Cubical.Data.Sigma
 
@@ -498,3 +499,45 @@ negsuc zero ≟ negsuc zero = eq refl
 negsuc zero ≟ negsuc (suc n) = gt (negsuc-≤-negsuc zero-≤pos)
 negsuc (suc m) ≟ negsuc zero = lt (negsuc-≤-negsuc zero-≤pos)
 negsuc (suc m) ≟ negsuc (suc n) = Trichotomy-pred (negsuc m ≟ negsuc n)
+
+0<_ : ℤ → Type
+0< pos zero = ⊥
+0< pos (suc n) = Unit
+0< negsuc n = ⊥
+
+isProp0< : ∀ n → isProp (0< n)
+isProp0< (pos (suc _)) _ _ = refl
+
+·0< : ∀ m n → 0< m → 0< n → 0< (m ℤ.· n)
+·0< (pos (suc m)) (pos (suc n)) _ _ =
+ subst (0<_) (pos+ (suc n) (m ℕ.· (suc n)) ∙ cong (pos (suc n) ℤ.+_) (pos·pos m (suc n))) _
+
+0<·ℕ₊₁ : ∀ m n → 0< (m ℤ.· pos (ℕ₊₁→ℕ n)) → 0< m
+0<·ℕ₊₁ (pos (suc m)) n x = _
+0<·ℕ₊₁ (negsuc n₁) (1+ n) x =
+  ⊥.rec (subst 0<_ (negsuc·pos n₁ (suc n)
+   ∙ congS -_ (cong (pos (suc n) ℤ.+_)
+     (sym (pos·pos n₁ (suc n))) ∙
+        sym (pos+ (suc n) (n₁ ℕ.· suc n)))) x)
+
++0< : ∀ m n → 0< m → 0< n → 0< (m ℤ.+ n)
++0< (pos (suc m)) (pos (suc n)) _ _ =
+ subst (0<_) (cong sucℤ (pos+ (suc m) n)) _
+
+0<→ℕ₊₁ : ∀ n → 0< n → Σ ℕ₊₁ λ m → n ≡ pos (ℕ₊₁→ℕ m)
+0<→ℕ₊₁ (pos (suc n)) x = (1+ n) , refl
+
+min-0< : ∀ m n → 0< m → 0< n → 0< (ℤ.min m n)
+min-0< (pos (suc zero)) (pos (suc n)) x x₁ = tt
+min-0< (pos (suc (suc n₁))) (pos (suc zero)) x x₁ = tt
+min-0< (pos (suc (suc n₁))) (pos (suc (suc n))) x x₁ =
+  +0< (sucℤ (ℤ.min (pos n₁) (pos n))) 1 (min-0< (pos (suc n₁)) (pos (suc n)) _ _) _
+
+ℕ≤→pos-≤-pos : ∀ m n → m ℕ.≤ n → pos m ≤ pos n
+ℕ≤→pos-≤-pos m n (k , p) = k , sym (pos+ m k) ∙∙ cong pos (ℕ.+-comm m k) ∙∙ cong pos p
+
+
+0≤x² : ∀ n → 0 ≤ n ℤ.· n
+0≤x² (pos n) = subst (0 ≤_) (pos·pos n n) zero-≤pos
+0≤x² (negsuc n) = subst (0 ≤_) (pos·pos (suc n) (suc n)
+  ∙ sym (negsuc·negsuc n n)) zero-≤pos

Cubical/Data/Int/Properties.agda

@@ -11,7 +11,7 @@ open import Cubical.Relation.Nullary
 
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Bool
-open import Cubical.Data.Nat
+open import Cubical.Data.Nat as ℕ
   hiding   (+-assoc ; +-comm ; min ; max ; minComm ; maxComm)
   renaming (_·_ to _·ℕ_; _+_ to _+ℕ_ ; ·-assoc to ·ℕ-assoc ;
             ·-comm to ·ℕ-comm ; isEven to isEvenℕ ; isOdd to isOddℕ)
@@ -1505,3 +1505,24 @@ sumFinℤ0 n = sumFinGen0 _+_ 0 (λ _ → refl) n (λ _ → 0) λ _ → refl
 sumFinℤHom : {n : ℕ} (f g : Fin n → ℤ)
   → sumFinℤ {n = n} (λ x → f x + g x) ≡ sumFinℤ {n = n} f + sumFinℤ {n = n} g
 sumFinℤHom {n = n} = sumFinGenHom _+_ 0 (λ _ → refl) +Comm +Assoc n
+
+abs-max : ∀ n → pos (abs n) ≡ max n (- n)
+abs-max (pos zero) = refl
+abs-max (pos (suc n)) = refl
+abs-max (negsuc n) = refl
+
+min-pos-pos : ∀ m n → min (pos m) (pos n) ≡ pos (ℕ.min m n)
+min-pos-pos zero n = refl
+min-pos-pos (suc m) zero = refl
+min-pos-pos (suc m) (suc n) = cong sucℤ (min-pos-pos m n)
+
+max-pos-pos : ∀ m n → max (pos m) (pos n) ≡ pos (ℕ.max m n)
+max-pos-pos zero n = refl
+max-pos-pos (suc m) zero = refl
+max-pos-pos (suc m) (suc n) = cong sucℤ (max-pos-pos m n)
+
+
+sign : ℤ → ℤ
+sign (pos zero) = 0
+sign (pos (suc n)) = 1
+sign (negsuc n) = -1

Cubical/Data/Nat/Mod.agda

@@ -4,7 +4,8 @@ module Cubical.Data.Nat.Mod where
 open import Cubical.Foundations.Prelude
 open import Cubical.Data.Nat
 open import Cubical.Data.Nat.Order
-open import Cubical.Data.Empty
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Sum as ⊎
 
 -- Defining x mod 0 to be 0. This way all the theorems below are true
 -- for n : ℕ instead of n : ℕ₊₁.
@@ -36,6 +37,9 @@ mod< n =
               , cong (λ x → fst ind + suc x)
                      (modIndStep n x) ∙ snd ind
 
+<→mod : (n x : ℕ) → x < (suc n) → x mod (suc n) ≡ x
+<→mod = modIndBase
+
 mod-rUnit : (n x : ℕ) → x mod n ≡ ((x + n) mod n)
 mod-rUnit zero x = refl
 mod-rUnit (suc n) x =
@@ -153,6 +157,7 @@ mod-lCancel n x y =
   ∙∙ mod-rCancel n y x
   ∙∙ cong (_mod n) (+-comm y (x mod n))
 
+
 -- remainder and quotient after division by n
 -- Again, allowing for 0-division to get nicer syntax
 remainder_/_ : (x n : ℕ) → ℕ
@@ -192,3 +197,117 @@ private
 
   test₁ : ((11 + (10 mod 3)) mod 3) ≡ 0
   test₁ = refl
+
+
+
+·mod : ∀ k n m → (k · n) mod (k · m)
+             ≡ k · (n mod m)
+·mod zero n m = refl
+·mod (suc k) n zero = cong ((n + k · n) mod_) (sym (0≡m·0 (suc k)))
+                  ∙ 0≡m·0 (suc k)
+·mod (suc k) n (suc m) = ·mod' n n ≤-refl (splitℕ-≤ (suc m) n)
+
+ where
+ ·mod' : ∀ N n → n ≤ N → ((suc m) ≤ n) ⊎ (n < suc m) →
+    ((suc k · n) mod (suc k · suc m)) ≡ suc k · (n mod suc m)
+ ·mod' _ zero x _ = cong (modInd (m + k · suc m)) (sym (0≡m·0 (suc k)))
+                  ∙ 0≡m·0 (suc k)
+ ·mod' zero (suc n) x _ = ⊥.rec (¬-<-zero x)
+ ·mod' (suc N) n@(suc n') x (inl (m' , p)) =
+  let z = ·mod' N m' (≤-trans (m
+               , +-comm m m' ∙ injSuc (sym (+-suc m' m) ∙ p))
+              (pred-≤-pred x)) (splitℕ-≤ _ _) ∙ cong ((suc k) ·_)
+            (sym (modIndStep m m') ∙
+             cong (_mod (suc m)) (+-comm (suc m) m' ∙ p))
+  in (cong (λ y → ((suc k · y) mod (suc k · suc m))) (sym p)
+       ∙ cong {x = (m' + suc m + k · (m' + suc m))}
+               {suc (m + k · suc m + (m' + k · m'))}
+            (modInd (m + k · suc m))
+              (cong (_+ k · (m' + suc m)) (+-suc m' m ∙ cong suc (+-comm m' m))
+                 ∙ cong suc
+                  (sym (+-assoc m m' _)
+                    ∙∙ cong (m +_)
+                       (((cong (m' +_) (sym (·-distribˡ k _ _)
+                         ∙ +-comm (k · m') _) ∙ +-assoc m' (k · suc m) (k · m'))
+                        ∙ cong (_+ k · m') (+-comm m' _))
+                        ∙ sym (+-assoc (k · suc m) m' (k · m')) )
+                    ∙∙ +-assoc m _ _))
+         ∙ modIndStep (m + k · suc m) (m' + k · m')) ∙ z
+ ·mod' (suc N) n x (inr x₁) =
+   modIndBase _ _ (
+     subst2 _<_ (·-comm n (suc k)) (·-comm _ (suc k))
+      (<-·sk {n} {suc m} {k = k} x₁) )
+    ∙ cong ((suc k) ·_) (sym (modIndBase _ _ x₁))
+
+2≤x→1<quotient[x/2] : ∀ n → 0 < quotient (2 + n) / 2
+2≤x→1<quotient[x/2] n =
+ let z : 0 < ((quotient (2 + n) / 2) · 2)
+     z = subst (0 <_) (·-comm 2 (quotient (2 + n) / 2))
+          (≤<-trans {m = n }
+             {n = 2 · (quotient (2 + n) / 2)} zero-≤
+            (<-k+-cancel (subst (_< 2 +
+             (2 · (quotient (2 + n) / 2)))
+           (≡remainder+quotient 2 (2 + n))
+             (<-+k {k = 2 · (quotient (2 + n) / 2)}
+              (mod< 1 (2 + n))))))
+ in <-·sk-cancel {0} {quotient (2 + n) / 2 } {k = 1} z
+
+
+
+2≤x→quotient[x/2]<x : ∀ n → quotient (2 + n) / 2 < (2 + n)
+2≤x→quotient[x/2]<x n =
+  subst ((quotient 2 + n / 2) <_)
+    (≡remainder+quotient 2 (2 + n))
+    (<≤-trans
+      ( subst ((quotient 2 + n / 2) <_)
+          ((cong ((quotient 2 + n / 2) +_)
+            (sym (+-zero (quotient 2 + n / 2)))))
+            (<-+k {k = (quotient 2 + n / 2)}
+             (2≤x→1<quotient[x/2] n)) )
+      (≤SumRight {_} {(remainder 2 + n / 2)}))
+
+
+-- -- TODO: shoulld be easy to generalise to other nuumbers than 2
+
+-- log2ℕ : ∀ n → Σ _ (Minimal.Least (λ k → n < 2 ^ k))
+-- log2ℕ n = w n n ≤-refl
+--  where
+
+--   w : ∀ N n → n ≤ N
+--           → Σ _ (Minimal.Least (λ k → n < 2 ^ k))
+--   w N zero x = 0 , (≤-refl , λ k' q → ⊥.rec (¬-<-zero q))
+--   w N (suc zero) x = 1 , (≤-refl ,
+--      λ { zero q → <-asym (suc-≤-suc ≤-refl)
+--       ; (suc k') q → ⊥.rec (¬-<-zero (pred-≤-pred q))})
+--   w zero (suc (suc n)) x = ⊥.rec (¬-<-zero x)
+--   w (suc N) (suc (suc n)) x =
+--    let (k , (X , Lst)) = w N
+--           (quotient 2 + n / 2)
+--           (≤-trans (pred-≤-pred (2≤x→quotient[x/2]<x n))
+--              (pred-≤-pred x))
+--        z = ≡remainder+quotient 2 (2 + n)
+--        zz = <-+-≤ X X
+--        zzz : suc (suc n) < (2 ^ suc k)
+--        zzz = subst2 (_<_)
+--            (+-comm ({!remainder 2 + n / 2!} +
+--                      (({!!})))
+--                       ({!!})
+--               ∙ sym (+-assoc _ _ _)
+--                ∙ cong ((remainder 2 + n / 2) +_)
+--              ((cong ((quotient 2 + n / 2) +_)
+--               (sym (+-zero (quotient 2 + n / 2)))))
+--              ∙ z)
+--            (cong ((2 ^ k) +_) (sym (+-zero (2 ^ k))))
+--            ((≤<-trans
+--              (≤-k+ {k = _}
+--                (≤-+k {k = {!!}} (pred-≤-pred (mod< 1 (2 + n))))) zz))
+--    in (suc k)
+--        , zzz
+--         , λ { zero 0'<sk 2+n<2^0' →
+--                 ⊥.rec (¬-<-zero (pred-≤-pred 2+n<2^0'))
+--             ; (suc k') k'<sk 2+n<2^k' →
+--                Lst k' (pred-≤-pred k'<sk)
+--                 (<-·sk-cancel {k = 1}
+--                     (subst2 _<_ (·-comm _ _) (·-comm _ _)
+--                       (≤<-trans (_ , z)
+--                          2+n<2^k' )))}

Cubical/Data/Nat/Order.agda

@@ -142,6 +142,11 @@ suc-< p = pred-≤-pred (≤-suc p)
            (d + m) · k   ≡⟨ cong (_· k) r ⟩
            n · k         ∎
 
+≤-k· : m ≤ n → k · m ≤ k · n
+≤-k· {m} {n} {k} p =
+  subst2 _≤_ (·-comm m k) (·-comm n k)
+    (≤-·k p)
+
 <-k+-cancel : k + m < k + n → m < n
 <-k+-cancel {k} {m} {n} = ≤-k+-cancel ∘ subst (_≤ k + n) (sym (+-suc k m))
 
@@ -224,6 +229,17 @@ predℕ-≤-predℕ {suc m} {suc n} ineq = pred-≤-pred ineq
            (d + suc m) · suc k               ≡⟨ cong (_· suc k) r ⟩
            n · suc k                         ∎
 
+
+<-·sk-cancel : ∀ {m n k} → m · suc k < n · suc k → m < n
+<-·sk-cancel {n = zero} x = ⊥.rec (¬-<-zero x)
+<-·sk-cancel {zero} {n = suc n} x = suc-≤-suc (zero-≤ {n})
+<-·sk-cancel {suc m} {n = suc n} {k} x =
+  suc-≤-suc {suc m} {n}
+    (<-·sk-cancel {m} {n} {k}
+     (≤-k+-cancel (subst (_≤ (k + n · suc k))
+       (sym (+-suc _ _)) (pred-≤-pred x))))
+
+
 ∸-≤ : ∀ m n → m ∸ n ≤ m
 ∸-≤ m zero = ≤-refl
 ∸-≤ zero (suc n) = ≤-refl
@@ -480,6 +496,12 @@ n∸l>0  zero   (suc l) r = ⊥.rec (¬-<-zero r)
 n∸l>0 (suc n)  zero   r = suc-≤-suc zero-≤
 n∸l>0 (suc n) (suc l) r = n∸l>0 n l (pred-≤-pred r)
 
+[n-m]+m : ∀ m n → m ≤ n → (n ∸ m) + m ≡ n
+[n-m]+m zero n _ = +-zero n
+[n-m]+m (suc m) zero p = ⊥.rec (¬-<-zero p)
+[n-m]+m (suc m) (suc n) p =
+  +-suc _ _ ∙ cong suc ([n-m]+m m n (pred-≤-pred p))
+
 -- automation
 
 ≤-solver-type : (m n : ℕ) → Trichotomy m n → Type
@@ -545,3 +567,25 @@ pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 ≤-∸-≥ n (suc l)  zero   r = ⊥.rec (¬-<-zero r)
 ≤-∸-≥  zero   (suc l) (suc k) r = ≤-refl
 ≤-∸-≥ (suc n) (suc l) (suc k) r = ≤-∸-≥ n l k (pred-≤-pred r)
+
+elimBy≤ : ∀ {ℓ} {A : ℕ → ℕ → Type ℓ}
+  → (∀ x y → A x y → A y x)
+  → (∀ x y → x ≤ y → A x y)
+  → ∀ x y → A x y
+elimBy≤ {A = A} s f n m = ≤CaseInduction {P = A}
+  (f _ _) (s _ _ ∘ f _ _ )
+
+elimBy≤+ : ∀ {ℓ} {A : ℕ → ℕ → Type ℓ}
+  → (∀ x y → A x y → A y x)
+  → (∀ x y → A x (y + x))
+  → ∀ x y → A x y
+elimBy≤+ {A = A} s f =
+ elimBy≤ s λ x y (y' , p) → subst (A x) p (f x y')
+
+module Minimal where
+  Least : ∀{ℓ} → (ℕ → Type ℓ) → (ℕ → Type ℓ)
+  Least P m = P m × (∀ n → n < m → ¬ P n)
+
+  isPropLeast : {P : ℕ → Type ℓ} → (∀ m → isProp (P m)) → ∀ m → isProp (Least P m)
+  isPropLeast pP m
+    = isPropΣ (pP m) (λ _ → isPropΠ3 λ _ _ _ → isProp⊥)

Cubical/Data/Nat/Order/Recursive.agda

@@ -54,6 +54,26 @@ isProp≤ {suc m} {suc n} = isProp≤ {m} {n}
 ≤-k+ {k = zero}  m≤n = m≤n
 ≤-k+ {k = suc k} m≤n = ≤-k+ {k = k} m≤n
 
+<-weaken : m < n → m ≤ n
+<-weaken {zero} _ = _
+<-weaken {suc m} {suc n} = <-weaken {m}
+
+<-+-weaken : m < n → m < k + n
+<-+-weaken {k = zero} x = x
+<-+-weaken {m = zero} {n = suc n} {k = suc k} x = _
+<-+-weaken {m = suc m} {n = n} {k = suc k} x = <-+-weaken {m = m} {n = n} {k = k} (<-weaken {suc m} {n} x)
+
++-<-+ : k < l → m < n →  k + m < l + n
++-<-+ {zero} {l = suc l} {m} {n = suc n} x x₁ = <-+-weaken {m = m} {n = suc n} {k = 1 + l} x₁
++-<-+ {suc k} {l = suc l} {m} {n = n} x x₁ = +-<-+ {k} {l} {m} {n} x x₁
+
++-≤-+ : k ≤ l → m ≤ n →  k + m ≤ l + n
++-≤-+ {zero} {zero} {n = n} _ x = x
++-≤-+ {zero} {suc l} {zero} {n = n} x y = _
++-≤-+ {zero} {suc l} {suc m} {n = n} x y = +-≤-+ {0} {l} {m} {n} x (<-weaken {m} {n} y)
++-≤-+ {suc k} {zero} {n = n} ()
++-≤-+ {suc k} {suc l} {m} {n = n} = +-≤-+ {k} {l} {m} {n}
+
 ≤-+k : m ≤ n → m + k ≤ n + k
 ≤-+k {m} {n} {k} m≤n
   = transport (λ i → +-comm k m i ≤ +-comm k n i) (≤-k+ {m} {n} {k} m≤n)
@@ -87,10 +107,6 @@ isProp≤ {suc m} {suc n} = isProp≤ {m} {n}
 ¬m+n<m : ¬ m + n < m
 ¬m+n<m {suc m} = ¬m+n<m {m}
 
-<-weaken : m < n → m ≤ n
-<-weaken {zero} _ = _
-<-weaken {suc m} {suc n} = <-weaken {m}
-
 <-trans : k < m → m < n → k < n
 <-trans {k} {m} {n} k<m m<n
   = ≤-trans {suc k} {m} {n} k<m (<-weaken {m} m<n)
@@ -125,6 +141,10 @@ n≤k+n {k} n = transport (λ i → n ≤ +-comm n k i) (k≤k+n n)
 ≤-split {suc m} {suc n} m≤n
   = Sum.map (idfun _) (cong suc) (≤-split {m} {n} m≤n)
 
+<→¬≥ : n < m → ¬ m ≤ n
+<→¬≥ {suc n} {suc m} p q = <→¬≥ {n} {m} p q
+
+
 module WellFounded where
   wf-< : WellFounded _<_
   wf-rec-< : ∀ n → WFRec _<_ (Acc _<_) n

Cubical/Data/Nat/Properties.agda

@@ -56,6 +56,10 @@ codeℕ zero (suc m) = ⊥
 codeℕ (suc n) zero = ⊥
 codeℕ (suc n) (suc m) = codeℕ n m
 
+codeℕ-trans : codeℕ n m → codeℕ m l → codeℕ n l
+codeℕ-trans {zero} {zero} {zero} _ _ = tt
+codeℕ-trans {suc n} {suc m} {suc l} = codeℕ-trans {n} {m} {l}
+
 encodeℕ : (n m : ℕ) → (n ≡ m) → codeℕ n m
 encodeℕ n m p = subst (λ m → codeℕ n m) p (reflCode n)
  where