From 3f44be507f3e3114db9a0488bc193face9586c25 Mon Sep 17 00:00:00 2001 From: Damien Pous Date: Fri, 20 Oct 2023 12:57:20 +0200 Subject: [PATCH] cleaned deprecated references and calls to intuition --- examples/paterson.v | 2 +- theories/kat_completeness.v | 18 +++++++++--------- theories/lang.v | 10 +++++----- theories/nfa.v | 2 +- theories/ugregex.v | 4 ++-- theories/ugregex_dec.v | 2 +- 6 files changed, 19 insertions(+), 19 deletions(-) diff --git a/examples/paterson.v b/examples/paterson.v index 9c61fcc..11eb726 100644 --- a/examples/paterson.v +++ b/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 *) diff --git a/theories/kat_completeness.v b/theories/kat_completeness.v index 252d9d8..dc80a52 100644 --- a/theories/kat_completeness.v +++ b/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. diff --git a/theories/lang.v b/theories/lang.v index 7da5e36..5430d9f 100644 --- a/theories/lang.v +++ b/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. diff --git a/theories/nfa.v b/theories/nfa.v index 58963a8..4767913 100644 --- a/theories/nfa.v +++ b/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. diff --git a/theories/ugregex.v b/theories/ugregex.v index be1f9a8..f885e70 100644 --- a/theories/ugregex.v +++ b/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. diff --git a/theories/ugregex_dec.v b/theories/ugregex_dec.v index dd834db..d2b2cb6 100644 --- a/theories/ugregex_dec.v +++ b/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.