Merge pull request #1250 from ecavallo/nat-minor

Some Nat/Bijections simplification suggested by @anshwad10

Author: ecavallo

Cubical/Data/Nat/Bijections/Sum.agda

@@ -16,59 +16,46 @@ open <-Reasoning
 open import Cubical.Tactics.NatSolver
 open import Cubical.Data.Nat.Bijections.IncreasingFunction
 
-double : ℕ → ℕ
-double n = n + n
-
 private
-  2Sn=2n+2 : {n : ℕ} → double (suc n) ≡ double n + 2
-  2Sn=2n+2 = solveℕ!
+  2Sn=2n+2 : {n : ℕ} → doubleℕ (suc n) ≡ doubleℕ n + 2
+  2Sn=2n+2 = +-comm 2 (doubleℕ _)
 
-  doubleGrows : (n : ℕ) → double n < double (suc n)
-  doubleGrows n = double n
-                    ≡<⟨ refl ⟩
-                  n + n
-                    <≡⟨ <SumLeft ⟩
-                  n + n + 2
-                    ≡⟨ sym 2Sn=2n+2 ⟩
-                  double (suc n) ∎
+  doubleGrows : (n : ℕ) → doubleℕ n < doubleℕ (suc n)
+  doubleGrows n = <-trans <-suc <-suc
 
-  ¬2n+2+k<2n : (n : ℕ) → (k : ℕ) → ¬ ( suc (suc k) + double n < double (suc n))
+  ¬2n+2+k<2n : (n : ℕ) → (k : ℕ) → ¬ ( suc (suc k) + doubleℕ n < doubleℕ (suc n))
   ¬2n+2+k<2n n k p = ex-falso (¬-<-zero k<0) where
-      2n+k+2<2n+2 : double n + suc (suc k) < double n + 2
-      2n+k+2<2n+2 = double n + suc (suc k)
-                      ≡<⟨ +-comm (n + n) (suc (suc k)) ⟩
-                    suc (suc k) + double n
+      2n+k+2<2n+2 : doubleℕ n + suc (suc k) < doubleℕ n + 2
+      2n+k+2<2n+2 = doubleℕ n + suc (suc k)
+                      ≡<⟨ +-comm (doubleℕ n) (suc (suc k)) ⟩
+                    suc (suc k) + doubleℕ n
                       <≡⟨ p ⟩
-                    double (suc n)
+                    doubleℕ (suc n)
                       ≡⟨ 2Sn=2n+2 ⟩
-                    double n + 2 ∎
+                    doubleℕ n + 2 ∎
       k+2<2 : suc (suc k) < suc (suc 0)
       k+2<2 = <-k+-cancel 2n+k+2<2n+2
       k<0 : k < 0
       k<0 = pred-≤-pred (pred-≤-pred k+2<2)
 
-doubleInc : isStrictlyIncreasing double
-doubleInc = sucIncreasing→StrictlyIncreasing double doubleGrows
+doubleInc : isStrictlyIncreasing doubleℕ
+doubleInc = sucIncreasing→StrictlyIncreasing doubleℕ doubleGrows
 
 private
