# HG changeset patch
# User Chengsong
# Date 1552652832 0
# Node ID 7a349fe58bf400eeff2c19a195435be61b92842c
# Parent  f15dccc42c7b07ca866c9c64e4588b2eeb9b610d
:test whether bsimp(bders(r, s)) == ders_simp(r,s)
This does not hold. As illustrated by the output of the example where string is abaa and regex is (a* + ab)*
this property still holds when s = aba
but after the derivative of the last character a, the result is negative.
However this seems easily fixable as the difference is relatively small, it might be possible to find where the difference happens
and by taking that difference into accound we have some function f s.t.
f(bsimp(r,s)) = ders_simp(r,s)
and mkeps(f(r)) = mkeps(r)
This will complete the correctness proof.
Even if finding such f is hard, it would still provide insights for the real difference between simp(der(simp(der(simp(der...... and simp(ders

diff -r f15dccc42c7b -r 7a349fe58bf4 Spiral.scala
--- a/Spiral.scala	Fri Mar 15 10:46:46 2019 +0000
+++ b/Spiral.scala	Fri Mar 15 12:27:12 2019 +0000
@@ -312,7 +312,12 @@
   }
   def size_comp(anatomy: List[Rexp], pd: Set[Rexp]):Boolean = {println("size of PD and bspilled simp regx: ", pd.size, anatomy.size); true}
   def size_expansion_rate(anatomy: List[Rexp], pd: Set[Rexp]): Boolean = if(anatomy.size > (pd.size)*2 ) {println("size of PD and bspilled simp regx: ", pd.size, anatomy.size); inclusion_truth(anatomy, pd); false }else {true}
-  
+  def ders_simp(r: ARexp, s: List[Char]): ARexp = {
+    s match {
+      case Nil => r 
+      case c::cs => ders_simp(bsimp(bder(c, r)), cs)
+    }
+  }
   def check_all(){
     for(i <- 1 to 1)
     {
@@ -322,8 +327,29 @@
         weak_sub_check(r, s, 5, size_expansion_rate)
     }
   }
+  def correctness_proof_convenient_path(){
+    for(i <- 1 to 1)
+    {
+        val s = "abaa"//rd_string_gen(alphabet_size, 3)
+        val r = ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
+        for(j <- 0 to s.length - 1){
+          val ss = s.slice(0, j+ 1)
+          val nangao = ders_simp(r, ss.toList)
+          val easy = bsimp(bders(ss.toList, r))
+          if(nangao != easy|| j == 2){
+            println(j)
+            if(j == 3) println("not equal")
+            println(ss)
+            println(r)
+            println(nangao)
+            println(easy)
+          }
+        }
+    }
+  }
   def main(args: Array[String]) {
-    check_all()   
+    //check_all()   
+    correctness_proof_convenient_path
   } 
 }