Mercurial > hg > Members > kono > Proof > automaton

changeset 77:faf6fcd36018

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 08 Nov 2019 14:42:28 +0900
parents 7b357b295272
children df35d0f41ccd
files agda/finiteSet.agda
diffstat 1 files changed, 20 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Fri Nov 08 13:40:25 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 08 14:42:28 2019 +0900
@@ -48,17 +48,27 @@
               ≡⟨ not-found2 m (lt2 m<n)  ⟩
                   false
               ∎  where open ≡-Reasoning
-     not-found1 : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
-     not-found1 {p} ne q =  not-found3 n (lt0 n) where
-         not-found3 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → p q ≡ false 
-         not-found3  zero  _ = {!!}
-         not-found3 ( suc m ) m<n = {!!}
+     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})
      found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
-     found {p} {q} pt with bool-≡-? (exists p) true
-     ... | yes eq1 = eq1
-     ... | no ne = ⊥-elim ( contra-position not-found1 notall (¬-bool-t ne) ) where
-         notall : ¬ ((q1 : Q) → p q1 ≡ false)
-         notall ne = ¬-bool (ne q) pt 
+     found {p} {q} pt = found1 n (lt0 n) (toℕ (F←Q q)) fin<n where
+         q=q : (i : Fin n) → i ≡ F←Q q → p (Q←F i) ≡ true 
+         q=q = {!!}
+         found1 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) (qn : ℕ ) → qn < m → exists1 m m<n p ≡ true
+         found1 zero _ _ () 
+         found1 (suc m) m<n qn qn<m with Data.Nat._≟_ m qn
+         found1 (suc m) m<n qn qn<m | yes refl = {!!}
+         found1 (suc m) m<n zero qn<m | no ¬p = {!!}
+         found1 (suc m) m<n (suc qn) qn<m | no ¬p = begin
+                  p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p
+              ≡⟨ {!!}  ⟩
+                  false \/ exists1 m (lt2 m<n) p
+              ≡⟨ bool-or-1 refl  ⟩
+                  exists1 m (lt2 m<n) p
+              ≡⟨ found1 m (lt2 m<n) qn {!!} ⟩
+                  true
+              ∎  where open ≡-Reasoning
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
 fless zero = s≤s z≤n