Mercurial > hg > Members > kono > Proof > automaton

changeset 83:92f396c3a1d7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add end function
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Nov 2019 00:05:05 +0900
parents ed6a39c20098
children 29d81bcff049
files agda/finiteSet.agda agda/nat.agda
diffstat 2 files changed, 38 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Fri Nov 08 21:30:14 2019 +0900
+++ b/agda/finiteSet.agda	Sat Nov 09 00:05:05 2019 +0900
@@ -1,7 +1,7 @@
 module finiteSet  where
 
 open import Data.Nat hiding ( _≟_ )
-open import Data.Fin renaming ( _<_ to _<<_ )
+open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
 open import Data.Fin.Properties
 open import Data.Empty
 open import Relation.Nullary
@@ -39,29 +39,26 @@
      equal? q0 q1 with F←Q q0 ≟ F←Q q1
      ... | yes p = true
      ... | no ¬p = false
-     not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
-     not-found {p} pn = not-found2 n (lt0 n) where
-         not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false
-         not-found2  zero  _ = refl
-         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  ⟩
-                  exists1 m (lt2 m<n) p 
-              ≡⟨ not-found2 m (lt2 m<n)  ⟩
-                  false
-              ∎  where open ≡-Reasoning
      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 = found1 n  (lt0 n) where
-         found1 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) →  exists1 m m<n p ≡ true
-         found1 0 m<n = ?
-         found1 (suc m)  m<n with fromℕ≤ m<n ≟ F←Q q
-         found1 (suc m)  m<n | yes eq = begin
+     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 )
+              → (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
+              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
+         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
@@ -77,18 +74,31 @@
               ≡⟨⟩
                  true 
               ∎  where open ≡-Reasoning
-         found1 (suc m)  m<n | no ¬p with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
-         found1 (suc m)  m<n | 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 | no ¬p | no np = begin
+         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
                  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) ⟩
+              ≡⟨ found1 m (lt2 m<n) (next-end neg m<n (¬-bool-t np )) ⟩
                  true
               ∎  where open ≡-Reasoning
-
+     not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
+     not-found {p} pn = not-found2 n (lt0 n) where
+         not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false
+         not-found2  zero  _ = refl
+         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  ⟩
+                  exists1 m (lt2 m<n) p 
+              ≡⟨ not-found2 m (lt2 m<n)  ⟩
+                  false
+              ∎  where open ≡-Reasoning
              
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
--- a/agda/nat.agda	Fri Nov 08 21:30:14 2019 +0900
+++ b/agda/nat.agda	Sat Nov 09 00:05:05 2019 +0900
@@ -10,6 +10,9 @@
 nat-<> : { x y : Nat } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 
+nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥
+nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+
 nat-<≡ : { x : Nat } → x < x → ⊥
 nat-<≡  (s≤s lt) = nat-<≡ lt