Mercurial > hg > Members > kono > Proof > galois
annotate src/FLComm.agda @ 255:6d1619d9f880
library
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 Jan 2021 10:18:08 +0900 |
| parents | FLComm.agda@d782dd481a26 |
| children | 77f01da94c4e |
| 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 |
| 210 | 39 open import fin |
| 231 | 40 |
| 249 | 41 -- all cobmbination in P and Q (could be more general) |
| 242 | 42 record AnyComm {n m l : ℕ} (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where |
| 211 | 43 field |
| 242 | 44 commList : FList l |
| 45 commAny : (p : FL n) (q : FL m) | |
| 224 | 46 → Any ( p ≡_ ) P → Any ( q ≡_ ) Q |
| 228 | 47 → Any (fpq p q ≡_) commList |
| 211 | 48 |
| 225 | 49 ------------- |
| 50 -- (p,q) (p,qn) .... (p,q0) | |
| 51 -- pn,q | |
| 52 -- : AnyComm FL0 FL0 P Q | |
| 53 -- p0,q | |
| 54 | |
| 228 | 55 open AnyComm |
| 242 | 56 anyComm : {n m l : ℕ } → (P : FList n) (Q : FList m) → (fpq : (p : FL n) (q : FL m) → FL l) → AnyComm P Q fpq |
| 228 | 57 anyComm [] [] _ = record { commList = [] ; commAny = λ _ _ () } |
| 58 anyComm [] (cons q Q qr) _ = record { commList = [] ; commAny = λ _ _ () } | |
| 59 anyComm (cons p P pr) [] _ = record { commList = [] ; commAny = λ _ _ _ () } | |
| 242 | 60 anyComm {n} {m} {l} (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q) ; commAny = anyc0n } where |
| 61 commListP : (P1 : FList n) → FList l | |
| 62 commListP [] = commList (anyComm P Q fpq) | |
| 225 | 63 commListP (cons p₁ P1 x) = FLinsert (fpq p₁ q) (commListP P1) |
| 242 | 64 commListQ : (Q1 : FList m) → FList l |
| 225 | 65 commListQ [] = commListP P |
| 66 commListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (commListQ Q1) | |
| 242 | 67 anyc0n : (p₁ : FL n) (q₁ : FL m) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr) |
| 228 | 68 → Any (_≡_ (fpq p₁ q₁)) (FLinsert (fpq p q) (commListQ Q)) |
| 69 anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (commListQ Q ) | |
| 227 | 70 anyc0n p₁ q₁ (here refl) (there anyq) = insAny (commListQ Q) (anyc01 Q anyq) where |
| 242 | 71 anyc01 : (Q1 : FList m) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) |
| 227 | 72 anyc01 (cons q Q1 qr₂) (here refl) = x∈FLins _ _ |
| 73 anyc01 (cons q₂ Q1 qr₂) (there any) = insAny _ (anyc01 Q1 any) | |
| 74 anyc0n p₁ q₁ (there anyp) (here refl) = insAny _ (anyc02 Q) where | |
| 75 anyc03 : (P1 : FList n) → Any (_≡_ p₁) P1 → Any (_≡_ (fpq p₁ q₁)) (commListP P1) | |
| 76 anyc03 (cons a P1 x) (here refl) = x∈FLins _ _ | |
| 77 anyc03 (cons a P1 x) (there any) = insAny _ ( anyc03 P1 any) | |
| 242 | 78 anyc02 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) |
| 227 | 79 anyc02 [] = anyc03 P anyp |
| 80 anyc02 (cons a Q1 x) = insAny _ (anyc02 Q1) | |
| 81 anyc0n p₁ q₁ (there anyp) (there anyq) = insAny (commListQ Q) (anyc04 Q) where | |
| 82 anyc05 : (P1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListP P1) | |
| 228 | 83 anyc05 [] = commAny (anyComm P Q fpq) p₁ q₁ anyp anyq |
| 227 | 84 anyc05 (cons a P1 x) = insAny _ (anyc05 P1) |
| 242 | 85 anyc04 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) |
| 227 | 86 anyc04 [] = anyc05 P |
| 87 anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1) | |
| 211 | 88 |
| 249 | 89 ------------- |
| 90 -- # 0 :: # 0 :: # 0 : # 0 :: f0 | |
| 91 -- # 0 :: # 0 :: # 1 : # 0 :: f0 | |
| 92 -- # 0 :: # 1 :: # 0 : # 0 :: f0 | |
| 93 -- # 0 :: # 1 :: # 1 : # 0 :: f0 | |
| 94 -- # 0 :: # 2 :: # 0 : # 0 :: f0 | |
| 95 -- ... | |
| 96 -- # 3 :: # 2 :: # 0 : # 0 :: f0 | |
| 97 -- # 3 :: # 2 :: # 1 : # 0 :: f0 | |
| 248 | 98 |
| 249 | 99 -- all FL |
| 100 record AnyFL (n : ℕ) : Set where | |
| 242 | 101 field |
| 249 | 102 allFL : FList n |
| 103 anyP : (x : FL n) → Any (x ≡_ ) allFL | |
| 242 | 104 |
| 251 | 105 open AnyFL |
| 106 | |
| 249 | 107 -- all FL as all combination |
| 108 -- anyComm ( #0 :: FL0 ... # n :: FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n) | |
| 242 | 109 |
| 110 anyFL01 : (n : ℕ) → AnyFL (suc n) | |
| 249 | 111 anyFL01 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl } where |
| 112 anyFL2 : (x : FL 1) → (y : FList 1) → y ≡ ((zero :: f0) ∷# []) → Any (_≡_ x) y | |
| 113 anyFL2 (zero :: f0) .(cons (zero :: f0) [] (Level.lift tt)) refl = here refl | |
| 244 | 114 anyFL01 (suc n) = record { allFL = commList anyC ; anyP = anyFL02 } where |
| 249 | 115 anyFL05 : {n i : ℕ} → (i < suc n) → FList (suc n) |
| 116 anyFL05 {_} {0} (s≤s z≤n) = zero :: FL0 ∷# [] | |
| 117 anyFL05 {n} {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {n} {i} (<-trans i<n a<sa)) | |
| 118 anyFL08 : {n i : ℕ} {x : Fin (suc n)} {i<n : suc i < suc n} → toℕ x ≡ suc i → x ≡ suc (fromℕ< (≤-pred i<n)) | |
| 119 anyFL08 {n} {i} {x} {i<n} eq = toℕ-injective ( begin | |
| 247 | 120 toℕ x ≡⟨ eq ⟩ |
| 121 suc i ≡⟨ cong suc (≡-sym (toℕ-fromℕ< _ )) ⟩ | |
| 122 suc (toℕ (fromℕ< (≤-pred i<n)) ) | |
| 123 ∎ ) where open ≡-Reasoning | |
| 249 | 124 anyFL06 : {n i : ℕ} → (i<n : i < suc n) → (x : Fin (suc n)) → toℕ x < suc i → Any (_≡_ (x :: FL0)) (anyFL05 i<n) |
| 125 anyFL06 (s≤s z≤n) zero (s≤s lt) = here refl | |
| 126 anyFL06 {n} {suc i} (s≤s (s≤s i<n)) x (s≤s lt) with <-cmp (toℕ x) (suc i) | |
| 127 ... | tri< a ¬b ¬c = insAny _ (anyFL06 (<-trans (s≤s i<n) a<sa) x a) | |
| 128 ... | tri≈ ¬a b ¬c = subst (λ k → Any (_≡_ (x :: FL0)) (FLinsert (k :: FL0) (anyFL05 {n} {i} (<-trans (s≤s i<n) a<sa)))) | |
| 129 (anyFL08 {n} {i} {x} {s≤s (s≤s i<n)} b) (x∈FLins (x :: FL0) (anyFL05 {n} {i} (<-trans (s≤s i<n) a<sa))) | |
| 130 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (s≤s lt) ) | |
| 131 anyC = anyComm (anyFL05 a<sa) (allFL (anyFL01 n)) (λ p q → FLpos p :: q ) | |
| 244 | 132 anyFL02 : (x : FL (suc (suc n))) → Any (_≡_ x) (commList anyC) |
| 133 anyFL02 (x :: y) = commAny anyC (x :: FL0) y | |
| 249 | 134 (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyFL06 a<sa (fromℕ< x≤n) fin<n) ) (anyP (anyFL01 n) y) where |
| 244 | 135 x≤n : suc (toℕ x) ≤ suc (suc n) |
| 136 x≤n = toℕ<n x | |
| 242 | 137 |
| 248 | 138 anyFL : (n : ℕ) → AnyFL n |
| 139 anyFL zero = record { allFL = f0 ∷# [] ; anyP = anyFL4 } where | |
| 140 anyFL4 : (x : FL zero) → Any (_≡_ x) ( f0 ∷# [] ) | |
| 141 anyFL4 f0 = here refl | |
| 142 anyFL (suc n) = anyFL01 n | |
| 143 | |
| 144 at1 = proj₁ (toList (allFL (anyFL 1))) | |
| 145 at2 = proj₁ (toList (allFL (anyFL 2))) | |
| 146 at3 = proj₁ (toList (allFL (anyFL 3))) | |
| 147 at4 = proj₁ (toList (allFL (anyFL 4))) | |
| 148 | |
| 240 | 149 CommFListN : ℕ → FList n |
| 150 CommFListN zero = allFL (anyFL n) | |
| 151 CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q → perm→FL [ FL→perm p , FL→perm q ] )) | |
|
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
|
152 |
| 240 | 153 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i) |
| 154 CommStage→ zero x (Level.lift tt) = anyP (anyFL n) (perm→FL x) | |
| 155 CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 where | |
| 156 G = perm→FL g | |
| 157 H = perm→FL h | |
| 158 comm3 : perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ] | |
| 159 comm3 = begin | |
| 160 perm→FL [ FL→perm G , FL→perm H ] | |
| 161 ≡⟨ pcong-pF (comm-resp (FL←iso _) (FL←iso _)) ⟩ | |
| 162 perm→FL [ g , h ] | |
| 163 ∎ where open ≡-Reasoning | |
| 164 comm2 : Any (_≡_ (perm→FL [ g , h ])) (CommFListN (suc i)) | |
| 165 comm2 = subst (λ k → Any (_≡_ k) (CommFListN (suc i)) ) comm3 | |
| 166 ( commAny ( anyComm (CommFListN i) (CommFListN i) (λ p q → perm→FL [ FL→perm p , FL→perm q ] )) G H (CommStage→ i g p) (CommStage→ i h q) ) | |
| 167 CommStage→ (suc i) x (ccong {f} {x} eq p) = | |
| 168 subst (λ k → Any (k ≡_) (commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q → perm→FL [ FL→perm p , FL→perm q ] )))) | |
| 169 (comm4 eq) (CommStage→ (suc i) f p ) where | |
| 186 | 170 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
|
171 comm4 = pcong-pF |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
172 |
| 184 | 173 CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid |
| 174 CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0 |