cleaned deprecated references and calls to intuition

examples/paterson.v

@@ -51,7 +51,7 @@ Proof. destruct x; destruct y; simpl; try constructor; congruence. Qed.
 Lemma eqb_false x y: x<>y -> eqb x y = false.
 Proof. case eqb_spec; congruence. Qed.
 Lemma neqb_spec x y: negb (eqb x y) <-> x<>y.
-Proof. case eqb_spec; intuition; congruence. Qed.
+Proof. case eqb_spec; intuition easy. Qed.
 
 
 (** * Arithmetic and Boolean expressions *)

theories/kat_completeness.v

@@ -440,8 +440,8 @@ Import syntax.
 Lemma o_pred_level x: e_level (o_pred x) ≪ BKA
   with o_npred_level x: e_level (o_npred x) ≪ BKA. 
 Proof.
-  destruct x; simpl o_pred; simpl e_level; rewrite ?merge_spec; intuition. 
-  destruct x; simpl o_npred; simpl e_level; rewrite ?merge_spec; intuition. 
+  destruct x; simpl o_pred; simpl e_level; rewrite ?merge_spec; intuition easy. 
+  destruct x; simpl o_npred; simpl e_level; rewrite ?merge_spec; intuition easy. 
 Qed.
 End n.
 
@@ -461,7 +461,7 @@ Proof. apply f_sup_eq; now f_equal. Qed.
 Lemma o_level n m (e: gregex n m): e_level (o e) ≪ BKA. 
 Proof.
   pose proof o_pred_level. 
