Sudoku reproved, phew !

examples/TODO

@@ -14,7 +14,6 @@ linked_list_rev.mlw
 optimal_replay.mlw
 queens.mlw
 random_access_list.mlw
-sudoku.mlw
 sum_of_digits.mlw
 topological_sorting.mlw
 tortoise_and_hare.mlw

examples/sudoku.mlw

@@ -330,6 +330,30 @@ module Solver
     ensures  { full_up_to g2 i }
   = assert { grid_eq_sub g1 g2 0 i }
 
+  let lemma valid_chunk_frame (start:array int) (offsets:array int) (g1 g2:grid) (i:int)
+    requires { chunk_valid_indexes start offsets }
+    requires { 0 <= i < 81 }
+    requires { grid_eq g1 g2 }
+    requires { valid_chunk g1 i start offsets }
+    ensures  { valid_chunk g2 i start offsets }
+  = ()
+
+  let rec lemma valid_up_to_frame (s:sudoku_chunks) (g1 g2:grid) (i:int)
+    requires { well_formed_sudoku s }
+    requires { 0 <= i <= 81 }
+    requires { grid_eq g1 g2 }
+    requires { valid_up_to s g1 i }
+    variant  { i }
+    ensures  { valid_up_to s g2 i }
+  = if i > 0 then
+      begin
+        assert { valid_up_to s g1 (i-1) };
+        valid_up_to_frame s g1 g2 (i-1);
+	valid_chunk_frame s.column_start s.column_offsets g1 g2 (i-1);
+	valid_chunk_frame s.row_start s.row_offsets g1 g2 (i-1);
+	valid_chunk_frame s.square_start s.square_offsets g1 g2 (i-1);
+      end
+
 
 
 (** how to prove the "hard" property : if
@@ -384,14 +408,16 @@ this is true but with 2 different possible reasons:
       valid_chunk h i2 start offsets
 
 
-  lemma valid_up_to_change :
-    forall s:sudoku_chunks, g:grid, i x : int.
-      well_formed_sudoku s /\
-      is_index i /\ valid_up_to s g i /\ 1 <= x <= 9 /\
-      valid_column s (Map.set g i x) i /\
-      valid_row s (Map.set g i x) i /\
-      valid_square s (Map.set g i x) i
-      -> valid_up_to s (Map.set g i x) (i+1)
+  let ghost valid_up_to_change (s:sudoku_chunks) (g:grid) (i x : int)
+    requires {  well_formed_sudoku s }
+    requires { is_index i }
+    requires { valid_up_to s g i }
+    requires { 1 <= x <= 9 }
+    requires { valid_column s (Map.set g i x) i }
+    requires { valid_row s (Map.set g i x) i }
+    requires { valid_square s (Map.set g i x) i }
+    ensures  { valid_up_to s (Map.set g i x) (i+1) }
+  = ()
 
 
   (** {3 The main solver loop} *)
@@ -422,41 +448,42 @@ this is true but with 2 different possible reasons:
       end
     else
       begin
-      label L in
+      let ghost old_g = g.elts in
       for k = 1 to 9 do
-        invariant { grid_eq (g at L).elts (Map.set g.elts i 0) }
+        invariant { grid_eq old_g (Map.set g.elts i 0) }
         invariant { full_up_to g.elts i }
         invariant { (* for completeness *)
           forall k'. 1 <= k' < k ->
-          let g' = Map.set (g at L).elts i k' in
+          let g' = Map.set old_g i k' in
           forall h : grid. included g' h /\ full h -> not (valid s h) }
         g[i] <- k;
+	valid_up_to_frame s old_g (Map.set g.elts i 0) i;
         try
           check_valid_chunk g i s.column_start s.column_offsets;
           check_valid_chunk g i s.row_start s.row_offsets;
           check_valid_chunk g i s.square_start s.square_offsets;
             (* the hard part: see lemma valid_up_to_change *)
-          assert { let grid' = Map.set (g at L).elts i k in
+          assert { let grid' = Map.set old_g i k in
             grid_eq grid' g.elts &&
             valid_chunk grid' i s.column_start s.column_offsets &&
             valid_chunk grid' i s.row_start s.row_offsets &&
             valid_chunk grid' i s.square_start s.square_offsets &&
             valid_up_to s grid' (i+1) };
-          assert { valid_up_to s g.elts (i+1) };
+          valid_up_to_change s old_g i k;
           solve_aux s g (i + 1)
         with Invalid ->
           assert { (* for completeness *)
-            not (valid s (Map.set (g at L).elts i k)) };
+            not (valid s (Map.set old_g i k)) };
           assert { (* for completeness *)
-            let g' = Map.set (g at L).elts i k in
+            let g' = Map.set old_g i k in
             forall h : grid. included g' h /\ full h -> not (valid s h) }
         end
       done;
       g[i] <- 0;
       assert { (* for completeness *)
-        forall h:grid. included (g at L).elts h /\ full h ->
+        forall h:grid. included old_g h /\ full h ->
           let k' = Map.get h i in
-          let g' = Map.set (g at L).elts i k' in
+          let g' = Map.set old_g i k' in
           included g' h }
       end
 
@@ -491,6 +518,7 @@ this is true but with 2 different possible reasons:
 
 end
 
+(* Proof in progress
 module RandomSolver
 
   (* a variant: solve using a random order of cells *)
@@ -602,6 +630,7 @@ module RandomSolver
     if check_valid s g then solve s g else raise NoSolution
 
 end
+*)
 
 
 (** {2 Some Tests} *)