(**************************************************************************) (* Le damier de Cachan *) (* Coq V7 *) (**************************************************************************) (* Na szachownicy 3x3 jest 9 piokow dwukolorowych (z jednej strony *) (* biale - z drugiej czarne). Operacje wykonywane na szachownicy to *) (* odwracanie wszystkich pionkow danego wiersza lub kolumny. *) (* Bedziemy badac pozycje osiagalne ze stanu poczatkowego *) (* (wszystkie pionki same biale) *) (* I- Kolory Modelujemy kolory, jako typ color z dwoma elementami Black i White *) Inductive color : Set := ... Definition turn_color : color -> color := ... (* Testujemy... *) Eval compute in (turn_color White). (* II- Trojki Modelujemy pojecie trojki dowolnego typu M. Szachownica bedzie reprezentowana jako trojka trojek kolorow, reprezentujacych pionki lezace na odpowiedniej pozycji szachownicy. Trzywartosciowy typ pozycji pomaga indeksowac. *) Section Polymorphic_Triple. Variable M : Set. Inductive triple : Set := ... (* Check Triple : M -> M -> M -> triple. *) Definition triple_x : M -> triple := fun m => Triple m m m. Inductive pos : Set := A : pos | B : pos | C : pos. (* rzutowanie trojki wg pozycji *) Definition proj_triple : pos -> triple -> M := ... Variable f : M -> M. Definition triple_map : triple -> triple := ... Definition triple_map_select : pos -> triple -> triple := ... End Polymorphic_Triple. (* Zaobserwowac typ obiektow zdefiniowanych w sekcji po jej zamknieciu! *) (* III- Szachownica *) Definition board := ... Definition white_board : board := ... (* **O *OO OOO *) Definition start : board := ... (* OO* O** OOO *) Definition target : board := ... Definition proj_board : pos -> pos -> board -> color := ... Definition turn_line : pos -> board -> board := ... Definition turn_col : pos -> board -> board := ... (* Test *) Eval compute in (turn_line A (turn_col B white_board)). (* IV-Ruchy *) ... (* Check move. move : board -> board -> Prop Check move_line. move_line : forall (b1:board)(p:pos), move b1 (turn_line p b1) Check move_col. move_col : forall (b1:board)(p:pos), move b1 (turn_col p b1) *) Inductive moves (b1:board): board -> Prop := ... | moves_step : forall (b2,b3:board), moves b1 b2 -> move b2 b3 -> moves b1 b3. (* Check moves_init : (b1:board)(moves b1 b1) Check move_moves : (b1,b2:board)(move b1 b2) -> (moves b1 b2) Check moves_trans : (b1,b2,b3:board)(moves b1 b2)->(moves b2 b3)->(moves b1 b3) *) (* target jest dostepny z start *) Lemma acessible : moves start target. (* White_board nie jest dostepny z start *) (* Tu trzeba wymyslec cos sprytnego... *) Definition odd_board : board -> bool := ... Lemma odd_invariant_move : forall (b1,b2:board), move b1 b2 -> odd_board b1 = odd_board b2. Lemma odd_invariant_moves : forall (b1,b2:board), (moves b1 b2) -> (odd_board b1) = (odd_board b2). Lemma not_accessible : ~(moves start white_board).