comment on ssrlia tactic

util/ssrlia.v

@@ -3,32 +3,36 @@ Require Import Lia.
 
 (* Adopted from http://github.com/pi8027/formalized-postscript/blob/master/stdlib_ext.v *)
 
+(** This tactic matches over the hypotheses, searching for expressions that can 
+      be converted from [ssreflect] arithmetic to Coq arithmetic. *) 
 Ltac arith_hypo_ssrnat2coqnat :=
   match goal with
-    | H : context [andb _ _] |- _ => let H0 := fresh in case/andP: H => H H0
-    | H : context [orb _ _] |- _ => case/orP: H => H
-    | H : context [?L <= ?R] |- _ => move/leP: H => H
-    | H : context [?L < ?R] |- _ => move/ltP : H => H
-    | H : context [?L == ?R] |- _ => move/eqP : H => H
-    | H : context [addn ?L ?R] |- _ => rewrite -plusE in H
-    | H : context [muln ?L ?R] |- _ => rewrite -multE in H
-    | H : context [subn ?L ?R] |- _ => rewrite -minusE in H
+  | H : context [andb _ _] |- _ => let H0 := fresh in case/andP: H => H H0
+  | H : context [orb _ _] |- _ => case/orP: H => H
+  | H : context [?L <= ?R] |- _ => move/leP: H => H
+  | H : context [?L < ?R] |- _ => move/ltP : H => H
+  | H : context [?L == ?R] |- _ => move/eqP : H => H
+  | H : context [addn ?L ?R] |- _ => rewrite -plusE in H
+  | H : context [muln ?L ?R] |- _ => rewrite -multE in H
+  | H : context [subn ?L ?R] |- _ => rewrite -minusE in H
   end.
 
+(** This tactic matches the goal, searching for expressions that can be 
+      converted from [ssreflect] arithmetic to Coq arithmetic. *) 
 Ltac arith_goal_ssrnat2coqnat :=
   rewrite ?NatTrec.trecE -?plusE -?minusE -?multE -?leqNgt -?ltnNge;
   repeat match goal with
-    | |- is_true (andb _ _) => apply/andP; split
-    | |- is_true (orb _ _) => try apply/orP
-    | |- is_true (_ <= _) => try apply/leP
-    | |- is_true (_ < _) => try apply/ltP
-  end.
-
-(** Solve arithmetic goals.
-  This tactic first rewrites the context to replace operations from ssreflect
-  to the corresponding operations in the Coq library, then calls [lia]. *)
+         | |- is_true (andb _ _) => apply/andP; split
+         | |- is_true (orb _ _) => try apply/orP
+         | |- is_true (_ <= _) => try apply/leP
+         | |- is_true (_ < _) => try apply/ltP
+         end.
 
+(** Solves linear integer arithmetic goals containing [ssreflect] expressions. 
+    This tactic first rewrites the context to replace operations from [ssreflect]
+    to the corresponding operations in the Coq library, then calls [lia]. *)
 Ltac ssrlia :=
-  repeat arith_hypo_ssrnat2coqnat;
-  arith_goal_ssrnat2coqnat; simpl;
+  repeat arith_hypo_ssrnat2coqnat; arith_goal_ssrnat2coqnat;
+  simpl;
   lia.
+