Mercurial > hg > Members > kono > Proof > galois

comparison FL.agda @ 143:029a7885fe57

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 09:38:23 +0900
parents 435159e2897a
children 62364edeed3f
comparison
equal deleted inserted replaced
142:435159e2897a 143:029a7885fe57
158 -- ttf< : {n : ℕ } → {x a : FL n } → x f< a → T (isYes (x f<? a)) 158 -- ttf< : {n : ℕ } → {x a : FL n } → x f< a → T (isYes (x f<? a))
159 -- ttf< {n} {x} {a} x<a with x f<? a 159 -- ttf< {n} {x} {a} x<a with x f<? a
160 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt 160 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
161 -- ... | no nn = ⊥-elim ( nn x<a ) 161 -- ... | no nn = ⊥-elim ( nn x<a )
162 162
163 ttf : {n : ℕ } (a x : FL (suc n)) → x f< a → (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y 163 ttf : {n : ℕ } {x a : FL (suc n)} → x f< a → (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y
164 ttf a x _ [] fr = Level.lift tt 164 ttf _ [] fr = Level.lift tt
165 ttf a x lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf a₁ x (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 FLinsert : {n : ℕ } → FL n → FList {n} → FList {n} 169 FLinsert : {n : ℕ } → FL n → FList {n} → FList {n}
170 FLinsert {zero} f0 y = f0 ∷# [] 170 FLinsert {zero} f0 y = f0 ∷# []
171 FLinsert {suc n} x [] = x ∷# [] 171 FLinsert {suc n} x [] = x ∷# []
172 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
173 ... | inj₁ (case1 eq) = cons a y x₁ 173 ... | inj₁ (case1 eq) = cons a y x₁
174 FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf a x lt y x₁) 174 FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁)
175 ... | inj₂ (case1 eq) = cons a y x₁ 175 ... | inj₂ (case1 eq) = cons a y x₁
176 FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) [] 176 FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
177 ... | [] | () 177 ... | [] | ()
178 ... | cons a₁ t x₂ | e = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) 178 ... | cons a₁ t x₂ | e = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt )
179 FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) with FLinsert x (cons a₁ y x₂) 179 FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) with FLcmp x a₁ | FLinsert x (cons a₁ y x₂)
180 ... | [] = cons a (cons x ( cons a₁ [] (Level.lift tt) ) {!!} ) {!!} 180 ... | _ | [] = []
181 ... | cons a₂ t x₁ = cons a ( cons a₂ t x₁) ( Level.lift (fromWitness (ttf2 {!!} {!!})) , ( ttf a₂ a (ttf2 {!!} {!!} ) t x₁ )) where 181 ... | tri< x<a₁ ¬b ¬c | cons a₂ t x₁ = cons a (cons a₂ t x₁) ( Level.lift (fromWitness ttf2 ) , (ttf ttf2 t x₁)) where -- a₂ ≡ x
182 ttf2 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a₂ t → a f< a₂ 182 ttf2 : a f< a₂
183 ttf2 = {!!} 183 ttf2 = {!!}
184 ... | tri≈ ¬a b ¬c | cons a₂ t x₁ = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
185 ... | tri> ¬a ¬b a₁<x | cons a₂ t x₁ = cons a (cons a₂ t x₁) ( Level.lift (fromWitness ttf3 ) , (ttf ttf3 t x₁)) where -- a₂ < x
186 ttf3 : a f< a₂
187 ttf3 = {!!}
184 188
185 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 189 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1