Mercurial > hg > Members > kono > Proof > galois

comparison FL.agda @ 145:0d59dcbbd0e1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 11 Sep 2020 12:26:22 +0900
parents 62364edeed3f
children 173b0541c766
comparison
equal deleted inserted replaced
144:62364edeed3f 145:0d59dcbbd0e1
164 ttf _ [] fr = Level.lift tt 164 ttf _ [] fr = Level.lift tt
165 ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where 165 ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where
166 ttf1 : True (a f<? a₁) → x f< a → x f< a₁ 166 ttf1 : True (a f<? a₁) → x f< a → x f< a₁
167 ttf1 t x<a = f<-trans x<a (toWitness t) 167 ttf1 t x<a = f<-trans x<a (toWitness t)
168 168
169 FLmin : {n : ℕ } → FList {n} → FL n
170 FLmin {zero} [] = {!!}
171 FLmin {zero} (cons a x x₁) = {!!}
172 FLmin {suc n} x = {!!}
173
174 FLinsert : {n : ℕ } → FL n → FList {n} → FList {n} 169 FLinsert : {n : ℕ } → FL n → FList {n} → FList {n}
175 FLinsert {zero} f0 y = f0 ∷# [] 170 FLinsert {zero} f0 y = f0 ∷# []
176 FLinsert {suc n} x [] = x ∷# [] 171 FLinsert {suc n} x [] = x ∷# []
177 FLinsert {suc n} x (cons a y x₁) with total x a 172 FLinsert {suc n} x (cons a y x₁) with total x a
178 ... | inj₁ (case1 eq) = cons a y x₁ 173 ... | inj₁ (case1 eq) = cons a y x₁
188 ... | inj₁ (case2 lt2) = cons a (cons a₂ t x₁) ( Level.lift (fromWitness a<a₂) , ttf a<a₂ t x₁) where 183 ... | inj₁ (case2 lt2) = cons a (cons a₂ t x₁) ( Level.lift (fromWitness a<a₂) , ttf a<a₂ t x₁) where
189 a<a₂ : a f< a₂ 184 a<a₂ : a f< a₂
190 a<a₂ = f<-trans (toWitness a<a₁) lt2 185 a<a₂ = f<-trans (toWitness a<a₁) lt2
191 ... | inj₂ (case1 refl) = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay) 186 ... | inj₂ (case1 refl) = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
192 ... | inj₂ (case2 lt2) = cons a (cons x (cons a₁ y x₂) ttf2) ( Level.lift (fromWitness lt) , ttf3 ) where 187 ... | inj₂ (case2 lt2) = cons a (cons x (cons a₁ y x₂) ttf2) ( Level.lift (fromWitness lt) , ttf3 ) where
188 x<a₂ : x f< a₂
189 x<a₂ = ?
193 ttf2 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ x (cons a₁ y x₂) -- a f< x , a₂ f< a₁, a < a₁ → x < a₁ , x f< a₂ 190 ttf2 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ x (cons a₁ y x₂) -- a f< x , a₂ f< a₁, a < a₁ → x < a₁ , x f< a₂
194 ttf2 = {!!} , ttf (f<-trans {!!} lt2 ) y x₂ 191 ttf2 = {!!} , ttf (f<-trans {!!} lt2 ) y x₂
195 ttf3 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (cons a₁ y x₂) 192 ttf3 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (cons a₁ y x₂)
196 ttf3 = Level.lift a<a₁ , fr-ay 193 ttf3 = Level.lift a<a₁ , fr-ay
197 194
198 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 195 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1