Mercurial > hg > Members > kono > Proof > galois
annotate FLComm.agda @ 236:f8bfda8d0669
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 09 Dec 2020 11:33:43 +0900 |
| parents | d204b7f9b89a |
| children | 3aafd76f21c1 |
| rev | line source |
|---|---|
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 {-# OPTIONS --allow-unsolved-metas #-} |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 module FLComm (n : ℕ) where |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Level renaming ( suc to Suc ; zero to Zero ) hiding (lift) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import Data.Fin.Permutation |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Data.Nat.Properties |
| 186 | 10 open import Relation.Binary.PropositionalEquality hiding ( [_] ) renaming ( sym to ≡-sym ) |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev ) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 open import Data.Product hiding (_,_ ) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 open import Relation.Nullary |
| 232 | 14 open import Data.Unit hiding (_≤_) |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open import Data.Empty |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 open import Relation.Binary.Core |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 open import Relation.Binary.Definitions hiding (Symmetric ) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 open import logic |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 open import nat |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 open import FLutil |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 open import Putil |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 import Solvable |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 open import Symmetric |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 -- infixr 100 _::_ |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
| 188 | 28 open import Relation.Nary using (⌊_⌋) |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 open import Data.List.Fresh hiding ([_]) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 open import Data.List.Fresh.Relation.Unary.Any |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
| 208 | 32 open import Algebra |
| 33 open Group (Symmetric n) hiding (refl) | |
| 186 | 34 open Solvable (Symmetric n) |
| 208 | 35 open _∧_ |
| 211 | 36 -- open import Relation.Nary using (⌊_⌋) |
| 37 open import Relation.Nullary.Decidable hiding (⌊_⌋) | |
| 208 | 38 |
| 39 -- Flist : {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n) | |
| 40 -- Flist zero i<n [] _ = [] | |
| 41 -- Flist zero i<n (a ∷# x ) z = FLinsert ( zero :: a ) (Flist zero i<n x z ) | |
| 42 -- Flist (suc i) (s≤s i<n) [] z = Flist i (<-trans i<n a<sa) z z | |
| 43 -- Flist (suc i) i<n (a ∷# x ) z = FLinsert ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z ) | |
| 44 -- | |
| 45 -- ∀Flist : {n : ℕ } → FL n → FList n | |
| 46 -- ∀Flist {zero} f0 = f0 ∷# [] | |
| 47 -- Flist {suc n} (x :: y) = Flist n a<sa (∀Flist y) (∀Flist y) | |
| 48 | |
| 229 | 49 ------------- |
| 233 | 50 -- # 0 : # 0 : .... # 0 : # 0 :: f0 |
| 51 -- # 0 : # 0 : .... # 1 : # 0 :: f0 | |
| 52 -- | |
| 53 -- # sn: # 0 : .... # 0 : # 0 :: f0 | |
| 54 -- | |
| 55 -- # sn: # n : .... # 1 : # 0 :: f0 | |
| 56 -- | |
| 229 | 57 |
| 208 | 58 -- all FL |
| 236 | 59 record AnyFL (n : ℕ) (y : FL n) : Set where |
| 208 | 60 field |
| 236 | 61 allFL : FList n |
| 62 anyP : (x : FL n) → Any (x ≡_ ) allFL | |
| 208 | 63 |
| 210 | 64 open import fin |
| 208 | 65 open AnyFL |
| 231 | 66 |
| 233 | 67 -- {-# TERMINATING #-} |
| 236 | 68 anyFL0 : (n : ℕ) → AnyFL (suc n) fmax |
| 69 anyFL0 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = anyFL2 } where | |
| 70 anyFL2 : (x : FL 1) → Any (_≡_ x) (cons (zero :: f0) [] (Level.lift tt)) | |
| 71 anyFL2 (zero :: f0) = here refl | |
| 72 anyFL0 (suc n) = record { allFL = allListF a<sa []; anyP = λ x → anyFL3 a<sa x (fin≤n (FLpos x)) [] } where | |
| 233 | 73 allListFL : (x : Fin (suc (suc n))) → FList (suc n) → FList (suc (suc n)) → FList (suc (suc n)) |
| 74 allListFL _ [] y = y | |
| 234 | 75 allListFL x (cons y L yr) z = FLinsert (x :: y) (allListFL x L z) |
| 233 | 76 allListF : {i : ℕ} → (i<n : i < suc (suc n)) → FList (suc (suc n)) → FList (suc (suc n)) |
| 236 | 77 allListF (s≤s z≤n) z = allListFL zero (allFL (anyFL0 n)) z |
| 78 allListF (s≤s (s≤s i<n)) z = allListFL (suc (fromℕ< (s≤s i<n ))) (allFL (anyFL0 n)) (allListF (<-trans (s≤s i<n) a<sa) z) | |
| 79 anyFL3 : {i : ℕ} → (i<n : i < suc (suc n)) (x : FL (suc (suc n))) → (toℕ (FLpos x ) ≤ i) → (z : FList (suc (suc n))) → Any (_≡_ x) (allListF i<n z) | |
| 80 anyFL3 {zero} (s≤s z≤n) (x :: y) x<i z = {!!} where | |
| 81 anyFL5 : toℕ x ≤ zero → x ≡ zero | |
| 82 anyFL5 lt with <-fcmp x zero | |
| 83 ... | tri≈ ¬a b ¬c = b | |
| 84 ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c) | |
| 85 anyFL3 {suc i} (s≤s i<n) (x :: y) x<i z with <-cmp (toℕ x) (suc i) | |
| 86 ... | tri< a ¬b ¬c = anyFL1 i<n where | |
| 87 anyFL1 : {i : ℕ } → (i<n : i < suc n) → Any (_≡_ (x :: y)) (allListF (s≤s i<n) z) | |
| 88 anyFL1 L = {!!} | |
| 235 | 89 ... | tri≈ ¬a b ¬c = {!!} |
| 90 ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c) | |
| 91 | |
| 236 | 92 anyFL : (n : ℕ) → AnyFL n fmax |
| 93 anyFL zero = record { allFL = f0 ∷# [] ; anyP = anyFL4 } where | |
| 94 anyFL4 : (x : FL zero) → Any (_≡_ x) ( f0 ∷# [] ) | |
| 95 anyFL4 f0 = here refl | |
| 96 anyFL (suc n) = anyFL0 n | |
| 97 | |
| 235 | 98 at1 = allFL (anyFL 1) |
| 99 at2 = allFL (anyFL 2) | |
| 100 at3 = allFL (anyFL 3) | |
| 208 | 101 |
| 186 | 102 tl3 : (FL n) → ( z : FList n) → FList n → FList n |
| 103 tl3 h [] w = w | |
| 104 tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w ) | |
| 105 tl2 : ( x z : FList n) → FList n → FList n | |
| 106 tl2 [] _ x = x | |
| 107 tl2 (h ∷# x) z w = tl2 x z (tl3 h z w) | |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 CommFList : FList n → FList n |
| 186 | 110 CommFList x = tl2 x x [] |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 CommFListN : ℕ → FList n |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 CommFListN 0 = ∀Flist fmax |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 CommFListN (suc i) = CommFList (CommFListN i) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 |
| 229 | 116 -- all cobmbination in P and Q |
| 228 | 117 record AnyComm (P Q : FList n) (fpq : (p q : FL n) → FL n) : Set where |
| 211 | 118 field |
| 119 commList : FList n | |
| 224 | 120 commAny : (p q : FL n) |
| 121 → Any ( p ≡_ ) P → Any ( q ≡_ ) Q | |
| 228 | 122 → Any (fpq p q ≡_) commList |
| 211 | 123 |
| 225 | 124 ------------- |
| 125 -- (p,q) (p,qn) .... (p,q0) | |
| 126 -- pn,q | |
| 127 -- : AnyComm FL0 FL0 P Q | |
| 128 -- p0,q | |
| 129 | |
| 226 | 130 p<anyL : {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → p f≤ p₁ |
| 131 p<anyL {p} {p₁} {P} {pr} (here refl) = case1 refl | |
| 132 p<anyL {p} {p₁} {cons a P x} { Data.Product._,_ (Level.lift p<a) snd} (there any) with p<anyL any | |
| 133 ... | case1 refl = case2 (toWitness p<a) | |
| 134 ... | case2 a<p₁ = case2 (f<-trans (toWitness p<a) a<p₁) | |
| 135 | |
| 136 p<anyL1 : {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → ¬ (p ≡ p₁) → p f< p₁ | |
| 137 p<anyL1 {p} {p₁} {P} {pr} any neq with p<anyL any | |
| 138 ... | case1 eq = ⊥-elim ( neq eq ) | |
| 139 ... | case2 x = x | |
| 140 | |
| 228 | 141 open AnyComm |
| 142 anyComm : (P Q : FList n) → (fpq : (p q : FL n) → FL n) → AnyComm P Q fpq | |
| 143 anyComm [] [] _ = record { commList = [] ; commAny = λ _ _ () } | |
| 144 anyComm [] (cons q Q qr) _ = record { commList = [] ; commAny = λ _ _ () } | |
| 145 anyComm (cons p P pr) [] _ = record { commList = [] ; commAny = λ _ _ _ () } | |
| 146 anyComm (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q) ; commAny = anyc0n } where | |
| 225 | 147 commListP : (P1 : FList n) → FList n |
| 228 | 148 commListP [] = commList (anyComm P Q fpq) |
| 225 | 149 commListP (cons p₁ P1 x) = FLinsert (fpq p₁ q) (commListP P1) |
| 150 commListQ : (Q1 : FList n) → FList n | |
| 151 commListQ [] = commListP P | |
| 152 commListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (commListQ Q1) | |
| 226 | 153 anyc0n : (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr) |
| 228 | 154 → Any (_≡_ (fpq p₁ q₁)) (FLinsert (fpq p q) (commListQ Q)) |
| 155 anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (commListQ Q ) | |
| 227 | 156 anyc0n p₁ q₁ (here refl) (there anyq) = insAny (commListQ Q) (anyc01 Q anyq) where |
| 157 anyc01 : (Q1 : FList n) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) | |
| 158 anyc01 (cons q Q1 qr₂) (here refl) = x∈FLins _ _ | |
| 159 anyc01 (cons q₂ Q1 qr₂) (there any) = insAny _ (anyc01 Q1 any) | |
| 160 anyc0n p₁ q₁ (there anyp) (here refl) = insAny _ (anyc02 Q) where | |
| 161 anyc03 : (P1 : FList n) → Any (_≡_ p₁) P1 → Any (_≡_ (fpq p₁ q₁)) (commListP P1) | |
| 162 anyc03 (cons a P1 x) (here refl) = x∈FLins _ _ | |
| 163 anyc03 (cons a P1 x) (there any) = insAny _ ( anyc03 P1 any) | |
| 164 anyc02 : (Q1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) | |
| 165 anyc02 [] = anyc03 P anyp | |
| 166 anyc02 (cons a Q1 x) = insAny _ (anyc02 Q1) | |
| 167 anyc0n p₁ q₁ (there anyp) (there anyq) = insAny (commListQ Q) (anyc04 Q) where | |
| 168 anyc05 : (P1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListP P1) | |
| 228 | 169 anyc05 [] = commAny (anyComm P Q fpq) p₁ q₁ anyp anyq |
| 227 | 170 anyc05 (cons a P1 x) = insAny _ (anyc05 P1) |
| 171 anyc04 : (Q1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) | |
| 172 anyc04 [] = anyc05 P | |
| 173 anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1) | |
| 211 | 174 |
| 200 | 175 -- {-# TERMINATING #-} |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
176 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i ) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
177 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x) |
| 188 | 178 CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where |
| 186 | 179 G = perm→FL g |
| 180 H = perm→FL h | |
|
204
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
181 |
|
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
182 -- tl3 case |
| 222 | 183 commc : (L3 L1 : FList n) → Any ((perm→FL [ FL→perm G , FL→perm H ]) ≡_) L3 |
| 184 → Any ((perm→FL [ FL→perm G , FL→perm H ]) ≡_) (tl3 G L1 L3) | |
| 197 | 185 commc L3 [] any = any |
| 198 | 186 commc L3 (cons a L1 _) any = commc (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3) L1 (insAny _ any) |
|
204
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
187 comm6 : perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ] |
|
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
188 comm6 = pcong-pF (comm-resp (FL←iso _) (FL←iso _)) |
| 222 | 189 comm3 : (L1 : FList n) → Any (H ≡_) L1 → (L3 : FList n) → Any ((perm→FL [ g , h ]) ≡_) (tl3 G L1 L3) |
| 190 comm3 (H ∷# []) (here refl) L3 = subst (λ k → Any (k ≡_) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) ) | |
| 189 | 191 comm6 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3 ) |
| 222 | 192 comm3 (cons H L1 x₁) (here refl) L3 = subst (λ k → Any (k ≡_) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))) comm6 |
| 197 | 193 (commc (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) L1 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3)) |
| 190 | 194 comm3 (cons a L _) (there b) L3 = comm3 L b (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3) |
|
204
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
195 |
|
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
196 -- tl2 case |
| 222 | 197 comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ] ≡_ ) (tl2 L L1 L3) |
| 189 | 198 comm2 (cons G L xr) L1 (here refl) b L3 = comm7 L L3 where |
| 203 | 199 comm8 : (L L4 L2 : FList n) → (a : FL n) |
| 222 | 200 → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2) |
| 201 → Any ((perm→FL [ g , h ]) ≡_ ) (tl2 L4 L1 (tl3 a L L2)) | |
|
204
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
202 comm8← : (L L4 L2 : FList n) → (a : FL n) → ¬ ( a ≡ perm→FL g ) |
| 222 | 203 → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (tl3 a L L2)) |
| 204 → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2) | |
|
204
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
205 comm9← : (L4 L2 : FList n) → (a a₁ : FL n) → ¬ ( a ≡ perm→FL g ) |
| 222 | 206 → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2)) |
| 207 → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2) | |
| 208 -- Any (_≡ (perm→FL [ g , h ])) (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) → Any ((perm→FL [ g , h ]) ≡_) L2 | |
|
204
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
209 comm9← [] L2 a a₁ not any = {!!} |
| 206 | 210 comm9← (cons a₂ L4 x) L2 a a₁ not any = comm8 L1 L4 L2 a₂ |
| 207 | 211 (comm9← L4 L2 a a₁ not |
| 206 | 212 (comm8← L1 L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2 ) a₂ {!!} any)) |
| 222 | 213 -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))) → |
| 214 -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2)) | |
| 215 -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 L2) | |
| 216 -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 L2)) | |
|
204
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
217 comm8← [] L4 L2 a _ any = any |
| 206 | 218 comm8← (cons a₁ L x) L4 L2 a not any = comm8← L L4 L2 a not |
| 222 | 219 (comm9← L4 (tl3 a L L2 ) a a₁ not (subst (λ k → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 k )) {!!} any )) |
| 220 -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))) → | |
| 221 -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) (tl3 a L L2))) | |
| 222 comm9 : (L4 L2 : FList n) → (a a₁ : FL n) → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2) → | |
| 223 Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2)) | |
| 203 | 224 comm8 [] L4 L2 a any = any |
|
204
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
225 comm8 (cons a₁ L x) L4 L2 a any = comm8 L L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a (comm9 L4 L2 a a₁ any) |
|
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
226 comm9 [] L2 a a₁ any = insAny _ any |
|
84795e6638ce
commutativity of Any _ (tl2 L4 L1 L2) and Any _ (tl2 L4 L1 (tl3 a L L2))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
203
diff
changeset
|
227 comm9 (cons a₂ L4 x) L2 a a₁ any = comm8 L1 L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a₂ (comm9 L4 L2 a a₁ (comm8← L1 L4 L2 a₂ {!!} any)) |
| 201 | 228 -- found g, we have to walk thru till the end |
| 222 | 229 comm7 : (L L3 : FList n) → Any ((perm→FL [ g , h ]) ≡_) (tl2 L L1 (tl3 G L1 L3)) |
| 201 | 230 -- at the end, find h |
| 189 | 231 comm7 [] L3 = comm3 L1 b L3 |
| 201 | 232 -- add n path |
| 203 | 233 comm7 (cons a L4 xr) L3 = comm8 L1 L4 (tl3 G L1 L3) a (comm7 L4 L3) |
| 201 | 234 -- accumerate tl3 |
| 200 | 235 comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b (tl3 x L1 L3) |
| 186 | 236 CommStage→ (suc i) x (ccong {f} {x} eq p) = subst (λ k → Any (k ≡_) (tl2 (CommFListN i) (CommFListN i) [])) (comm4 eq) (CommStage→ (suc i) f p ) where |
| 237 comm4 : f =p= x → perm→FL f ≡ perm→FL x | |
|
187
c22ef5bc695a
remove gen/uni from Commutator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
186
diff
changeset
|
238 comm4 = pcong-pF |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
239 |
| 184 | 240 CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid |
| 241 CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0 |