(WIP) continued dyck words & Warshall algorithm

examples/in_progress/dyck.mlw

@@ -15,16 +15,16 @@ theory Dyck
   | Dyck_ind:
       forall w1 w2. dyck w1 -> dyck w2 -> dyck (Cons L (w1 ++ Cons R w2))
 
-  lemma dyck_concat:
-    forall w1 w2. dyck w1 -> dyck w2 -> dyck (w1 ++ w2)
-
   (* the first letter, if any, must be L *)
   lemma dyck_word_first:
     forall w: word. dyck w ->
     match w with Nil -> true | Cons c _ -> c = L end
+  
+  (*(* Concatenation of dyck words is a dyck word. *)
+  lemma dyck_concat : forall w1 w2:word. dyck w1 -> dyck w2 -> dyck (w1 ++ w2)
 
   lemma dyck_decomp:
-    forall w1 w2: word. dyck (w1 ++ w2) -> dyck w1 -> dyck w2
+    forall w1 w2: word. dyck (w1 ++ w2) -> dyck w1 -> dyck w2*)
 
 end
 
@@ -32,29 +32,53 @@ module Check
 
   use import Dyck
   use import list.Length
+  use import ref.Ref
 
   exception Failure
 
-  let rec is_dyck_rec (w: word) : word
-    ensures { exists p: word. dyck p && w = p ++ result &&
-              match result with Cons L _ -> false | _ -> true end }
-    raises  { Failure -> forall p s: word. w = p ++ s -> not (dyck p) }
+  (* A fall of a word is a decomposition p ++ s with p a dyck word
+     and s a word not starting by L. *)
+  predicate fall (p s:word) = dyck p /\
+    match s with Cons L _ -> false | _ -> true end
+
+  let rec lemma same_prefix (p s s2:word) : unit
+    requires { p ++ s = p ++ s2 }
+    ensures { s = s2 }
+    variant { p }
+  = match p with Nil -> () | Cons _ q -> same_prefix q s s2 end
+
+  (* Compute the fall decomposition, if it exists. As a side-effect,
+     prove its unicity. *)
+  let rec is_dyck_rec (ghost p:ref word) (w: word) : word
+    ensures { w = !p ++ result && fall !p result &&
+      (forall p2 s: word. w = p2 ++ s /\ fall p2 s -> p2 = !p && s = result) }
+    writes { p }
+    raises  { Failure -> (forall p s:word. w = p ++ s -> not fall p s) }
     variant { length w }
   =
     match w with
-    | Cons L w ->
-       match is_dyck_rec w with
-       | Cons R w -> is_dyck_rec w
-       | _        -> raise Failure
-       end
-    | _ ->
-       w
+    | Cons L w0 -> let ghost p0 = ref Nil in
+      match is_dyck_rec p0 w0 with
+      | Cons _ w1 -> assert { forall p s p1 p2:word.
+        dyck p /\ w = p ++ s /\ dyck p1 /\ dyck p2 /\
+        p = Cons L (p1 ++ Cons R p2) ->
+        w0 = p1 ++ (Cons R (p2 ++ s)) && p1 = !p0 && w1 = p2 ++ s };
+        let ghost p1 = ref Nil in
+        let w = is_dyck_rec p1 w1 in
+        p := Cons L (!p0 ++ Cons R !p1);
+        w
+      | _         -> raise Failure
+      end
+    | _ -> p := Nil; w
     end
 
   let is_dyck (w: word) : bool
     ensures { result <-> dyck w }
   =
-    try is_dyck_rec w = Nil with Failure -> false end
+    try match is_dyck_rec (ref Nil) w with
+      | Nil -> true
+      | _ -> false
+    end with Failure -> false end
 
 end
 

examples/in_progress/warshall_algorithm.mlw

@@ -20,8 +20,12 @@ module WarshallAlgorithm
       0 <= x < k -> path m i x k -> path m x j k -> path m i j k
 
   lemma weakening:
-    forall m i j k1 k2. 0 <= k2 <= k1 ->
+    forall m i j k1 k2. 0 <= k1 <= k2 ->
     path m i j k1 -> path m i j k2
+  
+  lemma decomposition:
+    forall m i j k. 0 <= k /\ path m i j (k+1) ->
+      (path m i j k \/ (path m i k k /\ path m k j k))
 
   let transitive_closure (m: matrix bool) : matrix bool
     requires { m.rows = m.columns }
@@ -37,12 +41,15 @@ module WarshallAlgorithm
       for i = 0 to n - 1 do
         invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
                     get t (x,y) <->
-                    (path m x y k || x < i && path m x y (k+1)) }
+                    if x < i
+                    then path m x y (k+1)
+                    else path m x y k }
         for j = 0 to n - 1 do
           invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
                       get t (x,y) <->
-                      (path m x y k || x < i && path m x y (k+1)
-                                    || x = i && y < j && path m x y (k+1)) }
+                      if x < i \/ (x = i /\ y < j)
+                      then path m x y (k+1)
+                      else path m x y k }
           set t (i,j) (get t (i,j) || get t (i,k) && get t (k,j))
         done
       done