Merge pull request #26 : replace omega with lia

coq-community · Dec 14, 2020 · fe2d457 · fe2d457
2 parents 135b108 + f4d36a6
commit fe2d457
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 27 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -2,7 +2,6 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -duplicate-clear
 -arg -w -arg -notation-incompatible-format
--arg -w -arg -omega-is-deprecated
 theories/misc.v
 theories/setoid_leq.v
 theories/languages.v

diff --git a/theories/nfa.v b/theories/nfa.v
@@ -240,7 +240,8 @@ Qed.
 Lemma enfa_concIr (p : A2) x : nfa_accept p x -> @enfa_accept enfa_conc (inr p) x.
 Proof.
   elim: x p => [p Hp|a x IH p /= /exists_inP [q q1 q2]].
-  - by constructor; rewrite mem_imset.
+  - (* compat: <mathcomp-1.12 *)
+    constructor; solve [exact: imset_f|exact:mem_imset]. 
   - apply: (@EnfaSome enfa_conc _ _ (inr q)) => //. exact: IH.
 Qed.
 
@@ -255,7 +256,8 @@ Qed.
 Lemma enfa_concP x : reflect (enfa_lang enfa_conc x) (conc (nfa_lang A1) (nfa_lang A2) x).
 Proof.
   apply: (iffP (@concP _ _ _ _)) => [[x1] [x2] [X1 [X2 X3]] |].
