From 17a143ccdc22a8133f7d70a5346271a8805c4f2a Mon Sep 17 00:00:00 2001 From: Andrej Dudenhefner Date: Mon, 15 Jul 2024 16:11:06 +0200 Subject: [PATCH] dealt with some 8.20 warnings --- theories/FOL/TRAKHTENBROT/Sig2_Sign.v | 2 +- theories/FOL/TRAKHTENBROT/Sig_one_rel.v | 2 +- theories/FOL/TRAKHTENBROT/Sig_rem_cst.v | 2 +- theories/FOL/TRAKHTENBROT/Sig_rem_props.v | 2 +- theories/FOL/TRAKHTENBROT/Sign_Sig.v | 4 ++-- theories/FOL/TRAKHTENBROT/Sign_Sig2.v | 2 +- theories/FOL/TRAKHTENBROT/btree.v | 2 +- theories/FOL/TRAKHTENBROT/fo_logic.v | 4 ++-- theories/FOL/TRAKHTENBROT/membership.v | 6 +++--- theories/FOL/TRAKHTENBROT/notations.v | 8 ++++---- theories/L/Prelim/ARS.v | 13 +++++++++---- .../StringRewriting/Reductions/SBTM_HALT_to_SR.v | 15 +++++++++++---- theories/_CoqProject | 2 +- 13 files changed, 38 insertions(+), 26 deletions(-) diff --git a/theories/FOL/TRAKHTENBROT/Sig2_Sign.v b/theories/FOL/TRAKHTENBROT/Sig2_Sign.v index f9878a096..85131f3c1 100644 --- a/theories/FOL/TRAKHTENBROT/Sig2_Sign.v +++ b/theories/FOL/TRAKHTENBROT/Sig2_Sign.v @@ -52,7 +52,7 @@ Section Sig2_Sig_n_encoding. Variable (X : Type) (M2 : fo_model Σ2 X) (Mn : fo_model Σn X). Notation "⟪ A ⟫" := (fun ψ => fol_sem M2 ψ A). - Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 1, format "⟪ A ⟫'"). + Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 0, format "⟪ A ⟫'"). Let P2 a b := fom_rels M2 tt (a##b##ø). Let Pn a b := fom_rels Mn tt (a##vec_set_pos (fun _ => b)). diff --git a/theories/FOL/TRAKHTENBROT/Sig_one_rel.v b/theories/FOL/TRAKHTENBROT/Sig_one_rel.v index ba6237ac0..33416f961 100644 --- a/theories/FOL/TRAKHTENBROT/Sig_one_rel.v +++ b/theories/FOL/TRAKHTENBROT/Sig_one_rel.v @@ -30,7 +30,7 @@ Set Implicit Arguments. (* * From several relations to one, arity incremented by 1 *) -Local Reserved Notation "⟪ A ⟫'" (at level 1, format "⟪ A ⟫'"). +Local Reserved Notation "⟪ A ⟫'" (at level 0, format "⟪ A ⟫'"). Local Notation ø := vec_nil. diff --git a/theories/FOL/TRAKHTENBROT/Sig_rem_cst.v b/theories/FOL/TRAKHTENBROT/Sig_rem_cst.v index b612cdb8b..6841010c6 100644 --- a/theories/FOL/TRAKHTENBROT/Sig_rem_cst.v +++ b/theories/FOL/TRAKHTENBROT/Sig_rem_cst.v @@ -24,7 +24,7 @@ Set Implicit Arguments. (* * From signatures with only constants functions to function symbol free signatures *) -Local Reserved Notation "⟪ A ⟫'" (at level 1, format "⟪ A ⟫'"). +Local Reserved Notation "⟪ A ⟫'" (at level 0, format "⟪ A ⟫'"). Local Notation ø := vec_nil. diff --git a/theories/FOL/TRAKHTENBROT/Sig_rem_props.v b/theories/FOL/TRAKHTENBROT/Sig_rem_props.v index 8fb0f12d7..cf3ce3715 100644 --- a/theories/FOL/TRAKHTENBROT/Sig_rem_props.v +++ b/theories/FOL/TRAKHTENBROT/Sig_rem_props.v @@ -24,7 +24,7 @@ Set Implicit Arguments. (* * Removing constant propositions from monadic signatures *) -Local Reserved Notation "⟪ A ⟫'" (at level 1, format "⟪ A ⟫'"). +Local Reserved Notation "⟪ A ⟫'" (at level 0, format "⟪ A ⟫'"). Local Notation ø := vec_nil. diff --git a/theories/FOL/TRAKHTENBROT/Sign_Sig.v b/theories/FOL/TRAKHTENBROT/Sign_Sig.v index 0b76a241b..e627c1537 100644 --- a/theories/FOL/TRAKHTENBROT/Sign_Sig.v +++ b/theories/FOL/TRAKHTENBROT/Sign_Sig.v @@ -53,7 +53,7 @@ Section Sig_n_Sig. Defined. Notation "⟪ A ⟫" := (fun ψ => fol_sem M ψ A). - Notation "⟪ A ⟫'" := (fun φ => fol_sem M_enc_n φ A) (at level 1, format "⟪ A ⟫'"). + Notation "⟪ A ⟫'" := (fun φ => fol_sem M_enc_n φ A) (at level 0, format "⟪ A ⟫'"). Local Fact enc_correct_1 A φ : ⟪ A ⟫' φ <-> ⟪ enc A ⟫ φ. Proof. @@ -96,7 +96,7 @@ Section Sig_n_Sig. Defined. Notation "⟪ A ⟫" := (fun ψ => fol_sem Mn_enc ψ A). - Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 1, format "⟪ A ⟫'"). + Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 0, format "⟪ A ⟫'"). Local Fact enc_correct_2 A φ : ⟪ A ⟫' φ <-> ⟪ enc A ⟫ φ. Proof. diff --git a/theories/FOL/TRAKHTENBROT/Sign_Sig2.v b/theories/FOL/TRAKHTENBROT/Sign_Sig2.v index 66374e794..914367a71 100644 --- a/theories/FOL/TRAKHTENBROT/Sign_Sig2.v +++ b/theories/FOL/TRAKHTENBROT/Sign_Sig2.v @@ -86,7 +86,7 @@ Section Sign_Sig2_encoding. -> P v <-> mb_is_tuple_in (fun a b => a ∈ₘ b) r w. Notation "⟪ A ⟫" := (fun ψ => fol_sem M2 ψ A). - Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 1, format "⟪ A ⟫'"). + Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 0, format "⟪ A ⟫'"). (* The correctness lemma *) diff --git a/theories/FOL/TRAKHTENBROT/btree.v b/theories/FOL/TRAKHTENBROT/btree.v index cc197291a..36e54e884 100644 --- a/theories/FOL/TRAKHTENBROT/btree.v +++ b/theories/FOL/TRAKHTENBROT/btree.v @@ -934,7 +934,7 @@ Proof. intros ? ? H; apply bte_ext; intro; do 2 rewrite bt_pow_spec; rewrite H; Definition bt_opair s t := (s⪧∅)⪧(s⪧t⪧∅)⪧∅. -Local Notation "⟬ s , t ⟭" := (bt_opair s t) (at level 1, format "⟬ s , t ⟭"). +Local Notation "⟬ s , t ⟭" := (bt_opair s t) (at level 0, format "⟬ s , t ⟭"). Section ordered_pairs. diff --git a/theories/FOL/TRAKHTENBROT/fo_logic.v b/theories/FOL/TRAKHTENBROT/fo_logic.v index 2c2a7324a..4d41e5541 100644 --- a/theories/FOL/TRAKHTENBROT/fo_logic.v +++ b/theories/FOL/TRAKHTENBROT/fo_logic.v @@ -606,10 +606,10 @@ Section fo_model_simulation. Infix "⋈" := R (at level 70, no associativity). Notation "⟦ t ⟧" := (fun φ => fo_term_sem M φ t). - Notation "⟦ t ⟧'" := (fun φ => fo_term_sem N φ t) (at level 1, format "⟦ t ⟧'"). + Notation "⟦ t ⟧'" := (fun φ => fo_term_sem N φ t) (at level 0, format "⟦ t ⟧'"). Notation "⟪ A ⟫" := (fun φ => fol_sem M φ A). - Notation "⟪ A ⟫'" := (fun φ => fol_sem N φ A) (at level 1, format "⟪ A ⟫'"). + Notation "⟪ A ⟫'" := (fun φ => fol_sem N φ A) (at level 0, format "⟪ A ⟫'"). (* The simulation lifts from variables to terms *) diff --git a/theories/FOL/TRAKHTENBROT/membership.v b/theories/FOL/TRAKHTENBROT/membership.v index f170d236c..16f8a7ddb 100644 --- a/theories/FOL/TRAKHTENBROT/membership.v +++ b/theories/FOL/TRAKHTENBROT/membership.v @@ -98,9 +98,9 @@ Section membership. + rewrite H1, H2; auto. Qed. - Reserved Notation "p ≋ ⦃ a , b ⦄" (at level 70, format "p ≋ ⦃ a , b ⦄"). - Reserved Notation "p ≋ ⦅ a , b ⦆" (at level 70, format "p ≋ ⦅ a , b ⦆"). - Reserved Notation "t ≋ ⦉ v ⦊" (at level 70, format "t ≋ ⦉ v ⦊"). + Reserved Notation "p ≋ ⦃ a , b ⦄" (at level 1, format "p ≋ ⦃ a , b ⦄"). + Reserved Notation "p ≋ ⦅ a , b ⦆" (at level 1, format "p ≋ ⦅ a , b ⦆"). + Reserved Notation "t ≋ ⦉ v ⦊" (at level 1, format "t ≋ ⦉ v ⦊"). Definition mb_is_pair p x y := forall a, a ∈ p <-> a ≈ x \/ a ≈ y. diff --git a/theories/FOL/TRAKHTENBROT/notations.v b/theories/FOL/TRAKHTENBROT/notations.v index 5161f99b7..026278037 100644 --- a/theories/FOL/TRAKHTENBROT/notations.v +++ b/theories/FOL/TRAKHTENBROT/notations.v @@ -74,15 +74,15 @@ Reserved Notation "⇡ sig" (at level 1, format "⇡ sig"). (* Term substitution and semantics *) Reserved Notation "t '⟬' σ '⟭'" (at level 1, format "t ⟬ σ ⟭"). -Reserved Notation "'⟦' t '⟧'" (at level 1, format "⟦ t ⟧"). +Reserved Notation "'⟦' t '⟧'" (at level 0, format "⟦ t ⟧"). (* Formula subsitution and semantics*) Reserved Notation "f '⦃' σ '⦄'" (at level 1, format "f ⦃ σ ⦄"). -Reserved Notation "'⟪' f '⟫'" (at level 1, format "⟪ f ⟫"). +Reserved Notation "'⟪' f '⟫'" (at level 0, format "⟪ f ⟫"). (* Unary ops *) -Reserved Notation "⌞ x ⌟" (at level 1, format "⌞ x ⌟"). +Reserved Notation "⌞ x ⌟" (at level 0, format "⌞ x ⌟"). Reserved Notation "↓ x" (at level 1, format "↓ x"). Reserved Notation "x †" (at level 1, format "x †"). @@ -92,7 +92,7 @@ Reserved Notation "x ∙ y" (at level 2, right associativity, format "x ∙ y") Reserved Notation "x ⪧ y" (at level 2, right associativity, format "x ⪧ y"). Reserved Notation "x → y" (at level 2, right associativity, format "x → y"). -Reserved Notation "⟬ s , t ⟭" (at level 1, format "⟬ s , t ⟭"). +Reserved Notation "⟬ s , t ⟭" (at level 0, format "⟬ s , t ⟭"). Reserved Notation "x ∪ y" (at level 52, left associativity). (* Infix Binary rels *) diff --git a/theories/L/Prelim/ARS.v b/theories/L/Prelim/ARS.v index 80e293816..3770c88b6 100644 --- a/theories/L/Prelim/ARS.v +++ b/theories/L/Prelim/ARS.v @@ -106,7 +106,8 @@ Section FixX. Lemma ecl_sym R : symmetric (ecl R). Proof. - induction 1; eauto using ecl, (@ecl_trans R). + pose proof (@ecl_trans R). + induction 1; eauto using ecl. Qed. Lemma star_ecl R : @@ -164,7 +165,9 @@ Section FixX. + exists y. eauto using star. + destruct (A _ _ _ D B) as [v [E F]]. destruct (IH _ E) as [u [G H]]. - exists u. eauto using (@star_trans R). + exists u. + pose proof (@star_trans R). + eauto. - apply (A x y z); eauto using star. Qed. @@ -179,14 +182,16 @@ Section FixX. Proof. split; intros A. - intros x y z B C. apply A. - eauto using (@ecl_trans R), star_ecl, (@ecl_sym R). + pose proof (@ecl_trans R). + pose proof (@ecl_sym R). + eauto using star_ecl. - intros x y B. apply semi_confluent_confluent in A. induction B as [x|x x' y C B IH|x x' y C B IH]. + exists x. eauto using star. + destruct IH as [z [D E]]. exists z. eauto using star. + destruct IH as [u [D E]]. destruct (A _ _ _ C D) as [z [F G]]. - exists z. eauto using (@star_trans R). + exists z. pose proof (@star_trans R). eauto. Qed. diff --git a/theories/StringRewriting/Reductions/SBTM_HALT_to_SR.v b/theories/StringRewriting/Reductions/SBTM_HALT_to_SR.v index 184d78eb2..66e76f243 100644 --- a/theories/StringRewriting/Reductions/SBTM_HALT_to_SR.v +++ b/theories/StringRewriting/Reductions/SBTM_HALT_to_SR.v @@ -85,14 +85,21 @@ Section Construction. Lemma In_srsI u v : In (u, v) srs -> In_srs u v. Proof. move=> /in_flat_map [[q a]] [_] /=. + have ? := In_srs_l2 _ true. + have ? := In_srs_l2 _ false. + have ? := In_srs_r2 _ true. + have ? := In_srs_r2 _ false. + have ? := In_srs_dl _ true. + have ? := In_srs_dl _ false. + have ? := In_srs_dr _ true. + have ? := In_srs_dr _ false. case E: (trans' M (q, a)) => [[[q' a'] []]|] /=. - move=> [|[|[|[]]]] => - [<- <-]. - all: by auto using In_srs_l1, (In_srs_l2 _ true), (In_srs_l2 _ false). + all: by auto using In_srs_l1. - move=> [|[|[|[]]]] => - [<- <-]. - all: by auto using In_srs_r1, (In_srs_r2 _ true), (In_srs_r2 _ false). + all: by auto using In_srs_r1. - move=> [|[|[|[|[|[]]]]]] => - [<- <-]. - all: by auto using In_srs_f, (In_srs_dl _ true), (In_srs_dl _ false), - (In_srs_dr _ true), (In_srs_dr _ false). + all: by auto using In_srs_f. Qed. (* step simulation *) diff --git a/theories/_CoqProject b/theories/_CoqProject index 1b4def43e..2eae7a83c 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -1,6 +1,6 @@ -Q . Undecidability --arg -w -arg -notation-overridden,-stdlib-vector +-arg -w -arg -notation-overridden,-stdlib-vector,-notation-incompatible-prefix -arg "-set" -arg "'Default Proof Using = Type'" COQDOCFLAGS = "--charset utf-8 -s --with-header ../website/resources/header.html --with-footer ../website/resources/footer.html --index indexpage"