Mercurial > hg > Members > kono > Proof > automaton

changeset 52:8438c989d5a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 02 Oct 2019 13:19:44 +0900
parents bc0400528027
children f443cd9de556
files a02/agda/practice-logic.agda a02/agda/practice-nat.agda agda/flcagl.agda
diffstat 3 files changed, 199 insertions(+), 48 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/practice-logic.agda	Wed Oct 02 13:19:44 2019 +0900
@@ -0,0 +1,74 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module practice-logic where
+
+postulate A : Set
+postulate B : Set
+
+Lemma1 : Set
+Lemma1 = A -> ( A -> B ) -> B
+
+lemma1 : Lemma1
+lemma1 a b = {!!}
+
+-- lemma1 a a-b = a-b a
+
+lemma2 : Lemma1
+lemma2 = \a b -> {!!}
+
+-- lemma1 = \a a-b -> a-b a
+-- lemma1 = \a b -> b a
+-- lemma1  a b = b a
+
+lemma3 : Lemma1
+lemma3 = \a -> ( \b -> {!!} )
+
+record _∧_ (A B : Set) : Set where
+   field 
+      and1 : A
+      and2 : B
+
+data _∧d_ ( A B : Set ) : Set where
+  and : A -> B -> A ∧d B
+
+Lemma4 : Set
+Lemma4 = B -> A -> (B ∧ A)
+
+lemma4 : Lemma4
+lemma4 = \b -> \a -> {!!}
+
+Lemma5 : Set
+Lemma5 = (A ∧ B) -> B
+
+lemma5 : Lemma5
+lemma5 = \a -> {!!}
+
+data _∨_  (A B : Set) : Set where
+  or1 : A -> A ∨ B
+  or2 : B -> A ∨ B
+
+Lemma6  : Set
+Lemma6 = B -> ( A ∨ B )
+
+lemma6 : Lemma6
+lemma6 = \b ->  {!!}
+
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+
+contra-position :  {A : Set } {B : Set } → (A → B) → ¬ B → ¬ A
+contra-position {A} {B}  f ¬b a = {!!}
+
+double-neg :  {A : Set } → A → ¬ ¬ A
+double-neg = {!!}
+
+double-neg2 :  {A : Set } → ¬ ¬ ¬ A → ¬ A
+double-neg2 = {!!}
+
+de-morgan :  {A B : Set } →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {A} {B} = {!!}
+
+dont-or : {A  : Set } { B : Set  } →  A ∨ B → ¬ A → B
+dont-or {A} {B} = {!!}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/practice-nat.agda	Wed Oct 02 13:19:44 2019 +0900
@@ -0,0 +1,79 @@
+module practice-nat where
+
+open import Data.Nat 
+open import Data.Empty
+open import Relation.Nullary
+open import  Relation.Binary.PropositionalEquality
+open import  practice-logic
+
+
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<>  = {!!}
+
+nat-<≡ : { x : ℕ } → x < x → ⊥
+nat-<≡  = {!!}
+
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
+nat-≡< = {!!}
+
+¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
+¬a≤a  = {!!}
+
+a<sa : {la : ℕ} → la < suc la 
+a<sa = {!!}
+
+=→¬< : {x : ℕ  } → ¬ ( x < x )
+=→¬< = {!!}
+
+>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
+>→¬< = {!!}
+
+<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ = {!!}
+
+max : (x y : ℕ) → ℕ
+max = {!!}
+
+sum :  (x y : ℕ) → ℕ
+sum = {!!}
+
+sum-6 : sum 3 4 ≡ 7
+sum-6 = {!!}
+
+sum1 : (x y : ℕ) → sum x (suc y)  ≡ suc (sum x y )
+sum1 x y = let open ≡-Reasoning in 
+   begin 
+       sum x (suc y)
+   ≡⟨ {!!} ⟩
+       suc (sum x y )
+   ∎
+
+
+sum-sym : (x y : ℕ) → sum x y  ≡ sum y x
+sum-sym = {!!}
+
+sum-assoc : (x y z : ℕ) → sum x (sum y z ) ≡ sum (sum x y)  z 
+sum-assoc = {!!}
+
+mul :  (x y : ℕ) → ℕ
+mul = {!!}
+
+mul-9 : mul 3 4 ≡ 12
+mul-9 = {!!}
+
+mul-distr1 : (x y : ℕ) → mul x (suc y) ≡ sum x ( mul x y )
+mul-distr1 = {!!}
+
+mul-sym0 : (x : ℕ) → mul zero x  ≡ mul x zero 
+mul-sym0 = {!!}
+
+mul-sym : (x y : ℕ) → mul x y  ≡ mul y x
+mul-sym = {!!}
+
+mul-distr : (y z w : ℕ) → sum (mul y z) ( mul w z ) ≡ mul (sum y w)  z
+mul-distr = {!!}
+
+mul-assoc : (x y z : ℕ) → mul x (mul y z ) ≡ mul (mul x y)  z 
+mul-assoc = {!!}
+
+
--- a/agda/flcagl.agda	Sun Apr 07 18:22:16 2019 +0900
+++ b/agda/flcagl.agda	Wed Oct 02 13:19:44 2019 +0900
@@ -71,16 +71,16 @@
         δ (k ∪ l) x = δ k x ∪ δ l x
 
 
