RP2

Cubical/Algebra/CommRing/Instances/Polynomials/MultivariatePoly-notationZ.agda

@@ -93,6 +93,6 @@ open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quot
 ℤ'[X]/X : CommRing ℓ-zero
 ℤ'[X]/X = A[X1,···,Xn]/<X1,···,Xn> ℤCommRing 1
 
--- there is a unification problem that keep pop in up everytime I modify something
+-- there is a unification problem that keep poping up everytime I modify something
 -- equivℤ[X] : ℤ'[X]/X ≡ ℤ[X]/X
 -- equivℤ[X] = cong₂ _/_ refl (cong (λ X → genIdeal (A[X1,···,Xn] ℤCommRing {!!}) X) {!!})

Cubical/Data/Bool/Base.agda

@@ -81,6 +81,10 @@ dichotomyBool : (x : Bool) → (x ≡ true) ⊎ (x ≡ false)
 dichotomyBool true  = inl refl
 dichotomyBool false = inr refl
 
+dichotomyBoolSym : (x : Bool) → (x ≡ false) ⊎ (x ≡ true)
+dichotomyBoolSym false = inl refl
+dichotomyBoolSym true = inr refl
+
 -- TODO: this should be uncommented and implemented using instance arguments
 -- _==_ : {dA : Discrete A} → A → A → Bool
 -- _==_ {dA = dA} x y = Dec→Bool (dA x y)

Cubical/Data/Int/IsEven.agda

@@ -0,0 +1,137 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Int.IsEven where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Nullary
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Bool
+open import Cubical.Data.Nat
+  using (ℕ ; zero ;  suc ; +-zero ; +-suc ; injSuc ; +-comm ;snotz ; znots ; ·-distribˡ)
+  renaming
+  (_+_    to _+ℕ_ ;
+   _·_    to _·ℕ_ ;
+   isEven to isEvenℕ ;
+   isOdd  to isOddℕ)
+import Cubical.Data.Nat.IsEven as ℕeven
+
+open import Cubical.Data.Int
+open import Cubical.Data.Sum
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Instances.Bool
+
+open GroupStr (snd BoolGroup) using ()
+  renaming ( _·_ to _+Bool_ )
+
+-----------------------------------------------------------------------------
+-- Lemma over ℤ
+
+2negsuc : (k : ℕ) → 2 · negsuc k ≡ negsuc (1 +ℕ 2 ·ℕ k)
+2negsuc k = sym
+            (negsuc (1 +ℕ 2 ·ℕ k) ≡⟨ refl ⟩
+             neg (suc (1 +ℕ 2 ·ℕ k))        ≡⟨ cong neg refl ⟩
+             neg (2 +ℕ 2 ·ℕ k)              ≡⟨ cong neg (·-distribˡ 2 1 k) ⟩
+             neg (2 ·ℕ (suc k))              ≡⟨ refl ⟩
+             - pos (2 ·ℕ (suc k))            ≡⟨ cong -_ (pos·pos 2 (suc k)) ⟩
+             - (2 · pos (suc k))              ≡⟨ -DistR· 2 (pos (suc k)) ⟩
+             2 · neg (suc k)                  ≡⟨ refl ⟩
+             2 · negsuc k ∎)
+
+1+2kNegsuc : (k : ℕ) → 1 + 2 · negsuc k ≡ negsuc (2 ·ℕ k)
+1+2kNegsuc k = cong (λ X → 1 + X)
+                    ( 2negsuc k
+                    ∙ cong negsuc (+-comm 1 (2 ·ℕ k))
+                    ∙ negsuc+ (2 ·ℕ k) 1
+                    ∙ +Comm (negsuc (2 ·ℕ k)) (- 1))
+               ∙ +Assoc 1 (- 1) (negsuc (2 ·ℕ k))
+               ∙ sym (pos0+ (negsuc (2 ·ℕ k)))
+
+1+2kPos : (k : ℕ) → pos (1 +ℕ 2 ·ℕ k) ≡ 1 + 2 · (pos k)
+1+2kPos k = pos+ 1 (2 ·ℕ k) ∙ cong (λ X → 1 + X) (pos·pos 2 k)
+
+-- isEven → 2k / isOdd → 1 + 2k
+isEvenTrue : (a : ℤ) → (isEven a ≡ true) → Σ[ m ∈ ℤ ] a ≡ (2 · m)
+isEvenTrue (pos n) p = (pos k) , (cong pos pp ∙ pos·pos 2 k )
+  where
+  k = fst (ℕeven.isEvenTrue n p)
+  pp = snd (ℕeven.isEvenTrue n p)
+isEvenTrue (negsuc n) p = (negsuc k) , cong negsuc pp ∙ sym (2negsuc k)
+  where
+  k = fst (ℕeven.isOddTrue n p)
+  pp = snd (ℕeven.isOddTrue n p)
+
+isEvenFalse : (a : ℤ) → (isEven a ≡ false) → Σ[ m ∈ ℤ ] a ≡ 1 + (2 · m)
+isEvenFalse (pos n) p = (pos k) , (cong pos pp ∙ 1+2kPos k)
+  where
+  k = fst (ℕeven.isEvenFalse n p)
+  pp = snd (ℕeven.isEvenFalse n p)
+isEvenFalse (negsuc n) p = (negsuc k) , (cong negsuc pp ∙ sym (1+2kNegsuc k))
+  where
+  k = fst (ℕeven.isOddFalse n p)
+  pp = snd (ℕeven.isOddFalse n p)
+
+
+-- 2k → isEven / 1 + 2k → isOdd
+trueIsEven : (a : ℤ)  → Σ[ m ∈ ℤ ] a ≡ (2 · m) → (isEven a ≡ true)
+trueIsEven (pos n) (pos m , p) = ℕeven.trueIsEven n (m , injPos (p ∙ sym (pos·pos 2 m)))
+trueIsEven (pos n) (negsuc m , p) = ⊥.rec (posNotnegsuc n (1 +ℕ 2 ·ℕ m) (p ∙ 2negsuc m))
+trueIsEven (negsuc n) (pos m , p) = ⊥.rec (negsucNotpos n (2 ·ℕ m) (p ∙ sym (pos·pos 2 m)))
+trueIsEven (negsuc n) (negsuc m , p) = ℕeven.¬IsEvenFalse n (ℕeven.falseIsEven n
+                                       (m , (injNegsuc (p ∙ 2negsuc m))))
+
+falseIsEven : (a : ℤ) → Σ[ m ∈ ℤ ] a ≡ 1 + (2 · m) → isEven a ≡ false
+falseIsEven (pos n) (pos m , p) = ℕeven.falseIsEven n
+                                  (m , (injPos (p ∙ sym (1+2kPos m))))
+falseIsEven (pos n) (negsuc m , p) = ⊥.rec (posNotnegsuc n (2 ·ℕ m) (p ∙ 1+2kNegsuc m))
+falseIsEven (negsuc n) (pos m , p) = ⊥.rec (negsucNotpos n (1 +ℕ 2 ·ℕ m) (p ∙ sym (1+2kPos m)))
+falseIsEven (negsuc n) (negsuc m , p) = ℕeven.¬IsEvenTrue n (ℕeven.trueIsEven n (m , (injNegsuc (p ∙ 1+2kNegsuc m ))))
+
+
+-- Value of isEven (x + y)  depending on IsEven x, IsEven y
+isOddIsOdd→IsEven : (x y : ℤ) → isEven x ≡ false → isEven y ≡ false → isEven (x + y) ≡ true
+isOddIsOdd→IsEven x y px py = trueIsEven (x + y) ((1 + k + l) , cong₂ _+_ qk ql ∙ sym helper)
+  where
+  k =  fst (isEvenFalse x px)
+  qk = snd (isEvenFalse x px)
+  l = fst (isEvenFalse y py)
+  ql = snd (isEvenFalse y py)
+  helper : 2 · ((1 + k) + l) ≡ (1 + 2 · k) + (1 + 2 · l)
+  helper = 2 · ((1 + k) + l)        ≡⟨ ·DistR+ 2 (1 + k) l ⟩
+           2 · (1 + k) + 2 · l      ≡⟨ cong (λ X → X + 2 · l)
+                                            (·DistR+ 2 1 k ∙ sym (+Assoc 1 1 (2 · k)) ∙ +Comm 1 (1 + 2 · k)) ⟩
+           ((1 + 2 · k) + 1) + 2 · l     ≡⟨ sym (+Assoc (1 + 2 · k) 1 (2 · l)) ⟩
+           (1 + 2 · k) + (1 + 2 · l) ∎
+
+isOddIsEven→IsOdd : (x y : ℤ) → isEven x ≡ false → isEven y ≡ true → isEven (x + y) ≡ false
+isOddIsEven→IsOdd x y px py = falseIsEven (x + y) ((k + l) , ( cong₂ _+_ qk ql ∙ helper))
+  where
+  k =  fst (isEvenFalse x px)
+  qk = snd (isEvenFalse x px)
+  l = fst (isEvenTrue y py)
+  ql = snd (isEvenTrue y py)
+  helper : _
+  helper = (1 + 2 · k) + 2 · l ≡⟨ sym (+Assoc 1 (2 · k) (2 · l)) ⟩
+           1 + (2 · k + 2 · l) ≡⟨ cong (λ X → 1 + X) (sym (·DistR+ 2 k l)) ⟩
+           1 + 2 · (k + l) ∎
+
+isEvenIsOdd→IsOdd : (x y : ℤ) → isEven x ≡ true → isEven y ≡ false → isEven (x + y) ≡ false
+isEvenIsOdd→IsOdd x y px py = cong isEven (+Comm x y) ∙ isOddIsEven→IsOdd y x py px
+
+isEvenIsEven→IsEven : (x y : ℤ) → isEven x ≡ true → isEven y ≡ true → isEven (x + y) ≡ true
+isEvenIsEven→IsEven x y px py = trueIsEven (x + y) ((k + l) , cong₂ _+_ qk ql ∙ sym (·DistR+ 2 k l))
+  where
+  k =  fst (isEvenTrue x px)
+  qk = snd (isEvenTrue x px)
+  l = fst (isEvenTrue y py)
+  ql = snd (isEvenTrue y py)
+
+
+-- Proof that isEven is morphism
+isEven-pres+ : (x y : ℤ) → isEven (x + y) ≡ isEven x +Bool isEven y
+isEven-pres+ x y with (dichotomyBoolSym (isEven x)) | dichotomyBoolSym (isEven y)
+... | inl xf | inl yf = isOddIsOdd→IsEven x y xf yf ∙ sym (cong₂ _+Bool_ xf yf)
+... | inl xf | inr yt = isOddIsEven→IsOdd x y xf yt ∙ sym (cong₂ _+Bool_ xf yt)
+... | inr xt | inl yf = isEvenIsOdd→IsOdd x y xt yf ∙ sym (cong₂ _+Bool_ xt yf)
+... | inr xt | inr yt = isEvenIsEven→IsEven x y xt yt ∙ sym (cong₂ _+Bool_ xt yt)

