Commit 2f5854bd authored by Robbert's avatar Robbert

Merge branch 'robbert/coq_12512' into 'master'

Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512

See merge request !166
parents 2ec23bde 6af69af1
Pipeline #29592 failed with stage
in 10 minutes and 37 seconds
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment