--- a/regex.agda	Mon Nov 16 14:41:00 2020 +0900
+++ b/regex.agda	Mon Nov 16 18:51:29 2020 +0900
@@ -12,6 +12,8 @@
 
 
 data Regex   ( Σ : Set  ) : Set  where
+   φ     : Regex  Σ 
+   ε     : Regex  Σ 
    _*    : Regex  Σ → Regex  Σ
    _&_   : Regex  Σ → Regex  Σ → Regex Σ
    _||_  : Regex  Σ → Regex  Σ → Regex Σ
@@ -37,6 +39,8 @@
 
 data regular-expr  {Σ : Set} : Regex Σ → List Σ → Set where
    atom : (x :  Σ ) →  regular-expr < x > ( x ∷ [] )
+   empty : regular-expr φ [] 
+   none : ⊥ → regular-expr φ [] 
    concat : {x y : Regex Σ} {t s : List Σ} →  regular-expr x t →  regular-expr y s →  regular-expr (x & y) (t ++ s )
    select : {x y : Regex Σ} {t : List Σ} →  regular-expr x t ∨  regular-expr y t →  regular-expr (x || y) t
    star-nil : {x : Regex Σ}  →  regular-expr (x *) []
@@ -56,6 +60,8 @@
 -- test-regex-even = (s : List char ) → regular-expr ( ( any & any ) * )  s  → (length s) mod 2 ≡ zero
 
 empty? : {Σ : Set} →  Regex Σ → Bool
+empty? φ = false
+empty? ε = true
 empty? (r *) = true
 empty? (r & s) with empty? r
 ... | false = false
@@ -72,6 +78,8 @@
    continue : (Regex Σ) → RexResult
 
 derivative : {Σ : Set} →  Regex Σ → Σ → ((i j : Σ ) → Dec ( i ≡ j )) → RexResult
+derivative φ x dec  = fail
+derivative ε x dec  = fail
 derivative (r *) x dec  with derivative r x dec 
 ... | continue r1 = continue (r1 & (r *))
 ... | finish = continue (r *)
@@ -156,22 +164,65 @@
 
 
 
--- charRE-dec : (x y : Regex char) → Dec (x ≡ y)
--- charRE-dec (x *) (y *) with charRE-dec x y
--- ... | yes refl = yes refl
--- ... | no n = no {!!}
--- charRE-dec (x *) (_ & _) = no (λ ())
--- charRE-dec (x *) (_ || _) = no (λ ())
--- charRE-dec (x *) < _ > = no (λ ())
--- charRE-dec (x & x1) (y & y1) with charRE-dec x y | charRE-dec x1 y1
--- ... | yes refl | yes refl = yes refl
--- ... | no n | _ = no {!!}
--- ... |  _ | no n = no {!!}
--- charRE-dec (x & x1) (y *) = no (λ ())
--- charRE-dec (x & x1) (_ || _) = no (λ ())
--- charRE-dec (x & x1) < _ > = no (λ ())
--- charRE-dec (x || x₁) y = {!!}
--- charRE-dec < x > y = {!!}
+RE-dec : {Σ : Set} → ((s t : Σ) → Dec (s ≡ t))  → (x y : Regex Σ) →  Dec (x ≡ y)
+RE-dec dec (x *) (y *) with RE-dec dec x y
+... | yes refl = yes refl
+... | no n = no (contra-position relem1 n ) where
+   relem1 : (x *) ≡ (y *) → x ≡ y
+   relem1 refl = refl
+RE-dec dec (x *) (_ & _) = no (λ ())
+RE-dec dec (x *) (_ || _) = no (λ ())
+RE-dec dec (x *) < _ > = no (λ ())
+RE-dec dec (x & x1) (y & y1) with RE-dec dec x y | RE-dec dec x1 y1
+... | yes refl | yes refl = yes refl
+... | no n | _ = no (contra-position relem2 n ) where
+   relem2 : x & x1 ≡ y & y1 → x ≡ y
+   relem2 refl = refl
+... |  _ | no n = no (contra-position relem3 n ) where
+   relem3 :  x & x1 ≡ y & y1 → x1 ≡ y1
+   relem3 refl = refl
+RE-dec dec (x & x1) (y *) = no (λ ())
+RE-dec dec (x & x1) (_ || _) = no (λ ())
+RE-dec dec (x & x1) < _ > = no (λ ())
+RE-dec dec (x || x1) φ = no (λ ())
+RE-dec dec (x || x1) ε = no (λ ())
+RE-dec dec (x || x1) (y *) = no (λ ())
+RE-dec dec (x || x1) (y & y₁) = no (λ ())
+RE-dec dec (x || x1) (y || y1) with RE-dec dec x y | RE-dec dec x1 y1
+... | yes refl | yes refl = yes refl
+... | no n | _ = no (contra-position relem4 n ) where
+   relem4 :   x || x1 ≡ y || y1 → x ≡ y
+   relem4 refl = refl
+... |  _ | no n = no (contra-position relem5 n ) where
+   relem5 :  x || x1 ≡ y || y1 → x1 ≡ y1
+   relem5 refl = refl
+RE-dec dec (x || x1) < x₁ > = no (λ ())
+RE-dec dec < x > φ = no (λ ()) 
+RE-dec dec < x > ε =  no (λ ())
+RE-dec dec < x > (y *) =  no (λ ())
+RE-dec dec < x > (y & y₁) =  no (λ ())
+RE-dec dec < x > (y || y₁) =  no (λ ())
+RE-dec dec < x > < x₁ > with dec x x₁
+... | yes refl = yes refl
+... | no n = no (contra-position relem6 n ) where
+   relem6 :  < x > ≡ < x₁ > → x ≡ x₁
+   relem6 refl = refl
+RE-dec dec φ φ = yes refl
+RE-dec dec φ ε = no (λ ())
+RE-dec dec φ (y *) = no (λ ())
+RE-dec dec φ (y & y₁) = no (λ ())
+RE-dec dec φ (y || y₁) = no (λ ())
+RE-dec dec φ < x > = no (λ ())
+RE-dec dec ε φ = no (λ ())
+RE-dec dec ε ε = yes refl
+RE-dec dec ε (y *) = no (λ ())
+RE-dec dec ε (y & y₁) = no (λ ())
+RE-dec dec ε (y || y₁) = no (λ ())
+RE-dec dec ε < x > = no (λ ())
+RE-dec dec (x *) φ = no (λ ())
+RE-dec dec (x *) ε = no (λ ())
+RE-dec dec (x & x1) φ = no (λ ())
+RE-dec dec (x & x1) ε = no (λ ())