Cubical/Data/Int/Properties.agda

@@ -4,22 +4,20 @@ module Cubical.Data.Int.Properties where
 open import Cubical.Core.Everything
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Transport
-open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
-open import Cubical.Foundations.Function
 
-open import Cubical.Data.Empty as Empty
+open import Cubical.Relation.Nullary
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Bool
 open import Cubical.Data.Nat
   hiding   (+-assoc ; +-comm)
-  renaming (_·_ to _·ℕ_; _+_ to _+ℕ_ ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
-open import Cubical.Data.Bool
+  renaming (_·_ to _·ℕ_; _+_ to _+ℕ_ ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm ; isEven to isEvenℕ ; isOdd to isOddℕ)
 open import Cubical.Data.Sum
-open import Cubical.Data.Int.Base
 
-open import Cubical.Relation.Nullary
+open import Cubical.Data.Int.Base
 
 sucPred : ∀ i → sucℤ (predℤ i) ≡ i
 sucPred (pos zero)    = refl
@@ -524,20 +522,20 @@ abs· (negsuc m) (negsuc n) = cong abs (negsuc·negsuc m n) ∙ absPos·Pos (suc
 -- ℤ is integral domain
 
 isIntegralℤPosPos : (c m : ℕ) → pos c · pos m ≡ 0 → ¬ c ≡ 0 → m ≡ 0
-isIntegralℤPosPos 0 m _ q = Empty.rec (q refl)
+isIntegralℤPosPos 0 m _ q = ⊥.rec (q refl)
 isIntegralℤPosPos (suc c) m p _ =
   sym (0≡n·sm→0≡n {n = m} {m = c} (sym (injPos (pos·pos (suc c) m ∙ p)) ∙ ·ℕ-comm (suc c) m))
 
 isIntegralℤ : (c m : ℤ) → c · m ≡ 0 → ¬ c ≡ 0 → m ≡ 0
 isIntegralℤ (pos c) (pos m) p h i = pos (isIntegralℤPosPos c m p (λ r → h (cong pos r)) i)
 isIntegralℤ (pos c) (negsuc m) p h =
-  Empty.rec (snotz (isIntegralℤPosPos c (suc m)
+  ⊥.rec (snotz (isIntegralℤPosPos c (suc m)
     (sym (-Involutive _) ∙ cong (-_) (sym (pos·negsuc c m) ∙ p)) (λ r → h (cong pos r))))
 isIntegralℤ (negsuc c) (pos m) p _ i =
   pos (isIntegralℤPosPos (suc c) m
     (sym (-Involutive _) ∙ cong (-_) (sym (negsuc·pos c m) ∙ p)) snotz i)
 isIntegralℤ (negsuc c) (negsuc m) p _ =
-  Empty.rec (snotz (isIntegralℤPosPos (suc c) (suc m) (sym (negsuc·negsuc c m) ∙ p) snotz))
+  ⊥.rec (snotz (isIntegralℤPosPos (suc c) (suc m) (sym (negsuc·negsuc c m) ∙ p) snotz))
 
 private
   ·lCancel-helper : (c m n : ℤ) → c · m ≡ c · n → c · (m - n) ≡ 0

Cubical/Data/Nat/IsEven.agda

@@ -0,0 +1,60 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Nat.IsEven where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Bool
+open import Cubical.Data.Nat
+
+-- negation result
+¬IsEvenFalse : (n : ℕ) → (isEven n ≡ false) → isOdd n ≡ true
+¬IsEvenFalse zero p = ⊥.rec (true≢false p)
+¬IsEvenFalse (suc zero) p = refl
+¬IsEvenFalse (suc (suc n)) p = ¬IsEvenFalse n p
+
+¬IsEvenTrue : (n : ℕ) → (isEven n ≡ true) → isOdd n ≡ false
+¬IsEvenTrue zero p = refl
+¬IsEvenTrue (suc zero) p = ⊥.rec (false≢true p)
+¬IsEvenTrue (suc (suc n)) p = ¬IsEvenTrue n p
+
+¬IsOddFalse : (n : ℕ) → (isOdd n ≡ false) → isEven n ≡ true
+¬IsOddFalse zero p = refl
+¬IsOddFalse (suc zero) p = ⊥.rec (true≢false p)
+¬IsOddFalse (suc (suc n)) p = ¬IsOddFalse n p
+
+¬IsOddTrue : (n : ℕ) → (isOdd n ≡ true) → isEven n ≡ false
+¬IsOddTrue zero p = ⊥.rec (false≢true p)
+¬IsOddTrue (suc zero) p = refl
+¬IsOddTrue (suc (suc n)) p = ¬IsOddTrue n p
+
+
+-- isEven → 2k / isOdd → 1 + 2k
+isEvenTrue : (n : ℕ) → (isEven n ≡ true) → Σ[ m ∈ ℕ ] n ≡ (2 · m)
+isOddTrue : (n : ℕ) → (isOdd n ≡ true) → Σ[ m ∈ ℕ ] n ≡ 1 + (2 · m)
+isEvenTrue zero p = 0 , refl
+isEvenTrue (suc n) p = (suc k) , cong suc pp ∙ cong suc (sym (+-suc _ _))
+       where
+       k = fst (isOddTrue n p)
+       pp = snd (isOddTrue n p)
+isOddTrue zero p = ⊥.rec (false≢true p)
+isOddTrue (suc n) p = (fst (isEvenTrue n p)) , (cong suc (snd (isEvenTrue n p)))
+
+isEvenFalse : (n : ℕ) → (isEven n ≡ false) → Σ[ m ∈ ℕ ] n ≡ 1 + (2 · m)
+isEvenFalse n p = isOddTrue n (¬IsEvenFalse n p)
+
+isOddFalse : (n : ℕ) → (isOdd n ≡ false) → Σ[ m ∈ ℕ ] n ≡ (2 · m)
+isOddFalse n p = isEvenTrue n (¬IsOddFalse n p)
+
+
+-- 2k -> isEven
+trueIsEven : (n : ℕ) → Σ[ m ∈ ℕ ] n ≡ (2 · m) → (isEven n ≡ true)
+trueIsEven zero (m , p) = refl
+trueIsEven (suc zero) (zero , p) = ⊥.rec (snotz p)
+trueIsEven (suc zero) (suc m , p) = ⊥.rec (znots (injSuc (p ∙ cong suc (+-suc _ _))))
+trueIsEven (suc (suc n)) (zero , p) = ⊥.rec (snotz p)
+trueIsEven (suc (suc n)) (suc m , p) = trueIsEven n (m , (injSuc (injSuc (p ∙ cong suc (+-suc _ _)))))
+
+falseIsEven : (n : ℕ) → Σ[ m ∈ ℕ ] n ≡ (1 + 2 · m) → (isEven n ≡ false)
+falseIsEven zero (m , p) = ⊥.rec (znots p)
+falseIsEven (suc n) (m , p) = ¬IsEvenTrue n (trueIsEven n (m , (injSuc p)))