# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607642293 -32400
# Node ID 3b7be8bfc72e184bb4a91867a9e679645dc06f97
# Parent  38e56ea7d09f9b19be79545f4e972778ffea743b
clean up

diff -r 38e56ea7d09f -r 3b7be8bfc72e FLComm.agda
--- a/FLComm.agda	Fri Dec 11 07:46:05 2020 +0900
+++ b/FLComm.agda	Fri Dec 11 08:18:13 2020 +0900
@@ -36,29 +36,10 @@
 -- open import Relation.Nary using (⌊_⌋)
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
 
--------------
---    # 0 :: # 0 :: # 0 : # 0 :: f0
---    # 0 :: # 0 :: # 1 : # 0 :: f0
---    # 0 :: # 1 :: # 0 : # 0 :: f0
---    # 0 :: # 1 :: # 1 : # 0 :: f0
---    # 0 :: # 2 :: # 0 : # 0 :: f0
---       ...
---    # 3 :: # 2 :: # 0 : # 0 :: f0
---    # 3 :: # 2 :: # 1 : # 0 :: f0
-
--- all FL
-record AnyFL (n : ℕ) : Set where
-   field
-     allFL : FList n
-     anyP : (x : FL n) → Any (x ≡_ ) allFL 
-
 open import fin
 open AnyFL
 
