|
72
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2
|
|
|
3 module fin where
|
|
|
4
|
|
83
|
5 open import Data.Fin hiding (_<_ ; _≤_ )
|
|
131
|
6 open import Data.Fin.Properties hiding ( <-trans )
|
|
72
|
7 open import Data.Nat
|
|
|
8 open import logic
|
|
|
9 open import nat
|
|
|
10 open import Relation.Binary.PropositionalEquality
|
|
|
11
|
|
|
12
|
|
|
13 n≤n : (n : ℕ) → n Data.Nat.≤ n
|
|
|
14 n≤n zero = z≤n
|
|
|
15 n≤n (suc n) = s≤s (n≤n n)
|
|
|
16
|
|
|
17 <→m≤n : {m n : ℕ} → m < n → m Data.Nat.≤ n
|
|
|
18 <→m≤n {zero} lt = z≤n
|
|
|
19 <→m≤n {suc m} {zero} ()
|
|
|
20 <→m≤n {suc m} {suc n} (s≤s lt) = s≤s (<→m≤n lt)
|
|
|
21
|
|
91
|
22 -- toℕ<n
|
|
72
|
23 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
|
|
|
24 fin<n {_} {zero} = s≤s z≤n
|
|
|
25 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
|
|
|
26
|
|
91
|
27 -- toℕ≤n
|
|
83
|
28 fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
|
|
|
29 fin≤n {_} zero = z≤n
|
|
|
30 fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)
|
|
|
31
|
|
72
|
32 pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0 → Data.Nat.pred (toℕ f) < n
|
|
|
33 pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
|
|
|
34 pred<n {suc n} {suc f} (s≤s z≤n) = fin<n
|
|
|
35
|
|
131
|
36 fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
|
|
|
37 fin<asa = toℕ-fromℕ< nat.a<sa
|
|
|
38
|
|
91
|
39 -- fromℕ<-toℕ
|
|
72
|
40 toℕ→from : {n : ℕ} {x : Fin (suc n)} → toℕ x ≡ n → fromℕ n ≡ x
|
|
|
41 toℕ→from {0} {zero} refl = refl
|
|
|
42 toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))
|
|
|
43
|
|
91
|
44 -- toℕ-injective
|
|
72
|
45 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
|
|
|
46 i=j {suc n} zero zero refl = refl
|
|
|
47 i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )
|
|
|
48
|
|
91
|
49 -- raise 1
|
|
72
|
50 fin+1 : { n : ℕ } → Fin n → Fin (suc n)
|
|
|
51 fin+1 zero = zero
|
|
|
52 fin+1 (suc x) = suc (fin+1 x)
|
|
|
53
|
|
|
54 open import Data.Nat.Properties as NatP hiding ( _≟_ )
|
|
|
55
|
|
74
|
56 fin+1≤ : { i n : ℕ } → (a : i < n) → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
|
|
72
|
57 fin+1≤ {0} {suc i} (s≤s z≤n) = refl
|
|
|
58 fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )
|
|
|
59
|
|
|
60 fin+1-toℕ : { n : ℕ } → { x : Fin n} → toℕ (fin+1 x) ≡ toℕ x
|
|
|
61 fin+1-toℕ {suc n} {zero} = refl
|
|
|
62 fin+1-toℕ {suc n} {suc x} = cong (λ k → suc k ) (fin+1-toℕ {n} {x})
|
|
|
63
|
|
|
64 open import Relation.Nullary
|
|
|
65 open import Data.Empty
|
|
|
66
|
|
|
67 fin-1 : { n : ℕ } → (x : Fin (suc n)) → ¬ (x ≡ zero ) → Fin n
|
|
|
68 fin-1 zero ne = ⊥-elim (ne refl )
|
|
|
69 fin-1 {n} (suc x) ne = x
|
|
|
70
|
|
|
71 fin-1-sx : { n : ℕ } → (x : Fin n) → fin-1 (suc x) (λ ()) ≡ x
|
|
|
72 fin-1-sx zero = refl
|
|
|
73 fin-1-sx (suc x) = refl
|
|
|
74
|
|
|
75 fin-1-xs : { n : ℕ } → (x : Fin (suc n)) → (ne : ¬ (x ≡ zero )) → suc (fin-1 x ne ) ≡ x
|
|
|
76 fin-1-xs zero ne = ⊥-elim ( ne refl )
|
|
|
77 fin-1-xs (suc x) ne = refl
|
|
|
78
|
|
91
|
79 -- suc-injective
|
|
72
|
80 -- suc-eq : {n : ℕ } {x y : Fin n} → Fin.suc x ≡ Fin.suc y → x ≡ y
|
|
|
81 -- suc-eq {n} {x} {y} eq = subst₂ (λ j k → j ≡ k ) {!!} {!!} (cong (λ k → Data.Fin.pred k ) eq )
|
|
|
82
|
|
91
|
83 -- this is refl
|
|
74
|
84 lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
|
|
72
|
85 lemma3 (s≤s lt) = refl
|
|
91
|
86
|
|
|
87 -- fromℕ<-toℕ
|
|
74
|
88 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m
|
|
72
|
89 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
|
|
91
|
90 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = cong suc ( lemma12 {n} {m} n<m f refl )
|
|
72
|
91
|
|
|
92 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
|
|
|
93 open import Data.Fin.Properties
|
|
|
94
|
|
91
|
95 -- <-irrelevant
|
|
|
96 <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
|
|
|
97 <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
|
|
|
98 <-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl )
|
|
|
99
|
|
72
|
100 lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
|
|
|
101 lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
|
|
|
102 lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl )
|
|
91
|
103
|
|
|
104 -- fromℕ<-irrelevant
|
|
74
|
105 lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
|
|
|
106 lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl ))
|
|
91
|
107
|
|
72
|
108 lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
|
|
|
109 lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl)
|
|
91
|
110
|
|
|
111 -- toℕ-fromℕ<
|
|
74
|
112 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
|
|
72
|
113 lemma11 {n} {m} {x} n<m = begin
|
|
74
|
114 toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
|
|
|
115 ≡⟨ toℕ-fromℕ< _ ⟩
|
|
72
|
116 toℕ x
|
|
|
117 ∎ where
|
|
|
118 open ≡-Reasoning
|
|
|
119
|
|
|
120
|
