Book cauchy reals

Cubical/Algebra/Group/MorphismProperties.agda

@@ -310,3 +310,18 @@ BijectionIso→GroupIso {G = G} {H = H} i = grIso
 
 BijectionIsoToGroupEquiv : BijectionIso G H → GroupEquiv G H
 BijectionIsoToGroupEquiv i = GroupIso→GroupEquiv (BijectionIso→GroupIso i)
+
+Aut[_] : Group ℓ → Group ℓ
+Aut[ Ĝ@(G , Gstr) ] =
+  makeGroup {G = GroupIso Ĝ Ĝ}
+    idGroupIso compGroupIso
+      invGroupIso  (isSetΣ (isSet-SetsIso (is-set Gstr) (is-set Gstr)) (λ _ → isProp→isSet (isPropIsGroupHom _ _)))
+        (λ _ _ _ → GroupIso≡ (i≡ refl))
+         (λ _ → GroupIso≡ (i≡ refl))
+         (λ _ → GroupIso≡ (i≡ refl))
+         (λ (x , _) → GroupIso≡ (i≡ (funExt (Iso.leftInv x))))
+         (λ (x , _) → GroupIso≡ (i≡ (funExt (Iso.rightInv x))))
+ where
+ open GroupStr Gstr
+
+ i≡ = SetsIso≡fun (is-set Gstr) (is-set Gstr)

Cubical/Algebra/Ring/Properties.agda

