diff --git a/_CoqProject b/_CoqProject index dfe3d1a..673beee 100644 --- 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 index 8932f31..a67f001 100644 --- 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: //. 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: 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 index eeb440b..8e1f93d 100644 --- 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,7 +197,7 @@ 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. @@ -205,9 +205,9 @@ Section NFA2toAFA. 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 -> @@ -215,7 +215,7 @@ Section NFA2toAFA. 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) :=