Mercurial > hg > Members > kono > Proof > automaton

changeset 82:ed6a39c20098

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 21:30:14 +0900
parents 7c38ed740961
children 92f396c3a1d7
files agda/finiteSet.agda agda/logic.agda
diffstat 2 files changed, 21 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Fri Nov 08 20:23:35 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 08 21:30:14 2019 +0900
@@ -57,11 +57,11 @@
      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  (fin<n {n} {F←Q q}) (lt0 n) where
-         found1 : (m : ℕ ) {i : ℕ} (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) →  exists1 m m<n p ≡ true
-         found1 0 ()
-         found1 (suc m)  lt m<n with fromℕ≤ m<n ≟ F←Q q
-         found1 (suc m)  lt m<n | yes eq = begin
+     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
                  p (Q←F (fromℕ≤ m<n )) \/ exists1 m (lt2 m<n ) p
               ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (
                  begin
@@ -77,7 +77,18 @@
               ≡⟨⟩
                  true 
               ∎  where open ≡-Reasoning
-         found1 (suc m)  lt m<n | no ¬p = {!!}
+         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
+                 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) ⟩
+                 true
+              ∎  where open ≡-Reasoning
+
              
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
--- a/agda/logic.agda	Fri Nov 08 20:23:35 2019 +0900
+++ b/agda/logic.agda	Fri Nov 08 21:30:14 2019 +0900
@@ -118,6 +118,10 @@
 bool-or-3 {true} = refl
 bool-or-3 {false} = refl
 
+bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
+bool-or-4 {true} = refl
+bool-or-4 {false} = refl
+
 bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
 bool-and-1 {false} {b} refl = refl
 bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false