Mercurial > hg > Members > kono > Proof > automaton
changeset 85:9911911b77cb
all foundables
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 Nov 2019 10:04:34 +0900 |
| parents | 29d81bcff049 |
| children | 4c950a6ad6ce |
| files | agda/finiteSet.agda |
| diffstat | 1 files changed, 48 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- 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