Mercurial > hg > Members > kono > Proof > automaton1
changeset 0:9615a94b18ca
new automaton in agda
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 12 Nov 2020 11:45:34 +0900 |
| parents | |
| children | 7399aae907fc |
| files | Test.agda automaton.agda finiteSet.agda logic.agda nat.agda nfa.agda regular-language.agda |
| diffstat | 7 files changed, 1372 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Test.agda Thu Nov 12 11:45:34 2020 +0900 @@ -0,0 +1,32 @@ +module Test where +open import Level +open import Relation.Nullary +open import Relation.Binary -- hiding (_⇔_ ) +open import Data.Empty +open import Data.Nat hiding ( _⊔_ ) + +id : ( A : Set ) → A → A +id A x = x + +id1 : { A : Set } → A → A +id1 x = x + + +test1 = id ℕ 1 +test2 = id1 1 + + + +data Bool : Set where + true : Bool + false : Bool + +record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where + constructor ⟪_,_⟫ + field + proj1 : A + proj2 : B + +data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where + case1 : A → A ∨ B + case2 : B → A ∨ B
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/automaton.agda Thu Nov 12 11:45:34 2020 +0900 @@ -0,0 +1,217 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module automaton where +open import Level hiding ( suc ; zero ) +open import Data.Empty +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality -- hiding (_⇔_) +open import logic +open import Data.List + +record Automaton {n : Level} (Q : Set n) (Σ : Set ) : Set ((Level.suc n) ) where + field + δ : Q → Σ → Q + F : Q → Set + exists : (Q → Set) → Set + +open Automaton + +accept : {n : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set +accept {Q} {Σ} atm q [] = F atm q +accept {Q} {Σ} atm q (x ∷ input) = + accept atm (δ atm q x ) input + +trace : {n : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q +trace {n} {Q} {Σ} A q [] a = q ∷ [] +trace {n} {Q} {Σ} A q (x ∷ t) a = q ∷ ( trace A (δ A q x) t a ) + +data Q3 : Set where + q₁ : Q3 + q₂ : Q3 + q₃ : Q3 + +data Σ2 : Set where + s0 : Σ2 + s1 : Σ2 + +δ16 : Q3 → Σ2 → Q3 +δ16 q₁ s0 = q₁ +δ16 q₁ s1 = q₂ +δ16 q₂ s0 = q₃ +δ16 q₂ s1 = q₂ +δ16 q₃ s0 = q₂ +δ16 q₃ s1 = q₂ + +δ16' : Q3 → Σ2 → Q3 +δ16' q₁ s0 = q₁ +δ16' q₁ s1 = q₂ +δ16' q₂ s0 = q₃ +δ16' q₂ s1 = q₂ +δ16' q₃ s0 = q₂ +δ16' q₃ s1 = q₃ + +data a16end : Q3 → Set where + a16q2 : a16end q₂ + +data exists-in-Q3 (P : Q3 → Set) : Set where + qe1 : P q₁ → exists-in-Q3 P + qe2 : P q₂ → exists-in-Q3 P + qe3 : P q₃ → exists-in-Q3 P + +a16 : Automaton Q3 Σ2 +a16 = record { δ = δ16 ; F = λ q → a16end q ; exists = exists-in-Q3 } + +a16' : Automaton Q3 Σ2 +a16' = record { δ = δ16' ; F = λ q → q ≡ q₂ ; exists = exists-in-Q3 } + +-- +-- ∷ → ∷ → ∷ → [] +-- ↓ ↓ ↓ +-- s0 s0 s1 +-- +input1 : List Σ2 +input1 = s0 ∷ s0 ∷ s1 ∷ [] + +input2 : List Σ2 +input2 = s0 ∷ s0 ∷ s0 ∷ [] + +test1 : accept a16 q₁ input1 +test1 = a16q2 + +lemma0 : accept a16 q₁ input1 ≡ a16end q₂ +lemma0 = begin + accept a16 q₁ ( s0 ∷ s0 ∷ s1 ∷ [] ) + ≡⟨ refl ⟩ -- x ≡ x + accept a16 q₁ ( s0 ∷ s1 ∷ [] ) + ≡⟨⟩ + accept a16 q₁ ( s1 ∷ [] ) + ≡⟨⟩ + accept a16 q₂ [] + ≡⟨⟩ + a16end q₂ + ∎ where open ≡-Reasoning + +lemma1 : List Q3 +lemma1 = trace a16 q₁ input1 a16q2 + +test1' : accept a16' q₁ input1 +test1' = refl + +lemma2 : List Q3 +lemma2 = trace a16' q₁ input1 refl + +test2 : ¬ ( accept a16 q₁ input2 ) +test2 () + +open import Data.Bool +open import Data.Unit + +-- contains at least 1 s1 +c1 : List Σ2 → Set +c1 [] = ⊥ +c1 (s1 ∷ t) = ⊤ +c1 (_ ∷ t) = c1 t + +-- even number of s0 +even0 : List Σ2 → Set +odd0 : List Σ2 → Set +odd0 [] = ⊥ +odd0 (s0 ∷ t) = even0 t +odd0 (s1 ∷ t) = odd0 t +even0 [] = ⊤ +even0 (s0 ∷ t) = odd0 t +even0 (s1 ∷ t) = even0 t + +-- after + +a0 : List Σ2 → Set +a0 [] = ⊥ +a0 (s1 ∷ t ) = even0 t +a0 (s0 ∷ t ) = a0 t + +-- data ⊥ : Set +-- +-- data ⊤ : Set where +-- tt : ⊤ +-- tt : ⊤ + +lemma-a : (x : List Σ2 ) → accept a16' q₁ x → a0 x +lemma-a x a = a1 x a where + a3 : (x : List Σ2 ) → accept a16' q₃ x → odd0 x + a2 : (x : List Σ2 ) → accept a16' q₂ x → even0 x + a3 [] () + a3 (s0 ∷ t) a = a2 t a + a3 (s1 ∷ t) a = a3 t a + a2 [] a = tt + a2 (s0 ∷ t) a = a3 t a + a2 (s1 ∷ t) a = a2 t a + a1 : (x : List Σ2 ) → accept a16' q₁ x → a0 x + a1 [] () -- a16' does not accept [] + a1 (s0 ∷ t) a = a1 t a + a1 (s1 ∷ t) a = a2 t a + +-- ¬_ : Set → Set +-- ¬_ _ = ⊥ + +lemma-not-a : ¬ ( (x : List Σ2 ) → accept a16 q₁ x → a0 x ) +lemma-not-a not1 with not1 (s1 ∷ s0 ∷ s1 ∷ [] ) a16q2 +... | () + +-- can we prove negation similar to the lemma-a? +-- lemma-not-a' : ¬ ((x : List Σ2 ) → accept a16 q₁ x → a0 x) +-- lemma-not-a' not = {!!} where +-- a3 : (x : List Σ2 ) → accept a16 q₃ x → odd0 x +-- a2 : (x : List Σ2 ) → accept a16 q₂ x → even0 x +-- a3 (s0 ∷ t) a = a2 t a +-- a3 (s1 ∷ t) a = {!!} +-- a2 [] a = tt +-- a2 (s0 ∷ t) a = a3 t a +-- a2 (s1 ∷ t) a = a2 t a +-- a1 : (x : List Σ2 ) → accept a16 q₁ x → a0 x +-- a1 [] () +-- a1 (s0 ∷ t) a = a1 t a +-- a1 (s1 ∷ t) a = a2 t a + +open import Data.Nat + +evenℕ : ℕ → Set +oddℕ : ℕ → Set +oddℕ zero = ⊥ +oddℕ (suc n) = evenℕ n +evenℕ zero = ⊤ +evenℕ (suc n) = oddℕ n + +count-s0 : (x : List Σ2 ) → ℕ +count-s0 [] = zero +count-s0 (s0 ∷ t) = suc ( count-s0 t ) +count-s0 (s1 ∷ t) = count-s0 t + +e1 : (x : List Σ2 ) → even0 x → evenℕ ( count-s0 x ) +o1 : (x : List Σ2 ) → odd0 x → oddℕ ( count-s0 x ) +e1 [] e = tt +e1 (s0 ∷ t) o = o1 t o +e1 (s1 ∷ t) e = e1 t e +o1 [] () +o1 (s0 ∷ t) e = e1 t e +o1 (s1 ∷ t) o = o1 t o + +δ19 : Q3 → Σ2 → Q3 +δ19 q₁ s0 = q₁ +δ19 q₁ s1 = q₂ +δ19 q₂ s0 = q₁ +δ19 q₂ s1 = q₂ +δ19 q₃ _ = q₁ + +a19 : Automaton Q3 Σ2 +a19 = record { δ = δ19 ; F = λ q → q ≡ q₁ ; exists = exists-in-Q3 } + +-- input is empty or ends in s0 + +end0 : List Σ2 → Set +end0 [] = ⊤ +end0 (s0 ∷ [] ) = ⊤ +end0 (s1 ∷ [] ) = ⊥ +end0 (x ∷ t ) = end0 t + +lemma-b : (x : List Σ2 ) → accept a19 q₁ x → end0 x +lemma-b = {!!} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/finiteSet.agda Thu Nov 12 11:45:34 2020 +0900 @@ -0,0 +1,536 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module finiteSet where + +open import Data.Nat hiding ( _≟_ ) +open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_) +open import Data.Fin.Properties hiding ( eq? ) +open import Data.Empty +open import Data.Bool renaming ( _∧_ to _/\_ ; _∨_ to _\/_ ) hiding ( _≟_ ; _<_ ; _≤_ ) +open import Relation.Nullary +open import Relation.Binary.Definitions +open import Relation.Binary.PropositionalEquality +open import logic +open import nat +open import Data.Nat.Properties as NatP hiding ( _≟_ ; eq? ) + +open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) + +record Found ( Q : Set ) (p : Q → Bool ) : Set where + field + found-q : Q + found-p : p found-q ≡ true + +lt0 : (n : ℕ) → n Data.Nat.≤ n +lt0 zero = z≤n +lt0 (suc n) = s≤s (lt0 n) +lt2 : {m n : ℕ} → m < n → m Data.Nat.≤ n +lt2 {zero} lt = z≤n +lt2 {suc m} {zero} () +lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt) + +record FiniteSet ( Q : Set ) { n : ℕ } : Set where + field + Q←F : Fin n → Q + F←Q : Q → Fin n + finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q + finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f + finℕ : ℕ + finℕ = n + exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool + exists1 zero _ _ = false + exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p + exists : ( Q → Bool ) → Bool + exists p = exists1 n (lt0 n) p + + all1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool + all1 zero _ _ = true + all1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) /\ all1 m (lt2 m<n) p + all : ( Q → Bool ) → Bool + all p = all1 n (lt0 n) p + + open import Data.List + list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q + list1 zero _ _ = [] + list1 ( suc m ) m<n p with ? (p (Q←F (fromℕ≤ {m} {n} m<n))) true + ... | yes _ = Q←F (fromℕ≤ {m} {n} m<n) ∷ list1 m (lt2 m<n) p + ... | no _ = list1 m (lt2 m<n) p + to-list : ( Q → Bool ) → List Q + to-list p = list1 n (lt0 n) p + + equal? : Q → Q → Bool + equal? q0 q1 with F←Q q0 ≟ F←Q q1 + ... | yes p = true + ... | no ¬p = false + + equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y + equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 + equal→refl {q0} {q1} refl | yes eq = begin + q0 + ≡⟨ sym ( finiso→ q0) ⟩ + Q←F (F←Q q0) + ≡⟨ cong (λ k → Q←F k ) eq ⟩ + Q←F (F←Q q1) + ≡⟨ finiso→ q1 ⟩ + q1 + ∎ where open ≡-Reasoning + equal→refl {q0} {q1} () | no ne + equal?-refl : {q : Q} → equal? q q ≡ true + equal?-refl {q} with F←Q q ≟ F←Q q + ... | yes p = refl + ... | no ne = ⊥-elim (ne refl) + + eq? : (x y : Q) → Dec ( x ≡ y ) + eq? x y with F←Q x ≟ F←Q y + eq? x y | yes p = yes ( begin + x + ≡⟨ sym ( finiso→ x ) ⟩ + Q←F (F←Q x) + ≡⟨ cong (λ k → Q←F k ) p ⟩ + Q←F (F←Q y) + ≡⟨ finiso→ y ⟩ + y + ∎ ) where open ≡-Reasoning + eq? x y | no ¬p = no ( λ eq → ¬p (cong (λ k → F←Q k ) eq )) + + 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}) + 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) ) + -- ¬∀⟶∃¬ : ∀ 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 + → End m p + next-end {m} p prev m<n np i m<i with NatP.<-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 ( ? (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt ) + found1 (suc m) m<n end with ? (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) (? {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 + ≡⟨ ? ? ⟩ + exists1 m (lt2 m<n) p + ≡⟨ found1 m (lt2 m<n) (next-end p end m<n (? 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 + ≡⟨ ? 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 ( ? (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 ? (p (Q←F (fromℕ≤ m<n))) true + found2 (suc m) m<n end | yes eq = record { found-q = 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 (? np )) + not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false + not-found← {p} np q = ? ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ? np ep ) ) + +record ISO (A B : Set) : Set where + field + A←B : B → A + B←A : A → B + iso← : (q : A) → A←B ( B←A q ) ≡ q + iso→ : (f : B) → B←A ( A←B f ) ≡ f + +iso-fin : {A B : Set} → {n : ℕ } → FiniteSet A {n} → ISO A B → FiniteSet B {n} +iso-fin {A} {B} {n} fin iso = record { + Q←F = λ f → ISO.B←A iso ( FiniteSet.Q←F fin f ) + ; F←Q = λ b → FiniteSet.F←Q fin ( ISO.A←B iso b ) + ; finiso→ = finiso→ + ; finiso← = finiso← + } where + finiso→ : (q : B) → ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) ≡ q + finiso→ q = begin + ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) + ≡⟨ cong (λ k → ISO.B←A iso k ) (FiniteSet.finiso→ fin _ ) ⟩ + ISO.B←A iso (ISO.A←B iso q) + ≡⟨ ISO.iso→ iso _ ⟩ + q + ∎ where + open ≡-Reasoning + finiso← : (f : Fin n) → FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) ≡ f + finiso← f = begin + FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) + ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (ISO.iso← iso _) ⟩ + FiniteSet.F←Q fin (FiniteSet.Q←F fin f) + ≡⟨ FiniteSet.finiso← fin _ ⟩ + f + ∎ where + open ≡-Reasoning + +data One : Set where + one : One + +fin-∨1 : {B : Set} → { b : ℕ } → FiniteSet B {b} → FiniteSet (One ∨ B) {suc b} +fin-∨1 {B} {b} fb = record { + Q←F = Q←F + ; F←Q = F←Q + ; finiso→ = finiso→ + ; finiso← = finiso← + } where + Q←F : Fin (suc b) → One ∨ B + Q←F zero = case1 one + Q←F (suc f) = case2 (FiniteSet.Q←F fb f) + F←Q : One ∨ B → Fin (suc b) + F←Q (case1 one) = zero + F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) + finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q + finiso→ (case1 one) = refl + finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b) + finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q + finiso← zero = refl + finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f) + + +fin-∨2 : {B : Set} → ( a : ℕ ) → { b : ℕ } → FiniteSet B {b} → FiniteSet (Fin a ∨ B) {a Data.Nat.+ b} +fin-∨2 {B} zero {b} fb = iso-fin fb iso where + iso : ISO B (Fin zero ∨ B) + iso = record { + A←B = A←B + ; B←A = λ b → case2 b + ; iso→ = iso→ + ; iso← = λ _ → refl + } where + A←B : Fin zero ∨ B → B + A←B (case2 x) = x + iso→ : (f : Fin zero ∨ B ) → case2 (A←B f) ≡ f + iso→ (case2 x) = refl +fin-∨2 {B} (suc a) {b} fb = iso-fin (fin-∨1 (fin-∨2 a fb) ) iso + where + iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B) + ISO.A←B iso (case1 zero) = case1 one + ISO.A←B iso (case1 (suc f)) = case2 (case1 f) + ISO.A←B iso (case2 b) = case2 (case2 b) + ISO.B←A iso (case1 one) = case1 zero + ISO.B←A iso (case2 (case1 f)) = case1 (suc f) + ISO.B←A iso (case2 (case2 b)) = case2 b + ISO.iso← iso (case1 one) = refl + ISO.iso← iso (case2 (case1 x)) = refl + ISO.iso← iso (case2 (case2 x)) = refl + ISO.iso→ iso (case1 zero) = refl + ISO.iso→ iso (case1 (suc x)) = refl + ISO.iso→ iso (case2 x) = refl + + +FiniteSet→Fin : {A : Set} → { a : ℕ } → (fin : FiniteSet A {a} ) → ISO (Fin a) A +ISO.A←B (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f +ISO.B←A (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f +ISO.iso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin +ISO.iso→ (FiniteSet→Fin fin) = FiniteSet.finiso→ fin + + +fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a Data.Nat.+ b} +fin-∨ {A} {B} {a} {b} fa fb = iso-fin (fin-∨2 a fb ) iso2 where + ia = FiniteSet→Fin fa + iso2 : ISO (Fin a ∨ B ) (A ∨ B) + ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x ) + ISO.A←B iso2 (case2 x) = case2 x + ISO.B←A iso2 (case1 x) = case1 ( ISO.B←A ia x ) + ISO.B←A iso2 (case2 x) = case2 x + ISO.iso← iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso← ia x) + ISO.iso← iso2 (case2 x) = refl + ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x) + ISO.iso→ iso2 (case2 x) = refl + +open import Data.Product + +fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b} +fin-× {A} {B} {a} {b} fa fb with FiniteSet→Fin fa +... | a=f = iso-fin (fin-×-f a ) iso-1 where + iso-1 : ISO (Fin a × B) ( A × B ) + ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x) , proj₂ x) + ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x) , proj₂ x) + ISO.iso← iso-1 x = lemma where + lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x ) + lemma = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso← fa _ ) + ISO.iso→ iso-1 x = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso→ fa _ ) + + iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B) + ISO.A←B iso-2 (zero , b ) = case1 b + ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b ) + ISO.B←A iso-2 (case1 b) = ( zero , b ) + ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b ) + ISO.iso← iso-2 (case1 x) = refl + ISO.iso← iso-2 (case2 x) = refl + ISO.iso→ iso-2 (zero , b ) = refl + ISO.iso→ iso-2 (suc a , b ) = refl + + fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B) {a * b} + fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () } + fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 + +open _∧_ + +fin-∧ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∧ B) {a * b} +fin-∧ {A} {B} {a} {b} fa fb with FiniteSet→Fin fa -- same thing for our tool +... | a=f = iso-fin (fin-×-f a ) iso-1 where + iso-1 : ISO (Fin a ∧ B) ( A ∧ B ) + ISO.A←B iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x) ; proj2 = proj2 x} + ISO.B←A iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x) ; proj2 = proj2 x} + ISO.iso← iso-1 x = lemma where + lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 = proj2 x} ≡ record {proj1 = proj1 x ; proj2 = proj2 x } + lemma = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso← fa _ ) + ISO.iso→ iso-1 x = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso→ fa _ ) + + iso-2 : {a : ℕ } → ISO (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B) + ISO.A←B iso-2 (record { proj1 = zero ; proj2 = b }) = case1 b + ISO.A←B iso-2 (record { proj1 = suc fst ; proj2 = b }) = case2 ( record { proj1 = fst ; proj2 = b } ) + ISO.B←A iso-2 (case1 b) = record {proj1 = zero ; proj2 = b } + ISO.B←A iso-2 (case2 (record { proj1 = a ; proj2 = b })) = record { proj1 = suc a ; proj2 = b } + ISO.iso← iso-2 (case1 x) = refl + ISO.iso← iso-2 (case2 x) = refl + ISO.iso→ iso-2 (record { proj1 = zero ; proj2 = b }) = refl + ISO.iso→ iso-2 (record { proj1 = suc a ; proj2 = b }) = refl + + fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) ∧ B) {a * b} + fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () } + fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 + +import Data.Nat.DivMod + +open import Data.Vec +import Data.Product + +exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n +exp2 n = begin + exp 2 (suc n) + ≡⟨⟩ + 2 * ( exp 2 n ) + ≡⟨ *-comm 2 (exp 2 n) ⟩ + ( exp 2 n ) * 2 + ≡⟨ +-*-suc ( exp 2 n ) 1 ⟩ + (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1 + ≡⟨ cong ( λ k → (exp 2 n ) Data.Nat.+ k ) (proj₂ *-identity (exp 2 n) ) ⟩ + exp 2 n Data.Nat.+ exp 2 n + ∎ where + open ≡-Reasoning + open Data.Product + +cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f +cast-iso refl zero = refl +cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) + + +fin2List : {n : ℕ } → FiniteSet (Vec Bool n) {exp 2 n } +fin2List {zero} = record { + Q←F = λ _ → Vec.[] + ; F←Q = λ _ → # 0 + ; finiso→ = finiso→ + ; finiso← = finiso← + } where + Q = Vec Bool zero + finiso→ : (q : Q) → [] ≡ q + finiso→ [] = refl + finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f + finiso← zero = refl +fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) {k} ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List {n}) (fin2List {n})) iso ) + where + QtoR : Vec Bool (suc n) → Vec Bool n ∨ Vec Bool n + QtoR ( true ∷ x ) = case1 x + QtoR ( false ∷ x ) = case2 x + RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n) + RtoQ ( case1 x ) = true ∷ x + RtoQ ( case2 x ) = false ∷ x + isoRQ : (x : Vec Bool (suc n) ) → RtoQ ( QtoR x ) ≡ x + isoRQ (true ∷ _ ) = refl + isoRQ (false ∷ _ ) = refl + isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x + isoQR (case1 x) = refl + isoQR (case2 x) = refl + iso : ISO (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n)) + iso = record { A←B = QtoR ; B←A = RtoQ ; iso← = isoQR ; iso→ = isoRQ } + +F2L : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} ) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n → Bool ) → Vec Bool n +F2L {Q} {zero} fin _ Q→B = [] +F2L {Q} {suc n} (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) lemma6 ∷ F2L {Q} {n} (NatP.<-trans n<m a<sa ) fin qb1 where + lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))) < suc n + lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ≤ n<m )) a<sa ) + qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool + qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa) + +List2Func : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → Vec Bool n → Q → Bool +List2Func {Q} {zero} (s≤s z≤n) fin [] q = false +List2Func {Q} {suc n} {m} (s≤s n<m) fin (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m +... | yes _ = h +... | no _ = List2Func {Q} {n} {m} (NatP.<-trans n<m a<sa ) fin t q + +F2L-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (x : Vec Bool n ) → F2L a<sa fin (λ q _ → List2Func a<sa fin x q ) ≡ x +F2L-iso {Q} {m} fin x = f2l m a<sa x where + f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L n<m fin (λ q q<n → List2Func n<m fin x q ) ≡ x + f2l zero (s≤s z≤n) [] = refl + f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3 where + lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 → h ∷ t ≡ h1 ∷ t1 + lemma1 refl refl = refl + lemma2 : List2Func (s≤s n<m) fin (h ∷ t) (FiniteSet.Q←F fin (fromℕ≤ n<m)) ≡ h + lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m)) ≟ fromℕ≤ n<m + lemma2 | yes p = refl + lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) ) + lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func (s≤s n<m) fin (h ∷ t) q ≡ List2Func (NatP.<-trans n<m a<sa) fin t q + lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m + lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ≤ n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where + lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n + lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s z≤n + lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl) + lemma4 q _ | no ¬p = refl + lemma3 : F2L (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q ) ≡ t + lemma3 = begin + F2L (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q ) + ≡⟨ cong (λ k → F2L (NatP.<-trans n<m a<sa) fin ( λ q q<n → k q q<n )) + (FiniteSet.f-extensionality fin ( λ q → + (FiniteSet.f-extensionality fin ( λ q<n → lemma4 q q<n )))) ⟩ + F2L (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (NatP.<-trans n<m a<sa) fin t q ) + ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩ + t + ∎ where + open ≡-Reasoning + + +L2F : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} ) → Vec Bool n → (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → Bool +L2F n<m fin x q q<n = List2Func n<m fin x q + +L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (L2F a<sa fin (F2L a<sa fin (λ q _ → f q) )) q (toℕ<n _) ≡ f q +L2F-iso {Q} {m} fin f q = l2f m a<sa (toℕ<n _) where + lemma11 : {n : ℕ } → (n<m : n < m ) → ¬ ( FiniteSet.F←Q fin q ≡ fromℕ≤ n<m ) → toℕ (FiniteSet.F←Q fin q) ≤ n → toℕ (FiniteSet.F←Q fin q) < n + lemma11 {n} n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where + lemma13 : {n nq : ℕ } → (n<m : n < m ) → ¬ ( nq ≡ n ) → nq ≤ n → nq < n + lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl ) + lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n + lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n) + lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ≤ (s≤s lt) ≡ suc (fromℕ≤ lt) + lemma3 (s≤s lt) = refl + lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ≤ n<m + lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl + lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3 n<m) ) ( cong ( λ k → suc k ) ( lemma12 {n} {m} n<m f refl ) ) + l2f : (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n ) → (L2F n<m fin (F2L n<m fin (λ q _ → f q))) q q<n ≡ f q + l2f zero (s≤s z≤n) () + l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m + l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin + f (FiniteSet.Q←F fin (fromℕ≤ n<m)) + ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p) ⟩ + f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q )) + ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩ + f q + ∎ where + open ≡-Reasoning + l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11 n<m ¬p n<q) + +fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a} +fin→ {A} {a} fin = iso-fin fin2List iso where + iso : ISO (Vec Bool a ) (A → Bool) + ISO.A←B iso x = F2L a<sa fin ( λ q _ → x q ) + ISO.B←A iso x = List2Func a<sa fin x + ISO.iso← iso x = F2L-iso fin x + ISO.iso→ iso x = lemma where + lemma : List2Func a<sa fin (F2L a<sa fin (λ q _ → x q)) ≡ x + lemma = FiniteSet.f-extensionality fin ( λ q → L2F-iso fin x q ) + + +Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) {n} +Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl } + +data fin-less { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where + elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less n<m fa + +get-elm : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → fin-less n<m fa → A +get-elm (elm1 a _ ) = a + +get-< : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → (f : fin-less n<m fa ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n +get-< (elm1 _ b ) = b + +fin-less-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) + → (x y : fin-less n<m fa ) → get-elm {n} {m} {n<m} {A} {fa} x ≡ get-elm {n} {m} {n<m} {A} {fa} y → get-< x ≅ get-< y → x ≡ y +fin-less-cong n<m fa (elm1 elm x) (elm1 elm x) refl HE.refl = refl + +fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (fin-less n<m fa) {n} +fin-< {A} {n} {m} n<m fa = iso-fin (Fin2Finite n) iso where + iso : ISO (Fin n) (fin-less n<m fa) + lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n + lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl + lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl ) + lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ≤ i<n ≡ fromℕ≤ j<n + lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ≤ k ) (lemma8 refl )) + lemma3 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c + lemma3 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) + lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x + lemma11 {n} {m} {x} n<m = begin + toℕ (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)) + ≡⟨ toℕ-fromℕ≤ _ ⟩ + toℕ x + ∎ where + open ≡-Reasoning + ISO.A←B iso (elm1 elm x) = fromℕ≤ x + ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ≤ (NatP.<-trans x<n n<m ))) to<n where + x<n : toℕ x < n + x<n = toℕ<n x + to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (NatP.<-trans x<n n<m)))) < n + to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ≤ (NatP.<-trans x<n n<m) )) x<n ) + ISO.iso← iso x = lemma2 where + lemma2 : fromℕ≤ (subst (λ k → toℕ k < n) (sym + (FiniteSet.finiso← fa (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) + (sym (toℕ-fromℕ≤ (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x + lemma2 = begin + fromℕ≤ (subst (λ k → toℕ k < n) (sym + (FiniteSet.finiso← fa (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) + (sym (toℕ-fromℕ≤ (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) + ≡⟨⟩ + fromℕ≤ ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 ) + ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩ + fromℕ≤ lemma6 + ≡⟨ lemma10 (lemma11 n<m ) ⟩ + fromℕ≤ ( toℕ<n x ) + ≡⟨ fromℕ≤-toℕ _ _ ⟩ + x + ∎ where + open ≡-Reasoning + lemma6 : toℕ (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)) < n + lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ≤ (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x ) + ISO.iso→ iso (elm1 elm x) = fin-less-cong n<m fa _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where + lemma13 : toℕ (fromℕ≤ x) ≡ toℕ (FiniteSet.F←Q fa elm) + lemma13 = begin + toℕ (fromℕ≤ x) + ≡⟨ toℕ-fromℕ≤ _ ⟩ + toℕ (FiniteSet.F←Q fa elm) + ∎ where open ≡-Reasoning + lemma : FiniteSet.Q←F fa (fromℕ≤ (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm + lemma = begin + FiniteSet.Q←F fa (fromℕ≤ (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) + ≡⟨⟩ + FiniteSet.Q←F fa (fromℕ≤ ( NatP.<-trans (toℕ<n ( fromℕ≤ x ) ) n<m)) + ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ + FiniteSet.Q←F fa (fromℕ≤ ( NatP.<-trans x n<m)) + ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ≤ k )) lemma3 ⟩ + FiniteSet.Q←F fa (fromℕ≤ ( toℕ<n (FiniteSet.F←Q fa elm))) + ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ≤-toℕ _ _ ) ⟩ + FiniteSet.Q←F fa (FiniteSet.F←Q fa elm ) + ≡⟨ FiniteSet.finiso→ fa _ ⟩ + elm + ∎ where open ≡-Reasoning + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/logic.agda Thu Nov 12 11:45:34 2020 +0900 @@ -0,0 +1,91 @@ +module logic where + +open import Level +open import Relation.Nullary +open import Relation.Binary.Definitions +open import Relation.Binary.PropositionalEquality + +open import Data.Empty +open import Data.Nat hiding (_⊔_) + + +data Bool : Set where + true : Bool + false : Bool + +record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where + constructor [_,_] + field + proj1 : A + proj2 : B + +data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where + case1 : A → A ∨ B + case2 : B → A ∨ B + +_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m) +_⇔_ A B = ( A → B ) ∧ ( B → A ) + +contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A +contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) + +double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A +double-neg A notnot = notnot A + +double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A +double-neg2 notnot A = notnot ( double-neg A ) + +de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) ) +de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and )) +de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and )) + +dont-or : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B +dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a ) +dont-or {A} {B} (case2 b) ¬A = b + +dont-orb : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A +dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b ) +dont-orb {A} {B} (case1 a) ¬B = a + + +infixr 130 _∧_ +infixr 140 _∨_ +infixr 150 _⇔_ + +_/\_ : Bool → Bool → Bool +true /\ true = true +_ /\ _ = false + +_<B?_ : ℕ → ℕ → Bool +ℕ.zero <B? x = true +ℕ.suc x <B? ℕ.zero = false +ℕ.suc x <B? ℕ.suc xx = x <B? xx + +-- _<BT_ : ℕ → ℕ → Set +-- ℕ.zero <BT ℕ.zero = ⊤ +-- ℕ.zero <BT ℕ.suc b = ⊤ +-- ℕ.suc a <BT ℕ.zero = ⊥ +-- ℕ.suc a <BT ℕ.suc b = a <BT b + + +_≟B_ : Decidable {A = Bool} _≡_ +true ≟B true = yes refl +false ≟B false = yes refl +true ≟B false = no λ() +false ≟B true = no λ() + +_\/_ : Bool → Bool → Bool +false \/ false = false +_ \/ _ = true + +not_ : Bool → Bool +not true = false +not false = true + +_<=>_ : Bool → Bool → Bool +true <=> true = true +false <=> false = true +_ <=> _ = false + +infixr 130 _\/_ +infixr 140 _/\_
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/nat.agda Thu Nov 12 11:45:34 2020 +0900 @@ -0,0 +1,290 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module nat where + +open import Data.Nat +open import Data.Nat.Properties +open import Data.Empty +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Definitions +-- open import Relation.Binary.Core +open import logic + + +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ +nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x + +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ +nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x + +nat-<≡ : { x : ℕ } → x < x → ⊥ +nat-<≡ (s≤s lt) = nat-<≡ lt + +nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ +nat-≡< refl lt = nat-<≡ lt + +¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ +¬a≤a (s≤s lt) = ¬a≤a lt + +a<sa : {la : ℕ} → la < suc la +a<sa {zero} = s≤s z≤n +a<sa {suc la} = s≤s a<sa + +=→¬< : {x : ℕ } → ¬ ( x < x ) +=→¬< {zero} () +=→¬< {suc x} (s≤s lt) = =→¬< lt + +>→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) +>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x + +<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) ) +<-∨ {zero} {zero} (s≤s z≤n) = case1 refl +<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n) +<-∨ {suc x} {zero} (s≤s ()) +<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt +<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) +<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) + +max : (x y : ℕ) → ℕ +max zero zero = zero +max zero (suc x) = (suc x) +max (suc x) zero = (suc x) +max (suc x) (suc y) = suc ( max x y ) + +-- _*_ : ℕ → ℕ → ℕ +-- _*_ zero _ = zero +-- _*_ (suc n) m = m + ( n * m ) + +exp : ℕ → ℕ → ℕ +exp _ zero = 1 +exp n (suc m) = n * ( exp n m ) + +minus : (a b : ℕ ) → ℕ +minus a zero = a +minus zero (suc b) = zero +minus (suc a) (suc b) = minus a b + +_-_ = minus + +m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j +m+= {i} {j} {zero} refl = refl +m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq ) + ++m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j ++m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq ) + +less-1 : { n m : ℕ } → suc n < m → n < m +less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n +less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt) + +sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m +sa=b→a<b {0} {suc zero} refl = s≤s z≤n +sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl) + +minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x +minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl +minus+n {zero} {suc y} (s≤s ()) +minus+n {suc x} {suc y} (s≤s lt) = begin + minus (suc x) (suc y) + suc y + ≡⟨ +-comm _ (suc y) ⟩ + suc y + minus x y + ≡⟨ cong ( λ k → suc k ) ( + begin + y + minus x y + ≡⟨ +-comm y _ ⟩ + minus x y + y + ≡⟨ minus+n {x} {y} lt ⟩ + x + ∎ + ) ⟩ + suc x + ∎ where open ≡-Reasoning + + +-- open import Relation.Binary.PropositionalEquality + +-- postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n) + +-- <-≡-iff : {A B : (a b : ℕ ) → Set } → {a b : ℕ } → (A a b → B a b ) → (B a b → A a b ) → A ≡ B +-- <-≡-iff {A} {B} ab ba = {!!} + + +0<s : {x : ℕ } → zero < suc x +0<s {_} = s≤s z≤n + +<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y +<-minus-0 {x} {suc _} {zero} lt = lt +<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt + +<-minus : {x y z : ℕ } → x + z < y + z → x < y +<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt ) + +x≤x+y : {z y : ℕ } → z ≤ z + y +x≤x+y {zero} {y} = z≤n +x≤x+y {suc z} {y} = s≤s (x≤x+y {z} {y}) + +<-plus : {x y z : ℕ } → x < y → x + z < y + z +<-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y ) +<-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt) + +<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y +<-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt ) + +≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z +≤-plus {0} {y} {zero} z≤n = z≤n +≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y +≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt ) + +≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y +≤-plus-0 {x} {y} {zero} lt = lt +≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt ) + +x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z +x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n +x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 ) + +*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z +*≤ lt = *-mono-≤ lt ≤-refl + +*< : {x y z : ℕ } → x < y → x * suc z < y * suc z +*< {zero} {suc y} lt = s≤s z≤n +*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt) + +<to<s : {x y : ℕ } → x < y → x < suc y +<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n +<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt) + +<tos<s : {x y : ℕ } → x < y → suc x < suc y +<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n) +<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt) + +≤to< : {x y : ℕ } → x < y → x ≤ y +≤to< {zero} {suc y} (s≤s z≤n) = z≤n +≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y} lt) + +refl-≤s : {x : ℕ } → x ≤ suc x +refl-≤s {zero} = z≤n +refl-≤s {suc x} = s≤s (refl-≤s {x}) + +x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y +x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n +x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt) + +open import Data.Product + +minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0 +minus<=0 {0} {zero} z≤n = refl +minus<=0 {0} {suc y} z≤n = refl +minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le + +minus>0 : {x y : ℕ } → x < y → 0 < minus y x +minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n +minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt + +distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) +distr-minus-* {x} {zero} {z} = refl +distr-minus-* {x} {suc y} {z} with <-cmp x y +distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin + minus x (suc y) * z + ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩ + 0 * z + ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩ + minus (x * z) (z + y * z) + ∎ where + open ≡-Reasoning + le : x * z ≤ z + y * z + le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where + lemma : x * z ≤ y * z + lemma = *≤ {x} {y} {z} (≤to< a) +distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin + minus x (suc y) * z + ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩ + 0 * z + ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩ + minus (x * z) (z + y * z) + ∎ where + open ≡-Reasoning + lt : {x z : ℕ } → x * z ≤ z + x * z + lt {zero} {zero} = z≤n + lt {suc x} {zero} = lt {x} {zero} + lt {x} {suc z} = ≤-trans lemma refl-≤s where + lemma : x * suc z ≤ z + x * suc z + lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) +distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin + minus x (suc y) * z + suc y * z + ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩ + ( minus x (suc y) + suc y ) * z + ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩ + x * z + ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩ + minus (x * z) (suc y * z) + suc y * z + ∎ ) where + open ≡-Reasoning + lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z + lt {x} {y} {z} le = *≤ le + +minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z) +minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin + minus (minus x y) z + z + ≡⟨ minus+n {_} {z} lemma ⟩ + minus x y + ≡⟨ +m= {_} {_} {y} ( begin + minus x y + y + ≡⟨ minus+n {_} {y} lemma1 ⟩ + x + ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ + minus x (z + y) + (z + y) + ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ + minus x (z + y) + z + y + ∎ ) ⟩ + minus x (z + y) + z + ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ + minus x (y + z) + z + ∎ ) where + open ≡-Reasoning + lemma1 : suc x > y + lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt ) + lemma : suc (minus x y) > z + lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt ) + +minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M +minus-* {zero} {k} {n} lt = begin + minus k (suc n) * zero + ≡⟨ *-comm (minus k (suc n)) zero ⟩ + zero * minus k (suc n) + ≡⟨⟩ + 0 * minus k n + ≡⟨ *-comm 0 (minus k n) ⟩ + minus (minus k n * 0 ) 0 + ∎ where + open ≡-Reasoning +minus-* {suc m} {k} {n} lt with <-cmp k 1 +minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl +minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl +minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl +minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt +minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c +minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin + minus k (suc n) * M + ≡⟨ distr-minus-* {k} {suc n} {M} ⟩ + minus (k * M ) ((suc n) * M) + ≡⟨⟩ + minus (k * M ) (M + n * M ) + ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩ + minus (k * M ) ((n * M) + M ) + ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩ + minus (minus (k * M ) (n * M)) M + ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩ + minus (minus k n * M ) M + ∎ where + M = suc m + lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m + lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y )) + lemma {suc n} {suc k} {m} lt = begin + suc (suc m + suc n * suc m) + ≡⟨⟩ + suc ( suc (suc n) * suc m) + ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩ + suc (suc k * suc m) + ∎ where open ≤-Reasoning + open ≡-Reasoning
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/nfa.agda Thu Nov 12 11:45:34 2020 +0900 @@ -0,0 +1,109 @@ +module nfa where +open import Level renaming ( suc to Suc ; zero to Zero ) + +open import Relation.Binary.PropositionalEquality +open import Data.List +open import automaton +open import logic + +record NAutomaton {n : Level} ( Q : Set n ) ( Σ : Set ) + : Set (Suc n) where + field + Nδ : Q → Σ → Q → Set + NF : Q → Set + Nexists : (Q → Set) → Set + +open NAutomaton + +naccept : {n : Level} {Q : Set n} {Σ : Set} → NAutomaton Q Σ → (Q → Set) → List Σ → Set +naccept {n} {Q} {Σ} nfa qs [] = Nexists nfa (λ q → qs q ∧ NF nfa q ) +naccept {n} {Q} {Σ} nfa qs (x ∷ input) = + Nexists nfa (λ q → qs q ∧ (naccept nfa (Nδ nfa q x) input )) + +ntrace : {n : Level} {Q : Set n} {Σ : Set } → (NFA : NAutomaton Q Σ) → (start : Q → Set ) → (input : List Σ ) → naccept NFA start input + → ((Q → Set) → List Q) + → List (List Q) +ntrace {n} {Q} {Σ} A q [] a list = list q ∷ [] +ntrace {n} {Q} {Σ} A q (x ∷ t) a list = list q ∷ ( ntrace A {!!} t {!!} list ) + +data transition136 : Q3 → Σ2 → Q3 → Set where + d0 : transition136 q₁ s1 q₂ + d1 : transition136 q₁ s0 q₁ + d2 : transition136 q₂ s0 q₂ + d3 : transition136 q₂ s0 q₃ + d4 : transition136 q₂ s1 q₃ + d5 : transition136 q₃ s0 q₁ + +start136 : Q3 → Set +start136 q = q ≡ q₁ + +nfa136 : NAutomaton Q3 Σ2 +nfa136 = record { Nδ = transition136 ; NF = λ q → q ≡ q₁ ; Nexists = exists-in-Q3 } + +example136-1 = naccept nfa136 start136 ( s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) + +example136-0 = naccept nfa136 start136 ( s0 ∷ [] ) + +example136-2 = naccept nfa136 start136 ( s1 ∷ s0 ∷ s1 ∷ s0 ∷ s1 ∷ [] ) + +-- +-- ((Q → Set) → Set) → ((Q → Set) → Set) → Set +-- + +data Nexists→exits {n : Level} { Q : Set n } {Σ : Set} ( NFA : NAutomaton Q Σ ) : ((Q → Set) → Set) → Set where + one-of : Nexists→exits NFA (Nexists NFA) + +subset-construction : {n : Level} { Q : Set n } { Σ : Set } → + (NAutomaton Q Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ +subset-construction {n} {Q} { Σ} NFA = record { + δ = λ qs x qs → Nexists NFA (λ q → Nδ NFA q x qs ) + ; F = λ qs → Nexists NFA ( λ q → NF NFA q ) + ; exists = Nexists→exits NFA -- what this means? + } + +subset-construction-lemma→ : { Q : Set } { Σ : Set } → + (NFA : NAutomaton Q Σ ) → (astart : Q → Set ) + → (x : List Σ) + → naccept NFA ( λ q1 → astart q1) x + → accept ( subset-construction NFA ) ( λ q1 → astart q1) x +subset-construction-lemma→ = {!!} + +subset-construction-lemma← : { Q : Set } { Σ : Set } → + (NFA : NAutomaton Q Σ ) → (astart : Q → Set ) + → (x : List Σ) + → accept ( subset-construction NFA ) ( λ q1 → astart q1) x + → naccept NFA ( λ q1 → astart q1) x +subset-construction-lemma← = {!!} + +open import regular-language + +open RegularLanguage +open Automaton +open import Data.Empty + +Concat-exists : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → (states A ∨ states B → Set) → Set +Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ q → P (case2 q)) + +Concat-NFA : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ +Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend ; Nexists = Concat-exists A B } + module Concat-NFA where + data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where + a-case : {q : states A} {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i)) + ab-trans : {q : states A} {i : Σ } → F (automaton A) q → δnfa ( case1 q) i (case2 (δ (automaton B) (astart B) i)) + b-case : {q : states B} {i : Σ } → δnfa ( case2 q) i (case2 (δ (automaton B) q i)) + nend : states A ∨ states B → Set + nend (case2 q) = F (automaton B) q + nend (case1 q) = F (automaton A) q ∧ F (automaton B) (astart B) -- empty B case + +data state-is {n : Level} {Σ : Set } (A : RegularLanguage {n} Σ ) : (a : states A ) → Set where + this : (a : states A) → state-is A a + +closed-in-concat : {n : Level} {Σ : Set } → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) + → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A) + ; automaton = subset-construction ( Concat-NFA A B )} +closed-in-concat {Σ} A B x = {!!} + + + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/regular-language.agda Thu Nov 12 11:45:34 2020 +0900 @@ -0,0 +1,97 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module regular-language where + +open import Level renaming ( suc to Suc ; zero to Zero ) +open import Data.List +-- open import Data.Nat hiding ( _≟_ ) +-- open import Data.Bool +-- open import Data.Fin hiding ( _+_ ) +open import Data.Empty +open import Data.Unit +open import Data.Product +open import Data.Maybe +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Binary.Definitions +open import logic +open import nat +open import automaton +-- open import finiteSet + +language : { Σ : Set } → Set (Suc Zero) +language {Σ} = List Σ → Set + +open Automaton + +record RegularLanguage {n : Level} ( Σ : Set ) : Set (Level.suc n ) where + field + states : Set n + astart : states + automaton : Automaton states Σ + contain : List Σ → Set + contain x = accept automaton astart x + +split : {Σ : Set} → (List Σ → Set) + → ( List Σ → Set) → List Σ → Set +split x y [] = x [] ∧ y [] +split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ + split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t + +Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} +Union {Σ} A B x = (A x ) ∨ (B x) + +Concat : {n : Level} {Σ : Set } → ( A B : language {Σ} ) → language {Σ} +Concat {Σ} A B = split A B + +{-# TERMINATING #-} +Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ} +Star {Σ} A = split A ( Star {Σ} A ) + +data In2 : Set where + i0 : In2 + i1 : In2 + +test-AB→split : {Σ : Set} → {A B : List In2 → Set} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ ( + ( A [] ∧ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) ∨ + ( A ( i0 ∷ [] ) ∧ B ( i1 ∷ i0 ∷ [] ) ) ∨ + ( A ( i0 ∷ i1 ∷ [] ) ∧ B ( i0 ∷ [] ) ) ∨ + ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) ∧ B [] ) + ) +test-AB→split {_} {A} {B} = refl + +open RegularLanguage +isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set (Suc Zero) +isRegular A x r = A x ≡ contain r x + +-- +-- (states A × states B → Set) → ( states A → Set ) → ( states B → Set ) → Set +-- +exists-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → (states A × states B → Set) → Set +exists-Union A B Pab = exists (automaton A) (λ qa → exists (automaton B) (λ qb → Pab (qa , qb)) ) + +M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ +M-Union {n} {Σ} A B = record { + states = states A × states B + ; astart = ( astart A , astart B ) + ; automaton = record { + δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x ) + ; F = λ q → ( F (automaton A) (proj₁ q) ∨ F (automaton B) (proj₂ q) ) + ; exists = exists-Union A B + } + } + +closed-in-union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B ) +closed-in-union A B [] = lemma where + lemma : F (automaton A) (astart A) ∨ F (automaton B) (astart B) ≡ + F (automaton A) (astart A) ∨ F (automaton B) (astart B) + lemma = refl +closed-in-union {n} {Σ} A B ( h ∷ t ) = lemma4 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where + lemma4 : (t : List Σ) → (qa : states A ) → (qb : states B ) → + accept (automaton A) qa t ∨ accept (automaton B) qb t + ≡ accept (automaton (M-Union A B)) (qa , qb) t + lemma4 [] qa qb = refl + lemma4 (h ∷ t ) qa qb = lemma4 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h)) + +-- closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x {!!} +-- closed-in-concat = {!!} +