Mercurial > hg > Members > kono > Proof > galois

comparison FLComm.agda @ 224:71e08656273b

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 Mon, 07 Dec 2020 22:30:29 +0900
parents 9da456c2bfe3
children 08a99237e56e
comparison
equal deleted inserted replaced
223:9da456c2bfe3 224:71e08656273b
99 CommFListN : ℕ → FList n 99 CommFListN : ℕ → FList n
100 CommFListN 0 = ∀Flist fmax 100 CommFListN 0 = ∀Flist fmax
101 CommFListN (suc i) = CommFList (CommFListN i) 101 CommFListN (suc i) = CommFList (CommFListN i)
102 102
103 -- all comm cobmbination in P and Q 103 -- all comm cobmbination in P and Q
104 record AnyComm (P Q : FList n) : Set where 104 record AnyComm (p0 q0 : FL n) (P Q : FList n) : Set where
105 field 105 field
106 commList : FList n 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 107 commAny : (p q : FL n)
108 → Any ( p ≡_ ) P → Any ( q ≡_ ) Q
109 → p0 f≤ p → q0 f≤ q
110 → Any (perm→FL [ FL→perm p , FL→perm q ] ≡_) commList
108 111
109 open AnyComm -- q₂ 112 open AnyComm -- q₂
110 anyComm : (P Q : FList n) → AnyComm P Q 113 anyComm : (P Q : FList n) → AnyComm FL0 FL0 P Q
111 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () } 114 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () }
112 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () } 115 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
113 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () } 116 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
114 anyComm (cons p P pr) (cons q Q qr) = anyc0n (cons q Q qr) where 117 anyComm (cons p P pr) (cons q Q qr) = anyc0n (cons q Q qr) where
115 anyc0n : (Q1 : FList n) → AnyComm (cons p P pr) (cons q Q qr) 118 anyc0n : (Q1 : FList n) → AnyComm {!!} {!!} (cons p P pr) (cons q Q qr)
116 anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = anyc03 } where 119 anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = anyc03 } where
117 anyc03 : (p₁ q₁ : FL n) → 120 anyc03 : (p₁ q₁ : FL n) →
118 Any ( p₁ ≡_) (cons p P pr) → Any (q₁ ≡_) (cons q Q qr) 121 Any ( p₁ ≡_) (cons p P pr) → Any (q₁ ≡_) (cons q Q qr)
122 → {!!} → {!!}
119 → Any ((perm→FL [ FL→perm p₁ , FL→perm q₁ ]) ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr)))) 123 → Any ((perm→FL [ FL→perm p₁ , FL→perm q₁ ]) ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))))
120 anyc03 p₁ q₁ (there anyp) (here x) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (here x)) 124 anyc03 p₁ q₁ (there anyp) (here x) _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (here x) {!!} {!!} )
121 anyc03 p₁ q₁ (there anyp) (there anyq) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (there anyq)) 125 anyc03 p₁ q₁ (there anyp) (there anyq) _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (there anyq) {!!} {!!} )
122 anyc03 p₁ q₁ (here refl) (there anyq) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ (here refl) (there anyq)) 126 anyc03 p₁ q₁ (here refl) (there anyq) _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ {!!} (there anyq) {!!} {!!} )
123 anyc03 p₁ q₁ (here refl) (here x) = {!!} 127 anyc03 p₁ q₁ (here refl) (here x) _ _ = {!!}
124 anyc0n (cons q₂ Q1 qr₂ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) 128 anyc0n (cons q₂ Q1 qr₂ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1))
125 ; commAny = anyc01 Q1 q₂ qr₂ } where 129 ; commAny = anyc01 Q1 q₂ qr₂ } where
126 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 Q qr) → 130 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 Q qr)
127 Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) ) 131 → {!!} → {!!}
128 anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (there anyq) = insAny _ (commAny (anyc0n Q1) p₁ q₁ (here refl) (there anyq)) 132 → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) )
129 anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (here refl) = insAny _ (commAny (anyc0n Q1) p₁ q₁ (there anyp) (here refl)) 133 anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (there anyq) _ _ = insAny _ (commAny (anyc0n Q1) p₁ q₁ (here refl) (there anyq) {!!} {!!} )
130 anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (there anyq) = insAny _ (commAny (anyc0n Q1) p₁ q₁ (there anyp) (there anyq) ) 134 anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (here refl) _ _ = insAny _ (commAny (anyc0n Q1) p₁ q₁ (there anyp) (here refl) {!!} {!!} )
131 anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (here refl) with x∈FLins (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) 135 anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (there anyq) _ _ = insAny _ (commAny (anyc0n Q1) p₁ q₁ (there anyp) (there anyq) {!!} {!!} )
136 anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (here refl) _ _ with x∈FLins (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1))
132 ... | t = {!!} -- t : p₁ q₂ → p₁ q₁ 137 ... | t = {!!} -- t : p₁ q₂ → p₁ q₁
133 138
134 -- {-# TERMINATING #-} 139 -- {-# TERMINATING #-}
135 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i ) 140 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
136 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x) 141 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x)