Mercurial > hg > Members > kono > Proof > automaton
changeset 406:a60132983557
...
line wrap: on
line diff
--- a/a02/agda/data1.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/a02/agda/data1.agda Wed Nov 08 21:35:54 2023 +0900 @@ -28,20 +28,20 @@ open _∧_ ex3' : {A B : Set} → ( A ∨ B ) → A ∧ B -- this is wrong -ex3' = ? +ex3' (case1 x) = ? +ex3' (case2 x) = ? ex4' : {A B : Set} → ( A ∧ B ) → A ∨ B -ex4' ab = case1 (proj1 ab ) +ex4' ⟪ a , b ⟫ = ? --- ex5 : {A B C : Set} → (( A → C ) ∨ ( B → C ) ) → ( ( A ∨ B ) → C ) is wrong ex5 : {A B C : Set} → (( A → C ) ∨ ( B → C ) ) → ( ( A ∧ B ) → C ) -ex5 (case1 a→c) ab = a→c (proj1 ab) -ex5 (case2 b→c) ab = b→c (proj2 ab) +ex5 = ? data ⊥ : Set where -⊥-elim : {A : Set } -> ⊥ -> A -⊥-elim = {!!} +⊥-elim : {A : Set } → ⊥ → A +⊥-elim () ¬_ : Set → Set ¬ A = A → ⊥ @@ -76,6 +76,36 @@ problem2 = {!!} +data Nat : Set where + zero : Nat + suc : Nat → Nat + +one : Nat +one = suc zero + +five : Nat +five = suc (suc (suc (suc (suc zero)))) + +add : ( a b : Nat ) → Nat +add zero x = x +add (suc x) y = suc ( add x y ) + +data _≡_ {A : Set } : ( x y : A ) → Set where + refl : {x : A} → x ≡ x + +test11 : add one five ≡ suc five +test11 = refl + +mul : ( a b : Nat ) → Nat +mul zero x = zero +mul (suc x) y = add y (mul x y) + +ex6 : Nat +ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) + +ex7 : mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) ≡ suc (suc (suc (suc (suc (suc zero))))) +ex7 = refl + data Three : Set where t1 : Three t2 : Three @@ -95,27 +125,24 @@ r2 : 3Ring t2 t3 r3 : 3Ring t3 t1 -data Nat : Set where - zero : Nat - suc : Nat → Nat - -add : ( a b : Nat ) → Nat -add zero x = x -add (suc x) y = suc ( add x y ) - -mul : ( a b : Nat ) → Nat -mul zero x = zero -mul (suc x) y = add y (mul x y) - -ex6 : Nat -ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) - data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where direct : E x y -> connected E x y indirect : { z : V } -> E x z -> connected {V} E z y -> connected E x y -dag : { V : Set } ( E : V -> V -> Set ) -> Set +dag : { V : Set } ( E : V -> V -> Set ) → Set dag {V} E = ∀ (n : V) → ¬ ( connected E n n ) lemma : ¬ (dag 3Ring ) -lemma r = r t1 ( indirect r1 (indirect r2 (direct r3 ))) +lemma r = ? + +-- t1 → t2 → t3 +-- +data 3Line : (dom cod : Three) → Set where + line1 : 3Line t1 t2 + line2 : 3Line t2 t3 + +lemma1 : dag 3Line +lemma1 = ? + + +
--- a/a02/agda/equality.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/a02/agda/equality.agda Wed Nov 08 21:35:54 2023 +0900 @@ -1,26 +1,26 @@ module equality where -data _==_ {A : Set } : A → A → Set where - refl : {x : A} → x == x +data _≡_ {A : Set } : A → A → Set where + refl : {x : A} → x ≡ x -ex1 : {A : Set} {x : A } → x == x +ex1 : {A : Set} {x : A } → x ≡ x ex1 = ? -ex2 : {A : Set} {x y : A } → x == y → y == x +ex2 : {A : Set} {x y : A } → x ≡ y → y ≡ x ex2 = ? -ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z +ex3 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z ex3 = {!!} -ex4 : {A B : Set} {x y : A } { f : A → B } → x == y → f x == f y +ex4 : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y ex4 = {!!} -subst : {A : Set } → { x y : A } → ( f : A → Set ) → x == y → f x → f y +subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y subst {A} {x} {y} f refl fx = fx --- ex5 : {A : Set} {x y z : A } → x == y → y == z → x == z --- ex5 {A} {x} {y} {z} x==y y==z = subst (λ refl → {!!} ) x==y {!!} +-- ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z +-- ex5 {A} {x} {y} {z} x≡y y≡z = subst (λ refl → {!!} ) x≡y {!!}
--- a/a02/agda/logic.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/a02/agda/logic.agda Wed Nov 08 21:35:54 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module logic where open import Level
--- a/a02/agda/practice-nat.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/a02/agda/practice-nat.agda Wed Nov 08 21:35:54 2023 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible --safe #-} module practice-nat where open import Data.Nat @@ -6,24 +7,29 @@ open import Relation.Binary.PropositionalEquality hiding (_⇔_) open import logic +-- data _<=_ : ℕ → ℕ → Set where +-- z<=n : {x : ℕ} → zero <= x +-- s<=s : {x y : ℕ} → x <= y → suc x <= suc y + -- hint : it has two inputs, use recursion nat-<> : { x y : ℕ } → x < y → y < x → ⊥ -nat-<> = {!!} +nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x -- hint : use recursion nat-<≡ : { x : ℕ } → x < x → ⊥ -nat-<≡ = {!!} +nat-<≡ (s≤s x<x) = nat-<≡ x<x -- hint : use refl and recursion nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ -nat-≡< = {!!} +nat-≡< refl (s≤s x<y) = nat-≡< refl x<y ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ -¬a≤a = {!!} +¬a≤a (s≤s lt) = ¬a≤a lt -- hint : make case with la first -a<sa : {la : ℕ} → la < suc la -a<sa = {!!} +a<sa : {i : ℕ} → i < suc i +a<sa {zero} = s≤s z≤n +a<sa {suc i} = s≤s a<sa -- hint : ¬ has an input, use recursion =→¬< : {x : ℕ } → ¬ ( x < x )
--- a/a02/lecture.ind Sun Sep 24 18:02:04 2023 +0900 +++ b/a02/lecture.ind Wed Nov 08 21:35:54 2023 +0900 @@ -22,6 +22,7 @@ 論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。 +この章の内容は基本的には Girad 先生の Proofs and Typesに書いてある内容です。 --あらすじ @@ -162,7 +163,7 @@ record によって - record _∧_ A B : Set + record _∧_ A B : Set where field π1 : A π2 : B @@ -177,7 +178,7 @@ とかける。(Haskell では (∧) を使う) -は、型Aと型Bから作るデ0ータ構造である。オブジェクトあるいは構造体だと思って良い。 +は、型Aと型Bから作るデータ構造である。オブジェクトあるいは構造体だと思って良い。 record { π1 = x ; π2 = y }
--- a/automaton-in-agda/src/finiteSetUtil.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/automaton-in-agda/src/finiteSetUtil.agda Wed Nov 08 21:35:54 2023 +0900 @@ -371,6 +371,10 @@ Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl } +-- +-- fin→ is in finiteFunc.agda +-- we excludeit becauase it uses f-extensionarity + open import Data.List open FiniteSet
--- a/automaton-in-agda/src/flcagl.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/automaton-in-agda/src/flcagl.agda Wed Nov 08 21:35:54 2023 +0900 @@ -1,6 +1,35 @@ {-# OPTIONS --cubical-compatible #-} +{-# OPTIONS --sized-types #-} -{-# OPTIONS --sized-types #-} +-- +-- induction +-- data aaa where +-- aend : aaa +-- bb : (y : aaa) → aaa +-- cc : (y : aaa) → aaa +-- +-- (x : aaa) → bb → cc → aend +-- induction : ( P : aaa → Set ) → (x : aaa) → P x +-- induction P aend = ? +-- induction P (bb y) = ? where +-- lemma : P y +-- lemma = induction P y +-- induction P (cc y) = ? +-- +-- ∙ +-- / \ +-- bb cc +-- / +-- aend + +-- +-- coinduction +-- record AAA : Set where +-- field +-- bb : (y : AAA) +-- cc : (y : AAA) + + open import Relation.Nullary open import Relation.Binary.PropositionalEquality module flcagl @@ -11,6 +40,7 @@ -- open import Data.Maybe open import Level renaming ( zero to Zero ; suc to succ ) open import Size +open import Data.Empty module List where @@ -50,6 +80,14 @@ ν (trie f) = f [] δ (trie f) a = trie (λ as → f (a ∷ as)) + -- trie' : ∀{i} (f : List i A → Bool) → Lang i + -- trie' {i} f = record { + -- ν = f [] + -- ; δ = λ {j} a → lem {j} a -- we cannot write in this way + -- } where + -- lem : {j : Size< i} → A → Lang j + -- lem {j} a = trie' (λ as → f (a ∷ as)) + ∅ : ∀{i} → Lang i ν ∅ = false δ ∅ x = ∅ @@ -78,6 +116,33 @@ ν (k · l) = ν k ∧ ν l δ (k · l) x = let k′l = δ k x · l in if ν k then k′l ∪ δ l x else k′l + _+_ : ∀{i} (k l : Lang i) → Lang i + ν (k + l) = ν k ∧ ν l + δ (k + l) x with ν k + ... | false = δ k x + l + ... | true = (δ k x + l ) ∪ δ l x + + language : { Σ : Set } → Set + language {Σ} = List ∞ Σ → Bool + + split : {Σ : Set} → {i : Size } → (x y : language {Σ} ) → language {Σ} + split x y [] = x [] ∨ y [] + split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ + split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t + + LtoSplit : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ true → split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true + LtoSplit x y [] xy with ν x | ν y + ... | true | true = refl + LtoSplit x y (h ∷ z) xy = ? + + SplitoL : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ false → split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false + SplitoL x y [] xy with ν x | ν y + ... | false | false = refl + ... | false | true = ? + ... | true | false = ? + SplitoL x y (h ∷ z) xy = ? + + _*_ : ∀{i} (k l : Lang i ) → Lang i ν (k * l) = ν k ∧ ν l δ (_*_ {i} k l) {j} x = @@ -476,9 +541,9 @@ Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x )) Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) -nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i -Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa {!!} -Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) +-- nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i +-- Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa {!!} +-- Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) -- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i -- Lang.ν (nlang' nfa s) = DA.ν nfa s
--- a/automaton-in-agda/src/logic.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/automaton-in-agda/src/logic.agda Wed Nov 08 21:35:54 2023 +0900 @@ -58,7 +58,7 @@ false \/ false = false _ \/ _ = true -not_ : Bool → Bool +not : Bool → Bool not true = false not false = true
--- a/automaton-in-agda/src/nfa.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/automaton-in-agda/src/nfa.agda Wed Nov 08 21:35:54 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} +-- {-# OPTIONS --allow-unsolved-metas #-} module nfa where -- open import Level renaming ( suc to succ ; zero to Zero ) @@ -54,6 +55,12 @@ → ( Qs : Q → Bool ) → (s : Σ ) → ( Q → Bool ) Nmoves {Q} { Σ} M exists Qs s = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q ) )) +-- +-- Q is finiteSet +-- so we have +-- exists : ( P : Q → Bool ) → Bool +-- which checks if there is a q in Q such that P q is true + Naccept : { Q : Set } { Σ : Set } → NAutomaton Q Σ → (exists : ( Q → Bool ) → Bool) @@ -61,45 +68,22 @@ Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q ) Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t -{-# TERMINATING #-} -NtraceDepth : { Q : Set } { Σ : Set } - → NAutomaton Q Σ - → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → List (List ( Σ ∧ Q )) -NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where - ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) ) - ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q )) - ndepth1 q i [] is t t1 = t1 - ndepth1 q i (x ∷ qns) is t t1 = ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 ) - ndepth [] sb is t t1 = t1 - ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q - ... | true = ndepth qs sb [] t ( t ∷ t1 ) - ... | false = ndepth qs sb [] t t1 - ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q - ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 ) - ... | false = ndepth qs sb (i ∷ is) t t1 - -NtraceDepth1 : { Q : Set } { Σ : Set } - → NAutomaton Q Σ - → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → Bool ∧ List (List ( Σ ∧ Q )) -NtraceDepth1 {Q} {Σ} M sb all is = ndepth all sb is [] [] where - exists : (Q → Bool) → Bool - exists p = exists1 all where - exists1 : List Q → Bool - exists1 [] = false - exists1 (q ∷ qs) with p q - ... | true = true - ... | false = exists1 qs - ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (Bool ∧ List ( Σ ∧ Q ) ) → Bool ∧ List (List ( Σ ∧ Q ) ) - ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( Bool ∧ List ( Σ ∧ Q )) → List ( Bool ∧ List ( Σ ∧ Q )) - ndepth1 q i [] is t t1 = t1 - ndepth1 q i (x ∷ qns) is t t1 = ? -- ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 ) - ndepth [] sb is t t1 = ? -- ⟪ exists (λ q → Nend M q /\ sb q) ? ⟫ - ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q - ... | true = ndepth qs sb [] t ( ? ∷ t1 ) - ... | false = ndepth qs sb [] t t1 - ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q - ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 ) - ... | false = ndepth qs sb (i ∷ is) t t1 +-- {-# TERMINATING #-} +-- NtraceDepth : { Q : Set } { Σ : Set } +-- → NAutomaton Q Σ +-- → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → List (List ( Σ ∧ Q )) +-- NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where +-- ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) ) +-- ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q )) +-- ndepth1 q i [] is t t1 = t1 +-- ndepth1 q i (x ∷ qns) is t t1 = ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 ) +-- ndepth [] sb is t t1 = t1 +-- ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q +-- ... | true = ndepth qs sb [] t ( t ∷ t1 ) +-- ... | false = ndepth qs sb [] t t1 +-- ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q +-- ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 ) +-- ... | false = ndepth qs sb (i ∷ is) t t1 -- trace in state set -- @@ -156,9 +140,9 @@ t-1 : List ( List States1 ) t-1 = Ntrace am2 LStates1 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ (sr ∷ ss ∷ st ∷ []) ∷ (st ∷ []) ∷ [] t-2 = Ntrace am2 LStates1 existsS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ [] ∷ [] -t-3 = NtraceDepth am2 start1 LStates1 ( i1 ∷ i1 ∷ i1 ∷ [] ) -t-4 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ i0 ∷ [] ) -t-5 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ [] ) +-- t-3 = NtraceDepth am2 start1 LStates1 ( i1 ∷ i1 ∷ i1 ∷ [] ) +-- t-4 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ i0 ∷ [] ) +-- t-5 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ [] ) transition4 : States1 → In2 → States1 → Bool transition4 sr i0 sr = true
--- a/automaton-in-agda/src/regular-concat.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/automaton-in-agda/src/regular-concat.agda Wed Nov 08 21:35:54 2023 +0900 @@ -1,4 +1,10 @@ -module regular-concat where +{-# OPTIONS --cubical-compatible --safe #-} + +open import finiteSet +open import logic +-- open import finiteFunc -- we can prove fin→ , but it is unsafe + +module regular-concat (fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool )) where open import Level renaming ( suc to Suc ; zero to Zero ) open import Data.List @@ -10,18 +16,17 @@ -- open import Data.Maybe open import Relation.Nullary open import Relation.Binary.PropositionalEquality hiding ( [_] ) -open import logic open import nat open import automaton open import regular-language open import nfa open import sbconst2 -open import finiteSet open import finiteSetUtil open Automaton open FiniteSet +open Split open RegularLanguage @@ -56,93 +61,10 @@ finf : FiniteSet (states A ∨ states B → Bool ) finf = fin→ fin --- closed-in-concat' : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B ) --- closed-in-concat' {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where --- closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true --- closed-in-concat→ = {!!} --- closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true --- closed-in-concat← = {!!} - -record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where - field - sp0 : List Σ - sp1 : List Σ - sp-concat : sp0 ++ sp1 ≡ x - prop0 : A sp0 ≡ true - prop1 : B sp1 ≡ true - -open Split - -list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] ) -list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl } -list-empty++ [] (x ∷ y) () -list-empty++ (x ∷ x₁) y () - open _∧_ open import Relation.Binary.PropositionalEquality hiding ( [_] ) -c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true - → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) - → split (λ t1 → A (h ∷ t1)) B t ≡ true -c-split-lemma {Σ} A B h t eq p = sym ( begin - true - ≡⟨ sym eq ⟩ - split A B (h ∷ t ) - ≡⟨⟩ - A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t - ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩ - false \/ split (λ t1 → A (h ∷ t1)) B t - ≡⟨ bool-or-1 refl ⟩ - split (λ t1 → A (h ∷ t1)) B t - ∎ ) where - open ≡-Reasoning - lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false - lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A ) - lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B ) - -split→AB : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x -split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true -split→AB {Σ} A B [] eq | yes eqa | yes eqb = - record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb } -split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p )) -split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p )) -split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true -... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py } -... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) ) -... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } -split→AB {Σ} A B (h ∷ t ) eq | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) ) -... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } - -AB→split : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true -AB→split {Σ} A B [] [] eqa eqb = begin - split A B [] - ≡⟨⟩ - A [] /\ B [] - ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩ - true - ∎ where open ≡-Reasoning -AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin - split A B (h ∷ y ) - ≡⟨⟩ - A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y - ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩ - true /\ true \/ split (λ t1 → A (h ∷ t1)) B y - ≡⟨⟩ - true \/ split (λ t1 → A (h ∷ t1)) B y - ≡⟨⟩ - true - ∎ where open ≡-Reasoning -AB→split {Σ} A B (h ∷ t) y eqa eqb = begin - split A B ((h ∷ t) ++ y) - ≡⟨⟩ - A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y) - ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩ - A [] /\ B (h ∷ t ++ y) \/ true - ≡⟨ bool-or-3 ⟩ - true - ∎ where open ≡-Reasoning - open NAutomaton open import Data.List.Properties @@ -204,28 +126,38 @@ → (qa : states A ) → ( (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x ) → split (accept (automaton A) qa ) (contain B) x ≡ true contain-A [] nq fn qa cond with found← finab fn -- at this stage, A and B must be satisfied with [] (ab-case cond forces it) - ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) - ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S) - ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S))) + ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S)) + ... | case1 qa' | refl = lemma11 where + lemma12 : found-q S ≡ case1 qa → aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ Concat-NFA.nend A B (found-q S) + lemma12 refl = refl + lemma11 : aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ true + lemma11 = trans (lemma12 eq) ( bool-∧→tt-1 (found-p S) ) + ... | case2 qb | ab = ⊥-elim ( ab (lemma11 eq) ) where + lemma11 : found-q S ≡ case2 qb → aend (automaton B) qb ≡ true + lemma11 refl = bool-∧→tt-1 (found-p S) contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true ... | yes eq = bool-or-41 eq -- found A ++ B all end ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion --- prove ab-case condition (we haven't checked but case2 b may happen) lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t lemma11 (case1 qa') ex with found← finab ex - ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) - ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A) ( bool-∧→tt-1 (found-p S) )) -- continued A case - ... | case2 qb | record { eq = refl } | nb with bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false - ... | () + ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S)) + ... | case1 qa2 | refl = sym ( equal→refl (afin A) (lemma12 eq) ) where -- continued A case + lemma12 : found-q S ≡ case1 qa2 → equal? (afin A) (δ (automaton A) qa2 h) qa' ≡ true + lemma12 refl = bool-∧→tt-1 (found-p S) + ... | case2 qb | nb = ⊥-elim (¬-bool refl ((lemma12 eq)) ) where -- δnfa (case2 q) i (case1 q₁) is false + lemma12 : found-q S ≡ case2 qb → false ≡ true + lemma12 refl = bool-∧→tt-1 (found-p S) lemma11 (case2 qb) ex with found← finab ex - ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) - lemma11 (case2 qb) ex | S | case2 qb' | record { eq = refl } | nb = contra-position lemma13 nb where -- continued B case should fail - lemma13 : accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true - lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb - lemma11 (case2 qb) ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S) - ... | eee = contra-position lemma12 ne where -- starting B case should fail - lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true - lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb ) + ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S)) + lemma11 (case2 qb) ex | S | case2 qb' | nb = contra-position (lemma13 eq) nb where -- continued B case should fail + lemma13 : found-q S ≡ case2 qb' → accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true + lemma13 refl fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb + lemma11 (case2 qb) ex | S | case1 qa | refl with bool-∧→tt-1 (found-p S) + ... | eee = contra-position (lemma12 eq) ne where -- starting B case should fail + lemma12 : found-q S ≡ case1 qa → + accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true + lemma12 refl fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb ) lemma10 : Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x ≡ true → split (contain A) (contain B) x ≡ true lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where
--- a/automaton-in-agda/src/regular-language.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/automaton-in-agda/src/regular-language.agda Wed Nov 08 21:35:54 2023 +0900 @@ -53,6 +53,19 @@ Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool Star {Σ} x y = repeat x y +-- We have to prove definitions of Concat and Star are equivalent to the set theoretic definitions + +-- 1. A ∪ B = { x | x ∈ A \/ x ∈ B } +-- 2. A ∘ B = { x | ∃ y ∈ A, z ∈ B, x = y ++ z } +-- 3. A* = { x | ∃ n ∈ ℕ, y1, y2, ..., yn ∈ A, x = y1 ++ y2 ++ ... ++ yn } + +-- lemma-Union : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) → Union A B x ≡ ( A x \/ B x ) +-- lemma-Union = ? + +-- lemma-Concat : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) +-- → Concat A B x ≡ ( ∃ λ y → ∃ λ z → A y /\ B z /\ x ≡ y ++ z ) +-- lemma-Concat = ? + open import automaton-ex test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ ( @@ -119,3 +132,84 @@ lemma1 [] qa qb = refl lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h)) + + +record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where + field + sp0 sp1 : List Σ + sp-concat : sp0 ++ sp1 ≡ x + prop0 : A sp0 ≡ true + prop1 : B sp1 ≡ true + +open Split + +list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] ) +list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl } +list-empty++ [] (x ∷ y) () +list-empty++ (x ∷ x₁) y () + +open _∧_ + +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true + → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) + → split (λ t1 → A (h ∷ t1)) B t ≡ true +c-split-lemma {Σ} A B h t eq p = sym ( begin + true + ≡⟨ sym eq ⟩ + split A B (h ∷ t ) + ≡⟨⟩ + A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t + ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩ + false \/ split (λ t1 → A (h ∷ t1)) B t + ≡⟨ bool-or-1 refl ⟩ + split (λ t1 → A (h ∷ t1)) B t + ∎ ) where + open ≡-Reasoning + lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false + lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A ) + lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B ) + +split→AB : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x +split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true +split→AB {Σ} A B [] eq | yes eqa | yes eqb = + record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb } +split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p )) +split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p )) +split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true +... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py } +... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) ) +... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } +split→AB {Σ} A B (h ∷ t ) eq | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) ) +... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } + +AB→split : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true +AB→split {Σ} A B [] [] eqa eqb = begin + split A B [] + ≡⟨⟩ + A [] /\ B [] + ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩ + true + ∎ where open ≡-Reasoning +AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin + split A B (h ∷ y ) + ≡⟨⟩ + A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y + ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩ + true /\ true \/ split (λ t1 → A (h ∷ t1)) B y + ≡⟨⟩ + true \/ split (λ t1 → A (h ∷ t1)) B y + ≡⟨⟩ + true + ∎ where open ≡-Reasoning +AB→split {Σ} A B (h ∷ t) y eqa eqb = begin + split A B ((h ∷ t) ++ y) + ≡⟨⟩ + A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y) + ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩ + A [] /\ B (h ∷ t ++ y) \/ true + ≡⟨ bool-or-3 ⟩ + true + ∎ where open ≡-Reasoning +
--- a/automaton-in-agda/src/root2.agda Sun Sep 24 18:02:04 2023 +0900 +++ b/automaton-in-agda/src/root2.agda Wed Nov 08 21:35:54 2023 +0900 @@ -197,8 +197,24 @@ d2 * (Rational.i r * Rational.i r) ∎ ) ⟩ Rational.i r * Rational.i r ∎ where open ≡-Reasoning +-- data _≤_ : (i j : ℕ) → Set where +-- z≤n : {n : ℕ} → zero ≤ n +-- s≤s : {i j : ℕ} → i ≤ j → (suc i) ≤ (suc j) + *<-2 : {x y z : ℕ} → z > 0 → x < y → z * x < z * y -*<-2 {x} {y} {suc z} (s≤s z>0) x<y = ? -- *-monoʳ-< z x<y +*<-2 {zero} {suc y} {suc z} (s≤s z>0) x<y = begin + suc (z * zero) ≡⟨ cong suc (*-comm z _) ⟩ + suc (zero * z) ≡⟨ refl ⟩ + suc zero ≤⟨ s≤s z≤n ⟩ + suc (y + z * suc y) ∎ where open ≤-Reasoning +*<-2 {x} {y} {suc zero} (s≤s z>0) x<y = begin + suc (x + zero) ≡⟨ cong suc (+-comm x _) ⟩ + suc x ≤⟨ x<y ⟩ + y ≡⟨ +-comm zero _ ⟩ + y + zero ∎ where open ≤-Reasoning +*<-2 {x} {y} {suc (suc z)} (s≤s z>0) x<y = begin + suc (x + (x + z * x)) <⟨ +-mono-≤-< x<y (*<-2 {x} {y} {suc z} (s≤s z≤n) x<y) ⟩ + y + (y + z * y) ∎ where open ≤-Reasoning r15 : {p : ℕ} → p > 1 → p < p * p r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )