comparison src/fin.agda @ 320:8fb16f9a882a

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 19 Sep 2023 11:11:38 +0900
parents fff18d4a063b
children e9de2bfef88d
comparison
equal deleted inserted replaced
318:fff18d4a063b 320:8fb16f9a882a
101 -- 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 ) 101 -- 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 )
102 102
103 -- fromℕ<-irrelevant 103 -- fromℕ<-irrelevant
104 -- lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n 104 -- lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
105 -- lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl )) 105 -- lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl ))
106
107 lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
108 lemma10 {.(suc _)} {zero} {zero} refl {s≤s z≤n} {s≤s z≤n} = refl
109 lemma10 {suc n} {suc i} {suc i} refl {s≤s i<n} {s≤s j<n} = cong suc (lemma10 {n} {i} {i} refl {i<n} {j<n})
106 110
107 -- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c 111 -- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
108 -- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 112 -- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl)
109 113
110 -- toℕ-fromℕ< 114 -- toℕ-fromℕ<
131 f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y → toℕ x ≡ toℕ y 135 f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y → toℕ x ≡ toℕ y
132 f≡→≡ refl = refl 136 f≡→≡ refl = refl
133 137
134 open import Data.List 138 open import Data.List
135 open import Relation.Binary.Definitions 139 open import Relation.Binary.Definitions
136
137 140
138 ----- 141 -----
139 -- 142 --
140 -- find duplicate element in a List (Fin n) 143 -- find duplicate element in a List (Fin n)
141 -- 144 --