Mercurial > hg > Members > kono > Proof > galois

comparison FLComm.agda @ 213:f0ceffb6a7e9

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 Sun, 06 Dec 2020 00:08:47 +0900
parents fa1e0944d1a0
children b438377a7e11
comparison
equal deleted inserted replaced
212:fa1e0944d1a0 213:f0ceffb6a7e9
109 open AnyComm 109 open AnyComm
110 anyComm : (P Q : FList n) → AnyComm P Q 110 anyComm : (P Q : FList n) → AnyComm P Q
111 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () } 111 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () }
112 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () } 112 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
113 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () } 113 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
114 anyComm (cons p P pr) Q = anyc0n Q where 114 anyComm (cons p P pr) Q = anyc0n Q Q where
115 anyc00 : (Q : FList n) (q : FL n) → fresh (FL n) ⌊ _f<?_ ⌋ q Q → fresh (FL n) ⌊ _f<?_ ⌋ (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) 115 anyc0n : (Q Q1 : FList n) → AnyComm (cons p P pr) Q1
116 anyc00 : (Q 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))
116 anyc00 = {!!} 117 anyc00 = {!!}
117 anyc01 : (Q : FList n) (q : FL n) → (qr : fresh (FL n) ⌊ _f<?_ ⌋ q Q ) → (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr) → 118 anyc01 : (Q 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) →
118 Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) (anyc00 Q q qr)) 119 Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1)) (anyc00 Q Q1 q qr))
119 anyc01 Q q qr p q (here refl) (here refl) = here refl 120 anyc01 Q Q1 q qr p q (here refl) (here refl) = here refl
120 anyc01 Q q qr p q₁ (here refl) (there anyq) = there (commAny (anyComm (cons p P pr) Q) p q₁ (here refl) anyq ) 121 anyc01 Q Q1 q qr p q₁ (here refl) (there anyq) = there (commAny (anyc0n Q Q1) p q₁ (here refl) anyq )
121 anyc01 Q q qr p₁ q (there anyp) (here refl) = anyc02 Q q qr (commAny (anyComm P (cons q Q qr)) p₁ q anyp (here refl)) where 122 anyc01 Q Q1 q qr p₁ q (there anyp) (here refl) with commAny (anyc0n Q []) p₁ q (there anyp) {!!} -- Any (_≡_ q) Q
122 anyc02 : (Q : FList n) (q : FL n) → (qr : fresh (FL n) ⌊ _f<?_ ⌋ q Q ) 123 ... | t = {!!}
123 → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (commList (anyComm P (cons q Q qr))) 124 where
124 → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) (anyc00 Q q qr)) 125 -- anyc02 Q p₁ q qr anyp where
125 anyc02 Q q qr t = {!!} 126 anyc02 : {P : FList n} {p₂ : FL n} {pr₂ : fresh (FL n) ⌊ _f<?_ ⌋ p₂ P}
126 anyc01 Q q qr p₁ q₁ (there anyp) (there anyq) = there (commAny (anyComm (cons p P pr) Q) p₁ q₁ (there anyp) anyq ) 127 → (Q1 : FList n) (p₁ q : FL n) → (qr : fresh (FL n) ⌊ _f<?_ ⌋ q Q1 ) → Any (_≡_ p₁) (cons p₂ P pr₂)
127 anyc0n : (Q : FList n) → AnyComm (cons p P pr) Q 128 → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q ]) (cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q1)) (anyc00 Q Q1 q qr))
128 anyc0n [] = record { commList = [] ; commAny = λ _ _ _ () } 129 anyc02 {P} Q p₁ q qr (here refl) = {!!}
129 anyc0n (cons q Q qr ) = record { commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm (cons p P pr) Q)) (anyc00 Q q qr) 130 anyc02 {P} Q p₁ q qr (there any) = {!!}
130 ; commAny = anyc01 Q q qr } 131 anyc01 Q Q1 q qr p₁ q₁ (there anyp) (there anyq) = there (commAny (anyc0n Q Q1) p₁ q₁ (there anyp) anyq )
132 anyc0n Q1 [] = record { commList = (commList (anyComm P Q)) ; commAny = λ _ _ _ () }
133 anyc0n Q1 (cons q Q2 qr ) = record { commList = cons (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyc0n Q Q2)) (anyc00 Q Q2 q qr)
134 ; commAny = anyc01 Q Q2 q qr }
131 135
132 -- {-# TERMINATING #-} 136 -- {-# TERMINATING #-}
133 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i ) 137 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
134 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x) 138 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x)
135 CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where 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