Mercurial > hg > Members > kono > Proof > galois

annotate FLComm.agda @ 188:9e0d946d35b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 28 Nov 2020 21:50:16 +0900
parents c22ef5bc695a
children d0b678eec506
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
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
186
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
32 open Solvable (Symmetric n)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
33
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
34 tl3 : (FL n) → ( z : FList n) → FList n → FList n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
35 tl3 h [] w = w
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
36 tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
37 tl2 : ( x z : FList n) → FList n → FList n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
38 tl2 [] _ x = x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
39 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
40
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 CommFList : FList n → FList n
186
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
42 CommFList x = tl2 x x []
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 CommFListN : ℕ → FList n
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 CommFListN 0 = ∀Flist fmax
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 CommFListN (suc i) = CommFList (CommFListN i)
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 open import Algebra
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 open Group (Symmetric n)
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 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
52 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x)
188
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
53 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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
54 G = perm→FL g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
55 H = perm→FL h
188
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
56 comm3 : (L L1 : FList n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ G L ) → Any (H ≡_) L1 → (L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 (cons G L xr) L1 L3)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
57 comm3 [] L1 _ b L3 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
58 comm3 (cons a L x) L1 _ b L3 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
59 comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ] ≡_) (tl2 L L1 L3)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
60 comm2 (cons G L xr) L1 (here refl) b L3 = comm3 L L1 xr b L3
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
61 comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b {!!}
186
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
62 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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
63 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
64 comm4 = pcong-pF
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
66 CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
67 CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0