Mercurial > hg > Members > kono > Proof > galois
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 -- |