-  - case/exists_inP : X2 => s ? ?. exists (inl s); first by rewrite /enfa_conc /= mem_imset.
+  - (* compat: <mathcomp-1.12 *)
+    case/exists_inP : X2 => s ? ?. exists (inl s); first solve [exact: imset_f|exact:mem_imset].
     subst. exact: enfa_concIl.
   - move => [[s /imsetP [? ? [?]] /enfa_concE [x1] [x2] [? ? ?] |s]]; last by case/imsetP.
     exists x1; exists x2. repeat (split => //). apply/exists_inP. by exists s;subst.

diff --git a/theories/shepherdson.v b/theories/shepherdson.v
@@ -1,6 +1,6 @@
 (* Author: Christian Doczkal  *)
 (* Distributed under the terms of CeCILL-B. *)
-From Coq Require Import Omega.
+From Coq Require Import Lia.
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc setoid_leq languages dfa myhill_nerode two_way.
 
@@ -38,12 +38,12 @@ Proof.
   by rewrite !(tnth_nth a) /= -e nth_cat ltnNge leq_addr /= addKn.
 Qed.
 
-(** Wrapper for omega that uses ssreflects operators on [nat] *)
+(** Wrapper for [lia] that uses ssreflects operators on [nat] *)
 
 Ltac norm := rewrite ?(size_cat,cats0); simpl in *.
 Ltac normH := match goal with [ H : is_true (_ <= _) |- _] => move/leP : H end.
-Ltac somega :=
-  try (try (apply/andP; split); apply/leP; repeat normH; norm ; rewrite ?addnE /addn_rec ; intros; omega).
+Ltac ssrlia :=
+  try (try (apply/andP; split); apply/leP; repeat normH; norm ; rewrite ?addnE /addn_rec ; intros; lia).
 
 Section NFA2toAFA.
 
@@ -85,7 +85,7 @@ Section NFA2toAFA.
   Proof. move/srel_step. case/orP => /andP [_ /eqP ->]; tauto. Qed.
 
   Lemma srel1 k x c d : srel k x c d -> d.2 <= c.2.+1.
-  Proof. move: c d => [p i] [q j] /srelLR [<-|->] //=. by somega. Qed.
+  Proof. move: c d => [p i] [q j] /srelLR [<-|->] //=. by ssrlia. Qed.
 
   Lemma srelSr k' k x (c d : nfa2_config M x) : c.2 < k ->
     srel k x c d = srel (k+k') x c d. 
@@ -137,7 +137,7 @@ Section NFA2toAFA.
     - by rewrite /= -inord0 ord2P0.
     - apply: contraN Hk. by rewrite (eqP E). 
     - have oi : i < size (x++z) by rewrite size_cat ltn_addr.
-      have H_eq: (Ordinal oi).+1 = (inord k : pos (x++z)). by rewrite -Hi inordK // ; somega.
+      have H_eq: (Ordinal oi).+1 = (inord k : pos (x++z)). by rewrite -Hi inordK // ; ssrlia.
       by rewrite (ord2PC H_eq) -(tnthL (i := i)).
   Qed.
 
@@ -151,10 +151,10 @@ Section NFA2toAFA.
       srel (size x).+1 x (p,i) (q,j) = srel (size x).+1 (x++z) (p,inord i) (q,inord j).
     Proof.
       case: (boolP (i == (size x).+1 :> nat)) => Hi. 
-      - rewrite /srel (eqP Hi) /= inordK ?eqxx //= ?andbF //; somega.
+      - rewrite /srel (eqP Hi) /= inordK ?eqxx //= ?andbF //; ssrlia.
       - have Hi' : i < (size x).+1. by rewrite ltn_neqAle Hi -ltnS ltn_ord.
-        rewrite /srel /step readL // !inordK //; somega.
-        move: (ltn_ord j) => ?. somega.
+        rewrite /srel /step readL // !inordK //; ssrlia.
+        move: (ltn_ord j) => ?. ssrlia.
     Qed.
 
     Lemma runL (i j : pos x) p q :
@@ -165,7 +165,7 @@ Section NFA2toAFA.
       rewrite -[(p,inord i)]/(f (p,i)) -[(q,inord j)]/(f (q,j)).
       apply: connect_transfer => //.
       - move => {p q i j} [p i] [q j] /= [->] /inord_inj. 
-        case/(_ _)/Wrap => [|->//]. somega.
+        case/(_ _)/Wrap => [|->//]. ssrlia.
       - move => [? ?] [? ?]. rewrite /f /=. exact: srelL.  
       - move => {p q i j} [p i] [q j] step. exists (q,inord j). 
         rewrite /f /= inordK ?inord_val //.  move: (srel1 step) => /= Hs.
@@ -197,25 +197,25 @@ Section NFA2toAFA.
       - by rewrite -[k](@inordK (size z).+1) ?(eqP H) //= addnS -size_cat -inord_max ord2PM.
       - have Hi' : size x + i < size (x ++ z) by rewrite size_cat ltn_add2l.
         have X: (Ordinal Hi').+1 = (inord (size x + k) : pos (x ++ z)). 
-          by rewrite /= -addnS Hi !inordK //; somega. 
+          by rewrite /= -addnS Hi !inordK //; ssrlia. 
         by rewrite (ord2PC X) -(tnthR (i := i)). 
     Qed.
 
     Lemma srelR (m k k' : nat) p p' : k != 0 -> k < (size z).+2 -> k' < (size z).+2 ->
         srel ((size x).+1 + m) (x++z) (p,inord (size x + k)) (p',inord (size x + k'))
       = srel m.+1 z (p,inord k) (p',inord k').
     Proof.
-      move => Hk0 Hk Hk'. rewrite /srel /= !inordK ?addSnnS ?eqn_add2l //; somega.
+      move => Hk0 Hk Hk'. rewrite /srel /= !inordK ?addSnnS ?eqn_add2l //; ssrlia.
       case: (_ != _); rewrite ?andbT ?andbF // /step -?readR //. 
-      rewrite !inordK //; somega. by rewrite -!addnS !eqn_add2l.
+      rewrite !inordK //; ssrlia. by rewrite -!addnS !eqn_add2l.
     Qed.
 
     Lemma srelRE m k p c : k < (size z).+2 -> k != 0 -> 
       srel m (x++z) (p,inord (size x + k)) c -> 
       exists q k', k' < (size z).+2 /\ c = (q,inord (size x + k')).
     Proof.
       move: k c => [//|k] [q j] Hk _ /srelLR [/eqP C|/eqP C];
-        exists q; rewrite inordK addnS ?eqSS in C; somega.
+        exists q; rewrite inordK addnS ?eqSS in C; ssrlia.
       - exists k. by rewrite ltnW // -[j]inord_val (eqP C).
       - exists k.+2. rewrite !addnS -[j]inord_val (eqP C). split => //.
         rewrite eqn_leq in C. case/andP : C => _ C. 
@@ -239,14 +239,14 @@ Section NFA2toAFA.
     apply: (size_induction (measure := size)) => /= cs IH i Hi p.
     case: (boolP (i == 0)) => Hi0.
     - rewrite (eqP Hi0) !addn0 => p1 p2.
-      case: (srel_mid_path (k := (size x).+1) _ p1 p2); try solve [rewrite inordI; somega].
-      apply/andP; split; rewrite !inordK; somega. move => p' [cl] [cr] [Ecs Lcl Pcl].
-      apply/(@srel_mid (size y).+1) ; try solve [rewrite !inordK; somega|rewrite -addn1; somega].
+      case: (srel_mid_path (k := (size x).+1) _ p1 p2); try solve [rewrite inordI; ssrlia].
+      apply/andP; split; rewrite !inordK; ssrlia. move => p' [cl] [cr] [Ecs Lcl Pcl].
+      apply/(@srel_mid (size y).+1) ; try solve [rewrite !inordK; ssrlia|rewrite -addn1; ssrlia].
       + exists p'. apply/Tab2P. rewrite -Tab_eq. apply/Tab2P. by apply/connectP; exists cl.
       + subst cs. rewrite -[_.+1 as X in inord X]addn1. 
-        apply: (IH cr) => {IH} //; somega.
+        apply: (IH cr) => {IH} //; ssrlia.
         * destruct cl as [|c cs]; simpl in *. case: Lcl => _. 
-          -- move/(f_equal (@nat_of_ord _)); rewrite ?inordK; intros; somega.
+          -- move/(f_equal (@nat_of_ord _)); rewrite ?inordK; intros; ssrlia.
           -- by  rewrite[size (cs ++ cr)]size_cat -addnS leq_addl.
         * rewrite cat_path -Lcl addn1 in p1 *. by case/andP : p1.
         * by rewrite p2 last_cat -Lcl addn1.
@@ -275,8 +275,8 @@ Section NFA2toAFA.
     { by apply/idP/idP; exact: W. }
     case/exists_inP => f Hq1 Hq2. apply/exists_inP; exists f => //. move: Hq2.
     rewrite -[x]cats0 -[y]cats0 -!(eq_connect (@srel_step_max _)).
-    case/(@srel_mid (size x).+1); somega => q /Tab1P q1 q2.
-    apply/(@srel_mid (size y).+1); somega.
+    case/(@srel_mid (size x).+1); ssrlia => q /Tab1P q1 q2.
+    apply/(@srel_mid (size y).+1); ssrlia.
     - exists q. apply/Tab1P. by rewrite -E.
     - move: q2 => {q1}. rewrite !inord_max.
       apply: (runR_eq (i := 1) (j := 1) (k := 1)); rewrite ?addn1 ?cats0 //=.
@@ -292,11 +292,11 @@ Section NFA2toAFA.
     apply/setP => q /=. rewrite !inE.
     pose C x := connect (srel (size (x ++ [:: a])).+1 (x ++ [:: a])) (nfa2_s M, ord1) (q, ord_max).
     wlog suff W: x y E Tab2 / C x -> C y; [by apply/idP/idP; exact: W|].
-    case/(@srel_mid (size x).+1); somega => p /Tab1P p1 p2.
-    apply/(@srel_mid (size y).+1); somega. 
+    case/(@srel_mid (size x).+1); ssrlia => p /Tab1P p1 p2.
+    apply/(@srel_mid (size y).+1); ssrlia. 
     exists p; first by apply/Tab1P; rewrite -E. move: p2. 
     rewrite -![_.+1 as X in inord X]addn1 -[1]/(size [:: a]) -!size_cat.
-    rewrite !(@runL _ [::]) !inordK; somega. move/Tab2P => p2. by apply/Tab2P; rewrite -Tab2.
+    rewrite !(@runL _ [::]) !inordK; ssrlia. move/Tab2P => p2. by apply/Tab2P; rewrite -Tab2.
   Qed.
 
   Definition nfa2_to_classifier : classifier_for (nfa2_lang M) :=