Commit 5466df7b authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

solution td6

parent edcca26a
Set Implicit Arguments.
Inductive color := Bl | Wh.
Definition inv_color c :=
match c with
| Bl => Wh
| Wh => Bl
end.
Section Triple.
Variable X : Type.
Inductive triple :=
| Triple : X -> X -> X -> triple.
(* Or equivalently :
Inductive triple := Triple (x y z:X).
*)
Definition triple_x x := Triple x x x.
Definition triple_map f '(Triple x y z) := Triple (f x) (f y) (f z).
Inductive pos := A | B | C.
Definition triple_proj (p:pos) '(Triple x y z) :=
match p with
| A => x
| B => y
| C => z
end.
Definition triple_map_select f (p:pos) '(Triple x y z) :=
match p with
| A => Triple (f x) y z
| B => Triple x (f y) z
| C => Triple x y (f z)
end.
End Triple.
Definition board := triple (triple color).
Definition white_board : board := triple_x (triple_x Wh).
Definition start :=
Triple
(Triple Wh Wh Bl)
(Triple Bl Wh Wh)
(Triple Bl Bl Bl).
Definition target :=
Triple
(Triple Bl Bl Bl)
(Triple Wh Bl Wh)
(Triple Bl Bl Wh).
Definition board_proj (b:board) lin col :=
triple_proj col (triple_proj lin b).
Definition inv_row (b:board) p :=
triple_map_select (triple_map inv_color) p b.
Definition inv_col (b:board) p :=
triple_map (triple_map_select inv_color p) b.
Compute inv_row (inv_col (inv_col start B) A) C.
(* looks a lot like the 'target' board :) *)
Definition move b1 b2 :=
(exists p, b2 = inv_row b1 p) \/ (exists p, b2 = inv_col b1 p).
(* Or:
Definition move b1 b2 :=
exists p, b2 = inv_row b1 p \/ b2 = inv_col b1 p.
*)
(* Or:
Inductive move (b:board) : board -> Prop :=
| MoveRow p : move b (inv_row b p)
| MoveCol p : move b (inv_col b p).
*)
(* For the fun, let's do a computational proof :
enumerating all the boards and all the positions ! *)
Ltac break_all :=
match goal with
| c:color |- _ => destruct c; break_all
| t:triple _ |- _ => destruct t; break_all
| b:board |- _ => destruct b; break_all
| p:pos |- _ => destruct p; break_all
| _ => idtac
end.
Lemma inv_row_involutive b p : inv_row (inv_row b p) p = b.
Proof.
break_all; reflexivity.
Qed.
(* Alternatively, a "basic" proof by algebraic properties of triple_map
and triple_map_select *)
Definition Involutive {X} (f : X -> X) := forall x, f (f x) = x.
Lemma triple_map_involutive {X} (f:X->X) :
Involutive f -> Involutive (triple_map f).
Proof.
intros H (x,y,z). simpl. now rewrite !H.
Qed.
Lemma triple_map_select_involutive {X} (f:X->X) p :
Involutive f -> Involutive (triple_map_select f p).
Proof.
intros H (x,y,z). destruct p; simpl; now rewrite H.
Qed.
Lemma inv_col_involutive b p : inv_col (inv_col b p) p = b.
Proof.
unfold inv_col.
apply triple_map_involutive.
apply triple_map_select_involutive.
red. now destruct x.
Qed.
Lemma move_sym b1 b2 : move b1 b2 -> move b2 b1.
Proof.
intros [(p,->)|(p,->)]. (* breaks the "or", the two "exists" and rewrite
the equations in one go :-) *)
- left. exists p. now rewrite inv_row_involutive.
- right. exists p. now rewrite inv_col_involutive.
Qed.
Inductive moves : board -> board -> Prop :=
| MovesRefl b : moves b b
| MovesStep b1 b2 b3 : moves b1 b2 -> move b2 b3 -> moves b1 b3.
Lemma moves_refl b : moves b b.
Proof.
apply MovesRefl.
Qed.
(* Do not attempt to prove symmetry yet (requires transivity) *)
Lemma moves_trans b1 b2 b3 : moves b1 b2 -> moves b2 b3 -> moves b1 b3.
Proof.
intros H H'. induction H'; auto.
apply MovesStep with b2; auto.
Qed.
Lemma move_moves b1 b2 : move b1 b2 -> moves b1 b2.
Proof.
intros. apply MovesStep with b1. apply MovesRefl. auto.
Qed.
Lemma moves_sym b1 b2 : moves b1 b2 -> moves b2 b1.
Proof.
induction 1.
- apply MovesRefl.
- apply moves_trans with b2; auto.
apply move_sym in H0. apply move_moves; auto.
Qed.
Lemma moves_start_target : moves start target.
Proof.
apply moves_trans with (inv_col start B).
- apply move_moves. right. now exists B.
- apply moves_trans with (inv_col (inv_col start B) A).
+ apply move_moves. right. now exists A.
+ apply move_moves. left. now exists C.
Qed.
Definition force_row b p :=
match board_proj b p A with
| Wh => b
| Bk => inv_row b p
end.
Definition force_col b p :=
match board_proj b A p with
| Wh => b
| Bk => inv_col b p
end.
Definition force_white b :=
force_col (force_col (force_row (force_row (force_row b A) B) C) B) C.
Lemma force_row_moves b p : moves b (force_row b p).
Proof.
unfold force_row.
destruct (board_proj b p A).
- apply move_moves. left. now exists p.
- apply moves_refl.
Qed.
Lemma force_col_moves b p : moves b (force_col b p).
Proof.
unfold force_col.
destruct (board_proj b A p).
- apply move_moves. right. now exists p.
- apply moves_refl.
Qed.
Lemma force_white_moves b : moves b (force_white b).
Proof.
unfold force_white.
(* let's name all sub-expressions *)
set (b1 := force_row b A).
set (b2 := force_row b1 B).
set (b3 := force_row b2 C).
set (b4 := force_col b3 B).
set (b5 := force_col b4 C).
apply moves_trans with b1; [ apply force_row_moves | ].
apply moves_trans with b2; [ apply force_row_moves | ].
apply moves_trans with b3; [ apply force_row_moves | ].
apply moves_trans with b4; [ apply force_col_moves | ].
apply force_col_moves.
Qed.
(* for question 3, no easy way to go except via "computational" proof
(for inv_row and inv_col separatly) *)
Lemma inv_row_force_white b p : force_white (inv_row b p) = force_white b.
Proof.
break_all; reflexivity.
Qed.
Lemma inv_col_force_white b p : force_white (inv_col b p) = force_white b.
Proof.
break_all; reflexivity.
Qed.
Lemma move_force_white b1 b2 : move b1 b2 -> force_white b1 = force_white b2.
Proof.
intros [(p,->)|(p,->)].
- symmetry. apply inv_row_force_white.
- symmetry. apply inv_col_force_white.
Qed.
Lemma moves_force_white b1 b2 : moves b1 b2 <-> force_white b1 = force_white b2.
Proof.
split.
- induction 1; auto.
apply move_force_white in H0. now rewrite <- H0.
- intros H.
apply moves_trans with (force_white b1).
+ apply force_white_moves.
+ apply moves_trans with (force_white b2).
* rewrite H. apply moves_refl.
* apply moves_sym. apply force_white_moves.
Qed.
Lemma non_moves : ~(moves white_board start).
Proof.
intros H. apply moves_force_white in H. discriminate.
Qed.
Lemma moves_start_target_bis : moves start target.
Proof.
apply moves_force_white. reflexivity.
Qed.
(* Since decidability statements are "algorithmic", they are
usually done with a "Definition" keyword instead of a "Lemma".
Anyway, both syntax are equivalent here (as long as you do not
provide the definition body via := ). *)
Definition color_dec (c c' : color) : { c = c' }+{ c <> c' }.
Proof.
(*decide equality. *) (* specialized tactic for this kind of decidibility *)
(* Or otherwise : *)
destruct c, c'.
- now left.
- now right.
- now right.
- now left.
Defined. (* same as Qed, but allows computations in Coq later *)
Definition triple_dec {X} :
(forall x y : X, { x = y }+{ x<>y }) ->
forall t t' : triple X, { t = t' }+{ t<>t' }.
Proof.
(* decide equality. *)
(* Otherwise : *)
intros Xdec (x1,y1,z1) (x2,y2,z2).
destruct (Xdec x1 x2).
- destruct (Xdec y1 y2).
+ destruct (Xdec z1 z2).
* left. now f_equal.
* right. injection 1. auto.
+ right. injection 1. auto.
- right. injection 1. auto.
Defined.
Definition board_dec : forall b b' : board, { b = b' }+{ b <> b' }.
Proof.
apply triple_dec.
apply triple_dec.
apply color_dec.
Defined.
Definition moves_dec b b' : { moves b b' }+{ ~moves b b' }.
Proof.
destruct (board_dec (force_white b) (force_white b')).
- left. now apply moves_force_white.
- right. intro H. apply moves_force_white in H. auto.
Defined.
(* If "Defined" has been used at the end of the previous proofs,
the following computation will go through and end on "left" or "right" *)
Compute moves_dec start target.
(* left ... *)
Compute moves_dec white_board start.
(* right ... *)
(* You can also turn moves_dec into some OCaml code : *)
Require Extraction.
Recursive Extraction moves_dec start target white_board.
(* And then load all this code in an OCaml toplevel and run for instance:
moves_dec start target
*)
......@@ -48,7 +48,7 @@ It is recommended to use first the `Set Implicit Arguments` command to avoid wri
3. Define a relation `move : board -> board -> Prop` such that `move b1 b2` states that `b2` is obtained from `b1` by flipping over one row or one column.
4. Prove that this `move` relation is symmetric.
5. Define inductively the relation `moves : board -> board -> Prop` from the two following rules:
- Fora all `b`, we have `moves b b`
- For all `b`, we have `moves b b`
- If `moves b1 b2` and `move b2 b3` then `moves b1 b3` (for all `b1`, `b2`, `b3`).
6. Prove that the `moves` relation is reflexive, symmetric and transitive.
7. Prove that `moves start target`.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment