Commit 7680dca1 by MARCHE Claude

### sudoku reloaded: proof in progress

parent 3fb092c3
 ... ... @@ -341,9 +341,9 @@ module Solver use import Grid use import array.Array use import int.Int use import mach.int.Int31 use import int.Int use import mach.array.Array31 (** predicate for the loop invariant of next function *) ... ... @@ -380,6 +380,7 @@ module Solver let b = Array31.make n10 False in let off = ref n0 in while Int31.(<) !off n9 do invariant { 0 <= t !off <= 9 } invariant { valid_chunk_up_to g.elts (t i) start offsets (t !off) } invariant { forall o:int. 0 <= o < t !off -> let v = g[t s + t offsets[o]] in ... ... @@ -407,16 +408,23 @@ module Solver [g] is valid. (This function is not needed by the solver) *) let check_valid (s:sudoku_chunks) (g : array int31) : bool requires { well_formed_sudoku s } requires { g.length = 81 } requires { t g.length = 81 } requires { valid_values g.elts } ensures { result <-> valid s g.elts } = let n0 = of_int 0 in let n1 = of_int 1 in let n81 = of_int 81 in try for i = 0 to 80 do invariant { valid_up_to s g.elts i } 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 let i = ref n0 in while Int31.(<) !i n81 do invariant { 0 <= t !i <= 81 } invariant { valid_up_to s g.elts (t !i) } variant { 81 - t !i } 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; i := Int31.(+) !i n1; done; True with Invalid -> False ... ... @@ -424,12 +432,12 @@ module Solver (** [full_up_to g i] is true when all cells [0..i-1] in grid [g] are non empty *) predicate full_up_to (g : grid) (i : int) = forall j : int. 0 <= j < i -> 1 <= Map.get g j <= 9 predicate full_up_to (g : grid) (i : int) = forall j : int. 0 <= j < i -> 1 <= t (Map.get g j) <= 9 lemma full_up_to_change : forall g i x. is_index i /\ full_up_to g i -> 1 <= x <= 9 -> full_up_to (Map.set g i x) (i+1) -> 1 <= t x <= 9 -> full_up_to (Map.set g i x) (i + 1) let rec lemma full_up_to_frame (g1 g2:grid) (i:int) requires { 0 <= i <= 81 } ... ... @@ -485,9 +493,9 @@ this is true but with 2 different possible reasons: lemma valid_unchanged_chunks: forall g : grid, i1 i2 k:int, start offsets:array int31. forall g : grid, i1 i2:int, k:int31, start offsets:array int31. disjoint_chunks start offsets -> is_index i1 /\ is_index i2 /\ 1 <= k <= 9 -> is_index i1 /\ is_index i2 /\ 1 <= t k <= 9 -> let s1 = start[i1] in let s2 = start[i2] in let h = Map.set g i1 k in ... ... @@ -495,8 +503,8 @@ this is true but with 2 different possible reasons: valid_chunk h i2 start offsets lemma valid_changed_chunks: forall g : grid, i1 i2 k:int, start offsets:array int31. is_index i1 /\ is_index i2 /\ 1 <= k <= 9 -> forall g : grid, i1 i2:int, k:int31, start offsets:array int31. is_index i1 /\ is_index i2 /\ 1 <= t k <= 9 -> let s1 = start[i1] in let s2 = start[i2] in let h = Map.set g i1 k in ... ... @@ -505,9 +513,9 @@ this is true but with 2 different possible reasons: lemma valid_up_to_change : forall s:sudoku_chunks, g:grid, i x : int. forall s:sudoku_chunks, g:grid, i: int, x:int31. well_formed_sudoku s /\ is_index i /\ valid_up_to s g i /\ 1 <= x <= 9 /\ is_index i /\ valid_up_to s g i /\ 1 <= t 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 ... ... @@ -517,66 +525,74 @@ this is true but with 2 different possible reasons: (** {3 The main solver loop} *) exception SolutionFound let rec solve_aux (s:sudoku_chunks) (g : array int31) (i : int) let rec solve_aux (s:sudoku_chunks) (g : array int31) (i : int31) requires { well_formed_sudoku s } requires { g.length = 81 } requires { t g.length = 81 } requires { valid_values g.elts } requires { 0 <= i <= 81 } requires { valid_up_to s g.elts i } requires { full_up_to g.elts i } requires { 0 <= t i <= 81 } requires { valid_up_to s g.elts (t i) } requires { full_up_to g.elts (t i) } writes { g } variant { 81 - i } variant { 81 - t i } ensures { grid_eq (old g).elts g.elts } ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) } raises { SolutionFound -> is_solution_for s g.elts (old g).elts } = if i = 81 then raise SolutionFound; = let n0 = of_int 0 in let n1 = of_int 1 in let n9 = of_int 9 in let n81 = of_int 81 in if Int31.eq i n81 then raise SolutionFound; (* assert { is_index i }; *) if g[i] <> 0 then if g[i] <> n0 then try (* assert { 1 <= g[i] <= 9 }; *) (* assert { 1 <= t g[i] <= 9 }; *) 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; solve_aux s g (i + 1) solve_aux s g (Int31.(+) i n1) with Invalid -> () end else begin 'L: for k = 1 to 9 do invariant { grid_eq (at g 'L).elts (Map.set g.elts i 0) } invariant { full_up_to g.elts i } let k = ref n1 in while Int31.(<=) !k n9 do invariant { 1 <= t !k <= 10 } invariant { grid_eq (at g 'L).elts (Map.set g.elts (t i) n0) } invariant { full_up_to g.elts (t i) } invariant { (* for completeness *) forall k'. 1 <= k' < k -> let g' = Map.set (at g 'L).elts i k' in forall k'. 1 <= t k' < t !k -> let g' = Map.set (at g 'L).elts (t i) k' in forall h : grid. included g' h /\ full h -> not (valid s h) } g[i] <- k; variant { 9 - t !k } g[i] <- !k; 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 (at g 'L).elts i k in assert { let grid' = Map.set (at g 'L).elts (t 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) }; solve_aux s g (i + 1) valid_chunk grid' (t i) s.column_start s.column_offsets && valid_chunk grid' (t i) s.row_start s.row_offsets && valid_chunk grid' (t i) s.square_start s.square_offsets && valid_up_to s grid' (t i + 1) }; assert { valid_up_to s g.elts (t i + 1) }; solve_aux s g (Int31.(+) i n1) with Invalid -> assert { (* for completeness *) not (valid s (Map.set (at g 'L).elts i k)) }; not (valid s (Map.set (at g 'L).elts (t i) !k)) }; assert { (* for completeness *) let g' = Map.set (at g 'L).elts i k in let g' = Map.set (at g 'L).elts (t i) !k in forall h : grid. included g' h /\ full h -> not (valid s h) } end end; k := Int31.(+) !k n1; done; g[i] <- 0; g[i] <- n0; assert { (* for completeness *) forall h:grid. included (at g 'L).elts h /\ full h -> let k' = Map.get h i in let g' = Map.set (at g 'L).elts i k' in let k' = Map.get h (t i) in let g' = Map.set (at g 'L).elts (t i) k' in included g' h } end ... ... @@ -584,7 +600,7 @@ this is true but with 2 different possible reasons: let solve (s:sudoku_chunks) (g : array int31) requires { well_formed_sudoku s } requires { g.length = 81 } requires { t g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ... ... @@ -592,14 +608,14 @@ this is true but with 2 different possible reasons: raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = try solve_aux s g 0; try solve_aux s g (of_int 0); raise NoSolution with SolutionFound -> g end let check_then_solve (s:sudoku_chunks) (g : array int31) requires { well_formed_sudoku s } requires { g.length = 81 } requires { t g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ... ... @@ -607,12 +623,7 @@ this is true but with 2 different possible reasons: raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = if check_valid s g then try solve_aux s g 0; raise NoSolution with SolutionFound -> g end else raise NoSolution if check_valid s g then solve s g else raise NoSolution end ... ... @@ -625,13 +636,14 @@ module Test use import TheClassicalSudokuGrid use import Solver use array.Array use mach.array.Array31 use import map.Map use import mach.int.Int31 (** Solving the empty grid: easy, yet not trivial *) let test0 () raises { NoSolution -> true } = let a = Array.make 81 0 in = let a = Array31.make (of_int 81) (of_int 0) in solve (classical_sudoku()) a (* a possible solution: 1, 2, 3, 4, 5, 6, 7, 8, 9, ... ... @@ -657,6 +669,7 @@ module Test 8 0 0 0 0 1 0 0 5 0 0 0 0 0 0 0 7 6 *) (* constant solvable : grid = (const 0) [0<-2][2<-9][7<-1] ... ... @@ -679,6 +692,8 @@ module Test Array.([]<-) a i (Map.get solvable i) done; solve (classical_sudoku()) a *) (* the solution: 2, 6, 9, 3, 5, 7, 8, 1, 4, ... ... @@ -696,13 +711,13 @@ module Test (** A trivially unsolvable grid *) let test2 () raises { NoSolution -> true } = let a = Array.make 81 1 in = let a = Array31.make (of_int 81) (of_int 1) in solve (classical_sudoku()) a end (*** Local Variables: compile-command: "why3ide sudoku.mlw" compile-command: "why3 ide sudoku_reloaded.mlw" End: *)
This diff is collapsed.