-        _·'_ : ∀{i}  (k l : Lang i) → Lang i
-        ν (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 = 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
-        δ (_·_ {i} k  l) {j} x =
+        _*_ : ∀{i} (k l : Lang i )  → Lang i
+        ν (k * l) = ν k ∧ ν l
+        δ (_*_ {i} k  l) {j} x =
             let
                 k′l : Lang j
-                k′l  = _·_ {j} (δ k {j} x) l
+                k′l  = _*_ {j} (δ k {j} x) l
             in  if ν k then _∪_ {j}  k′l (δ l {j} x) else k′l 
 
         _* : ∀{i} (l : Lang i) → Lang i
@@ -218,43 +218,27 @@
            ∎
                where open EqR (Bis _)
         ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin
-               (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m)
-           ≈⟨ ≅refl ⟩
-               ((δ k a ∪ δ l a) · m ) ∪ δ m a
-           ≈⟨ union-congl (concat-union-distribl _) ⟩
-               (δ k a · m ∪ δ l a · m) ∪ δ m a
-           ≈⟨  union-assoc _ ⟩
-                δ k a · m ∪ ( δ l a · m ∪ δ m a )
-           ≈⟨  union-congr ( union-comm   _ _) ⟩
-                δ k a · m ∪ δ m a ∪ δ l a · m
-           ≈⟨ ≅sym ( union-assoc  _  ) ⟩
-               (δ k a · m ∪ δ m a) ∪ δ l a · m
-           ≈⟨ ≅refl ⟩
+               (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
+               ((δ k a ∪ δ l a) · m ) ∪ δ m a ≈⟨ union-congl (concat-union-distribl _) ⟩
+               (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _ ⟩
+                δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨  union-congr ( union-comm   _ _) ⟩
+                δ k a · m ∪ δ m a ∪ δ l a · m ≈⟨ ≅sym ( union-assoc  _  ) ⟩
+               (δ k a · m ∪ δ m a) ∪ δ l a · m ≈⟨ ≅refl ⟩
                ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m))
            ∎
                where open EqR (Bis _)
         ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin
-                (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m)
-           ≈⟨ ≅refl ⟩
-                (δ k a ∪ δ l a) · m ∪ δ m a
-           ≈⟨ union-congl ( concat-union-distribl _ ) ⟩
-               (δ k a · m ∪ δ l a · m) ∪ δ m a
-           ≈⟨  union-assoc _ ⟩
-               δ k a · m ∪ ( δ l a · m ∪ δ m a )
-           ≈⟨ ≅sym ( union-congr ( union-congr (  union-idem _ ) ) ) ⟩
-               δ k a · m ∪ ( δ l a · m ∪ (δ m a  ∪ δ m a) )
-           ≈⟨  ≅sym ( union-congr ( union-assoc _ )) ⟩
-               δ k a · m ∪ ( (δ l a · m ∪ δ m a  ) ∪ δ m a )
-           ≈⟨   union-congr (  union-congl  ( union-comm _  _) )   ⟩
-               δ k a · m ∪ ( (δ m a  ∪ δ l a · m ) ∪ δ m a )
-           ≈⟨  ≅sym ( union-assoc  _  ) ⟩
-               ( δ k a · m ∪  (δ m a  ∪ δ l a · m )) ∪ δ m a 
-           ≈⟨  ≅sym ( union-congl ( union-assoc _  ) ) ⟩
-               ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a
-           ≈⟨  union-assoc _  ⟩
-                (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a
-           ≈⟨ ≅refl ⟩
-                ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m))
+               (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
+               (δ k a ∪ δ l a) · m ∪ δ m a ≈⟨ union-congl ( concat-union-distribl _ ) ⟩
+               (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _ ⟩
+                δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ ≅sym ( union-congr ( union-congr (  union-idem _ ) ) ) ⟩
+                δ k a · m ∪ ( δ l a · m ∪ (δ m a  ∪ δ m a) ) ≈⟨  ≅sym ( union-congr ( union-assoc _ )) ⟩
+                δ k a · m ∪ ( (δ l a · m ∪ δ m a  ) ∪ δ m a ) ≈⟨   union-congr (  union-congl  ( union-comm _  _) )   ⟩
+                δ k a · m ∪ ( (δ m a  ∪ δ l a · m ) ∪ δ m a ) ≈⟨  ≅sym ( union-assoc  _  ) ⟩
+               ( δ k a · m ∪  (δ m a  ∪ δ l a · m )) ∪ δ m a ≈⟨  ≅sym ( union-congl ( union-assoc _  ) ) ⟩
+               ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _  ⟩
+               (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a ≈⟨ ≅refl ⟩
+               ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m))
            ∎
                where open EqR (Bis _)
 
@@ -310,14 +294,10 @@
         star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l *
         ≅ν (star-concat-idem l) = refl
         ≅δ (star-concat-idem l) a = begin
-               δ ((l *) · (l *)) a
-           ≈⟨ union-congl (concat-assoc _) ⟩
-               δ l a · (l * · l *) ∪ δ l a · l *
-           ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩
-               δ l a · l * ∪ δ l a · l *
-           ≈⟨ union-idem _ ⟩
-               δ (l *) a
-           ∎ where open EqR (Bis _)
+               δ ((l *) · (l *)) a ≈⟨ union-congl (concat-assoc _) ⟩
+               δ l a · (l * · l *) ∪ δ l a · l * ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩
+               δ l a · l * ∪ δ l a · l * ≈⟨ union-idem _ ⟩
+               δ (l *) a ∎ where open EqR (Bis _)
 
         star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l *
         ≅ν (star-idem l) = refl
@@ -477,3 +457,21 @@
  starA-correct : ∀{i S} (da : DA S) (s0 : S) →
    lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *
 
+record NAutomaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+              Nδ : Q → Σ → Q → Bool
+              Nstart : Q → Bool
+              Nend  :  Q → Bool
+
+postulate
+   exists : { S : Set} → ( S → Bool ) → Bool
+
+nlang : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
+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) 
+
+-- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i
+-- Lang.ν (nlang' nfa s) = DA.ν nfa  s
+-- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a)
+