Mercurial > hg > Members > kono > Proof > automaton
changeset 81:7c38ed740961
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 08 Nov 2019 20:23:35 +0900 |
| parents | 184752a8f0ed |
| children | ed6a39c20098 |
| files | agda/finiteSet.agda |
| diffstat | 1 files changed, 11 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/finiteSet.agda Fri Nov 08 20:18:10 2019 +0900 +++ b/agda/finiteSet.agda Fri Nov 08 20:23:35 2019 +0900 @@ -58,19 +58,19 @@ 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 - iq : {m : ℕ} (lt : suc m Data.Nat.≤ n ) → toℕ (F←Q q) ≡ m → Q←F (fromℕ≤ lt) ≡ q - iq {m} lt refl = begin - Q←F (fromℕ≤ lt) - ≡⟨ {!!} ⟩ - Q←F (F←Q q) - ≡⟨ finiso→ q ⟩ - q - ∎ where open ≡-Reasoning found1 : (m : ℕ ) {i : ℕ} (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ true - found1 (suc m) lt m<n with Data.Nat._≟_ m (toℕ (F←Q q)) - found1 (suc m) lt m<n | yes refl = begin + found1 0 () + found1 (suc m) lt m<n with fromℕ≤ m<n ≟ F←Q q + found1 (suc m) lt 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 )) (iq m<n refl ) ⟩ + ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) ( + begin + Q←F (fromℕ≤ m<n) + ≡⟨ cong ( λ k → Q←F k ) eq ⟩ + Q←F (F←Q q) + ≡⟨ finiso→ q ⟩ + q + ∎ ) ⟩ p q \/ exists1 m (lt2 m<n ) p ≡⟨ cong (λ k → ( k \/ exists1 m (lt2 m<n ) p )) pt ⟩ true \/ exists1 m (lt2 m<n ) p