Skip to content

Commit ab4a573

Browse files
Freek98Freek98
committed
renamings
1 parent 147fd63 commit ab4a573

File tree

4 files changed

+29
-59
lines changed

4 files changed

+29
-59
lines changed

‎Cubical/Data/Nat/Bijections/IncreasingFunction.agda‎

Lines changed: 6 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -15,42 +15,14 @@ open import Cubical.Foundations.HLevels
1515
open import Cubical.Data.Nat
1616
open import Cubical.Data.Nat.Order
1717
open <-Reasoning
18-
open import Cubical.Data.Nat.MoreOrderProperties
1918

2019
open import Cubical.Data.Sigma
2120
open import Cubical.Data.Sum
2221
open import Cubical.Relation.Nullary
2322
open import Cubical.Data.Empty renaming (rec to ex-falso)
2423

25-
isIncreasing : (f : ℕ → ℕ) → Type
26-
isIncreasing f = {m n : ℕ} → (m < n) → f m < f n
27-
28-
weakenIncreasing : {f : ℕ → ℕ} → {m n : ℕ} → isIncreasing f → m ≤ n → f m ≤ f n
29-
weakenIncreasing {f} {m} {n} fInc m≤n = case (≤-split m≤n) of
30-
λ { (inl m<n) → <-weaken (fInc m<n)
31-
; (inr m=n) → =→≤ (cong f m=n) }
32-
33-
strengthenIncreasing : (f : ℕ → ℕ) → ((n : ℕ) → f n < f (suc n)) → isIncreasing f
34-
strengthenIncreasing f fInc {m = m} {n = n} (k , m+k+1=n) =
35-
strengthenIncreasing' f fInc m n k m+k+1=n where
36-
37-
strengthenIncreasing' : (f : ℕ → ℕ) → ((n : ℕ) → f n < f (suc n)) →
38-
(m : ℕ) → (n : ℕ) → (k : ℕ) → (k + suc m ≡ n) →
39-
f m < f n
40-
41-
strengthenIncreasing' f fInc m n zero m+1=n =
42-
subst (λ n' → f m < f n') m+1=n (fInc m)
43-
44-
strengthenIncreasing' f fInc m n (suc k) sk+sm=n =
45-
transport (cong (λ { n' → f m < f n' }) sk+sm=n) (
46-
f m
47-
<⟨ strengthenIncreasing' f fInc m (k + suc m) k refl ⟩
48-
f (k + suc m)
49-
<≡⟨ fInc (k + suc m) ⟩
50-
f(suc k + suc m) ∎)
51-
5224
private
53-
kIsUnique : (f : ℕ → ℕ ) → isIncreasing f → (n : ℕ) →
25+
kIsUnique : (f : ℕ → ℕ ) → isStrictlyIncreasing f → (n : ℕ) →
5426
(k : ℕ) → ((f k ≤ n) × (n < f (suc k ))) →
5527
(k' : ℕ) → ((f k' ≤ n) × (n < f (suc k'))) →
5628
k ≡ k'
@@ -62,7 +34,7 @@ private
6234
n
6335
<≤⟨ n<fsl ⟩
6436
f (suc l)
65-
≤⟨ weakenIncreasing fInc l<l' ⟩
37+
≤⟨ strictlyIncreasing→Increasing fInc l<l' ⟩
6638
f l'
6739
≤≡⟨ fl'≤n ⟩
6840
n ∎
@@ -73,12 +45,12 @@ private
7345
... | eq k=k' = k=k'
7446
... | gt k'<k = ex-falso (compare k' k n<fsk' fk≤n k'<k)
7547

76-
approxFunction : (f : ℕ → ℕ) → (f 0 ≡ 0) → isIncreasing f →
48+
approxFunction : (f : ℕ → ℕ) → (f 0 ≡ 0) → isStrictlyIncreasing f →
7749
(n : ℕ) → Σ[ k ∈ ℕ ] (f k ≤ n) × (n < f (suc k))
7850
approxFunction f f0=0 fInc zero = 0 , f0≤0 , 0<f1 where
7951

8052
f0≤0 : f 0 ≤ 0
81-
f0≤0 = =→≤ f0=0
53+
f0≤0 = ≤-reflexive f0=0
8254

8355
f0<f1 : f 0 < f 1
8456
f0<f1 = fInc <-suc
@@ -102,7 +74,7 @@ private
10274

10375
newsol : Trichotomy (f (suc k)) (suc n) → Σ[ k' ∈ ℕ ] (f k' ≤ suc n) × (suc n < f (suc k'))
10476
newsol (lt fsk<sn) = ex-falso (¬squeeze< (n<fsk , fsk<sn))
105-
newsol (eq fsk=sn) = suc k , =→≤ fsk=sn , (
77+
newsol (eq fsk=sn) = suc k , ≤-reflexive fsk=sn , (
10678
suc n
10779
≡<⟨ sym fsk=sn ⟩
10880
f (suc k)
@@ -114,7 +86,7 @@ private
11486
≤≡⟨ <-weaken <-suc ⟩
11587
suc n ∎) , fsk>sn
11688

117-
module _ (f : ℕ → ℕ) (f0=0 : f 0 ≡ 0) (fInc : isIncreasing f) where
89+
module _ (f : ℕ → ℕ) (f0=0 : f 0 ≡ 0) (fInc : isStrictlyIncreasing f) where
11890
nearestValues : (n : ℕ) → ∃![ k ∈ ℕ ] (f k ≤ n) × (n < f (suc k))
11991
nearestValues n = uniqueExists k p goalIsProp (kIsUnique f fInc n k p) where
12092

‎Cubical/Data/Nat/Bijections/Product.agda‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,14 @@ open import Cubical.Foundations.Prelude
44
open import Cubical.Foundations.Isomorphism
55
open import Cubical.Data.Nat
66
open import Cubical.Data.Sigma
7-
open import Cubical.Data.Nat.Bijections.FinN
7+
open import Cubical.Data.Nat.Bijections.Triangle
88

9-
Finℕ≅ℕ×ℕ : Iso Finℕ (ℕ × ℕ)
10-
Iso.fun Finℕ≅ℕ×ℕ (_ , k , m , _) = m , k
11-
Iso.inv Finℕ≅ℕ×ℕ (m , k) = m + k , k , m , refl
12-
Iso.rightInv Finℕ≅ℕ×ℕ _ = refl
13-
Iso.leftInv Finℕ≅ℕ×ℕ (n , k , m , p) = J
14-
(λ { n q → (Iso.inv Finℕ≅ℕ×ℕ (Iso.fun Finℕ≅ℕ×ℕ (n , k , m , q))) ≡ (n , k , m , q) }) refl p
9+
Triangle⊂ℕ≅ℕ×ℕ : Iso Triangle⊂ℕ (ℕ × ℕ)
10+
Iso.fun Triangle⊂ℕ≅ℕ×ℕ (_ , k , m , _) = m , k
11+
Iso.inv Triangle⊂ℕ≅ℕ×ℕ (m , k) = m + k , k , m , refl
12+
Iso.rightInv Triangle⊂ℕ≅ℕ×ℕ _ = refl
13+
Iso.leftInv Triangle⊂ℕ≅ℕ×ℕ (n , k , m , p) = J
14+
(λ n q → (Iso.inv Triangle⊂ℕ≅ℕ×ℕ (Iso.fun Triangle⊂ℕ≅ℕ×ℕ (n , k , m , q))) ≡ (n , k , m , q)) refl p
1515

1616
ℕ×ℕ≅ℕ : Iso (ℕ × ℕ) ℕ
17-
ℕ×ℕ≅ℕ = compIso (invIso Finℕ≅ℕ×ℕ) Finℕ≅ℕ
17+
ℕ×ℕ≅ℕ = compIso (invIso Triangle⊂ℕ≅ℕ×ℕ) Triangle⊂ℕ≅ℕ

‎Cubical/Data/Nat/Bijections/Sum.agda‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ open <-Reasoning
1515

1616
open import Cubical.Tactics.NatSolver
1717
open import Cubical.Data.Nat.Bijections.IncreasingFunction
18-
open import Cubical.Data.Nat.MoreOrderProperties
1918

2019
double : ℕ → ℕ
2120
double n = n + n
@@ -48,8 +47,8 @@ private
4847
k<0 : k < 0
4948
k<0 = pred-≤-pred (pred-≤-pred k+2<2)
5049

51-
doubleInc : isIncreasing double
52-
doubleInc = strengthenIncreasing double doubleGrows
50+
doubleInc : isStrictlyIncreasing double
51+
doubleInc = sucIncreasing→StrictlyIncreasing double doubleGrows
5352

5453
private
5554
partitionDouble≅ℕ⊎ℕ : Iso (partition double refl doubleInc) (ℕ ⊎ ℕ)

Cubical/Data/Nat/Bijections/FinN.agda renamed to Cubical/Data/Nat/Bijections/Triangle.agda

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
module Cubical.Data.Nat.Bijections.FinN where
1+
module Cubical.Data.Nat.Bijections.Triangle where
22

33
open import Cubical.Foundations.Prelude
44
open import Cubical.Foundations.Isomorphism
@@ -9,16 +9,15 @@ open import Cubical.Data.Nat.Order
99
open <-Reasoning
1010
open import Cubical.Tactics.NatSolver
1111
open import Cubical.Data.Nat.Bijections.IncreasingFunction
12-
open import Cubical.Data.Nat.MoreOrderProperties
1312

14-
Finℕ = Σ[ k ∈ ℕ ] Σ[ i ∈ ℕ ] (i ≤ k)
13+
Triangle⊂ℕ = Σ[ k ∈ ℕ ] Σ[ i ∈ ℕ ] (i ≤ k)
1514

1615
triangle : ℕ → ℕ
1716
triangle zero = zero
1817
triangle (suc n) = n + suc (triangle n)
1918

20-
increasingTriangle : isIncreasing triangle
21-
increasingTriangle = strengthenIncreasing triangle triangleN<triangleSN where
19+
strictIncTriangle : isStrictlyIncreasing triangle
20+
strictIncTriangle = sucIncreasing→StrictlyIncreasing triangle triangleN<triangleSN where
2221
triangleN<triangleSN : (n : ℕ) → triangle n < triangle (suc n)
2322
triangleN<triangleSN n = n , refl
2423

@@ -28,26 +27,26 @@ private
2827
1+k+tk=tsk : (n : ℕ) → suc (n + triangle n) ≡ triangle (suc n)
2928
1+k+tk=tsk n = 1+k+t=k+t+1 n (triangle n)
3029

31-
partitionTriangle = partition triangle refl increasingTriangle
30+
partitionTriangle = partition triangle refl strictIncTriangle
3231

33-
Finℕ≅partitionTriangle : Iso Finℕ partitionTriangle
34-
Iso.fun Finℕ≅partitionTriangle (k , i , i≤k) = k , i , i+tk<tsk where
32+
Triangle⊂ℕ≅partitionTriangle : Iso Triangle⊂ℕ partitionTriangle
33+
Iso.fun Triangle⊂ℕ≅partitionTriangle (k , i , i≤k) = k , i , i+tk<tsk where
3534
i+tk<tsk : i + triangle k < triangle (suc k)
3635
i+tk<tsk = i + triangle k <≤⟨ suc-≤-suc (≤-+k {k = triangle k} i≤k) ⟩
3736
k + triangle k <≡⟨ <-suc ⟩ 1+k+tk=tsk k
3837

39-
Iso.inv Finℕ≅partitionTriangle (k , i , i+tk<tsk) = k , i , i≤k where
38+
Iso.inv Triangle⊂ℕ≅partitionTriangle (k , i , i+tk<tsk) = k , i , i≤k where
4039
i+tk<k+tk+1 : i + triangle k < suc (k + triangle k)
4140
i+tk<k+tk+1 = i + triangle k <≡⟨ i+tk<tsk ⟩ sym (1+k+tk=tsk k)
4241
i+tk≤k+tk : i + triangle k ≤ k + triangle k
4342
i+tk≤k+tk = pred-≤-pred i+tk<k+tk+1
4443
i≤k : i ≤ k
4544
i≤k = ≤-+k-cancel i+tk≤k+tk
46-
Iso.rightInv Finℕ≅partitionTriangle (k , i , _) = ΣPathP (refl , ΣPathPProp (λ _ → isProp≤) refl)
47-
Iso.leftInv Finℕ≅partitionTriangle (k , i , _) = ΣPathP (refl , ΣPathPProp (λ _ → isProp≤) refl)
45+
Iso.rightInv Triangle⊂ℕ≅partitionTriangle (k , i , _) = ΣPathP (refl , ΣPathPProp (λ _ → isProp≤) refl)
46+
Iso.leftInv Triangle⊂ℕ≅partitionTriangle (k , i , _) = ΣPathP (refl , ΣPathPProp (λ _ → isProp≤) refl)
4847

4948
partitionTriangle≅ℕ : Iso partitionTriangle ℕ
50-
partitionTriangle≅ℕ = partition≅ℕ triangle refl increasingTriangle
49+
partitionTriangle≅ℕ = partition≅ℕ triangle refl strictIncTriangle
5150

52-
Finℕ≅ℕ : Iso Finℕ ℕ
53-
Finℕ≅ℕ = (compIso Finℕ≅partitionTriangle partitionTriangle≅ℕ)
51+
Triangle⊂ℕ≅ℕ : Iso Triangle⊂ℕ ℕ
52+
Triangle⊂ℕ≅ℕ = (compIso Triangle⊂ℕ≅partitionTriangle partitionTriangle≅ℕ)

0 commit comments

Comments
 (0)