-  induction e; simpl o; simpl e_level; rewrite ?merge_spec; intuition. 
+  induction e; simpl o; simpl e_level; rewrite ?merge_spec; intuition easy. 
 Qed.
 
 (** ** [o': expr3 n m -> gregex n m] *)
@@ -587,15 +587,15 @@ Definition gword_to_word' (w: gword) :=
 
 Lemma gword_to_word_cut n w: 
   gword_to_word n w = atom_to_word n (thead w) ++ gword_to_word' w.
-Proof. destruct w. apply app_nil_end. reflexivity. Qed.
+Proof. destruct w. now rewrite app_nil_r. reflexivity. Qed.
 
 Lemma gword_tapp: forall x y z, tapp x y z -> 
   forall n, gword_to_word n z = gword_to_word n x ++ gword_to_word' y. 
 Proof.
   induction 1; simpl; intros n. 
-   apply app_nil_end.
+   now rewrite app_nil_r.
    reflexivity. 
-   now rewrite IHtapp, app_ass. 
+   now rewrite IHtapp, <-app_assoc. 
 Qed.
 
 
@@ -677,7 +677,7 @@ Proof.
     destruct (Hf (gword_to_word m y)) as [? <- [y' Hy' Hay']].
      repeat eexists; eauto. rewrite Ha. rewrite H1. apply tapp_nil_x.
     repeat eexists; eauto.
-    rewrite app_ass, <-Hay', (gword_to_word_cut m y), (gword_tapp Hg), <-app_ass.
+    rewrite <-app_assoc, <-Hay', (gword_to_word_cut m y), (gword_tapp Hg), app_assoc.
     congruence.
   - apply proj2 in He. apply proj2 in Hf.
     intros [ea [x Hx [? <- ->]] [y Hy ->]].
@@ -687,7 +687,7 @@ Proof.
     apply tapp_nil_x_eq in Hay' as [Ha ->].
     destruct (tapp_cat x' y' Ha) as [z Hz]. 
     repeat eexists; eauto. 2: apply tapp_x_nil.
-    rewrite (gword_tapp Hz), <-Hxa, app_ass, Hay, gword_to_word_cut, ass_app.
+    rewrite (gword_tapp Hz), <-Hxa, <-app_assoc, Hay, gword_to_word_cut, <-app_assoc.
     congruence.
 Qed.
 
@@ -727,7 +727,7 @@ Proof.
     apply Hext. clear Hext.
     eexists. eassumption. eexists. apply IHn. apply Haw. 
     assumption.
-    rewrite (gword_tapp H'), Hxe, gword_to_word_cut, Haw, app_ass. congruence.
+    rewrite (gword_tapp H'), Hxe, gword_to_word_cut, Haw, <-app_assoc. congruence.
   - apply itr_ind_l.
     now rewrite <-H, <-itr_ext, dotA.
     rewrite <-itr_cons at 2.

theories/lang.v

@@ -70,15 +70,15 @@ Lemma lang_dotA n m p q x y z:
   lang_dot n m q x (lang_dot m p q y z) ≡ lang_dot n p q (lang_dot n m p x y) z.
 Proof.
   intro w. split. 
-  intros [u Hu [v [u' Hu' [v' Hv' ->]] ->]]. repeat eexists; eauto. apply ass_app.
-  intros [u [u' Hu' [v' Hv' ->]] [v Hv ->]]. repeat eexists; eauto. apply app_ass.
+  intros [u Hu [v [u' Hu' [v' Hv' ->]] ->]]. repeat eexists; eauto. now rewrite app_assoc.
+  intros [u [u' Hu' [v' Hv' ->]] [v Hv ->]]. repeat eexists; eauto. now rewrite app_assoc.
 Qed.
 
 Lemma lang_dotx1 x: lang_dot tt tt tt x (lang_one tt) ≡ x.
 Proof.
   intro w. split. 
-   intros [u Hu [v <- ->]]. now rewrite <-app_nil_end. 
-   intro Hw. exists w; trivial. exists nil.  reflexivity. apply app_nil_end.
+   intros [u Hu [v <- ->]]. now rewrite app_nil_r. 
+   intro Hw. exists w; trivial. exists nil.  reflexivity. now rewrite app_nil_r.
 Qed.
 
 Lemma lang_dot_leq n m p: Proper (leq ==> leq ==> leq) (lang_dot n m p).
@@ -109,7 +109,7 @@ Proof.
    intros w [u Hu [v [i Hi] ->]]. exists (S i). repeat eexists; eauto.
    intros w [u [i Hu] [v Hv ->]]. revert u Hu. induction i. 
     now intros u <-.
-    intros u [u' Hu' [u'' Hu'' ->]]. apply H0. rewrite app_ass. eexists; eauto. 
+    intros u [u' Hu' [u'' Hu'' ->]]. apply H0. rewrite <-app_assoc. eexists; eauto. 
    intro w. split. 
     intros [i H']. apply lang_iter_S in H' as [? ? [? ? ?]]. repeat eexists; eauto.
     intros [? ? [? [i H'] ?]]. exists i. apply lang_iter_S. repeat eexists; eauto.

theories/nfa.v

@@ -93,7 +93,7 @@ Proof. intros ? ? H ? ? <-. now apply lang_weq. Qed.
 Lemma lang_empty n (u: rmx 1 n) M v: u ≡0 -> lang M v u ≡ bot.
 Proof. 
   intros Hu w. revert Hu. induction w; intro Hu. simpl; fold_regex. 
-  rewrite Hu, dot0x. intuition. 
+  rewrite Hu, dot0x. intuition discriminate. 
   simpl. rewrite <-IHw by assumption. now rewrite Hu, dot0x.
 Qed.
 

theories/ugregex.v

@@ -74,7 +74,7 @@ Proof.
    now intros ? ? ?.
    now intros _ ? ?.
    discriminate. 
-   intros _ [a|]; simpl; intuition; discriminate. 
+   intros _ [a|]; simpl; intuition discriminate. 
    discriminate. 
    discriminate.
    reflexivity. 
@@ -163,7 +163,7 @@ Proof.
 Qed.
 
 Lemma lang_0: lang u_zer ≡ 0.
-Proof. intros [?|???]; simpl; intuition; discriminate. Qed.
+Proof. intros [?|???]; simpl; intuition discriminate. Qed.
 
 Lemma lang_1: lang u_one ≡ 1.
 Proof. intros [a|???]; simpl. intuition. reflexivity. Qed.

theories/ugregex_dec.v

@@ -294,7 +294,7 @@ Proof.
   unfold loop. rewrite powerfix_linearfix. generalize (pow2 n). clear n. intro n.
   induction n; intros rel todo Hloop Hrel Hvars. discriminate. 
   simpl in Hloop. destruct todo as [|[e f] todo]. 
-   exists rel. split. now rewrite <- app_nil_end. now rewrite <-app_nil_end in Hrel. 
+   exists rel. split. now rewrite app_nil_r. now rewrite app_nil_r in Hrel. 
    revert Hloop. case rel_mem_spec. 
    intros Hef Hloop. apply IHn in Hloop as (rel'&H1&H2).
     eexists. split. 2: eassumption.