@@ -90,6 +90,13 @@ module RingTheory (R' : Ring ℓ) where
                     (0r · x) + (0r · x)  ∎
               in +Idempotency→0 _ 0·x-is-idempotent
 
+
+  0RightAnnihilates' : (x y : R) → y ≡ 0r → x · y ≡ 0r
+  0RightAnnihilates' x y p = cong (x ·_) p ∙ 0RightAnnihilates x
+
+  0LeftAnnihilates' : (x y : R) → x ≡ 0r → x · y ≡ 0r
+  0LeftAnnihilates' x y p = cong (_· y) p ∙ 0LeftAnnihilates y
+
   -DistR· : (x y : R) →  x · (- y) ≡ - (x · y)
   -DistR· x y = implicitInverse (x · y) (x · (- y))
 
@@ -152,6 +159,42 @@ module RingTheory (R' : Ring ℓ) where
   ·-assoc2 : (x y z w : R) → (x · y) · (z · w) ≡ x · (y · z) · w
   ·-assoc2 x y z w = ·Assoc (x · y) z w ∙ congL _·_ (sym (·Assoc x y z))
 
+  +IdR' : ∀ x y → y ≡ 0r → x + y ≡ x
+  +IdR' x y y=0 = cong (x +_) y=0 ∙ +IdR x
+
+  +IdL' : ∀ x y → x ≡ 0r → x + y ≡ y
+  +IdL' x y x=0 = cong (_+ y) x=0 ∙ +IdL y
+
+  +InvL' : ∀ x y → x ≡ y → - x + y ≡ 0r
+  +InvL' x y x=y = cong (- x +_) (sym x=y) ∙ (+InvL x)
+
+  +InvR' : ∀ x y → x ≡ y → x + - y ≡ 0r
+  +InvR' x y x=y = cong (_+ - y) x=y ∙ (+InvR y)
+
+  plusMinus : ∀ x y → (x + y) - y ≡ x
+  plusMinus x y = sym (+Assoc _ _ _) ∙ +IdR' _ _ (+InvR y)
+
+  plusMinus' : ∀ x y y' → y ≡ y' → (x + y) - y' ≡ x
+  plusMinus' x y y' p = sym (+Assoc _ _ _) ∙ +IdR' _ _ (+InvR' y y' p)
+
+  minusPlus : ∀ x y → (x - y) + y ≡ x
+  minusPlus x y = sym (+Assoc _ _ _) ∙ +IdR' _ _ (+InvL y)
+
+  minusPlus' : ∀ x y y' → y ≡ y' → (x - y) + y' ≡ x
+  minusPlus' x y y' p = sym (+Assoc _ _ _) ∙ +IdR' _ _ (+InvL' y y' p)
+
+  ·IdR' : ∀ x y → y ≡ 1r → x · y ≡ x
+  ·IdR' x y y=0 = cong (x ·_) y=0 ∙ ·IdR x
+
+  ·IdL' : ∀ x y → x ≡ 1r → x · y ≡ y
+  ·IdL' x y x=0 = cong (_· y) x=0 ∙ ·IdL y
+
+  ·DistR- : (x y z : R) → x · (y - z) ≡ (x · y) - (x · z)
+  ·DistR- _ _ _ = ·DistR+ _ _ _ ∙ cong (_ +_) (-DistR· _ _)
+
+  ·DistL- : (x y z : R) → (x - y) · z ≡ (x · z) - (y · z)
+  ·DistL- _ _ _ = ·DistL+ _ _ _ ∙ cong (_ +_) (-DistL· _ _)
+
 Ring→Semiring : Ring ℓ → Semiring ℓ
 Ring→Semiring R =
   let open RingStr (snd R)

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/Base.agda

@@ -6,7 +6,7 @@ module Cubical.Data.Int.Base where
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Data.Bool
-open import Cubical.Data.Nat hiding (_+_ ; _·_) renaming (isEven to isEvenℕ ; isOdd to isOddℕ)
+open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_) renaming (isEven to isEvenℕ ; isOdd to isOddℕ)
 open import Cubical.Data.Fin.Inductive.Base
 
 infix  8 -_
@@ -60,6 +60,13 @@ _+_ : ℤ → ℤ → ℤ
 m + pos n = m +pos n
 m + negsuc n = m +negsuc n
 
+_+f_ : ℤ → ℤ → ℤ
+pos n +f pos n₁ = pos (n ℕ.+ n₁)
+negsuc n +f negsuc n₁ = negsuc (suc (n ℕ.+ n₁))
+n +f m = n + m
+-- pos n +f negsuc n₁ = {!!}
+-- negsuc n +f pos n₁ = {!!}
+
 -_ : ℤ → ℤ
 - pos zero = pos zero
 - pos (suc n) = negsuc n
@@ -74,6 +81,16 @@ pos (suc n) · m = m + pos n · m
 negsuc zero · m = - m
 negsuc (suc n) · m = - m + negsuc n · m
 
+_·f_ : ℤ → ℤ → ℤ
+pos n ·f pos n₁ = pos (n ℕ.· n₁)
+pos zero ·f negsuc n₁ = pos zero
+pos (suc n) ·f negsuc n₁ = negsuc (suc n ℕ.· suc n₁)
+negsuc n ·f pos zero = pos zero
+negsuc n ·f pos (suc n₁) = negsuc (suc n ℕ.· suc n₁)
+negsuc n ·f negsuc n₁ = pos (suc n ℕ.· suc n₁)
+
+
+
 -- Natural number and negative integer literals for ℤ
 
 open import Cubical.Data.Nat.Literals public

Cubical/Data/Int/Order.agda

@@ -4,11 +4,12 @@ module Cubical.Data.Int.Order where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
-
+open import Cubical.Foundations.Equiv
 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,59 @@ 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
+
+ℕ≥→negsuc-≤-negsuc : ∀ m n → m ℕ.≤ n → negsuc n ≤ negsuc m
+ℕ≥→negsuc-≤-negsuc m n = negsuc-≤-negsuc ∘ ℕ≤→pos-≤-pos m n
+
+pos-≤-pos→ℕ≤ : ∀ m n → pos m ≤ pos n → m ℕ.≤ n
+pos-≤-pos→ℕ≤ m n (k , p) = k , injPos ((pos+ k m ∙ ℤ.+Comm (pos k) (pos m)) ∙ p)
+
+pos-≤-pos≃ℕ≤ : ∀ m n → (pos m ≤ pos n) ≃ (m ℕ.≤ n)
+pos-≤-pos≃ℕ≤ m n = propBiimpl→Equiv isProp≤ ℕ.isProp≤
+                (pos-≤-pos→ℕ≤ _ _) (ℕ≤→pos-≤-pos _ _)
+
+pos-<-pos≃ℕ< : ∀ m n → (pos m < pos n) ≃ (m ℕ.< n)
+pos-<-pos≃ℕ< m n = propBiimpl→Equiv (isProp< {pos m} {pos n}) ℕ.isProp≤
+                (pos-≤-pos→ℕ≤ _ _) (ℕ≤→pos-≤-pos (suc m) n)
+
+
+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

@@ -1,6 +1,7 @@
-{-# OPTIONS --safe #-}
+{-# OPTIONS --safe --v=tc.conv:20 #-}
 module Cubical.Data.Int.Properties where
 
+
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
@@ -11,7 +12,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 +1506,42 @@ 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
+
+sign·abs : ∀ m → sign m · pos (abs m) ≡ m
+sign·abs (pos zero) = refl
+sign·abs (pos (suc n)) = refl
+sign·abs (negsuc n) = refl
+
+-- abs[sign[m]·pos[n]]≡n : ∀ m n → abs (sign m · pos n) ≡ n
+-- abs[sign[m]·pos[n]]≡n m n = {!!}
+
+
+-- ·'≡· : ∀ n m → n · m ≡ n ·' m
+-- ·'≡· (pos n) (pos n₁) = sym (pos·pos n n₁)
+-- ·'≡· (pos zero) (negsuc n₁) = refl
+-- ·'≡· (pos (suc n)) (negsuc n₁) = {!!}
+-- ·'≡· (negsuc n) (pos zero) = ·AnnihilR (negsuc n)
+-- ·'≡· (negsuc n) (pos (suc n₁)) = negsuc·pos n (suc n₁) ∙
+--   {!!}
+-- ·'≡· (negsuc n) (negsuc n₁) = negsuc·negsuc n n₁ ∙ sym (pos·pos (suc n) (suc n₁))