Commit bfa8495f by Pierre-Marie Pédrot

### Adapt w.r.t. coq/coq#12512.

parent 6401d876
 ... ... @@ -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. epose delete_empty; destruct b; simpl; auto. Qed. Lemma lookup_binder_delete_None {A} (m : M A) b s : binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None. ... ...
 ... ... @@ -125,8 +125,8 @@ 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)). pose (empty_finite (C:=D)); pose (union_finite (C:=D)); pose (singleton_finite (C:=D)); eauto. 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. epose (NoDup_fmap_1 fst); apply NoDup_Permutation; auto. 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. ... ... @@ -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 (epose lookup_empty; auto). 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; epose NoDup_map_to_list; apply NoDup_submseteq; auto. 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}))). pose (reflexive_eq (R:=(⊆@{M A}))); auto. 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}))). pose (reflexive_eq (R:=(⊆@{M A}))); auto. 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. epose proof (union_minimal (C:=C)); epose proof (singleton_minimal (C:=C)); eauto using minimal_weaken. - exists x'; split; [set_solver|]. eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). } epose proof (union_minimal (C:=C)); epose proof (singleton_minimal_not_above (C:=C)); eauto. } 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; pose proof (finite_inj_surj f); auto. - 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&?); pose proof cancel_inj; eauto. 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. pose proof @elem_of_enum; eauto. 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. pose proof @elem_of_enum; eauto. - 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). } pose proof comm_L Qp_plus; eauto 10. } 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?; pose proof (comm_L Qp_plus); auto. - by rewrite (assoc_L _), (comm_L Qp_plus e). - by rewrite (assoc_L _), (comm_L Qp_plus a'). Qed. ... ...
 ... ... @@ -182,7 +182,7 @@ 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. constructor; epose proof total_not; 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