Mercurial > hg > Members > kono > Proof > automaton

changeset 137:08e2af685c69

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Nov 2019 19:13:44 +0900
parents 7c8460329f27
children 7a0634a7c25a
files agda/finiteSet.agda
diffstat 1 files changed, 88 insertions(+), 65 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Sun Nov 24 18:43:45 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 24 19:13:44 2019 +0900
@@ -10,7 +10,7 @@
 open import Relation.Binary.PropositionalEquality
 open import logic
 open import nat
-open import Data.Nat.Properties  hiding ( _≟_ )
+open import Data.Nat.Properties as NatP  hiding ( _≟_ )
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
@@ -82,7 +82,7 @@
      next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
               → (m<n : m < n ) → p (Q←F (fromℕ≤ m<n )) ≡ false
               → End m p
-     next-end {m} p prev m<n np i m<i with Data.Nat.Properties.<-cmp m (toℕ i) 
+     next-end {m} p prev m<n np i m<i with NatP.<-cmp m (toℕ i) 
      next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a
      next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c )
      next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where
@@ -237,11 +237,58 @@
     ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x)
     ISO.iso→ iso2 (case2 x) = refl
 
-import Data.Nat.DivMod
-import Data.Nat.Properties
+open import Data.Product
+
+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
+... | a=f = iso-fin (fin-×-f a ) iso-1 where
+   iso-1 : ISO (Fin a × B) ( A × B )
+   ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x) 
+   ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x) 
+   ISO.iso← iso-1 x  =  lemma  where
+      lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
+      lemma = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso← fa _ )
+   ISO.iso→ iso-1 x = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso→ fa _ )
+   iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B)
+   ISO.A←B iso-2 (zero , b ) = case1 b
+   ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b )
+   ISO.B←A iso-2 (case1 b) = ( zero , b )
+   ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b )
+   ISO.iso← iso-2 (case1 x) = refl
+   ISO.iso← iso-2 (case2 x) = refl
+   ISO.iso→ iso-2 (zero , b ) = refl
+   ISO.iso→ iso-2 (suc a , b ) = refl
+   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) × B) {a * b}
+   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () }
+   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
 
 open _∧_
 
+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
+... | a=f = iso-fin (fin-×-f a ) iso-1 where
+   iso-1 : ISO (Fin a ∧ B) ( A ∧ B )
+   ISO.A←B iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x)  ; proj2 =  proj2 x} 
+   ISO.B←A iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x)  ; proj2 =  proj2 x}
+   ISO.iso← iso-1 x  =  lemma  where
+      lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 =  proj2 x} ≡ record {proj1 =  proj1 x ; proj2 =  proj2 x }
+      lemma = cong ( λ k → record {proj1 = k ;  proj2 = proj2 x } )  (FiniteSet.finiso← fa _ )
+   ISO.iso→ iso-1 x = cong ( λ k → record {proj1 =  k ; proj2 =  proj2 x } )  (FiniteSet.finiso→ fa _ )
+   iso-2 : {a : ℕ } → ISO (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B)
+   ISO.A←B iso-2 (record { proj1 = zero ; proj2 =  b }) = case1 b
+   ISO.A←B iso-2 (record { proj1 = suc fst ; proj2 =  b }) = case2 ( record { proj1 = fst ; proj2 =  b } )
+   ISO.B←A iso-2 (case1 b) = record {proj1 =  zero ; proj2 =  b }
+   ISO.B←A iso-2 (case2 (record { proj1 = a ; proj2 =  b })) = record { proj1 =  suc a ; proj2 =  b }
+   ISO.iso← iso-2 (case1 x) = refl
+   ISO.iso← iso-2 (case2 x) = refl
+   ISO.iso→ iso-2 (record { proj1 = zero ; proj2 =  b }) = refl
+   ISO.iso→ iso-2 (record { proj1 = suc a ; proj2 =  b }) = refl
+   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) ∧ B) {a * b}
+   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () }
+   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
+
+import Data.Nat.DivMod
+
 open import Data.Vec
 import Data.Product
 
@@ -296,17 +343,17 @@
 
 F2L : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} ) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
 F2L  {Q} {zero} fin _ Q→B = []
-F2L  {Q} {suc n}  (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) lemma6 ∷ F2L {Q} {n} (Data.Nat.Properties.<-trans n<m a<sa ) fin qb1 where
+F2L  {Q} {suc n}  (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) lemma6 ∷ F2L {Q} {n} (NatP.<-trans n<m a<sa ) fin qb1 where
    lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))) < suc n
    lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ≤ n<m ))  a<sa )
    qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
-   qb1 q q<n = Q→B q (Data.Nat.Properties.<-trans q<n a<sa)
+   qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa)
 
 List2Func : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → Vec Bool n →  Q → Bool 
 List2Func {Q} {zero} (s≤s z≤n) fin [] q = false
 List2Func {Q} {suc n} {m} (s≤s n<m) fin (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ≤ n<m
 ... | yes _ = h
-... | no _ = List2Func {Q} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa ) fin t q
+... | no _ = List2Func {Q} {n} {m} (NatP.<-trans n<m a<sa ) fin t q
 
 F2L-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (x : Vec Bool n ) → F2L a<sa fin (λ q _ → List2Func a<sa fin x q ) ≡ x
 F2L-iso {Q} {m} fin x = f2l m a<sa x where
@@ -319,21 +366,21 @@
        lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))  ≟ fromℕ≤ n<m
        lemma2 | yes p = refl
        lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
-       lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func (s≤s n<m) fin (h ∷ t) q ≡ List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q
+       lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func (s≤s n<m) fin (h ∷ t) q ≡ List2Func (NatP.<-trans n<m a<sa) fin t q
        lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m 
        lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ≤ n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where 
            lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
            lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s  z≤n
            lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
        lemma4 q _ | no ¬p = refl
-       lemma3 :  F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q  ) ≡ t
+       lemma3 :  F2L (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q  ) ≡ t
        lemma3 = begin 
-            F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q )
-          ≡⟨ cong (λ k → F2L (Data.Nat.Properties.<-trans n<m a<sa) fin ( λ q q<n → k q q<n ))
+            F2L (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q )
+          ≡⟨ cong (λ k → F2L (NatP.<-trans n<m a<sa) fin ( λ q q<n → k q q<n ))
                  (FiniteSet.f-extensionality fin ( λ q →  
                  (FiniteSet.f-extensionality fin ( λ q<n →  lemma4 q q<n )))) ⟩
-            F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q )
-          ≡⟨ f2l n (Data.Nat.Properties.<-trans n<m a<sa ) t ⟩
+            F2L (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (NatP.<-trans n<m a<sa) fin t q )
+          ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩
             t
           ∎  where
             open ≡-Reasoning
@@ -349,7 +396,7 @@
        lemma13 : {n nq : ℕ } → (n<m : n < m )  → ¬ ( nq ≡ n ) → nq  ≤ n → nq < n
        lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
        lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
-       lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (Data.Nat.Properties.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
+       lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
        lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ≤ (s≤s lt) ≡ suc (fromℕ≤ lt)
        lemma3 (s≤s lt) = refl
        lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ≤ n<m 
@@ -367,7 +414,7 @@
              f q 
           ∎  where
             open ≡-Reasoning
-    l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (Data.Nat.Properties.<-trans n<m a<sa) (lemma11 n<m ¬p n<q)
+    l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11 n<m ¬p n<q)
 
 fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
 fin→ {A} {a} fin = iso-fin fin2List iso where
@@ -380,55 +427,53 @@
        lemma = FiniteSet.f-extensionality fin ( λ q → L2F-iso fin x q )
     
 
-open import Data.Product
-
 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) {n}
 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
 
-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
+data fin-less { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
+  elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less n<m fa
 
-get-elm : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → f-1 n<m fa → A
+get-elm : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → fin-less 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-< : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → (f : fin-less 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-less-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
+   → (x y : fin-less 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
+fin-less-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 : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (fin-less 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)
+    iso : ISO (Fin n) (fin-less 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 : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-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 : Fin n } → (n<m : n < m ) → toℕ (fromℕ≤ (NatP.<-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ℕ≤ (NatP.<-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
+    ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ≤ (NatP.<-trans x<n n<m ))) to<n where
         x<n : toℕ x < n
         x<n = toℕ<n x
-        to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m)))) < n
-        to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m) )) x<n )
+        to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (NatP.<-trans x<n n<m)))) < n
+        to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ≤ (NatP.<-trans x<n n<m) )) x<n )
     ISO.iso← iso x  = lemma2 where
         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
+          (FiniteSet.finiso← fa (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
+          (sym (toℕ-fromℕ≤ (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
         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))) 
+               (FiniteSet.finiso← fa (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
+                    (sym (toℕ-fromℕ≤ (NatP.<-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 _ ) ) ⟩
@@ -439,22 +484,22 @@
               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
+               lemma6 : toℕ (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)) < n
+               lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ≤ (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
+    ISO.iso→ iso (elm1 elm x) = fin-less-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 : FiniteSet.Q←F fa (fromℕ≤ (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm 
         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ℕ≤ (NatP.<-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))
+             FiniteSet.Q←F fa (fromℕ≤ ( NatP.<-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))
+              FiniteSet.Q←F fa (fromℕ≤ ( NatP.<-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ℕ _ _ ) ⟩
@@ -464,25 +509,3 @@
            ∎  where open ≡-Reasoning
 
 
-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
-... | a=f = iso-fin (fin-×-f a ) iso-1 where
-   iso-1 : ISO (Fin a × B) ( A × B )
-   ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x) 
-   ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x) 
-   ISO.iso← iso-1 x  =  lemma  where
-      lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
-      lemma = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso← fa _ )
-   ISO.iso→ iso-1 x = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso→ fa _ )
-   iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B)
-   ISO.A←B iso-2 (zero , b ) = case1 b
-   ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b )
-   ISO.B←A iso-2 (case1 b) = ( zero , b )
-   ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b )
-   ISO.iso← iso-2 (case1 x) = refl
-   ISO.iso← iso-2 (case2 x) = refl
-   ISO.iso→ iso-2 (zero , b ) = refl
-   ISO.iso→ iso-2 (suc a , b ) = refl
-   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) × B) {a * b}
-   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () }
-   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2