Mercurial > hg > Members > kono > Proof > galois

comparison FLutil.agda @ 174:8e8238b26ee7

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 Tue, 24 Nov 2020 15:59:42 +0900
parents 715093a948be
children 0394bc762a49
comparison
equal deleted inserted replaced
173:715093a948be 174:8e8238b26ee7
101 ... | case2 x = case2 (subst (λ k → (zero :: FL0) f< (k :: fmax)) b (f<t x) ) 101 ... | case2 x = case2 (subst (λ k → (zero :: FL0) f< (k :: fmax)) b (f<t x) )
102 102
103 open import Data.Nat.Properties using ( ≤-trans ; <-trans ) 103 open import Data.Nat.Properties using ( ≤-trans ; <-trans )
104 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 104 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n
105 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where 105 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
106 fsuc2 : toℕ x < toℕ (fromℕ< a<sa)
107 fsuc2 = lt
108 fsuc1 : suc (toℕ x) < n 106 fsuc1 : suc (toℕ x) < n
109 fsuc1 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) ) 107 fsuc1 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
110 fsuc (x :: y) (f<t lt) = x :: fsuc y lt 108 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
109
110 -- fsuc0 : { n : ℕ } → (x : FL n ) → FL n
111 -- fsuc0 {n} (x :: y) (f<n lt) = fromℕ< fsuc2 :: y where
112 -- fsuc2 : suc (toℕ x) < n
113 -- fsuc2 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
114 -- fsuc0 (x :: y) (f<t lt) = x :: fsuc y lt
115
116 open import Data.Maybe
117 open import fin
118
119 fpredm : { n : ℕ } → (x : FL n ) → Maybe (FL n)
120 fpredm f0 = nothing
121 fpredm (x :: y) with fpredm y
122 ... | just y1 = just (x :: y1)
123 fpredm (zero :: y) | nothing = nothing
124 fpredm (suc x :: y) | nothing = just (fin+1 x :: fmax)
125
126 ¬<FL0 : {n : ℕ} {y : FL n} → ¬ y f< FL0
127 ¬<FL0 {suc n} {zero :: y} (f<t lt) = ¬<FL0 {n} {y} lt
128
129 fpred : { n : ℕ } → (x : FL n ) → FL0 f< x → FL n
130 fpred (zero :: y) (f<t lt) = zero :: fpred y lt
131 fpred (x :: y) (f<n lt) with FLcmp FL0 y
132 ... | tri< a ¬b ¬c = x :: fpred y a
133 ... | tri> ¬a ¬b c = ⊥-elim (¬<FL0 c)
134 fpred {suc _} (suc x :: y) (f<n lt) | tri≈ ¬a b ¬c = fin+1 x :: fmax
135
136 fpred< : { n : ℕ } → (x : FL n ) → (lt : FL0 f< x ) → fpred x lt f< x
137 fpred< (zero :: y) (f<t lt) = f<t (fpred< y lt)
138 fpred< (suc x :: y) (f<n lt) with FLcmp FL0 y
139 ... | tri< a ¬b ¬c = f<t ( fpred< y a)
140 ... | tri> ¬a ¬b c = ⊥-elim (¬<FL0 c)
141 ... | tri≈ ¬a refl ¬c = f<n fpr1 where
142 fpr1 : {n : ℕ } {x : Fin n} → fin+1 x Data.Fin.< suc x
143 fpr1 {suc _} {zero} = s≤s z≤n
144 fpr1 {suc _} {suc x} = s≤s fpr1
111 145
112 flist1 : {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n)) 146 flist1 : {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n))
113 flist1 zero i<n [] _ = [] 147 flist1 zero i<n [] _ = []
114 flist1 zero i<n (a ∷ x ) z = ( zero :: a ) ∷ flist1 zero i<n x z 148 flist1 zero i<n (a ∷ x ) z = ( zero :: a ) ∷ flist1 zero i<n x z
115 flist1 (suc i) (s≤s i<n) [] z = flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z 149 flist1 (suc i) (s≤s i<n) [] z = flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z
121 155
122 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0) 156 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
123 fr22 = refl 157 fr22 = refl
124 158
125 fr4 : List (FL 4) 159 fr4 : List (FL 4)
126 fr4 = Data.List.reverse (flist (fmax {4}) ) 160 fr4 = Data.List.reverse (flist (fmax {4}) )
127
128 -- fr5 : List (List ℕ) 161 -- fr5 : List (List ℕ)
129 -- fr5 = map plist (map FL→perm (Data.List.reverse (flist (fmax {4}) ))) 162 -- fr5 = map plist (map FL→perm (Data.List.reverse (flist (fmax {4}) )))
130 163
131 164
132 open import Relation.Binary as B hiding (Decidable; _⇔_) 165 open import Relation.Binary as B hiding (Decidable; _⇔_)
211 fr8 = ∀Flist fmax 244 fr8 = ∀Flist fmax
212 245
213 fr9 : FList 3 246 fr9 : FList 3
214 fr9 = ∀Flist fmax 247 fr9 = ∀Flist fmax
215 248
249 ∀Flist' : (n : ℕ ) → FList n
250 ∀Flist' n = ∀Flist0' n n FL0 {!!} where
251 ∀Flist0' : (i j : ℕ) → (x : FL n) → x f< fmax → FList n
252 ∀Flist0' zero zero x _ = []
253 ∀Flist0' zero (suc j) x lt = ∀Flist0' j j fmax {!!}
254 ∀Flist0' (suc i) j x lt = cons (fsuc x lt) (∀Flist0' i j (fsuc x lt) {!!} ) {!!}
255
256 -- open import Size
257 --
258 -- record CFresh {n : ℕ } (i : Size) : Set where
259 -- coinductive
260 -- field
261 -- δ : ∀{j : Size< i} → (y : FL n) → CFresh {n} j
262 -- -- δ : ∀{j : Size< i} → (y : FL n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ y x) → CFresh {n} j (cons y x xr)
263 --
264 -- open CFresh
265 --
266 -- ∀CF : ∀{i} {n : ℕ } → FL n → CFresh {n} i ?
267 -- δ (∀CF x) y fr = {!!}
268
216 open import Data.List.Fresh.Relation.Unary.Any 269 open import Data.List.Fresh.Relation.Unary.Any
217 open import Data.List.Fresh.Relation.Unary.All 270 open import Data.List.Fresh.Relation.Unary.All
271
272 AnyFList' : (n : ℕ ) → (x : FL n ) → Any (x ≡_ ) (∀Flist' n)
273 AnyFList' 0 f0 = ?
274 AnyFList' (suc n) (x :: y) = {!!}
218 275
219 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs) 276 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs)
220 x∈FLins {zero} f0 [] = here refl 277 x∈FLins {zero} f0 [] = here refl
221 x∈FLins {zero} f0 (cons f0 xs x) = here refl 278 x∈FLins {zero} f0 (cons f0 xs x) = here refl
222 x∈FLins {suc n} x [] = here refl 279 x∈FLins {suc n} x [] = here refl
227 x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) ) 284 x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )
228 285
229 nextAny : {n : ℕ} → {x h : FL n } → {L : FList n} → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_ ) L → Any (x ≡_ ) (cons h L hr ) 286 nextAny : {n : ℕ} → {x h : FL n } → {L : FList n} → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_ ) L → Any (x ≡_ ) (cons h L hr )
230 nextAny (here x₁) = there (here x₁) 287 nextAny (here x₁) = there (here x₁)
231 nextAny (there any) = there (there any) 288 nextAny (there any) = there (there any)
232
233 open import fin
234 289
235 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where 290 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where
236 field 291 field
237 ∀list : FList n 292 ∀list : FList n
238 x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list 293 x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list