From 6af69af18de5fb6746c3f7ac7834c222d08570eb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Jun 2020 23:57:43 +0200
Subject: [PATCH] Avoid arbitrary terms in `auto using` to make std++ compliant
with Coq #12512.
---
theories/binders.v | 2 +-
theories/fin_map_dom.v | 6 +++---
theories/fin_maps.v | 12 ++++++------
theories/fin_sets.v | 4 ++--
theories/finite.v | 8 ++++----
theories/numbers.v | 4 ++--
theories/sorting.v | 3 ++-
7 files changed, 20 insertions(+), 19 deletions(-)
diff --git a/theories/binders.v b/theories/binders.v
index 995bbdf8..1448b0ac 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -81,7 +81,7 @@ Section binder_delete_insert.
Proof. destruct b; solve_proper. Qed.
Lemma binder_delete_empty {A} b : binder_delete b ∅ =@{M A} ∅.
- Proof. destruct b; simpl; auto using delete_empty. Qed.
+ Proof. destruct b; simpl; eauto using delete_empty. Qed.
Lemma lookup_binder_delete_None {A} (m : M A) b s :
binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index f061ada1..243b1644 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -124,9 +124,9 @@ Proof.
Qed.
Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
Proof.
- induction m using map_ind; rewrite ?dom_empty, ?dom_insert;
- eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
- (singleton_finite (C:=D)).
+ induction m using map_ind; rewrite ?dom_empty, ?dom_insert.
+ - by apply empty_finite.
+ - apply union_finite; [apply singleton_finite|done].
Qed.
Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡)) (dom D).
Proof.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index fd55a879..fc357d44 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -795,7 +795,7 @@ Lemma list_to_map_inj {A} (l1 l2 : list (K * A)) :
NoDup (l1.*1) → NoDup (l2.*1) →
(list_to_map l1 : M A) = list_to_map l2 → l1 ≡ₚ l2.
Proof.
- intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
+ intros ?? Hl1l2. apply NoDup_Permutation; [by eauto using NoDup_fmap_1..|].
intros [i x]. by rewrite !elem_of_list_to_map, Hl1l2.
Qed.
Lemma list_to_map_to_list {A} (m : M A) : list_to_map (map_to_list m) = m.
@@ -842,7 +842,7 @@ Lemma map_to_list_insert {A} (m : M A) i x :
Proof.
intros. apply list_to_map_inj; csimpl.
- apply NoDup_fst_map_to_list.
- - constructor; auto using NoDup_fst_map_to_list.
+ - constructor; [|by auto using NoDup_fst_map_to_list].
rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
rewrite elem_of_map_to_list in Hlookup. congruence.
- by rewrite !list_to_map_to_list.
@@ -851,13 +851,13 @@ Lemma map_to_list_singleton {A} i (x : A) :
map_to_list ({[i:=x]} : M A) = [(i,x)].
Proof.
apply Permutation_singleton. unfold singletonM, map_singleton.
- by rewrite map_to_list_insert, map_to_list_empty by auto using lookup_empty.
+ by rewrite map_to_list_insert, map_to_list_empty by eauto using lookup_empty.
Qed.
Lemma map_to_list_submseteq {A} (m1 m2 : M A) :
m1 ⊆ m2 → map_to_list m1 ⊆+ map_to_list m2.
Proof.
- intros; apply NoDup_submseteq; auto using NoDup_map_to_list.
+ intros; apply NoDup_submseteq; [by eauto using NoDup_map_to_list|].
intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
Qed.
Lemma map_to_list_fmap {A B} (f : A → B) (m : M A) :
@@ -1755,13 +1755,13 @@ Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) :
m1 ##ₘ m3 → m2 ##ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2.
Proof.
intros. apply (anti_symm (⊆)); apply map_union_reflecting_l with m3;
- auto using (reflexive_eq (R:=(⊆@{M A}))).
+ by try apply reflexive_eq.
Qed.
Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) :
m1 ##ₘ m3 → m2 ##ₘ m3 → m1 ∪ m3 = m2 ∪ m3 → m1 = m2.
Proof.
intros. apply (anti_symm (⊆)); apply map_union_reflecting_r with m3;
- auto using (reflexive_eq (R:=(⊆@{M A}))).
+ by try apply reflexive_eq.
Qed.
Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) :
m1 ∪ m2 ##ₘ m3 ↔ m1 ##ₘ m3 ∧ m2 ##ₘ m3.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index b91407f4..525e4aa8 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -260,9 +260,9 @@ Proof.
{ destruct IH as (x' & Hx' & Hmin); [set_solver|].
destruct (decide (R x x')).
- exists x; split; [set_solver|].
- eauto using (union_minimal (C:=C)), (singleton_minimal (C:=C)), minimal_weaken.
+ eapply union_minimal; [eapply singleton_minimal|by eapply minimal_weaken].
- exists x'; split; [set_solver|].
- eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). }
+ by eapply union_minimal; [apply singleton_minimal_not_above|]. }
exists x; split; [set_solver|].
rewrite HX, (right_id _ (∪)). apply singleton_minimal.
Qed.
diff --git a/theories/finite.v b/theories/finite.v
index d6ef2254..f5d516cc 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -154,10 +154,10 @@ Lemma finite_bijective A `{Finite A} B `{Finite B} :
Proof.
split.
- intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
- exists f; auto using (finite_inj_surj f).
+ exists f; eauto using finite_inj_surj.
- intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
+ by exists f.
- + destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
+ + destruct (surj_cancel f) as (g&?). exists g. apply cancel_inj.
Qed.
Lemma inj_card `{Finite A} `{Finite B} (f : A → B)
`{!Inj (=) (=) f} : card A ≤ card B.
@@ -274,7 +274,7 @@ Next Obligation.
Qed.
Next Obligation.
intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
- eauto using @elem_of_enum.
+ eauto using elem_of_enum.
Qed.
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
@@ -297,7 +297,7 @@ Next Obligation.
Qed.
Next Obligation.
intros ?????? [x y]. induction (elem_of_enum x); simpl.
- - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
+ - rewrite elem_of_app, !elem_of_list_fmap. eauto using elem_of_enum.
- rewrite elem_of_app; eauto.
Qed.
Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
diff --git a/theories/numbers.v b/theories/numbers.v
index ea913d89..fa5bf53a 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -792,10 +792,10 @@ Proof.
- auto.
- destruct (help c d a b); [done..|]. naive_solver.
- apply (inj (Qp_plus a)) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
- eauto 10 using (comm_L Qp_plus). }
+ exists a', q, q, d'. repeat split; done || by rewrite (comm_L Qp_plus). }
intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)).
destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
- eexists a', q, (q + e)%Qp, d'; split_and?; auto using (comm_L Qp_plus).
+ eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L Qp_plus)|..|done].
- by rewrite (assoc_L _), (comm_L Qp_plus e).
- by rewrite (assoc_L _), (comm_L Qp_plus a').
Qed.
diff --git a/theories/sorting.v b/theories/sorting.v
index 57936e1e..11fada6e 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -182,7 +182,8 @@ Section merge_sort_correct.
intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
repeat case_decide;
- constructor; eauto using HdRel_list_merge, HdRel_cons, total_not.
+ repeat match goal with H : ¬R _ _ |- _ => apply total_not in H end;
+ constructor; eauto using HdRel_list_merge, HdRel_cons.
Qed.
Lemma merge_Permutation l1 l2 : list_merge R l1 l2 ≡ₚ l1 ++ l2.
Proof.
--
GitLab