-  partitionDouble≅ℕ⊎ℕ : Iso (partition double refl doubleInc) (ℕ ⊎ ℕ)
-  Iso.fun partitionDouble≅ℕ⊎ℕ (n , zero        , p) = inl n
-  Iso.fun partitionDouble≅ℕ⊎ℕ (n , suc zero    , p) = inr n
-  Iso.fun partitionDouble≅ℕ⊎ℕ (n , suc (suc k) , p) = ex-falso (¬2n+2+k<2n n k p)
-  Iso.inv partitionDouble≅ℕ⊎ℕ (inl n) = n , zero , doubleGrows n
-  Iso.inv partitionDouble≅ℕ⊎ℕ (inr n) = n , 1 , (
-                 1 + n + n <≡⟨ <SumRight {k = 0} ⟩
-                 2 + n + n  ≡⟨ +-comm 2 (n + n)  ⟩
-                 n + n + 2  ≡⟨ sym 2Sn=2n+2      ⟩
-                 double (suc n) ∎         )
-  Iso.rightInv partitionDouble≅ℕ⊎ℕ (inl n) = refl
-  Iso.rightInv partitionDouble≅ℕ⊎ℕ (inr n) = refl
-  Iso.leftInv partitionDouble≅ℕ⊎ℕ (k , zero        , p) = ΣPathP (refl , ΣPathPProp (λ a → isProp≤) refl)
-  Iso.leftInv partitionDouble≅ℕ⊎ℕ (k , suc zero    , p) = ΣPathP (refl , ΣPathPProp (λ a → isProp≤) refl)
-  Iso.leftInv partitionDouble≅ℕ⊎ℕ (k , suc (suc i) , p) = ex-falso $ ¬2n+2+k<2n k i p
-
-  partitionDouble≅ℕ : Iso (partition double refl doubleInc) ℕ
-  partitionDouble≅ℕ = partition≅ℕ double refl doubleInc
+  partitionDoubleℕ≅ℕ⊎ℕ : Iso (partition doubleℕ refl doubleInc) (ℕ ⊎ ℕ)
+  Iso.fun partitionDoubleℕ≅ℕ⊎ℕ (n , zero        , p) = inl n
+  Iso.fun partitionDoubleℕ≅ℕ⊎ℕ (n , suc zero    , p) = inr n
+  Iso.fun partitionDoubleℕ≅ℕ⊎ℕ (n , suc (suc k) , p) = ex-falso (¬2n+2+k<2n n k p)
+  Iso.inv partitionDoubleℕ≅ℕ⊎ℕ (inl n) = n , zero , doubleGrows n
+  Iso.inv partitionDoubleℕ≅ℕ⊎ℕ (inr n) = n , 1 , <-suc
+  Iso.rightInv partitionDoubleℕ≅ℕ⊎ℕ (inl n) = refl
+  Iso.rightInv partitionDoubleℕ≅ℕ⊎ℕ (inr n) = refl
+  Iso.leftInv partitionDoubleℕ≅ℕ⊎ℕ (k , zero        , p) = ΣPathP (refl , ΣPathPProp (λ a → isProp≤) refl)
+  Iso.leftInv partitionDoubleℕ≅ℕ⊎ℕ (k , suc zero    , p) = ΣPathP (refl , ΣPathPProp (λ a → isProp≤) refl)
+  Iso.leftInv partitionDoubleℕ≅ℕ⊎ℕ (k , suc (suc i) , p) = ex-falso $ ¬2n+2+k<2n k i p
+
+  partitionDoubleℕ≅ℕ : Iso (partition doubleℕ refl doubleInc) ℕ
+  partitionDoubleℕ≅ℕ = partition≅ℕ doubleℕ refl doubleInc
 
 ℕ⊎ℕ≅ℕ : Iso (ℕ ⊎ ℕ) ℕ
-ℕ⊎ℕ≅ℕ = compIso (invIso partitionDouble≅ℕ⊎ℕ) partitionDouble≅ℕ
+ℕ⊎ℕ≅ℕ = compIso (invIso partitionDoubleℕ≅ℕ⊎ℕ) partitionDoubleℕ≅ℕ

Cubical/Data/Nat/Bijections/Triangle.agda

@@ -22,10 +22,8 @@ strictIncTriangle = sucIncreasing→StrictlyIncreasing triangle triangleN<triang
   triangleN<triangleSN n = n , refl
 
 private
-  1+k+t=k+t+1 : (n : ℕ) → (t : ℕ ) → suc (n + t) ≡ n + suc t
-  1+k+t=k+t+1 n t = solveℕ!
   1+k+tk=tsk : (n : ℕ) → suc (n + triangle n) ≡ triangle (suc n)
-  1+k+tk=tsk n = 1+k+t=k+t+1 n (triangle n)
+  1+k+tk=tsk n = sym (+-suc _ _)
 
   partitionTriangle = partition triangle refl strictIncTriangle
 

Cubical/Data/Nat/Order.agda

@@ -575,14 +575,12 @@ module _ (f : ℕ → ℕ) (fInc : ((n : ℕ) → f n < f (suc n))) where
   open <-Reasoning
   sucIncreasing→StrictlyIncreasing : isStrictlyIncreasing f
   sucIncreasing→StrictlyIncreasing {m = m} {n = n} (k , m+k+1=n) =
-    sucIncreasing→strictlyIncreasing' m n k m+k+1=n where
-
+    sucIncreasing→strictlyIncreasing' m n k m+k+1=n
+      where
       sucIncreasing→strictlyIncreasing' :
         (m : ℕ) → (n : ℕ) → (k : ℕ) → (k + suc m ≡ n) → f m < f n
-
       sucIncreasing→strictlyIncreasing' m _ zero m+1=n =
         subst (λ n' → f m < f n') m+1=n (fInc m)
-
       sucIncreasing→strictlyIncreasing' m _ (suc k) sk+sm=n =
         subst (λ n' → f m < f n') sk+sm=n $
           f m