# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573261474 -32400
# Node ID 9911911b77cbd60cab0750cd12a8951f65d0ddf7
# Parent  29d81bcff049c39d9be94537391eb47350124772
all foundables

diff -r 29d81bcff049 -r 9911911b77cb agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sat Nov 09 07:47:32 2019 +0900
+++ b/agda/finiteSet.agda	Sat Nov 09 10:04:34 2019 +0900
@@ -13,9 +13,12 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
+record Found ( Q : Set ) (p : Q → Bool ) : Set where
+     field
+       found : Q
+       found-p : p found ≡ true
 
-record FiniteSet ( Q : Set ) { n : ℕ }
-        : Set  where
+record FiniteSet ( Q : Set ) { n : ℕ } : Set  where
      field
         Q←F : Fin n → Q
         F←Q : Q → Fin n
@@ -45,28 +48,31 @@
      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 )
+     --   ¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P → ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
+     End : (m : ℕ ) → (p : Q → Bool ) → Set
+     End m p = (i : Fin n) → m ≤ toℕ i → p (Q←F i )  ≡ false 
+     next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
               → (m<n : m < n ) → p (Q←F (fromℕ≤ m<n )) ≡ false
-              → (i : Fin n) → m ≤ toℕ i → p (Q←F i) ≡ false
-         next-end {m} prev m<n np i m<i with Data.Nat.Properties.<-cmp m (toℕ i) 
-         next-end {m} prev m<n np i m<i | tri< a ¬b ¬c = prev i a
-         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
+              → End m p
+     next-end {m} p prev m<n np i m<i with Data.Nat.Properties.<-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
               m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n )  → fromℕ≤ m<n ≡ i
               m<n=i i eq m<n = i=j (fromℕ≤ m<n) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq )
+     first-end :  ( p : Q → Bool ) → End n p
+     first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {n} {i}) )
+     found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
+     found {p} {q} pt = found1 n  (lt0 n) ( first-end p ) where
          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 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 ⟩
+              ≡⟨ bool-or-1 (¬-bool-t np ) ⟩
                  exists1 m (lt2 m<n) p
-              ≡⟨ found1 m (lt2 m<n) (next-end end m<n (¬-bool-t np )) ⟩
+              ≡⟨ found1 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) ⟩
                  true
               ∎  where open ≡-Reasoning
      not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
@@ -76,13 +82,38 @@
          not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n))
          not-found2 (suc m) m<n | eq = begin
                   p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p 
-              ≡⟨ cong (λ k → k \/ exists1 m (lt2 m<n) p ) eq ⟩
-                  false \/ exists1 m (lt2 m<n) p 
-              ≡⟨ bool-or-1 refl  ⟩
+              ≡⟨ bool-or-1 eq ⟩
                   exists1 m (lt2 m<n) p 
               ≡⟨ not-found2 m (lt2 m<n)  ⟩
                   false
               ∎  where open ≡-Reasoning
+     open import Level
+     postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
+     found← : { p : Q → Bool } → exists p ≡ true → Found Q p
+     found← {p} exst = found2 n (lt0 n) (first-end p ) where
+         found2 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p →  Found Q p
+         found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q)  z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where
+             lemma : (λ z → p (Q←F (F←Q z))) ≡ p
+             lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl )
+         found2 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
+         found2 (suc m)  m<n end | yes eq = record { found = Q←F (fromℕ≤ m<n) ; found-p = eq }
+         found2 (suc m)  m<n end | no np = 
+               found2 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) 
+     not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
+     not-found← {p} ne q = not-found3 n (lt0 n) (first-end p ) ne where
+         not-found3 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p → exists1 m m<n p ≡ false  →  p q ≡ false
+         not-found3 0 m<n end prev = subst (λ k → p k ≡ false) (finiso→ q) ( end (F←Q q) z≤n ) 
+         not-found3 (suc m)  m<n end prev with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
+         not-found3 (suc m)  m<n end prev | yes eq =
+             ⊥-elim ( ¬-bool prev (subst (λ k → k \/  exists1 m (lt2 m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (lt2 m<n) p}) )) 
+         not-found3 (suc m)  m<n end prev | no np = 
+              not-found3 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) ( begin
+                     exists1 m (lt2 m<n) p 
+                  ≡⟨ sym (bool-or-1 (¬-bool-t np )) ⟩
+                     p (Q←F (fromℕ≤ m<n))  \/ exists1 m (lt2 m<n) p 
+                  ≡⟨ prev ⟩
+                     false 
+                  ∎ ) where open ≡-Reasoning
              
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n