Commit 664a8754 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'list_renaming_stuff'

parents 05b53000 ddf8ef49
Pipeline #3622 passed with stage
in 10 minutes and 41 seconds
...@@ -101,9 +101,9 @@ Proof. ...@@ -101,9 +101,9 @@ Proof.
- by trans (big_op xs2). - by trans (big_op xs2).
Qed. Qed.
Lemma big_op_contains xs ys : xs `contains` ys [] xs [] ys. Lemma big_op_submseteq xs ys : xs + ys [] xs [] ys.
Proof. Proof.
intros [xs' ->]%contains_Permutation. intros [xs' ->]%submseteq_Permutation.
rewrite big_op_app; apply cmra_included_l. rewrite big_op_app; apply cmra_included_l.
Qed. Qed.
...@@ -158,9 +158,9 @@ Section list. ...@@ -158,9 +158,9 @@ Section list.
Lemma big_opL_permutation (f : A M) l1 l2 : Lemma big_opL_permutation (f : A M) l1 l2 :
l1 ≡ₚ l2 ([ list] x l1, f x) ([ list] x l2, f x). l1 ≡ₚ l2 ([ list] x l1, f x) ([ list] x l2, f x).
Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed. Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed.
Lemma big_opL_contains (f : A M) l1 l2 : Lemma big_opL_submseteq (f : A M) l1 l2 :
l1 `contains` l2 ([ list] x l1, f x) ([ list] x l2, f x). l1 + l2 ([ list] x l1, f x) ([ list] x l2, f x).
Proof. intros Hl. apply big_op_contains. rewrite !imap_const. by rewrite ->Hl. Qed. Proof. intros Hl. apply big_op_submseteq. rewrite !imap_const. by rewrite ->Hl. Qed.
Global Instance big_opL_ne l n : Global Instance big_opL_ne l n :
Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
...@@ -230,7 +230,7 @@ Section gmap. ...@@ -230,7 +230,7 @@ Section gmap.
([ map] k x m1, f k x) [ map] k x m2, g k x. ([ map] k x m1, f k x) [ map] k x m2, g k x.
Proof. Proof.
intros Hm Hf. trans ([ map] kx m2, f k x). intros Hm Hf. trans ([ map] kx m2, f k x).
- by apply big_op_contains, fmap_contains, map_to_list_contains. - by apply big_op_submseteq, fmap_submseteq, map_to_list_submseteq.
- apply big_opM_forall; apply _ || auto. - apply big_opM_forall; apply _ || auto.
Qed. Qed.
Lemma big_opM_ext f g m : Lemma big_opM_ext f g m :
...@@ -345,7 +345,7 @@ Section gset. ...@@ -345,7 +345,7 @@ Section gset.
([ set] x X, f x) [ set] x Y, g x. ([ set] x X, f x) [ set] x Y, g x.
Proof. Proof.
intros HX Hf. trans ([ set] x Y, f x). intros HX Hf. trans ([ set] x Y, f x).
- by apply big_op_contains, fmap_contains, elements_contains. - by apply big_op_submseteq, fmap_submseteq, elements_submseteq.
- apply big_opS_forall; apply _ || auto. - apply big_opS_forall; apply _ || auto.
Qed. Qed.
Lemma big_opS_ext f g X : Lemma big_opS_ext f g X :
...@@ -446,7 +446,7 @@ Section gmultiset. ...@@ -446,7 +446,7 @@ Section gmultiset.
([ mset] x X, f x) [ mset] x Y, g x. ([ mset] x X, f x) [ mset] x Y, g x.
Proof. Proof.
intros HX Hf. trans ([ mset] x Y, f x). intros HX Hf. trans ([ mset] x Y, f x).
- by apply big_op_contains, fmap_contains, gmultiset_elements_contains. - by apply big_op_submseteq, fmap_submseteq, gmultiset_elements_submseteq.
- apply big_opMS_forall; apply _ || auto. - apply big_opMS_forall; apply _ || auto.
Qed. Qed.
Lemma big_opMS_ext f g X : Lemma big_opMS_ext f g X :
......
...@@ -29,9 +29,9 @@ Module ra_reflection. Section ra_reflection. ...@@ -29,9 +29,9 @@ Module ra_reflection. Section ra_reflection.
by rewrite fmap_app IH1 IH2 big_op_app. by rewrite fmap_app IH1 IH2 big_op_app.
Qed. Qed.
Lemma flatten_correct Σ e1 e2 : Lemma flatten_correct Σ e1 e2 :
flatten e1 `contains` flatten e2 eval Σ e1 eval Σ e2. flatten e1 + flatten e2 eval Σ e1 eval Σ e2.
Proof. Proof.
by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He. by intros He; rewrite !eval_flatten; apply big_op_submseteq; rewrite ->He.
Qed. Qed.
Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}. Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
......
...@@ -133,8 +133,8 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. ...@@ -133,8 +133,8 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs) ⊣⊢ [] Ps [] Qs. Lemma big_sep_app Ps Qs : [] (Ps ++ Qs) ⊣⊢ [] Ps [] Qs.
Proof. by rewrite big_op_app. Qed. Proof. by rewrite big_op_app. Qed.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps [] Ps [] Qs. Lemma big_sep_submseteq Ps Qs : Qs + Ps [] Ps [] Qs.
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed. Proof. intros. apply uPred_included. by apply: big_op_submseteq. Qed.
Lemma big_sep_elem_of Ps P : P Ps [] Ps P. Lemma big_sep_elem_of Ps P : P Ps [] Ps P.
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed. Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
Lemma big_sep_elem_of_acc Ps P : P Ps [] Ps P (P - [] Ps). Lemma big_sep_elem_of_acc Ps P : P Ps [] Ps P (P - [] Ps).
...@@ -220,9 +220,9 @@ Section list. ...@@ -220,9 +220,9 @@ Section list.
( k y, l !! k = Some y Φ k y ⊣⊢ Ψ k y) ( k y, l !! k = Some y Φ k y ⊣⊢ Ψ k y)
([ list] k y l, Φ k y) ⊣⊢ ([ list] k y l, Ψ k y). ([ list] k y l, Φ k y) ⊣⊢ ([ list] k y l, Ψ k y).
Proof. apply big_opL_proper. Qed. Proof. apply big_opL_proper. Qed.
Lemma big_sepL_contains (Φ : A uPred M) l1 l2 : Lemma big_sepL_submseteq (Φ : A uPred M) l1 l2 :
l1 `contains` l2 ([ list] y l2, Φ y) [ list] y l1, Φ y. l1 + l2 ([ list] y l2, Φ y) [ list] y l1, Φ y.
Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed. Proof. intros ?. apply uPred_included. by apply: big_opL_submseteq. Qed.
Global Instance big_sepL_mono' l : Global Instance big_sepL_mono' l :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ()) Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
...@@ -353,8 +353,8 @@ Section gmap. ...@@ -353,8 +353,8 @@ Section gmap.
([ map] k x m1, Φ k x) [ map] k x m2, Ψ k x. ([ map] k x m1, Φ k x) [ map] k x m2, Ψ k x.
Proof. Proof.
intros Hm HΦ. trans ([ map] kx m2, Φ k x)%I. intros Hm HΦ. trans ([ map] kx m2, Φ k x)%I.
- apply uPred_included. apply: big_op_contains. - apply uPred_included. apply: big_op_submseteq.
by apply fmap_contains, map_to_list_contains. by apply fmap_submseteq, map_to_list_submseteq.
- apply big_opM_forall; apply _ || auto. - apply big_opM_forall; apply _ || auto.
Qed. Qed.
Lemma big_sepM_proper Φ Ψ m : Lemma big_sepM_proper Φ Ψ m :
...@@ -517,8 +517,8 @@ Section gset. ...@@ -517,8 +517,8 @@ Section gset.
([ set] x X, Φ x) [ set] x Y, Ψ x. ([ set] x X, Φ x) [ set] x Y, Ψ x.
Proof. Proof.
intros HX HΦ. trans ([ set] x Y, Φ x)%I. intros HX HΦ. trans ([ set] x Y, Φ x)%I.
- apply uPred_included. apply: big_op_contains. - apply uPred_included. apply: big_op_submseteq.
by apply fmap_contains, elements_contains. by apply fmap_submseteq, elements_submseteq.
- apply big_opS_forall; apply _ || auto. - apply big_opS_forall; apply _ || auto.
Qed. Qed.
Lemma big_sepS_proper Φ Ψ X : Lemma big_sepS_proper Φ Ψ X :
...@@ -666,8 +666,8 @@ Section gmultiset. ...@@ -666,8 +666,8 @@ Section gmultiset.
([ mset] x X, Φ x) [ mset] x Y, Ψ x. ([ mset] x X, Φ x) [ mset] x Y, Ψ x.
Proof. Proof.
intros HX HΦ. trans ([ mset] x Y, Φ x)%I. intros HX HΦ. trans ([ mset] x Y, Φ x)%I.
- apply uPred_included. apply: big_op_contains. - apply uPred_included. apply: big_op_submseteq.
by apply fmap_contains, gmultiset_elements_contains. by apply fmap_submseteq, gmultiset_elements_submseteq.
- apply big_opMS_forall; apply _ || auto. - apply big_opMS_forall; apply _ || auto.
Qed. Qed.
Lemma big_sepMS_proper Φ Ψ X : Lemma big_sepMS_proper Φ Ψ X :
......
...@@ -30,9 +30,9 @@ Module uPred_reflection. Section uPred_reflection. ...@@ -30,9 +30,9 @@ Module uPred_reflection. Section uPred_reflection.
rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //. rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //.
Qed. Qed.
Lemma flatten_entails Σ e1 e2 : Lemma flatten_entails Σ e1 e2 :
flatten e2 `contains` flatten e1 eval Σ e1 eval Σ e2. flatten e2 + flatten e1 eval Σ e1 eval Σ e2.
Proof. Proof.
intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains. intros. rewrite !eval_flatten. by apply big_sep_submseteq, fmap_submseteq.
Qed. Qed.
Lemma flatten_equiv Σ e1 e2 : Lemma flatten_equiv Σ e1 e2 :
flatten e2 ≡ₚ flatten e1 eval Σ e1 ⊣⊢ eval Σ e2. flatten e2 ≡ₚ flatten e1 eval Σ e1 ⊣⊢ eval Σ e2.
......
...@@ -69,9 +69,9 @@ Proof. ...@@ -69,9 +69,9 @@ Proof.
apply Permutation_singleton. by rewrite <-(right_id () {[x]}), apply Permutation_singleton. by rewrite <-(right_id () {[x]}),
elements_union_singleton, elements_empty by set_solver. elements_union_singleton, elements_empty by set_solver.
Qed. Qed.
Lemma elements_contains X Y : X Y elements X `contains` elements Y. Lemma elements_submseteq X Y : X Y elements X + elements Y.
Proof. Proof.
intros; apply NoDup_contains; auto using NoDup_elements. intros; apply NoDup_submseteq; auto using NoDup_elements.
intros x. rewrite !elem_of_elements; auto. intros x. rewrite !elem_of_elements; auto.
Qed. Qed.
......
...@@ -699,10 +699,10 @@ Proof. ...@@ -699,10 +699,10 @@ Proof.
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 auto using lookup_empty.
Qed. Qed.
Lemma map_to_list_contains {A} (m1 m2 : M A) : Lemma map_to_list_submseteq {A} (m1 m2 : M A) :
m1 m2 map_to_list m1 `contains` map_to_list m2. m1 m2 map_to_list m1 + map_to_list m2.
Proof. Proof.
intros; apply NoDup_contains; auto using NoDup_map_to_list. intros; apply NoDup_submseteq; auto using NoDup_map_to_list.
intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken. intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
Qed. Qed.
Lemma map_to_list_fmap {A B} (f : A B) m : Lemma map_to_list_fmap {A B} (f : A B) m :
......
...@@ -107,17 +107,17 @@ Proof. ...@@ -107,17 +107,17 @@ Proof.
unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|]. unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
constructor; exact x. constructor; exact x.
Qed. Qed.
Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A B) Lemma finite_inj_submseteq `{finA: Finite A} `{finB: Finite B} (f: A B)
`{!Inj (=) (=) f} : f <$> enum A `contains` enum B. `{!Inj (=) (=) f} : f <$> enum A + enum B.
Proof. Proof.
intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2. intros. destruct finA, finB. apply NoDup_submseteq; auto using NoDup_fmap_2.
Qed. Qed.
Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A B) Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A B)
`{!Inj (=) (=) f} : card A = card B f <$> enum A ≡ₚ enum B. `{!Inj (=) (=) f} : card A = card B f <$> enum A ≡ₚ enum B.
Proof. Proof.
intros. apply contains_Permutation_length_eq. intros. apply submseteq_Permutation_length_eq.
- by rewrite fmap_length. - by rewrite fmap_length.
- by apply finite_inj_contains. - by apply finite_inj_submseteq.
Qed. Qed.
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A B) Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A B)
`{!Inj (=) (=) f} : card A = card B Surj (=) f. `{!Inj (=) (=) f} : card A = card B Surj (=) f.
...@@ -144,7 +144,7 @@ Proof. ...@@ -144,7 +144,7 @@ Proof.
destruct (finite_surj A B) as (g&?); auto with lia. destruct (finite_surj A B) as (g&?); auto with lia.
destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj. destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
- intros [f ?]. unfold card. rewrite <-(fmap_length f). - intros [f ?]. unfold card. rewrite <-(fmap_length f).
by apply contains_length, (finite_inj_contains f). by apply submseteq_length, (finite_inj_submseteq f).
Qed. Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} : Lemma finite_bijective A `{Finite A} B `{Finite B} :
card A = card B f : A B, Inj (=) (=) f Surj (=) f. card A = card B f : A B, Inj (=) (=) f Surj (=) f.
......
...@@ -345,14 +345,14 @@ Proof. ...@@ -345,14 +345,14 @@ Proof.
Qed. Qed.
(* Mononicity *) (* Mononicity *)
Lemma gmultiset_elements_contains X Y : X Y elements X `contains` elements Y. Lemma gmultiset_elements_submseteq X Y : X Y elements X + elements Y.
Proof. Proof.
intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union. intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union.
by apply contains_inserts_r. by apply submseteq_inserts_r.
Qed. Qed.
Lemma gmultiset_subseteq_size X Y : X Y size X size Y. Lemma gmultiset_subseteq_size X Y : X Y size X size Y.
Proof. intros. by apply contains_length, gmultiset_elements_contains. Qed. Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Lemma gmultiset_subset_size X Y : X Y size X < size Y. Lemma gmultiset_subset_size X Y : X Y size X < size Y.
Proof. Proof.
......
This diff is collapsed.
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