Mercurial > hg > Members > kono > Proof > galois
comparison FLutil.agda @ 152:be888cb9fe1b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 13 Sep 2020 10:54:42 +0900 |
| parents | c00eac825964 |
| children | d880595eae30 |
comparison
equal
deleted
inserted
replaced
| 151:c00eac825964 | 152:be888cb9fe1b |
|---|---|
| 144 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# | 144 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# |
| 145 [] | 145 [] |
| 146 | 146 |
| 147 open import Data.Product | 147 open import Data.Product |
| 148 open import Relation.Nullary.Decidable hiding (⌊_⌋) | 148 open import Relation.Nullary.Decidable hiding (⌊_⌋) |
| 149 open import Data.Bool -- hiding (T) | 149 open import Data.Bool hiding (_<_) |
| 150 open import Data.Unit.Base using (⊤ ; tt) | 150 open import Data.Unit.Base using (⊤ ; tt) |
| 151 | 151 |
| 152 -- fresh a [] = ⊤ | 152 -- fresh a [] = ⊤ |
| 153 -- fresh a (x ∷# xs) = R a x × fresh a xs | 153 -- fresh a (x ∷# xs) = R a x × fresh a xs |
| 154 | 154 |
| 193 FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x = | 193 FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x = |
| 194 Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y | 194 Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y |
| 195 | 195 |
| 196 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 | 196 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 |
| 197 | 197 |
| 198 -- open import Data.List.Fresh.Relation.Unary.All | |
| 199 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] ) | |
| 200 | |
| 201 Flist1 : {n : ℕ } (i : ℕ) → i < suc n → FList {n} → FList {n} → FList {suc n} | |
| 202 Flist1 zero i<n [] _ = [] | |
| 203 Flist1 zero i<n (a ∷# x ) z = FLinsert ( zero :: a ) (Flist1 zero i<n x z ) | |
| 204 Flist1 (suc i) (s≤s i<n) [] z = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z | |
| 205 Flist1 (suc i) i<n (a ∷# x ) z = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z ) | |
| 206 | |
| 207 Flist : {n : ℕ } → FL n → FList {n} | |
| 208 Flist {zero} f0 = f0 ∷# [] | |
| 209 Flist {suc n} (x :: y) = Flist1 n a<sa (Flist y) (Flist y) | |
| 210 | |
| 211 fr8 : FList {4} | |
| 212 fr8 = Flist (fmax {4}) | |
| 213 | |
| 214 -- FLinsert membership | |
| 215 | |
| 216 module FLMB { n : ℕ } where | |
| 217 | |
| 218 FL-Setoid : Setoid Level.zero Level.zero | |
| 219 FL-Setoid = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }} | |
| 220 | |
| 221 open import Data.List.Fresh.Membership.Setoid FL-Setoid | |
| 222 open import Data.List.Fresh.Relation.Unary.Any | |
| 223 | |
| 224 FLinsert-mb : (x : FL n ) → (xs : FList {n}) → x ∈ FLinsert x xs | |
| 225 FLinsert-mb x xs = {!!} |