Merge pull request #118 from coq-community/code-nitpicks

code formatting fixes

theories/AAC.v

@@ -57,27 +57,29 @@ End sigma.
 
 (** ** Classes for properties of operators *)
 
-Class Associative (X:Type) (R:relation X) (dot: X -> X -> X) :=
+Class Associative (X : Type) (R : relation X) (dot : X -> X -> X) :=
   law_assoc : forall x y z, R (dot x (dot y z)) (dot (dot x y) z).
-Class Commutative (X:Type) (R: relation X) (plus: X -> X -> X) :=
+Class Commutative (X : Type) (R : relation X) (plus : X -> X -> X) :=
   law_comm: forall x y, R (plus x y) (plus y x).
-Class Idempotent (X:Type) (R: relation X) (plus: X -> X -> X) :=
+Class Idempotent (X : Type) (R : relation X) (plus : X -> X -> X) :=
   law_idem: forall x, R (plus x x) x.
-Class Unit (X:Type) (R:relation X) (op : X -> X -> X) (unit:X) := {
+Class Unit (X : Type) (R : relation X) (op : X -> X -> X) (unit : X) := {
   law_neutral_left: forall x, R (op unit x) x;
   law_neutral_right: forall x, R (op x unit) x
-                                                               }.
+}.
+
 Register Associative as aac_tactics.classes.Associative.
 Register Commutative as aac_tactics.classes.Commutative.
 Register Idempotent as aac_tactics.classes.Idempotent.
 Register Unit as aac_tactics.classes.Unit.
 
 (** class used to find the equivalence relation on which operations
    are A or AC, starting from the relation appearing in the goal *)
-Class AAC_lift X (R: relation X) (E : relation X) := {
+Class AAC_lift (X : Type) (R : relation X) (E : relation X) := {
   aac_lift_equivalence : Equivalence E;
   aac_list_proper : Proper (E ==> E ==> iff) R
-                                                    }.
+}.
+
 Register AAC_lift as aac_tactics.internal.AAC_lift.
 Register aac_lift_equivalence as aac_tactics.internal.aac_lift_equivalence.
 
@@ -624,7 +626,8 @@ Section s.
           apply proper; [apply law_comm|reflexivity].     
       - induction k as [[b m]|[b m] k IHk]; simpl; simpl in IHh.
         * destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl.
-          rewrite  (law_comm _ (copy m (eval a))), law_assoc, <- copy_plus, Pplus_comm; auto.
+          rewrite  (law_comm _ (copy m (eval a))).
+          rewrite law_assoc, <- copy_plus, Pplus_comm; auto.
           rewrite <- law_assoc, IHh. reflexivity.
           rewrite law_comm. reflexivity.
         * simpl in IHk.
@@ -700,8 +703,7 @@ Section s.
     Proof.
       intros; unfold return_sum, run_msets.
       case (is_sum_spec); intros; subst.
-      - rewrite copy_mset_copy.
-        reflexivity.     
+      - rewrite copy_mset_copy; reflexivity.
       - rewrite eval_sum_nil. apply copy_n_unit. auto.
       - reflexivity.
     Qed.
@@ -768,7 +770,7 @@ Section s.
     | is_prd_spec_op :
       forall j l, j = i -> is_prd_spec_ind (prd j l) (Is_op l)
     | is_prd_spec_unit :
-      forall j, is_unit j = true ->  is_prd_spec_ind (unit j) (Is_unit j)
+      forall j, is_unit j = true -> is_prd_spec_ind (unit j) (Is_unit j)
     | is_prd_spec_nothing :
       forall u, is_prd_spec_ind u (Is_nothing).
 

theories/Caveats.v

@@ -372,6 +372,6 @@ Section Z.
   Abort.
 
   (** The behavior of the tactic is not satisfying in this case. It is
-    still unclear how to handle properly this kind of situation : we plan
-    to investigate on this in the future. *)
+    still unclear how to handle properly this kind of situation; we plan
+    to investigate this in the future. *)
 End Z.

