# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574588625 -32400
# Node ID 7c8460329f271d9ee3dd1ffc91c6448cb794f2fe
# Parent  2d70f90565c63111877ecee1be4eab642f8cd168
fin-< using data done

diff -r 2d70f90565c6 -r 7c8460329f27 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sun Nov 24 15:40:37 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 24 18:43:45 2019 +0900
@@ -388,13 +388,33 @@
 data f-1 { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
   elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → f-1 n<m fa
 
--- f-1-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
---    → ( elm s ≡ elm t) → ( elm<n s ≅ elm<n t ) → elm1 e0 e0<n ≡ elm1 e1 e1<n
--- f-1-<-cong n<m fa _ _ refl HE.refl = refl
+get-elm : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → f-1 n<m fa → A
+get-elm (elm1 a _ ) = a
+
+get-< : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → (f : f-1 n<m fa ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
+get-< (elm1 _ b ) = b
+
+f-1-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
+   → (x y : f-1 n<m fa ) → get-elm {n} {m} {n<m} {A} {fa} x ≡ get-elm {n} {m} {n<m} {A} {fa} y → get-< x ≅  get-< y → x ≡ y
+f-1-cong n<m fa (elm1 elm x) (elm1 elm x) refl HE.refl = refl
 
-fin-<' : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (f-1 n<m fa) {n}
-fin-<' {A} {n} {m} n<m fa  = iso-fin (Fin2Finite n) iso where
+fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (f-1 n<m fa) {n}
+fin-< {A} {n} {m} n<m fa  = iso-fin (Fin2Finite n) iso where
     iso : ISO (Fin n) (f-1 n<m fa)
+    lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+    lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+    lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
+    lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ≤ i<n ≡ fromℕ≤ j<n
+    lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ≤ k ) (lemma8 refl  ))
+    lemma3 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → Data.Nat.Properties.<-trans a<b b<c ≡ a<c
+    lemma3 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
+    lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m)) ≡ toℕ x
+    lemma11 {n} {m} {x} n<m  = begin
+              toℕ (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m))
+           ≡⟨ toℕ-fromℕ≤ _ ⟩
+              toℕ x
+           ∎  where
+               open ≡-Reasoning
     ISO.A←B iso (elm1 elm x) = fromℕ≤ x
     ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m ))) to<n where
         x<n : toℕ x < n
@@ -405,101 +425,44 @@
         lemma2 : fromℕ≤ (subst (λ k → toℕ k < n) (sym
           (FiniteSet.finiso← fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
           (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
-        lemma2 = {!!}
-    ISO.iso→ iso (elm1 elm x) = lemma1 where
+        lemma2 = begin
+             fromℕ≤ (subst (λ k → toℕ k < n) (sym
+               (FiniteSet.finiso← fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
+                    (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m))) (toℕ<n x))) 
+           ≡⟨⟩
+              fromℕ≤ ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 )
+           ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩
+              fromℕ≤ lemma6
+           ≡⟨ lemma10 (lemma11 n<m ) ⟩
+              fromℕ≤ ( toℕ<n x )
+           ≡⟨ fromℕ≤-toℕ _ _ ⟩
+              x 
+           ∎  where
+               open ≡-Reasoning
+               lemma6 : toℕ (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m)) < n
+               lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m))) (toℕ<n x )
+    ISO.iso→ iso (elm1 elm x) = f-1-cong n<m fa _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where
+        lemma13 : toℕ (fromℕ≤ x) ≡ toℕ (FiniteSet.F←Q fa elm)
+        lemma13 = begin
+              toℕ (fromℕ≤ x)
+           ≡⟨ toℕ-fromℕ≤ _ ⟩
+              toℕ (FiniteSet.F←Q fa elm)
+           ∎  where open ≡-Reasoning
         lemma : FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm 
-        lemma = {!!}
-        lemma1 : ISO.B←A iso (ISO.A←B iso (elm1 elm x)) ≡ elm1 elm x
-        lemma1 with lemma
-        ... | eq = {!!}
-
-
-record Fin-< { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) : Set where
-  field 
-    elm : A
-    elm<n : toℕ (FiniteSet.F←Q fa elm ) < n
-
-open Fin-<
-
-Fin-<-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
-   → ( s t : Fin-< n<m fa ) 
-   → ( elm s ≡ elm t) → ( elm<n s ≅ elm<n t ) → s ≡ t
-Fin-<-cong n<m fa _ _ refl HE.refl = refl
-
-lemma1 : {m n : ℕ } → ( i j : m < n ) → i ≡ j
-lemma1 {zero} {suc n} (s≤s z≤n) (s≤s z≤n) = refl
-lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j )
+        lemma = begin
+             FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m))
+           ≡⟨⟩
+             FiniteSet.Q←F fa (fromℕ≤ ( Data.Nat.Properties.<-trans (toℕ<n ( fromℕ≤ x ) ) n<m))
+           ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩
+              FiniteSet.Q←F fa (fromℕ≤ ( Data.Nat.Properties.<-trans x n<m))
+           ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ≤ k ))  lemma3 ⟩
+             FiniteSet.Q←F fa (fromℕ≤ ( toℕ<n (FiniteSet.F←Q fa elm)))
+           ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ≤-toℕ _ _ ) ⟩
+             FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
+           ≡⟨ FiniteSet.finiso→ fa _ ⟩
+              elm 
+           ∎  where open ≡-Reasoning
 
-fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (Fin-< n<m fa) {n}
-fin-< {A} {zero} {m} (s≤s z≤n) fa  = record { Q←F = λ () ; F←Q = λ () ; finiso← = λ () ; finiso→ = λ ()  }
-fin-< {A} {suc n} {m} (s≤s n<m) fa = iso-fin (fin-∨1 (fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa)) iso where
-   fin- : FiniteSet (Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa)
-   fin- = fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa
-   iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa)
-   lastf = FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ))
-   c1 : toℕ lastf ≡ n 
-   c1 = subst (λ k → toℕ k ≡ n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k ≡ n) (sym (toℕ-fromℕ≤ _ )) refl )
-   f<n : toℕ lastf < suc n
-   f<n = subst ( λ k → k < suc n ) (sym c1) a<sa
-   last1 = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
-   ISO.A←B iso x with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
-   ISO.A←B iso x | tri< a ¬b ¬c = case2 record { elm = elm x ; elm<n = a }
-   ISO.A←B iso x | tri≈ ¬a b ¬c = case1 one
-   ISO.A←B iso x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
-   ISO.B←A iso (case1 one)  = record { elm = last1 ; elm<n = f<n }
-   ISO.B←A iso (case2 x)  = record { elm = elm x ; elm<n = Data.Nat.Properties.<-trans (elm<n x) a<sa }
-   ISO.iso← iso (case1 one) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm (ISO.B←A iso (case1 one))))) n
-   ISO.iso← iso (case1 one) | tri< a ¬b ¬c = ⊥-elim ( ¬b c1 )
-   ISO.iso← iso (case1 one) | tri≈ ¬a b ¬c = refl
-   ISO.iso← iso (case1 one) | tri> ¬a ¬b c = ⊥-elim ( ¬b c1 )
-   ISO.iso← iso (case2 x) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x))) n
-   ISO.iso← iso (case2 x) | tri< a ¬b ¬c = cong ( λ k → case2 record { elm = elm x ; elm<n = k } ) (lemma1 _ _) where
-   ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) )
-   ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) )
-   ISO.iso→ iso x with ISO.A←B iso x  
-   ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n 
-   ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c (elm<n x) )
-   ... | tri< a ¬b ¬c =  {!!}
-   ... | tri≈ ¬a b ¬c =  begin
-           record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) ; elm<n = lemma5 }
-       ≡⟨ Fin-<-cong (s≤s n<m) fa _ _ (sym (lemma2 b)) lemma7 ⟩
-           record { elm = elm x ; elm<n = elm<n x }
-       ≡⟨⟩
-           x
-       ∎
-    where
-      open ≡-Reasoning
-      lemma3 : {n m : ℕ } (x : Fin m)  → toℕ x ≡ n → (n<m : n < m ) → x ≡ fromℕ≤ n<m
-      lemma3 _ refl n<m = sym ( fromℕ≤-toℕ  _ n<m )
-      lemma4 : {x : A } → (x=n : toℕ (FiniteSet.F←Q fa x)  ≡ n ) → fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ≡ FiniteSet.F←Q fa x
-      lemma4 {x} refl = sym ( lemma3 _ refl (Data.Nat.Properties.<-trans n<m a<sa)) 
-      lemma2 : {x : A} → toℕ (FiniteSet.F←Q fa x) ≡ n → x ≡ FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
-      lemma2 {x} refl = sym ( begin
-                 FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) 
-              ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma4 refl) ⟩
-                 FiniteSet.Q←F fa ( FiniteSet.F←Q fa x )
-              ≡⟨ FiniteSet.finiso→ fa _ ⟩
-                 x 
-              ∎ ) where open ≡-Reasoning
-      lemma5 : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) < suc n
-      lemma5 = subst (λ k → suc k ≤ suc n)
-            (sym
-             (subst (λ k → toℕ k ≡ n)
-              (sym
-               (FiniteSet.finiso← fa
-                (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))))
-              (subst (λ k → k ≡ n)
-               (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))) refl)))
-                    a<sa
-      lemma7 : lemma5 ≅ elm<n x
-      lemma7 with lemma2 b
-      ... | refl with lemma1 lemma5 (elm<n x)
-      ... | refl = HE.refl
-
-   ISO.iso→ iso x | case2 x1 = {!!}
-   -- ISO.iso→ iso x | case2 x1 | tri< a ¬b ¬c = ?
-   -- ISO.iso→ iso x | case2 x1 | tri≈ ¬a b ¬c = {!!}
-   -- ISO.iso→ iso x | case2 x1 | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
 
 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
 fin-× {A} {B} {a} {b} fa fb with FiniteSet→Fin fa