Mercurial > hg > Members > kono > Proof > galois
changeset 225:08a99237e56e
restart anyComm
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 08 Dec 2020 09:29:37 +0900 |
| parents | 71e08656273b |
| children | adcbf19410fe |
| files | FLComm.agda |
| diffstat | 1 files changed, 24 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/FLComm.agda Mon Dec 07 22:30:29 2020 +0900 +++ b/FLComm.agda Tue Dec 08 09:29:37 2020 +0900 @@ -109,32 +109,35 @@ → p0 f≤ p → q0 f≤ q → Any (perm→FL [ FL→perm p , FL→perm q ] ≡_) commList +------------- +-- (p,q) (p,qn) .... (p,q0) +-- pn,q +-- : AnyComm FL0 FL0 P Q +-- p0,q + open AnyComm -- q₂ anyComm : (P Q : FList n) → AnyComm FL0 FL0 P Q anyComm [] [] = record { commList = [] ; commAny = λ _ _ () } anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () } anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () } -anyComm (cons p P pr) (cons q Q qr) = anyc0n (cons q Q qr) where - anyc0n : (Q1 : FList n) → AnyComm {!!} {!!} (cons p P pr) (cons q Q qr) - anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = anyc03 } where - anyc03 : (p₁ q₁ : FL n) → - Any ( p₁ ≡_) (cons p P pr) → Any (q₁ ≡_) (cons q Q qr) - → {!!} → {!!} - → 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)))) - anyc03 p₁ q₁ (there anyp) (here x) _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (here x) {!!} {!!} ) - anyc03 p₁ q₁ (there anyp) (there anyq) _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (there anyq) {!!} {!!} ) - anyc03 p₁ q₁ (here refl) (there anyq) _ _ = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ {!!} (there anyq) {!!} {!!} ) - anyc03 p₁ q₁ (here refl) (here x) _ _ = {!!} - anyc0n (cons q₂ Q1 qr₂ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) - ; commAny = anyc01 Q1 q₂ qr₂ } where - 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) - → {!!} → {!!} - → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) ) - anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (there anyq) _ _ = insAny _ (commAny (anyc0n Q1) p₁ q₁ (here refl) (there anyq) {!!} {!!} ) - anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (here refl) _ _ = insAny _ (commAny (anyc0n Q1) p₁ q₁ (there anyp) (here refl) {!!} {!!} ) - anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (there anyq) _ _ = insAny _ (commAny (anyc0n Q1) p₁ q₁ (there anyp) (there anyq) {!!} {!!} ) - anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (here refl) _ _ with x∈FLins (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) - ... | t = {!!} -- t : p₁ q₂ → p₁ q₁ +anyComm (cons p P pr) (cons q Q qr) = record { commList = FLinsert (fpq p q) (commListQ Q) ; commAny = anyc0n } where + fpq : (p q : FL n) → FL n + fpq p q = perm→FL [ FL→perm p , FL→perm q ] + commListP : (P1 : FList n) → FList n + commListP [] = commList (anyComm P Q) + commListP (cons p₁ P1 x) = FLinsert (fpq p₁ q) (commListP P1) + commListQ : (Q1 : FList n) → FList n + commListQ [] = commListP P + commListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (commListQ Q1) + anyc0n : (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr) → + FL0 f≤ p₁ → FL0 f≤ q₁ → Any (_≡_ (perm→FL [ FL→perm p₁ , FL→perm q₁ ])) (FLinsert (fpq p q) (commListQ Q)) + anyc0n p₁ q₁ anyp anyq _ _ with FLcmp q q₁ | FLcmp p p₁ + ... | tri< a ¬b ¬c | _ = {!!} -- can't happen + ... | _ | tri< a ¬b ¬c₁ = {!!} -- can't happen + ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = x∈FLins (fpq p q) (commListQ Q) -- p,q case + ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!} -- p,qi case + ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = {!!} --- pi,q case + ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!} -- previous case -- {-# TERMINATING #-} CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )