Mercurial > hg > Members > kono > Proof > galois
annotate FLComm.agda @ 215:189ce31dc52a
Q Q1
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 06 Dec 2020 06:40:38 +0900 |
| parents | b438377a7e11 |
| children | 658789e98091 |
| 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 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 open import Data.Unit |
|
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 | |
| 49 -- all FL | |
| 50 record AnyFL (n : ℕ) (p : FL n) : Set where | |
| 51 field | |
| 52 anyList : FList n | |
| 53 anyP : (x : FL n) → p f≤ x → Any ( _≡ x ) anyList | |
| 54 | |
| 210 | 55 open import fin |
| 208 | 56 open AnyFL |
| 57 anyFL : (n : ℕ ) → AnyFL n FL0 | |
| 58 anyFL zero = record { anyList = f0 ∷# [] ; anyP = any00 } where | |
| 59 any00 : (p : FL zero) → FL0 f≤ p → Any (_≡ p) (f0 ∷# []) | |
| 60 any00 f0 (case1 refl) = here refl | |
| 210 | 61 anyFL (suc n) = any01 n (anyList (anyFL n)) (anyP (anyFL n) FL0 (case1 refl) ) {!!} where |
| 62 -- any03 : AnyFL (suc n) (fromℕ< a<sa :: fmax) → AnyFL (suc n) FL0 | |
| 63 -- loop on i | |
| 208 | 64 any02 : (i : ℕ ) → (i<n : i < suc n ) → (a : FL n) → AnyFL (suc n) (fromℕ< i<n :: a) → AnyFL (suc n) (zero :: a) |
| 65 any02 zero (s≤s z≤n) a any = any | |
| 211 | 66 any02 (suc i) (s≤s i<n) a any = any02 i (<-trans i<n a<sa) a record { anyList = cons ((fromℕ< (s≤s i<n )) :: a) (anyList any) any07 ; anyP = any08 } where |
| 67 any07 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) (anyList any) | |
| 68 any07 = {!!} | |
| 69 any08 : (x : FL (suc n)) → (fromℕ< (<-trans i<n a<sa) :: a) f≤ x → Any (_≡ x) (cons (fromℕ< (s≤s i<n) :: a) (anyList any) any07 ) | |
| 70 any08 = {!!} | |
| 210 | 71 -- loop on a |
| 72 any03 : (L : FList n) → (a : FL n) → fresh (FL n) ⌊ _f<?_ ⌋ a L → AnyFL (suc n) (fromℕ< a<sa :: a ) → AnyFL (suc n) FL0 | |
| 73 any03 [] a ar any = {!!} -- any02 n a<sa a any | |
| 211 | 74 any03 (cons b L br) a ( Data.Product._,_ (Level.lift a<b)_) any = any03 L b br record { anyList = anyList any04 ; anyP = any05 } where |
| 210 | 75 any04 : AnyFL (suc n) (zero :: a) |
| 76 any04 = any02 n a<sa a any | |
| 77 any05 : (x : FL (suc n)) → (fromℕ< a<sa :: b) f≤ x → Any (_≡ x) (anyList any04) -- 0<fmax : zero Data.Fin.< fromℕ< a<sa | |
| 211 | 78 any05 x mb≤x = anyP any04 x (any06 a b x (toWitness a<b) mb≤x) where |
| 79 any06 : {n : ℕ } → (a b : FL n) → (x : FL (suc n)) → a f< b → (fromℕ< {n} a<sa :: b) f≤ x → (zero :: a) f≤ x | |
| 80 any06 {suc n} a b x a<b (case1 refl) = case2 (f<n 0<fmax) | |
| 81 any06 {suc n} a b x a<b (case2 mb<x) = case2 (f<-trans (f<n 0<fmax) mb<x) | |
| 210 | 82 any01 : (i : ℕ ) → (L : FList n) → Any (_≡ FL0) L → AnyFL (suc n) fmax → AnyFL (suc n) FL0 |
| 83 any01 zero [] () | |
| 84 any01 (suc i) [] () | |
| 85 any01 zero (cons a L x) _ any = {!!} | |
| 86 any01 (suc i) (cons .FL0 L x) (here refl) any = any01 i L {!!} {!!} -- can't happen | |
| 87 any01 (suc i) (cons a L ar) (there b) any = any03 L a ar {!!} | |
| 208 | 88 |
| 186 | 89 tl3 : (FL n) → ( z : FList n) → FList n → FList n |
| 90 tl3 h [] w = w | |
| 91 tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w ) | |
| 92 tl2 : ( x z : FList n) → FList n → FList n | |
| 93 tl2 [] _ x = x | |
| 94 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
|
95 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 CommFList : FList n → FList n |
| 186 | 97 CommFList x = tl2 x x [] |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 CommFListN : ℕ → FList n |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 CommFListN 0 = ∀Flist fmax |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 CommFListN (suc i) = CommFList (CommFListN i) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 |
| 211 | 103 -- all comm cobmbination in P and Q |
| 104 record AnyComm (P Q : FList n) : Set where | |
| 105 field | |
| 106 commList : FList n | |
| 107 commAny : (p q : FL n) → Any (p ≡_) P → Any (q ≡_) Q → Any ( _≡ perm→FL [ FL→perm p , FL→perm q ] ) commList | |
| 108 | |
| 109 open AnyComm | |
| 110 anyComm : (P Q : FList n) → AnyComm P Q | |
| 111 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () } | |
| 112 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () } | |
| 113 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () } | |
| 215 | 114 anyComm (cons p P pr) Q = anyc0n Q Q where |
| 115 anyc0n : (Q Q1 : FList n) → AnyComm (cons p P pr) Q | |
| 116 anyc00 : (Q1 : FList n) (q : FL n) → fresh (FL n) ⌊ _f<?_ ⌋ q Q1 → fresh (FL n) ⌊ _f<?_ ⌋ (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1)) | |
| 211 | 117 anyc00 = {!!} |
| 214 | 118 anyc01 : (Q1 : FList n) (q : FL n) → (qr : fresh (FL n) ⌊ _f<?_ ⌋ q Q1 ) → (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q1 qr) → |
| 215 | 119 Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1)) (anyc00 Q1 q qr)) |
| 214 | 120 anyc01 Q1 q qr p q (here refl) (here refl) = here refl |
| 215 | 121 anyc01 Q1 q qr p q₁ (here refl) (there anyq) = there (commAny (anyc0n Q Q1) p q₁ (here refl) ? ) |
| 122 anyc01 Q1 q qr p₁ q (there anyp) (here refl) with commAny (anyc0n Q []) p₁ q (there anyp) {!!} -- Any (_≡_ q) Q | |
| 213 | 123 ... | t = {!!} |
| 124 where | |
| 125 -- anyc02 Q p₁ q qr anyp where | |
| 126 anyc02 : {P : FList n} {p₂ : FL n} {pr₂ : fresh (FL n) ⌊ _f<?_ ⌋ p₂ P} | |
| 127 → (Q1 : FList n) (p₁ q : FL n) → (qr : fresh (FL n) ⌊ _f<?_ ⌋ q Q1 ) → Any (_≡_ p₁) (cons p₂ P pr₂) | |
| 215 | 128 → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1)) (anyc00 Q1 q qr)) |
| 214 | 129 anyc02 {P} Q1 p₁ q qr (here refl) = {!!} |
| 130 anyc02 {P} Q1 p₁ q qr (there any) = {!!} | |
| 215 | 131 anyc01 Q1 q qr p₁ q₁ (there anyp) (there anyq) = there (commAny (anyc0n Q Q1) p₁ q₁ (there anyp) ? ) |
| 132 anyc0n Q [] = record { commList = (commList (anyComm P Q)) ; commAny = ? } | |
| 133 anyc0n Q (cons q Q1 qr ) = record { commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1)) ? | |
| 134 ; commAny = ? } | |
| 211 | 135 |
| 200 | 136 -- {-# TERMINATING #-} |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
137 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
|
138 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x) |
| 188 | 139 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 | 140 G = perm→FL g |
| 141 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
|
142 |
|
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
|
143 -- tl3 case |
| 197 | 144 commc : (L3 L1 : FList n) → Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) L3 |
| 145 → Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) (tl3 G L1 L3) | |
| 146 commc L3 [] any = any | |
| 198 | 147 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
|
148 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
|
149 comm6 = pcong-pF (comm-resp (FL←iso _) (FL←iso _)) |
| 189 | 150 comm3 : (L1 : FList n) → Any (H ≡_) L1 → (L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 L3) |
| 151 comm3 (H ∷# []) (here refl) L3 = subst (λ k → Any (_≡_ k) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) ) | |
| 152 comm6 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3 ) | |
| 197 | 153 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 |
| 154 (commc (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) L1 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3)) | |
| 190 | 155 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
|
156 |
|
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
|
157 -- tl2 case |
| 188 | 158 comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ] ≡_) (tl2 L L1 L3) |
| 189 | 159 comm2 (cons G L xr) L1 (here refl) b L3 = comm7 L L3 where |
| 203 | 160 comm8 : (L L4 L2 : FList n) → (a : FL n) |
| 161 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) | |
| 162 → 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
|
163 comm8← : (L L4 L2 : FList n) → (a : FL n) → ¬ ( a ≡ perm→FL g ) |
|
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
|
164 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2)) |
|
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
|
165 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) |
|
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
|
166 comm9← : (L4 L2 : FList n) → (a a₁ : FL n) → ¬ ( a ≡ perm→FL g ) |
|
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
|
167 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2)) |
|
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
|
168 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) |
|
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
|
169 -- Any (_≡_ (perm→FL [ g , h ])) (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) → Any (_≡_ (perm→FL [ g , h ])) L2 |
|
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
|
170 comm9← [] L2 a a₁ not any = {!!} |
| 206 | 171 comm9← (cons a₂ L4 x) L2 a a₁ not any = comm8 L1 L4 L2 a₂ |
| 207 | 172 (comm9← L4 L2 a a₁ not |
| 206 | 173 (comm8← L1 L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2 ) a₂ {!!} any)) |
| 174 -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))) → | |
| 175 -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2)) | |
| 176 -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) | |
| 177 -- 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
|
178 comm8← [] L4 L2 a _ any = any |
| 206 | 179 comm8← (cons a₁ L x) L4 L2 a not any = comm8← L L4 L2 a not |
| 180 (comm9← L4 (tl3 a L L2 ) a a₁ not (subst (λ k → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 k )) {!!} any )) | |
| 205 | 181 -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))) → |
| 182 -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) (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
|
183 comm9 : (L4 L2 : FList n) → (a a₁ : FL n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) → |
|
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
|
184 Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2)) |
| 203 | 185 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
|
186 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
|
187 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
|
188 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 | 189 -- found g, we have to walk thru till the end |
| 189 | 190 comm7 : (L L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L L1 (tl3 G L1 L3)) |
| 201 | 191 -- at the end, find h |
| 189 | 192 comm7 [] L3 = comm3 L1 b L3 |
| 201 | 193 -- add n path |
| 203 | 194 comm7 (cons a L4 xr) L3 = comm8 L1 L4 (tl3 G L1 L3) a (comm7 L4 L3) |
| 201 | 195 -- accumerate tl3 |
| 200 | 196 comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b (tl3 x L1 L3) |
| 186 | 197 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 |
| 198 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
|
199 comm4 = pcong-pF |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
200 |
| 184 | 201 CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid |
| 202 CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0 |