(* Ćwiczenie zapożyczone stąd: http://www.di.ens.fr/~zappa/teaching/coq/ecole11/ *) (* We consider the discrete plan the coordinate system of which is based on Z *) Require Import List. Require Import ZArith. Require Import Bool. Open Scope Z_scope. (* Define a record type for points in the plane *) Record Point : Type := {Point_x : Z; Point_y: Z}. Definition Point_O := Build_Point 0 0. Definition translate (dx dy:Z) (P : Point) := Build_Point (Point_x P + dx) (Point_y P + dy). (* Define a boolean function Point_eqb for deciding equality between Points *) (* Prove the correctness of Point_eqb *) (* Let us define a type for routes in the plane *) Inductive direction : Type := North | East | South | West. Definition route := list direction. (* We define a function move : Point -> route -> Point : move P r follows the route r starting from P *) Fixpoint move (P:Point) (r:route) : Point := match r with | nil => P | North :: r' => move (translate 0 1 P) r' | East :: r' => move (translate 1 0 P) r' | South :: r' => move (translate 0 (-1) P) r' | West :: r' => move (translate (-1) 0 P) r' end. (* We consider that two routes are "equivalent" if they define the same moves. For instance, the routes East::North::West::South::East::nil and East::nil are equivalent *) Definition route_equiv : relation route := fun r r' => forall P, move P r = move P r'. (* Prove the following equivalence. Hint : you may use f_equal and ring tactics *) Example Ex1 : route_equiv (East::North::West::South::East::nil) (East::nil). Admitted. (* Prove that route_equiv is reflexive, symmetric and transitive *) Lemma route_equiv_refl : reflexive _ route_equiv. Admitted. Lemma route_equiv_sym : symmetric _ route_equiv. Admitted. Lemma route_equiv_trans : transitive _ route_equiv. Admitted. (***** cut here for class 8 ****) Instance route_equiv_Equiv : Equivalence route_equiv. (* Do it yourself *) Admitted. (* Prove that cons and app are Proper wrt route_equiv *) Require Import Morphisms. Instance cons_route_Proper (d:direction): Proper (route_equiv ==> route_equiv) (cons d) . (* do it yourself *) Admitted. Lemma route_compose : forall r r' P, move P (r++r') = move (move P r) r'. (* do it yourself *) Admitted. Instance app_route_Proper : Proper (route_equiv ==>route_equiv==>route_equiv) (@app direction). (* do it yourself *) Admitted. (* Monoids w.r.t. some equivalence relation *) Class EMonoid {A:Type}(E_eq :relation A)(dot : A->A->A)(one : A):={ E_rel :> Equivalence E_eq; dot_proper :> Proper (E_eq ==> E_eq ==> E_eq) dot; E_dot_assoc : forall x y z:A, E_eq (dot x (dot y z)) (dot (dot x y) z); E_one_left : forall x, E_eq (dot one x) x; E_one_right : forall x, E_eq (dot x one) x}. Instance Route : EMonoid route_equiv (@app _) nil . (* do it yourself *) Admitted. (* (difficult) : prove the following lemmas *) Lemma translate_comm : forall dx dy dx' dy' P, translate dx dy (translate dx' dy' P) = translate dx' dy' (translate dx dy P). Proof. (* do it yourself *) Admitted. Lemma move_translate : forall r P dx dy , move (translate dx dy P) r = translate dx dy (move P r). (* do it yourself *) Admitted. Lemma route_equiv_Origin : forall r r', route_equiv r r' <-> move Point_O r = move Point_O r'. Proof. (* difficult *) Admitted. (* Then build a boolean function route_equivb for deciding route equivalence ... *) (* ... and prove its correctness *) (* Now, we can prove our previous example by reflexion, (using route_equivb) *) Example Ex1' : route_equiv (East::North::West::South::East::nil) (East::nil). Admitted. (* Using the tactics rewrite, setoid_replace, etc. prove the following lemmas *) Lemma north_south_0 : forall r, route_equiv (North::South::r) r. Admitted. Lemma north_south_simpl : forall r r', route_equiv (r++ North::South::r') (r++r'). Admitted.