# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573253252 -32400
# Node ID 29d81bcff049c39d9be94537391eb47350124772
# Parent  92f396c3a1d7d56343e97c412d5f709c65a1bcac
found done

diff -r 92f396c3a1d7 -r 29d81bcff049 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sat Nov 09 00:05:05 2019 +0900
+++ b/agda/finiteSet.agda	Sat Nov 09 07:47:32 2019 +0900
@@ -42,6 +42,9 @@
      fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
      fin<n {_} {zero} = s≤s z≤n
      fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
+     i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
+     i=j {suc n} zero zero refl = refl
+     i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )
      found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
      found {p} {q} pt = found1 n  (lt0 n) (λ i i>n → ⊥-elim (nat-≤> i>n (fin<n {n} {i}) )) where
          next-end : {m : ℕ } → ((i : Fin n) → suc m ≤ toℕ i → p (Q←F i) ≡ false )
@@ -52,37 +55,18 @@
          next-end {m} prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c )
          next-end {m} 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
               m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n )  → fromℕ≤ m<n ≡ i
-              m<n=i {suc n} zero  refl (s≤s z≤n) = refl
-              m<n=i {suc n} (suc i) refl (s≤s m<n) with m<n=i {n} i refl m<n
-              ... | t =  subst₂ ( λ j k →  j ≡ k ) {!!} {!!} t
+              m<n=i i eq m<n = i=j (fromℕ≤ m<n) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq )
          found1 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → ((i : Fin n) → m ≤ toℕ i → p (Q←F i )  ≡ false ) →  exists1 m m<n p ≡ true
          found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt )
-         found1 (suc m)  m<n neg with fromℕ≤ m<n ≟ F←Q q
-         found1 (suc m)  m<n neg | yes eq = begin
-                 p (Q←F (fromℕ≤ m<n )) \/ exists1 m (lt2 m<n ) p
-              ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (
-                 begin
-                    Q←F (fromℕ≤ m<n)
-                 ≡⟨ cong ( λ k → Q←F k ) eq ⟩
-                    Q←F (F←Q q)
-                 ≡⟨ finiso→  q ⟩
-                    q
-                 ∎ ) ⟩
-                 p q \/ exists1 m (lt2 m<n ) p
-              ≡⟨ cong (λ k → ( k \/ exists1 m (lt2 m<n ) p )) pt ⟩
-                  true \/ exists1 m (lt2 m<n ) p
-              ≡⟨⟩
-                 true 
-              ∎  where open ≡-Reasoning
-         found1 (suc m)  m<n neg | no ¬p with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
-         found1 (suc m)  m<n neg | no ¬p | yes eq = subst (λ k → k \/ exists1 m (lt2 m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (lt2 m<n) p} ) 
-         found1 (suc m)  m<n neg | no ¬p | no np = begin
+         found1 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
+         found1 (suc m)  m<n end | yes eq = subst (λ k → k \/ exists1 m (lt2 m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (lt2 m<n) p} ) 
+         found1 (suc m)  m<n end | no np = begin
                  p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p
               ≡⟨ cong (λ k → k \/ exists1 m (lt2 m<n) p) (¬-bool-t np )  ⟩
                  false  \/ exists1 m (lt2 m<n) p
               ≡⟨ bool-or-1 refl ⟩
                  exists1 m (lt2 m<n) p
-              ≡⟨ found1 m (lt2 m<n) (next-end neg m<n (¬-bool-t np )) ⟩
+              ≡⟨ found1 m (lt2 m<n) (next-end end m<n (¬-bool-t np )) ⟩
                  true
               ∎  where open ≡-Reasoning
      not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false