Mercurial > hg > Members > kono > Proof > galois
annotate FLutil.agda @ 179:abc6acbd4452
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 26 Nov 2020 00:30:05 +0900 |
| parents | 2b4eec28eb13 |
| children | d631469259f2 |
| rev | line source |
|---|---|
| 153 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 151 | 2 module FLutil where |
| 134 | 3 |
| 4 open import Level hiding ( suc ; zero ) | |
| 5 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) | |
| 156 | 6 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) |
| 172 | 7 open import Data.Fin.Permutation -- hiding ([_,_]) |
| 134 | 8 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) |
| 173 | 9 open import Data.Nat.Properties as DNP |
| 172 | 10 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 153 | 11 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev ) |
| 134 | 12 open import Data.Product |
| 13 open import Relation.Nullary | |
| 14 open import Data.Empty | |
| 15 open import Relation.Binary.Core | |
| 172 | 16 open import Relation.Binary.Definitions |
| 137 | 17 open import logic |
| 18 open import nat | |
| 134 | 19 |
| 20 infixr 100 _::_ | |
| 21 | |
| 22 data FL : (n : ℕ )→ Set where | |
| 23 f0 : FL 0 | |
| 24 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n) | |
| 25 | |
| 26 data _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set where | |
| 27 f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt ) | |
| 28 f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt ) | |
| 29 | |
| 30 FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n} → xn :: x ≡ yn :: y → ( xn ≡ yn ) × (x ≡ y ) | |
| 31 FLeq refl = refl , refl | |
| 32 | |
| 33 f-<> : {n : ℕ } {x : FL n } {y : FL n} → x f< y → y f< x → ⊥ | |
| 34 f-<> (f<n x) (f<n x₁) = nat-<> x x₁ | |
| 35 f-<> (f<n x) (f<t lt2) = nat-≡< refl x | |
| 36 f-<> (f<t lt) (f<n x) = nat-≡< refl x | |
| 37 f-<> (f<t lt) (f<t lt2) = f-<> lt lt2 | |
| 38 | |
| 39 f-≡< : {n : ℕ } {x : FL n } {y : FL n} → x ≡ y → y f< x → ⊥ | |
| 40 f-≡< refl (f<n x) = nat-≡< refl x | |
| 41 f-≡< refl (f<t lt) = f-≡< refl lt | |
| 42 | |
| 43 FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n} _≡_ _f<_ | |
| 44 FLcmp f0 f0 = tri≈ (λ ()) refl (λ ()) | |
| 45 FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn | |
| 46 ... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj₁ (FLeq eq)) ) a) (λ lt → f-<> lt (f<n a) ) | |
| 47 ... | tri> ¬a ¬b c = tri> (λ lt → f-<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj₁ (FLeq eq)) )) c) (f<n c) | |
| 48 ... | tri≈ ¬a refl ¬c with FLcmp xt yt | |
| 49 ... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj₂ (FLeq eq) )) (λ lt → f-<> lt (f<t a) ) | |
| 50 ... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt ) refl (λ lt → f-≡< refl lt ) | |
| 51 ... | tri> ¬a₁ ¬b c = tri> (λ lt → f-<> lt (f<t c) ) (λ eq → ¬b (proj₂ (FLeq eq) )) (f<t c) | |
| 52 | |
| 138 | 53 f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z |
| 54 f<-trans {suc n} (f<n x) (f<n x₁) = f<n ( Data.Fin.Properties.<-trans x x₁ ) | |
| 55 f<-trans {suc n} (f<n x) (f<t y<z) = f<n x | |
| 56 f<-trans {suc n} (f<t x<y) (f<n x) = f<n x | |
| 57 f<-trans {suc n} (f<t x<y) (f<t y<z) = f<t (f<-trans x<y y<z) | |
| 58 | |
| 134 | 59 infixr 250 _f<?_ |
| 60 | |
| 61 _f<?_ : {n : ℕ} → (x y : FL n ) → Dec (x f< y ) | |
| 62 x f<? y with FLcmp x y | |
| 63 ... | tri< a ¬b ¬c = yes a | |
| 64 ... | tri≈ ¬a refl ¬c = no ( ¬a ) | |
| 65 ... | tri> ¬a ¬b c = no ( ¬a ) | |
| 66 | |
| 67 _f≤_ : {n : ℕ } (x : FL n ) (y : FL n) → Set | |
| 68 _f≤_ x y = (x ≡ y ) ∨ (x f< y ) | |
| 69 | |
| 70 FL0 : {n : ℕ } → FL n | |
| 71 FL0 {zero} = f0 | |
| 72 FL0 {suc n} = zero :: FL0 | |
| 73 | |
| 74 | |
| 75 fmax : { n : ℕ } → FL n | |
| 76 fmax {zero} = f0 | |
| 77 fmax {suc n} = fromℕ< a<sa :: fmax {n} | |
| 78 | |
| 79 fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x ) | |
| 80 fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where | |
| 81 fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa) | |
| 82 fmax1 {zero} zero = z≤n | |
| 83 fmax1 {suc n} zero = z≤n | |
| 84 fmax1 {suc n} (suc x) = s≤s (fmax1 x) | |
| 85 fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt | |
| 86 | |
| 87 fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax | |
| 88 fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl ) | |
| 89 fmax¬ {suc n} {x} ne with FLcmp x fmax | |
| 90 ... | tri< a ¬b ¬c = a | |
| 91 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b) | |
| 92 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c) | |
| 93 | |
| 94 FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax | |
| 95 FL0≤ {zero} = case1 refl | |
| 96 FL0≤ {suc zero} = case1 refl | |
| 97 FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa) | |
| 98 ... | tri< a ¬b ¬c = case2 (f<n a) | |
| 99 ... | tri≈ ¬a b ¬c with FL0≤ {n} | |
| 100 ... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl ) | |
| 101 ... | case2 x = case2 (subst (λ k → (zero :: FL0) f< (k :: fmax)) b (f<t x) ) | |
| 102 | |
| 151 | 103 open import Data.Nat.Properties using ( ≤-trans ; <-trans ) |
| 104 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n | |
| 105 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where | |
| 106 fsuc1 : suc (toℕ x) < n | |
| 107 fsuc1 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) ) | |
| 108 fsuc (x :: y) (f<t lt) = x :: fsuc y lt | |
| 109 | |
| 174 | 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 | |
| 145 | |
| 151 | 146 flist1 : {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n)) |
| 147 flist1 zero i<n [] _ = [] | |
| 148 flist1 zero i<n (a ∷ x ) z = ( zero :: a ) ∷ flist1 zero i<n x z | |
| 149 flist1 (suc i) (s≤s i<n) [] z = flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z | |
| 150 flist1 (suc i) i<n (a ∷ x ) z = ((fromℕ< i<n ) :: a ) ∷ flist1 (suc i) i<n x z | |
| 151 | |
| 152 flist : {n : ℕ } → FL n → List (FL n) | |
| 153 flist {zero} f0 = f0 ∷ [] | |
| 154 flist {suc n} (x :: y) = flist1 n a<sa (flist y) (flist y) | |
| 155 | |
| 156 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0) | |
| 157 fr22 = refl | |
| 158 | |
| 159 fr4 : List (FL 4) | |
| 174 | 160 fr4 = Data.List.reverse (flist (fmax {4}) ) |
| 151 | 161 -- fr5 : List (List ℕ) |
| 162 -- fr5 = map plist (map FL→perm (Data.List.reverse (flist (fmax {4}) ))) | |
| 163 | |
| 164 | |
| 134 | 165 open import Relation.Binary as B hiding (Decidable; _⇔_) |
| 166 open import Data.Sum.Base as Sum -- inj₁ | |
| 138 | 167 open import Relation.Nary using (⌊_⌋) |
| 172 | 168 open import Data.List.Fresh hiding ([_]) |
| 134 | 169 |
| 153 | 170 FList : (n : ℕ ) → Set |
| 171 FList n = List# (FL n) ⌊ _f<?_ ⌋ | |
| 134 | 172 |
| 153 | 173 fr1 : FList 3 |
| 134 | 174 fr1 = |
| 175 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# | |
| 176 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# | |
| 177 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# | |
| 178 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# | |
| 179 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# | |
| 180 [] | |
| 181 | |
| 182 open import Data.Product | |
| 135 | 183 open import Relation.Nullary.Decidable hiding (⌊_⌋) |
| 172 | 184 -- open import Data.Bool hiding (_<_ ; _≤_ ) |
| 135 | 185 open import Data.Unit.Base using (⊤ ; tt) |
| 186 | |
| 138 | 187 -- fresh a [] = ⊤ |
| 188 -- fresh a (x ∷# xs) = R a x × fresh a xs | |
| 189 | |
| 190 -- toWitness | |
| 191 -- ttf< : {n : ℕ } → {x a : FL n } → x f< a → T (isYes (x f<? a)) | |
| 192 -- ttf< {n} {x} {a} x<a with x f<? a | |
| 193 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt | |
| 194 -- ... | no nn = ⊥-elim ( nn x<a ) | |
| 135 | 195 |
|
176
cf7622b185a6
∀Flist non terminating
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
175
diff
changeset
|
196 ttf : {n : ℕ } {x a : FL (n)} → x f< a → (y : FList (n)) → fresh (FL (n)) ⌊ _f<?_ ⌋ a y → fresh (FL (n)) ⌊ _f<?_ ⌋ x y |
| 143 | 197 ttf _ [] fr = Level.lift tt |
| 198 ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where | |
| 141 | 199 ttf1 : True (a f<? a₁) → x f< a → x f< a₁ |
| 200 ttf1 t x<a = f<-trans x<a (toWitness t) | |
| 201 | |
| 151 | 202 -- by https://gist.github.com/aristidb/1684202 |
| 203 | |
| 153 | 204 FLinsert : {n : ℕ } → FL n → FList n → FList n |
| 205 FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x | |
| 148 | 206 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y) |
| 138 | 207 FLinsert {zero} f0 y = f0 ∷# [] |
| 208 FLinsert {suc n} x [] = x ∷# [] | |
| 148 | 209 FLinsert {suc n} x (cons a y x₁) with FLcmp x a |
| 210 ... | tri≈ ¬a b ¬c = cons a y x₁ | |
| 211 ... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁) | |
| 153 | 212 FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) |
| 213 FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr ) | |
| 147 | 214 |
| 150 | 215 FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt |
| 216 FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b | |
| 151 | 217 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt |
| 149 | 218 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt |
| 151 | 219 ... | tri> ¬a ¬b b<x = Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt |
| 150 | 220 FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b |
| 151 | 221 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br |
| 222 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br | |
| 150 | 223 FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x = |
| 151 | 224 Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt |
| 150 | 225 FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x = |
| 151 | 226 Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y |
| 134 | 227 |
| 138 | 228 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 |
| 151 | 229 |
| 152 | 230 -- open import Data.List.Fresh.Relation.Unary.All |
| 231 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] ) | |
| 232 | |
| 179 | 233 Flist : {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n) |
| 234 Flist zero i<n [] _ = [] | |
| 235 Flist zero i<n (a ∷# x ) z = FLinsert ( zero :: a ) (Flist zero i<n x z ) | |
| 236 Flist (suc i) (s≤s i<n) [] z = Flist i (Data.Nat.Properties.<-trans i<n a<sa) z z | |
| 237 Flist (suc i) i<n (a ∷# x ) z = FLinsert ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z ) | |
| 152 | 238 |
| 179 | 239 ∀Flist : {n : ℕ } → FL n → FList n |
| 240 ∀Flist {zero} f0 = f0 ∷# [] | |
| 241 ∀Flist {suc n} (x :: y) = Flist n a<sa (∀Flist y) (∀Flist y) | |
|
176
cf7622b185a6
∀Flist non terminating
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
175
diff
changeset
|
242 |
|
cf7622b185a6
∀Flist non terminating
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
175
diff
changeset
|
243 ¬x<FL0 : {n : ℕ} {x : FL n} → ¬ ( x f< FL0 ) |
|
cf7622b185a6
∀Flist non terminating
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
175
diff
changeset
|
244 ¬x<FL0 {suc n} {zero :: y} (f<t not) = ¬x<FL0 {n} {y} not |
|
cf7622b185a6
∀Flist non terminating
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
175
diff
changeset
|
245 |
| 153 | 246 fr8 : FList 4 |
| 179 | 247 fr8 = ∀Flist fmax |
| 154 | 248 |
| 172 | 249 fr9 : FList 3 |
| 179 | 250 fr9 = ∀Flist fmax |
| 174 | 251 |
| 154 | 252 open import Data.List.Fresh.Relation.Unary.Any |
| 156 | 253 open import Data.List.Fresh.Relation.Unary.All |
| 154 | 254 |
| 179 | 255 AnyFList : {n : ℕ } → (x : FL (suc n) ) → Any (x ≡_ ) (∀Flist fmax) |
| 256 AnyFList {n} = {!!} | |
| 174 | 257 |
| 154 | 258 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs) |
| 259 x∈FLins {zero} f0 [] = here refl | |
| 260 x∈FLins {zero} f0 (cons f0 xs x) = here refl | |
| 261 x∈FLins {suc n} x [] = here refl | |
| 262 x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a | |
| 263 ... | tri< x<a ¬b ¬c = here refl | |
| 264 ... | tri≈ ¬a b ¬c = here b | |
| 265 x∈FLins {suc n} x (cons a [] x₁) | tri> ¬a ¬b a<x = there ( here refl ) | |
| 266 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₂) ) | |
| 267 | |
| 173 | 268 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 ) |
| 269 nextAny (here x₁) = there (here x₁) | |
| 270 nextAny (there any) = there (there any) | |
| 271 | |
| 156 | 272 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where |
| 273 field | |
| 274 ∀list : FList n | |
| 275 x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list | |
| 276 | |
| 172 | 277 open ∀FListP |
| 278 | |
| 279 -- tt1 : FList 3 | |
| 280 -- tt1 = ∀FListP.∀list (∀FList 3) | |
| 152 | 281 |
| 282 -- FLinsert membership | |
| 283 | |
| 284 module FLMB { n : ℕ } where | |
| 285 | |
| 286 FL-Setoid : Setoid Level.zero Level.zero | |
| 287 FL-Setoid = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }} | |
| 288 | |
| 289 open import Data.List.Fresh.Membership.Setoid FL-Setoid | |
| 290 | |
| 153 | 291 FLinsert-mb : (x : FL n ) → (xs : FList n) → x ∈ FLinsert x xs |
| 154 | 292 FLinsert-mb x xs = x∈FLins {n} x xs |
| 153 | 293 |
| 154 | 294 |