diff --git a/Cubical/Data/Fin/Properties.agda b/Cubical/Data/Fin/Properties.agda index dda477bf43..87ea9a5cd5 100644 --- a/Cubical/Data/Fin/Properties.agda +++ b/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 diff --git a/Cubical/Data/Int/Order.agda b/Cubical/Data/Int/Order.agda index fac79698da..e728308348 100644 --- a/Cubical/Data/Int/Order.agda +++ b/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 diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda index 1fc854cafa..088182ed42 100644 --- a/Cubical/Data/Int/Properties.agda +++ b/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 diff --git a/Cubical/Data/Nat/Mod.agda b/Cubical/Data/Nat/Mod.agda index 8911504e25..1d53e66990 100644 --- a/Cubical/Data/Nat/Mod.agda +++ b/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→10 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 : ∀ x → ⟨ openPred (λ y → (y <ᵣ x) , squash₁) ⟩ +openPred> x y = + PT.map (map-snd (λ {q} q 0 x) + + + +·invℝ' : ∀ r 0