theories/Instances.v

@@ -55,19 +55,19 @@ Module Z.
 
   (** ** Z instances *)
 
-  #[export] Instance aac_Zplus_Assoc : Associative eq Zplus :=  Zplus_assoc.
-  #[export] Instance aac_Zplus_Comm : Commutative eq Zplus :=  Zplus_comm.
+  #[export] Instance aac_Zplus_Assoc : Associative eq Zplus := Zplus_assoc.
+  #[export] Instance aac_Zplus_Comm : Commutative eq Zplus := Zplus_comm.
 
-  #[export] Instance aac_Zmult_Comm : Commutative eq Zmult :=  Zmult_comm.
-  #[export] Instance aac_Zmult_Assoc : Associative eq Zmult :=  Zmult_assoc.
+  #[export] Instance aac_Zmult_Comm : Commutative eq Zmult := Zmult_comm.
+  #[export] Instance aac_Zmult_Assoc : Associative eq Zmult := Zmult_assoc.
 
-  #[export] Instance aac_Zmin_Comm : Commutative eq Z.min :=  Z.min_comm.
-  #[export] Instance aac_Zmin_Assoc : Associative eq Z.min :=  Z.min_assoc.
-  #[export] Instance aac_Zmin_Idem : Idempotent eq Z.min :=  Z.min_idempotent.
+  #[export] Instance aac_Zmin_Comm : Commutative eq Z.min := Z.min_comm.
+  #[export] Instance aac_Zmin_Assoc : Associative eq Z.min := Z.min_assoc.
+  #[export] Instance aac_Zmin_Idem : Idempotent eq Z.min := Z.min_idempotent.
 
-  #[export] Instance aac_Zmax_Comm : Commutative eq Z.max :=  Z.max_comm.
-  #[export] Instance aac_Zmax_Assoc : Associative eq Z.max :=  Z.max_assoc.
-  #[export] Instance aac_Zmax_Idem : Idempotent eq Z.max :=  Z.max_idempotent.
+  #[export] Instance aac_Zmax_Comm : Commutative eq Z.max := Z.max_comm.
+  #[export] Instance aac_Zmax_Assoc : Associative eq Z.max := Z.max_assoc.
+  #[export] Instance aac_Zmax_Idem : Idempotent eq Z.max := Z.max_idempotent.
 
   #[export] Instance aac_one : Unit eq Zmult 1 :=
     Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. 

theories/Tutorial.v

@@ -364,13 +364,11 @@ Section AAC_normalise.
     aac_normalise.
   Abort.
 
-  Print HintDb typeclass_instances.
-
   Goal Z.max (a+b) (b+a) = a+b.
     aac_reflexivity.
     Show Proof.
   Abort.
-  
+
 End AAC_normalise.
 
 (** ** Examples from previous website *)
@@ -411,9 +409,12 @@ Section Examples.
   Notation "x ^2" := (x*x) (at level 40).
   Notation "2 ⋅ x" := (x+x) (at level 41).
 
-  Lemma Hbin1: forall x y, (x+y)^2   = x^2 + y^2 +  2⋅x*y. Proof. intros; ring. Qed.
-  Lemma Hbin2: forall x y, x^2 + y^2 = (x+y)^2   + -(2⋅x*y). Proof. intros; ring.  Qed.
-  Lemma Hopp : forall x, x + -x = 0. Proof. apply Zplus_opp_r. Qed.
+  Lemma Hbin1: forall x y, (x+y)^2   = x^2 + y^2 +  2⋅x*y.
+  Proof. intros; ring. Qed.
+  Lemma Hbin2: forall x y, x^2 + y^2 = (x+y)^2   + -(2⋅x*y).
+  Proof. intros; ring. Qed.
+  Lemma Hopp : forall x, x + -x = 0.
+  Proof. apply Zplus_opp_r. Qed.
 
   Variables a b c : Z.
   Hypothesis H : c^2 + 2⋅(a+1)*b  = (a+1+b)^2.