(**************************************************************************) (* Le damier de Cachan *) (* Coq V8 *) (**************************************************************************) (* 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 *) (*Set Implicit Arguments.*) Inductive color : Set := | White : color | Black : color. Definition turn_color : color -> color := fun (c:color) => match c with | White => Black | Black => White end. (* 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 := | Triple : M -> M -> M -> triple. (* 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 := fun (p:pos)(t:triple) => match t with | Triple a b c => match p with | A => a | B => b | C => c end end. Variable f : M -> M. Definition triple_map : triple -> triple := fun (t:triple) => match t with | Triple a b c => Triple (f a) (f b) (f c) end. Definition triple_map_select : pos -> triple -> triple := fun (p:pos)(t:triple) => match t with | Triple a b c => match p with | A => Triple (f a) b c | B => Triple a (f b) c | C => Triple a b (f c) end end. End Polymorphic_Triple. Print triple_map. Print Triple. (*Implicit Arguments Triple. Print Triple.*) (* Zaobserwowac typ obiektow zdefiniowanych w sekcji po jej zamknieciu! *) (* III- Szachownica *) Definition board := triple (triple color). Print triple_x. Definition white_board : board := @triple_x (triple color) (@triple_x color White). (* Definition white_board : board := @triple_x (triple color) (@triple_x color White). *) (* **O *OO OOO *) (* Implicit Arguments Triple. Print Triple. *) Definition start : board := Triple (triple color) (Triple color Black Black White) (Triple color Black White White) (Triple color White White White). (* OO* O** OOO *) Definition target : board := Triple (triple color) (Triple color White White Black) (Triple color White Black Black) (Triple color White White White). (*usunac typy color ponizej, triple color i color powyzej*) Definition proj_board : pos -> pos -> board -> color := fun (x y: pos)(b: board) => match b with | Triple l1 l2 l3 => match x with | A => proj_triple color y l1 | B => proj_triple color y l2 | C => proj_triple color y l3 end end. Print triple_map_select. Definition turn_line : pos -> board -> board := fun (p:pos)(b:board) => triple_map_select (triple color) (fun (l:triple color)=> triple_map color turn_color l) p b. Definition turn_col : pos -> board -> board := fun (p:pos)(b:board) => triple_map (triple color) (fun (l:triple color) => triple_map_select color turn_color p l) b. (* Test *) Eval compute in (turn_line A (turn_col B white_board)). (* IV-Ruchy *) Inductive move: board -> board -> Prop:= | move_line : forall (b1:board)(p:pos), move b1 (turn_line p b1) | move_col : forall (b1:board)(p:pos), move b1 (turn_col p b1). (* 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_init : moves b1 b1 | moves_move : forall (b2:board),move b1 b2 -> moves b1 b2 | moves_step : forall (b2 b3:board), moves b1 b2 -> move b2 b3 -> moves b1 b3. Hint Constructors move moves. (* Check moves_init : forall (b1:board), moves b1 b1 Check moves_move : forall (b1 b2:board), move b1 b2 -> moves b1 b2 Check moves_step : forall (b1 b2 b3:board), moves b1 b2->move b2 b3 ->moves b1 b3 *) (* target jest dostepny z start *) Lemma acessible : moves start target. Proof. change target with (turn_line A (turn_line B start)). eauto. Qed. (* White_board nie jest dostepny z start *) (* Tu trzeba wymyslec cos sprytnego... *) Definition czarne : color -> bool := fun c: color => match c with | Black => true | White => false end. Require Import Bool. Definition odd_board : board -> bool := fun b: board => xorb (xorb (czarne (proj_board A A b)) (czarne (proj_board A C b))) (xorb (czarne (proj_board C A b)) (czarne (proj_board C C b))). Ltac rozloz := fun l k b => destruct l;destruct k;destruct b as [l1 l2 l3]; destruct l1; destruct l2;destruct l3. Ltac uprosc := fun H => simpl in H; simpl; rewrite H;reflexivity. Lemma same_czarne: forall (b:board)(l k:pos)(w:pos) , (l <> w) -> czarne (proj_board l k b) = czarne (proj_board l k (turn_line w b)). Proof. intros. apply f_equal with (A:=color). destruct w; rozloz l k b; simpl;tauto. Save. Lemma neg_czarne: forall (b:board)(l k:pos), negb (czarne (proj_board l k b)) = czarne (proj_board l k (turn_line l b)). Proof. intros. remember (proj_board l k b) as c. symmetry in Heqc. destruct c; rozloz l k b;uprosc Heqc. Qed. Lemma same_czarne_col: forall (b:board)(l k:pos)(w:pos) , (k <> w) -> czarne (proj_board l k b) = czarne (proj_board l k (turn_col w b)). Proof. intros. apply f_equal with (A:=color). destruct w; rozloz l k b; simpl; tauto. Save. Lemma neg_czarne_col: forall (b:board)(l k:pos), negb (czarne (proj_board l k b)) = czarne (proj_board l k (turn_col k b)). Proof. intros. remember (proj_board l k b) as c. symmetry in Heqc. destruct c; rozloz l k b; uprosc Heqc. Qed. Lemma neg_xorb1: forall(b b': bool), xorb b (negb b') = negb (xorb b b'). Proof. destruct b; destruct b'; auto. Save. Lemma neg_xorb2: forall(b b': bool), xorb (negb b) b' = negb (xorb b b'). Proof. destruct b; destruct b'; auto. Save. Ltac ar := repeat(rewrite neg_xorb2 || rewrite neg_xorb1 || rewrite negb_involutive). Lemma odd_invariant_move : forall (b1 b2:board), move b1 b2 -> odd_board b1 = odd_board b2. Proof. intros. unfold odd_board. destruct H. destruct p; repeat rewrite <- neg_czarne; repeat rewrite <- same_czarne; ar; reflexivity || discriminate. destruct p; repeat rewrite <- neg_czarne_col; repeat rewrite <- same_czarne_col; ar; reflexivity || discriminate. Save. Lemma odd_invariant_moves : forall (b1 b2:board), (moves b1 b2) -> (odd_board b1) = (odd_board b2). Proof. induction 1. reflexivity. apply odd_invariant_move; assumption. rewrite IHmoves. apply odd_invariant_move; assumption. Save. Lemma not_accessible : ~(moves start white_board). Proof. intro. apply odd_invariant_moves in H. discriminate. Save.