-anyFL2 : (x : FL 1) → (y : FList 1) → y ≡ ((zero :: f0) ∷# []) → Any (_≡_ x) y
-anyFL2 (zero :: f0) .(cons (zero :: f0) [] (Level.lift tt)) refl = here refl
-
--- all cobmbination in P and Q
+-- all cobmbination in P and Q (could be more general)
 record AnyComm {n m l : ℕ}  (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where
    field
      commList : FList l
@@ -72,17 +53,6 @@
 --     :        AnyComm FL0 FL0 P  Q
 --    p0,q       
 
-p<anyL : {n : ℕ } {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → p f≤ p₁
-p<anyL {n} {p} {p₁} {P} {pr} (here refl) = case1 refl
-p<anyL {n} {p} {p₁} {cons a P x} { Data.Product._,_ (Level.lift p<a) snd} (there any) with p<anyL any
-... | case1 refl = case2 (toWitness p<a)
-... | case2 a<p₁ = case2 (f<-trans (toWitness p<a) a<p₁)
-
-p<anyL1 : {n : ℕ } {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → ¬ (p ≡ p₁)  → p f< p₁
-p<anyL1 {n} {p} {p₁} {P} {pr} any neq with p<anyL any
-... | case1 eq = ⊥-elim ( neq eq )
-... | case2 x = x
-
 open AnyComm 
 anyComm : {n m l : ℕ } → (P : FList n) (Q : FList m) → (fpq : (p : FL n) (q : FL m) → FL l)  → AnyComm P Q fpq
 anyComm [] [] _ = record { commList = [] ; commAny = λ _ _ () }
@@ -117,40 +87,50 @@
      anyc04 [] = anyc05 P 
      anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1)
 
---   anyComm ( #0 :: FL0 ... # n :: FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n)
+-------------
+--    # 0 :: # 0 :: # 0 : # 0 :: f0
+--    # 0 :: # 0 :: # 1 : # 0 :: f0
+--    # 0 :: # 1 :: # 0 : # 0 :: f0
+--    # 0 :: # 1 :: # 1 : # 0 :: f0
+--    # 0 :: # 2 :: # 0 : # 0 :: f0
+--       ...
+--    # 3 :: # 2 :: # 0 : # 0 :: f0
+--    # 3 :: # 2 :: # 1 : # 0 :: f0
 
-record AnyFin (n : ℕ)  : Set where
+-- all FL
+record AnyFL (n : ℕ) : Set where
    field
-     allFin : FList (suc n)
-     anyF : (x : Fin (suc n)) → Any (x :: FL0 ≡_ ) allFin 
+     allFL : FList n
+     anyP : (x : FL n) → Any (x ≡_ ) allFL 
 
-open AnyFin
+--   all FL as all combination  
+--      anyComm ( #0 :: FL0 ... # n :: FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n)
 
 anyFL01 :  (n : ℕ) → AnyFL (suc n) 
-anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl } 
+anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl }  where
+     anyFL2 : (x : FL 1) → (y : FList 1) → y ≡ ((zero :: f0) ∷# []) → Any (_≡_ x) y
+     anyFL2 (zero :: f0) .(cons (zero :: f0) [] (Level.lift tt)) refl = here refl
 anyFL01 (suc n) = record { allFL = commList anyC ;  anyP =  anyFL02 } where
-     anyFL04 :  (n : ℕ) → AnyFin n
-     anyFL04 n = record { allFin = anyFL05 a<sa ; anyF = λ x → anyFL06 a<sa x fin<n } where 
-         anyFL05 : {i : ℕ} → (i < suc n) → FList (suc n)
-         anyFL05 {0} (s≤s z≤n) = zero :: FL0 ∷# []
-         anyFL05 {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {i} (<-trans i<n a<sa))
-         anyFL08 : {n i : ℕ} {x : Fin (suc n)} {i<n : suc i < suc n}  → toℕ x ≡ suc i → x ≡ suc (fromℕ< (≤-pred i<n))
-         anyFL08 {n} {i} {x} {i<n} eq = toℕ-injective ( begin
+     anyFL05 : {n i : ℕ} → (i < suc n) → FList (suc n)
+     anyFL05 {_} {0} (s≤s z≤n) = zero :: FL0 ∷# []
+     anyFL05 {n} {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {n} {i} (<-trans i<n a<sa))
+     anyFL08 : {n i : ℕ} {x : Fin (suc n)} {i<n : suc i < suc n}  → toℕ x ≡ suc i → x ≡ suc (fromℕ< (≤-pred i<n))
+     anyFL08 {n} {i} {x} {i<n} eq = toℕ-injective ( begin
                 toℕ x                               ≡⟨ eq ⟩
                 suc i                               ≡⟨ cong suc (≡-sym (toℕ-fromℕ< _ )) ⟩
                 suc (toℕ (fromℕ< (≤-pred i<n)) )
           ∎ ) where open ≡-Reasoning
-         anyFL06 : {i : ℕ} → (i<n : i < suc n) → (x : Fin (suc n)) → toℕ x < suc i → Any (_≡_ (x :: FL0)) (anyFL05 i<n)
-         anyFL06 (s≤s z≤n) zero (s≤s lt) = here refl
-         anyFL06 {suc i} (s≤s (s≤s i<n)) x (s≤s lt) with <-cmp (toℕ x) (suc i)
-         ... | tri< a ¬b ¬c = insAny _ (anyFL06 (<-trans (s≤s i<n) a<sa) x a) 
-         ... | tri≈ ¬a b ¬c = subst (λ k →  Any (_≡_ (x :: FL0)) (FLinsert (k :: FL0) (anyFL05 {i} (<-trans (s≤s i<n) a<sa))))
-                  (anyFL08 {n} {i} {x} {s≤s (s≤s i<n)} b) (x∈FLins (x :: FL0)  (anyFL05 {i} (<-trans (s≤s i<n) a<sa)))
-         ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (s≤s lt) )
-     anyC = anyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q )
+     anyFL06 : {n i : ℕ} → (i<n : i < suc n) → (x : Fin (suc n)) → toℕ x < suc i → Any (_≡_ (x :: FL0)) (anyFL05 i<n)
+     anyFL06 (s≤s z≤n) zero (s≤s lt) = here refl
+     anyFL06 {n} {suc i} (s≤s (s≤s i<n)) x (s≤s lt) with <-cmp (toℕ x) (suc i)
+     ... | tri< a ¬b ¬c = insAny _ (anyFL06 (<-trans (s≤s i<n) a<sa) x a) 
+     ... | tri≈ ¬a b ¬c = subst (λ k →  Any (_≡_ (x :: FL0)) (FLinsert (k :: FL0) (anyFL05 {n} {i} (<-trans (s≤s i<n) a<sa))))
+                  (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)))
+     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (s≤s lt) )
+     anyC = anyComm (anyFL05 a<sa) (allFL (anyFL01 n)) (λ p q → FLpos p :: q )
      anyFL02 : (x : FL (suc (suc n))) → Any (_≡_ x) (commList anyC)
      anyFL02 (x :: y) = commAny anyC (x :: FL0) y
-                       (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyF (anyFL04 (suc n)) (fromℕ< x≤n) )) (anyP (anyFL01 n) y) where
+                       (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyFL06 a<sa (fromℕ< x≤n) fin<n) ) (anyP (anyFL01 n) y) where
          x≤n : suc (toℕ x)  ≤ suc (suc n)
          x≤n = toℕ<n x