Commit 54a3198d authored by Hai Dang's avatar Hai Dang

bump iris

parent 404deb03
Pipeline #15034 passed with stage
in 16 minutes and 10 seconds
......@@ -10,5 +10,5 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [
"coq" { (>= "8.8.2" & < "8.10~") | (= "dev") }
"coq-iris" { (= "dev.2019-02-07.0.0655aa19") | (= "dev") }
"coq-iris" { (= "dev.2019-02-22.1.9c04e2b4") | (= "dev") }
]
......@@ -23,7 +23,7 @@ Proof. solve_inG. Qed.
(* Definition to_view (σ : language.state ra_lang) : Views := (Excl <$> threads σ). *)
Definition loc_sets (σ : language.state ra_lang) : gmap loc (gset message) :=
let locs := {[ mloc m | m <- msgs (mem σ) ]} in
map_imap (λ l _, Some {[ m <- msgs (mem σ) | mloc m = l ]}) (to_gmap () locs).
map_imap (λ l _, Some {[ m <- msgs (mem σ) | mloc m = l ]}) (gset_to_gmap () locs).
Definition to_hist (σ : language.state ra_lang) : Hists :=
let maxsets := (λ M, {[ m <- M | set_Forall (λ m', mtime m' mtime m) M ]} ) <$> loc_sets σ in
let hists := map_vt <$> maxsets in
......@@ -32,7 +32,7 @@ Definition to_hist (σ : language.state ra_lang) : Hists :=
(* TODO: can we avoid this? *)
(* Definition to_info (σ : language.state ra_lang) : Infos := *)
(* let locs := {[ mloc m | m <- msgs (mem σ) ]} in *)
(* let infos : gmap loc (frac.fracR * _) := to_gmap (1%Qp, to_agree 1%positive) locs in *)
(* let infos : gmap loc (frac.fracR * _) := gset_to_gmap (1%Qp, to_agree 1%positive) locs in *)
(* (infos). *)
Definition to_info (σ : language.state ra_lang) : Infos :=
(λ _, (1%Qp, to_agree 1%positive)) <$> to_hist σ.
......@@ -56,7 +56,7 @@ Proof.
rewrite /map_imap /dom /= /gset_dom /mapset_dom /= => x.
rewrite !elem_of_mapset_dom_with.
setoid_rewrite (_ : P, P true P); [|naive_solver|naive_solver].
setoid_rewrite <-(elem_of_map_of_list _ _ _ _); last first.
setoid_rewrite <-(elem_of_list_to_map _ _ _ _); last first.
{ apply NoDup_fmap_fst; last apply NoDup_omap; last apply NoDup_map_to_list.
- intros ? ? ?. rewrite !elem_of_list_omap.
assert (R : (a : K) (b : B) x, (pair (x.1) <$> curry (λ x y, Some (f x y)) x = Some (a, b)) (x.1 = a f (x.1) (x.2) = b)).
......@@ -77,9 +77,9 @@ Proof.
naive_solver.
Qed.
Lemma dom_to_gmap `{Countable K} {B} (g : gset K) (b:B) : dom (gset K) (to_gmap b g) g.
Lemma dom_gset_to_gmap `{Countable K} {B} (g : gset K) (b:B) : dom (gset K) (gset_to_gmap b g) g.
Proof.
rewrite /to_gmap dom_fmap => ?. rewrite elem_of_dom.
rewrite /gset_to_gmap dom_fmap => ?. rewrite elem_of_dom.
split.
- move => [[] ?]. by do !red.
- eauto.
......@@ -87,7 +87,7 @@ Qed.
Lemma loc_sets_dom σ : dom _ (loc_sets σ) {[ mloc m | m <- mem σ ]}.
rewrite /loc_sets.
by rewrite dom_map_imap dom_to_gmap.
by rewrite dom_map_imap dom_gset_to_gmap.
Qed.
(* Lemma elements_map_gset `{Countable T} `{Countable B} `{Equiv B} (f : T -> B) g : *)
......@@ -96,7 +96,7 @@ Qed.
(* rewrite /map_gset. elim: (elements g) => [|? L IHL] /=. *)
(* - rewrite elements_empty. constructor. *)
(* - rewrite elements_union. *)
(* by rewrite elem_of_elements elem_of_of_list. Qed. *)
(* by rewrite elem_of_elements elem_of_list_to_set. Qed. *)
(* Instance foldl_proper `{Equiv T} `{Equiv B} (f : B -> list T -> B) : `(Proper (() ==> (≡ₚ) ==> ()) f) -> Proper (() ==> (≡ₚ) ==> ()) (foldl f). *)
(* Proof. *)
......@@ -114,7 +114,7 @@ Lemma loc_sets_lookup σ l h :
(loc_sets σ) !! l = Some h l {[ mloc m | m <- mem σ ]} h = {[ m <- msgs (mem σ) | mloc m = l ]}.
Proof.
rewrite /loc_sets.
rewrite lookup_imap lookup_to_gmap /=.
rewrite lookup_imap lookup_gset_to_gmap /=.
case: (decide (l {[ mloc m | m <- mem σ ]})) => ?.
- rewrite option_guard_True // /=. naive_solver.
- rewrite option_guard_False // /=. naive_solver.
......
......@@ -1694,7 +1694,7 @@ Section proof.
Permutation (map_to_list (m1 m2)) (map_to_list m1 ++ map_to_list m2).
Proof.
intro Hdisj.
rewrite -(map_of_to_list m1) -foldr_insert_union.
rewrite -(list_to_map_to_list m1) -foldr_insert_union.
pose proof (NoDup_fst_map_to_list m1) as HNoDup.
remember (map_to_list m1) as l1.
assert (Permutation (map_to_list m1) l1) as Hl1 by (rewrite Heql1; done).
......@@ -1703,10 +1703,10 @@ Section proof.
pose proof (map_to_list_insert_inv _ _ _ _ Hl1); subst; simpl.
inversion HNoDup as [|??? HNoDup']; subst.
apply map_disjoint_insert_l in Hdisj as [].
pose proof (not_elem_of_map_of_list_1 _ _ H1).
pose proof (not_elem_of_list_to_map_1 _ _ H1).
rewrite !map_to_list_insert; auto.
constructor; apply (IHl1 HNoDup' (map_of_list l1)); try done.
{ rewrite map_to_of_list; done. }
constructor; apply (IHl1 HNoDup' (list_to_map l1)); try done.
{ rewrite map_to_list_to_map; done. }
{ rewrite foldr_insert_union lookup_union_None; auto. }
Qed.
......
......@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
From igps Require Export malloc repeat notation escrows.
From igps Require Import persistor viewpred proofmode weakestpre protocols singlewriter logically_atomic
invariants fork.
From igps.gps Require Import shared plain recursive.
From igps.gps Require Import shared plain.
From igps.examples Require Import abs_hashtable snapshot hist_protocol repeat for_loop list_lemmas.
Require Recdef.
......@@ -186,7 +186,7 @@ Section proof.
Set Default Proof Using "Type".
(* The collection of protocol assertions that describes a stable state of the node. *)
(* The set of protocol assertions that describes a stable state of the node. *)
Definition node_state_R L v n g :=
(map_size L 8 /\ exists vs, log_latest L v vs
[XP (ZplusPos version n) in v | versionP n g]_R @own _ _ histG g (Snapshot L)
......@@ -468,7 +468,6 @@ Section proof.
Proof.
iIntros "(#kI & out & #node_state)" (Φ) "shift"; iDestruct "shift" as (P) "[HP #Hshift]".
match goal with |-context[( P ={_,_}= ?R)%I] => set (Q := R) end.
unfold read.
unfold of_val.
wp_rec'. wp_rec'.
......@@ -848,7 +847,7 @@ Section proof.
Lemma writer_spec n L v g N (HN : base_mask ## N):
{{{ PSCtx node_state_W L v n g inv N ( L, own g (Master (1/2) L)) }}} writer #n
{{{ RET #();
let L' := map_of_list (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 3))) L in
let L' := list_to_map (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 3))) L in
node_state_W L' (v + 6) n g }}}.
Proof.
intros; iIntros "(#kI & node_state & #I) Hpost".
......@@ -893,7 +892,7 @@ Section proof.
iApply (wp_for_simple with "[] [node_state data]").
- apply I.
- instantiate (1 := (fun i => 0 <= i <= 3 ([ list] j seq 0 8, (ZplusPos (Z.of_nat j) l i))
let L' := map_of_list (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 (Z.to_nat i))))
let L' := list_to_map (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 (Z.to_nat i))))
L in node_state_W L' (v + (2 * Z.to_nat i)) n g)%I).
iIntros "!#" (i ?) "!# (% & % & data & node_state) Hpost".
match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
......@@ -944,11 +943,10 @@ Section proof.
iDestruct "H" as (?) "(% & ? & ?)"; subst.
rewrite big_sepL_replicate; iFrame.
rewrite Z2Nat.inj_add; try omega.
rewrite Nat.add_1_r seq_S List.map_app rev_app_distr; simpl.
rewrite Z2Nat.id; last omega.
rewrite Nat.add_1_r seq_S List.map_app rev_app_distr.
rewrite /= Z2Nat.id; last omega.
by rewrite -(Nat.add_1_r (Z.to_nat i)) !Nat.mul_add_distr_l -!plus_assoc insert_union_l.
- simpl; change (seq 0 (Z.to_nat 0)) with (@nil nat); simpl.
rewrite left_id Nat.add_0_r; iFrame; auto.
- rewrite /= left_id Nat.add_0_r; iFrame; auto.
- iNext; iIntros "H"; iDestruct "H" as (i) "(% & % & data & node_state)".
assert (i = 3) by omega; subst.
by iApply "Hpost".
......
......@@ -309,7 +309,7 @@ Section proof.
- rewrite lookup_insert_ne; last done.
rewrite Hin.
split; intros []; split; auto; try omega.
destruct (decide (n' = n + 1)%nat); last omega.
destruct (decide (n' = n + 1)%nat); last lia.
subst; rewrite Nat.even_add Heven in H; done.
Qed.
......@@ -320,11 +320,11 @@ Section proof.
intros; destruct (decide (n' = O)).
+ subst; rewrite lookup_insert; split; eauto.
+ rewrite lookup_insert_ne; last done.
rewrite lookup_empty; split; intros []; [done | omega].
rewrite lookup_empty; split; intros []; [done | lia].
- assert (n = (n - 2) + 2)%nat as Heq.
{ rewrite Nat.sub_add; first done.
destruct n; first done.
destruct n; [done | omega]. }
destruct n; [done | lia]. }
rewrite {1 3}Heq.
eapply log_latest_insert, IHg.
rewrite Heq Nat.even_add in H.
......@@ -366,7 +366,7 @@ Section proof.
destruct (decide (i < length l)); [rewrite app_nth1 | rewrite app_nth2]; try omega;
destruct (decide _); auto; try omega.
- subst; rewrite minus_diag; auto.
- rewrite !nth_overflow; auto; simpl; omega.
- rewrite !nth_overflow; auto; simpl; lia.
Qed.
Lemma map_nth_app {A} m1 n m2 i (d : A) (Hm1: map_size m1 n)
......@@ -393,7 +393,7 @@ Section proof.
Proof.
intros; induction vals using rev_ind; simpl; iIntros "H".
{ iExists (make_log v nil); iFrame; iPureIntro.
split; last by (split; [apply make_log_latest | intros; omega]).
split; last by (split; [apply make_log_latest | intros; lia]).
intros ???%make_log_lookup; subst; auto. }
rewrite big_sepL_app; simpl.
iDestruct "H" as "(H & Hi & _)".
......@@ -419,7 +419,7 @@ Section proof.
intros; erewrite map_nth_app; eauto.
rewrite Nat.add_0_r in H4.
destruct (decide _); first by subst.
apply H2; omega.
apply H2; lia.
- rewrite big_sepL_app; simpl.
erewrite Nat.add_0_r, map_nth_app; eauto.
rewrite decide_True; last done; iFrame.
......
......@@ -8,24 +8,24 @@ From igps Require Import arith infrastructure.
Definition Pos_upto_set (up: nat) : gset positive :=
match up with
| O =>
| S i => map_gset Pos.of_nat (seq_set 1 up)
| S i => map_gset Pos.of_nat (set_seq 1 up)
end.
Definition coPset_from_ex (i: nat): coPset
:= coPset.of_gset (Pos_upto_set i).
:= gset_to_coPset (Pos_upto_set i).
Lemma coPset_from_ex_gt i p:
p coPset_from_ex i (i < Pos.to_nat p)%nat.
Proof.
rewrite elem_of_difference coPset.elem_of_of_gset.
rewrite elem_of_difference elem_of_gset_to_coPset.
destruct i as [|i].
- split; move => _; [by apply Pos2Nat.is_pos|done].
- rewrite elem_of_map_gset. split.
+ move => [_ /= NIn].
apply: not_ge => ?. apply: NIn.
exists (Pos.to_nat p). set_unfold; rewrite elem_of_seq_set. lia'.
exists (Pos.to_nat p). set_unfold. lia'.
+ move => Lt. split; first done.
move => [n [Eqn /elem_of_seq_set [Ge1 Lt2]]].
move => [n [Eqn /elem_of_set_seq [Ge1 Lt2]]].
subst. lia'.
Qed.
......@@ -43,25 +43,25 @@ Qed.
Lemma coPset_of_gset_union X Y :
coPset.of_gset (X Y) = coPset.of_gset X coPset.of_gset Y.
gset_to_coPset (X Y) = gset_to_coPset X gset_to_coPset Y.
Proof.
apply leibniz_equiv.
move => ?. by rewrite elem_of_union !coPset.elem_of_of_gset elem_of_union.
move => ?. by rewrite elem_of_union !elem_of_gset_to_coPset elem_of_union.
Qed.
Lemma coPset_of_gset_difference X Y:
coPset.of_gset (X Y) = coPset.of_gset X coPset.of_gset Y.
gset_to_coPset (X Y) = gset_to_coPset X gset_to_coPset Y.
Proof.
apply leibniz_equiv. move => x.
by rewrite elem_of_difference !coPset.elem_of_of_gset elem_of_difference.
by rewrite elem_of_difference !elem_of_gset_to_coPset elem_of_difference.
Qed.
Lemma coPset_of_gset_difference_union (X Y Z: gset positive)
(Disj: Y ## Z) (Sub: Y X):
coPset.of_gset (X Z) = coPset.of_gset (X (Y Z)) coPset.of_gset Y.
gset_to_coPset (X Z) = gset_to_coPset (X (Y Z)) gset_to_coPset Y.
Proof.
apply leibniz_equiv. move => x.
rewrite elem_of_union !coPset.elem_of_of_gset
rewrite elem_of_union !elem_of_gset_to_coPset
!elem_of_difference elem_of_union.
split.
- move => [InX NIn]. case (decide (x Y)) => [?|NInY].
......@@ -71,33 +71,33 @@ Proof.
Qed.
Lemma coPset_of_gset_difference_disjoint (X Y Z: gset positive):
coPset.of_gset (X (Y Z)) ## coPset.of_gset Y.
gset_to_coPset (X (Y Z)) ## gset_to_coPset Y.
Proof.
rewrite elem_of_disjoint.
move => x. rewrite !coPset.elem_of_of_gset elem_of_difference elem_of_union.
move => x. rewrite !elem_of_gset_to_coPset elem_of_difference elem_of_union.
set_solver.
Qed.
Lemma coPset_of_gset_top_difference (X Y: gset positive) (Disj: X ## Y):
coPset.of_gset X = ( coPset.of_gset (Y X)) coPset.of_gset Y.
gset_to_coPset X = ( gset_to_coPset (Y X)) gset_to_coPset Y.
Proof.
apply leibniz_equiv. move => x.
rewrite elem_of_union !elem_of_difference
!coPset.elem_of_of_gset elem_of_union.
!elem_of_gset_to_coPset elem_of_union.
split.
- move => [_ NIn]. case (decide (x Y)) => [|?]; [by right|left]. set_solver.
- set_solver.
Qed.
Lemma coPset_of_gset_top_disjoint (X Y: gset positive):
( coPset.of_gset (Y X)) ## coPset.of_gset Y.
( gset_to_coPset (Y X)) ## gset_to_coPset Y.
Proof.
rewrite elem_of_disjoint.
move => x. rewrite elem_of_difference coPset_of_gset_union. set_solver.
Qed.
Lemma coPset_of_gset_empty :
coPset.of_gset = .
gset_to_coPset = .
Proof. by apply leibniz_equiv. Qed.
Lemma coPset_difference_top_empty:
......
This diff is collapsed.
......@@ -212,14 +212,14 @@ Section TicketLock.
Qed.
Lemma Waiting_dom_size (M: gmapNOpN)
(DS : dom (gset nat) M seq_set 0 (Pos.to_nat C)):
(DS : dom (gset nat) M set_seq 0 (Pos.to_nat C)):
Z.pos C = size (dom (gset nat) M).
Proof.
by rewrite (collection_size_proper _ _ DS) -positive_nat_Z seq_set_size.
by rewrite (set_size_proper _ _ DS) -positive_nat_Z set_seq_size.
Qed.
Lemma Waiting_size_le (M: gmapNOpN) (n: nat)
(DS: dom (gset nat) M seq_set 0 (Pos.to_nat C)):
(DS: dom (gset nat) M set_seq 0 (Pos.to_nat C)):
Ws M n Z.pos C.
Proof.
rewrite (_: Z.pos C = size (dom (gset nat) M)).
......@@ -228,7 +228,7 @@ Section TicketLock.
Qed.
Lemma Waiting_size_lt (M: gmapNOpN) (n i: nat) (ot: option nat)
(DS: dom (gset nat) M seq_set 0 (Pos.to_nat C))
(DS: dom (gset nat) M set_seq 0 (Pos.to_nat C))
(Ini: M !! i = Excl' ot) (Lt: ot = None t, ot = Some t t < n):
Ws M n < Z.pos C.
Proof.
......@@ -266,7 +266,7 @@ Section TicketLock.
Lemma ns_tkt_bound_update (M: gmapNOpN) (t n i: nat) (ot : option nat)
(Ini: M !! i = Excl' ot) (BO: ns_tkt_bound M t n)
(DS: dom (gset nat) M seq_set 0 (Pos.to_nat C)):
(DS: dom (gset nat) M set_seq 0 (Pos.to_nat C)):
(n': nat),
(ot = None n' = n)
( t0, ot = Some t0 n' = S t0 n' = n) t < n' + Z.pos C
......@@ -286,7 +286,7 @@ Section TicketLock.
apply Zplus_le_compat_r. etrans; first apply LE2.
assert (Eqs :=
subseteq_union_1 _ _ (Waiting_subseteq_update _ _ t _ _ Ini Le)).
rewrite /Ws -(collection_size_proper _ _ Eqs) size_union_alt.
rewrite /Ws -(set_size_proper _ _ Eqs) size_union_alt.
rewrite Nat2Z.inj_add (Z.add_comm (size _)) Zplus_assoc.
apply Zplus_le_compat_r. etrans.
{ instantiate (1:= n + size (Mtkt_range M n t0)).
......@@ -410,21 +410,21 @@ Section TicketLock.
apply: singleton_local_update; [eauto| exact: exclusive_local_update].
Qed.
Definition map_excl (S: gset nat) (t : option nat) := to_gmap (Excl t) S.
Definition setC: gset nat := seq_set 0 (Pos.to_nat C).
Definition map_excl (S: gset nat) (t : option nat) := gset_to_gmap (Excl t) S.
Definition setC: gset nat := set_seq 0 (Pos.to_nat C).
Definition firstMap := map_excl setC None.
Lemma Tkt_set_alloc γ j n t:
own γ (ε, map_excl (seq_set j n) t)
([ set] i seq_set j n, MyTkt γ i t)%I.
own γ (ε, map_excl (set_seq j n) t)
([ set] i set_seq j n, MyTkt γ i t)%I.
Proof.
revert j. induction n => j /=; iIntros "MyTkts".
- by rewrite big_sepS_empty.
- rewrite big_sepS_insert; last first.
{ move => /elem_of_seq_set [Le _]. omega. }
rewrite /map_excl to_gmap_union_singleton insert_singleton_op;
{ move => /elem_of_set_seq [Le _]. omega. }
rewrite /map_excl gset_to_gmap_union_singleton insert_singleton_op;
last first.
{ apply lookup_to_gmap_None. move => /elem_of_seq_set [Le _]. omega. }
{ apply lookup_gset_to_gmap_None. move => /elem_of_set_seq [Le _]. omega. }
iDestruct "MyTkts" as "[$ MyTkts]".
by iApply IHn.
Qed.
......@@ -438,7 +438,7 @@ Section TicketLock.
as (γ) "Own".
{ split; first done. apply auth_valid_discrete_2. split; first done.
move => i. destruct (firstMap !! i) eqn:Eq; last by rewrite Eq.
rewrite Eq. by move :Eq => /lookup_to_gmap_Some [_ <-]. }
rewrite Eq. by move :Eq => /lookup_gset_to_gmap_Some [_ <-]. }
iExists γ. rewrite pair_split.
iDestruct "Own" as "[$ [$ MyTkts]]". iModIntro.
rewrite /firstMap /setC. by iApply Tkt_set_alloc.
......@@ -488,7 +488,7 @@ Section TicketLock.
if b
then ( (t n: nat) (M: gmapNOpN),
AllTkts γ M Perms γ t
dom (gset nat) M seq_set 0 (Pos.to_nat C)
dom (gset nat) M set_seq 0 (Pos.to_nat C)
y = t `mod` Z.pos C ns_tkt_bound M t n
[XP (ZplusPos ns x) in n | NSP P γ ]_R)
else True.
......@@ -571,11 +571,12 @@ Section TicketLock.
iPureIntro. split; last split.
+ rewrite /firstMap /map_excl. apply set_unfold_2. move => i.
rewrite elem_of_dom. split.
* move => [e /lookup_to_gmap_Some [//]].
* move => In. exists (Excl None). by apply lookup_to_gmap_Some.
* move => [e /lookup_gset_to_gmap_Some [/elem_of_set_seq //]].
* move => In. exists (Excl None).
by rewrite lookup_gset_to_gmap_Some elem_of_set_seq.
+ by rewrite Zmod_0_l.
+ split; [done|split]; first omega.
move => ? ? /lookup_to_gmap_Some [_ //].
move => ? ? /lookup_gset_to_gmap_Some [_ //].
}
iNext. iIntros "#TCP". wp_seq.
......
......@@ -135,10 +135,10 @@ Section Setup.
st_time l S1 st_time l S2 st_prst S1 st_prst S2.
Definition Consistent ζ h : Prop :=
@equiv _ collection_equiv {[ (VInj (st_val e), st_view e) | e <- ζ]} h.
@equiv _ set_equiv {[ (VInj (st_val e), st_view e) | e <- ζ]} h.
Instance Consistent_proper:
Proper (collection_equiv ==> collection_equiv ==> (flip impl) ) Consistent.
Proper (set_equiv ==> set_equiv ==> (flip impl) ) Consistent.
Proof.
unfold Consistent.
move => X Y HXY h1 h2 Hh12 ?.
......
......@@ -123,10 +123,10 @@ Section Setup.
st_time l S1 st_time l S2 st_prst S1 st_prst S2.
Definition Consistent ζ h : Prop :=
@equiv _ collection_equiv {[ (st_val e, st_view e) | e <- ζ]} h.
@equiv _ set_equiv {[ (st_val e, st_view e) | e <- ζ]} h.
Instance Consistent_proper:
Proper (collection_equiv ==> collection_equiv ==> (flip impl) ) Consistent.
Proper (set_equiv ==> set_equiv ==> (flip impl) ) Consistent.
Proof.
unfold Consistent.
move => X Y HXY h1 h2 Hh12 ?.
......
From Coq.ssr Require Import ssreflect.
From stdpp Require Export strings list numbers sorting gmap finite set mapset.
From stdpp Require Export strings list numbers sorting gmap finite propset mapset.
Global Generalizable All Variables.
Global Set Asymmetric Patterns.
......
From Coq.ssr Require Export ssreflect.
From stdpp Require Export list numbers set gmap finite mapset fin_collections.
Global Generalizable All Variables.
Global Set Asymmetric Patterns.
From stdpp Require Export list numbers propset gmap finite mapset fin_sets.
Global Set Bullet Behavior "Strict Subproofs".
From Coq Require Export Utf8.
Require Import Setoid.
Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
Lemma seq_set_size (s n: nat): size (seq_set s n : gset nat) = n.
Lemma set_seq_size (s n: nat): size (set_seq s n : gset nat) = n.
Proof.
induction n; [done|].
rewrite seq_set_S_union_L /=.
rewrite set_seq_S_end_union_L /=.
rewrite size_union.
+ rewrite IHn size_singleton. lia.
+ apply disjoint_singleton_l.
move => /elem_of_seq_set [_ ?]. omega.
move => /elem_of_set_seq [_ ?]. omega.
Qed.
Lemma seq_S i n : seq i (S n) = (seq i n ++ (i + n)%nat::nil)%list.
......@@ -85,17 +83,17 @@ Section suffixes.
symmetry in H1. apply app_nil in H1 as [_ ?]. by subst y1.
Qed.
Lemma of_list_nil_eq
Lemma list_to_set_nil_eq
{C : Type} `{Empty C} `{ElemOf A C} `{Singleton A C} `{Union C}
`{SimpleCollection A C} (l: list A):
of_list l ( : C) l = nil.
`{SemiSet A C} (l: list A):
list_to_set l ( : C) l = nil.
Proof.
split.
- move => Eq. destruct l; first done.
rewrite of_list_cons in Eq. exfalso.
rewrite list_to_set_cons in Eq. exfalso.
apply empty_union in Eq as [Eq _].
eapply not_elem_of_empty. rewrite -Eq elem_of_singleton. done.
- move => ->. by rewrite of_list_nil.
- move => ->. by rewrite list_to_set_nil.
Qed.
Lemma hd_error_some_elem a l :
......@@ -144,7 +142,7 @@ Section suffixes.
End suffixes.
Section Max.
Context {A C : Type} `{Collection A C}.
Context {A C : Type} `{Set_ A C}.
Inductive Max (R : relation A) (c : C) : Type :=
| max_none (HEmp : c )
......@@ -242,7 +240,7 @@ Proof. set_solver. Qed.
(* Extra lemmas for set difference *)
Lemma difference_mono `{Collection A C}:
Lemma difference_mono `{Set_ A C}:
Proper (() ==> () ==> ()) (@difference C _).
Proof.
intros X1 X2 HX Y1 Y2 HY. rewrite HY.
......@@ -260,7 +258,7 @@ Lemma gset_difference_mono `{Countable A} (X Y Z: gset A):
X Y X Z Y Z.
Proof. intro Sub. by apply (difference_mono). Qed.
Lemma difference_twice_union `{Collection A C} (X Y Z: C):
Lemma difference_twice_union `{Set_ A C} (X Y Z: C):
(X Y Z X (Y Z))%stdpp.
Proof.
apply elem_of_equiv. move => ?.
......@@ -330,12 +328,12 @@ Section Map_GSet.
{CB : @Countable B EqDecB}.
Set Default Proof Using "Type* EqDecA EqDecB CA CB".
Definition map_gset f (M : gset A) : gset B
:= of_list (f <$> (elements M)).
:= list_to_set (f <$> (elements M)).
Typeclasses Opaque map_gset.
Lemma elem_of_map_gset f M b : b map_gset f M a, b = f a a M.
Proof.
rewrite elem_of_of_list elem_of_list_fmap.
rewrite elem_of_list_to_set elem_of_list_fmap.
by setoid_rewrite elem_of_elements.
Qed.
Global Instance set_unfold_map_gset f M b Q :
......@@ -812,7 +810,7 @@ Lemma gset_neg_Forall `{Countable A} (P : A -> Prop)
: ¬ set_Forall P s set_Exists (λ x, ¬ P x) s.
Proof.
split.
- case: (collection_choose_or_empty (filter (λ x, ¬ P x) s)) => [[x]|].
- case: (set_choose_or_empty (filter (λ x, ¬ P x) s)) => [[x]|].
+ set_unfold => [[? ?]] _. by exists x.
+ set_unfold => H2 H3. exfalso. apply: H3 => x Inx.
specialize (H2 x).
......@@ -976,8 +974,8 @@ Proof.
move => m'. case (decide (m = m')) => [-> //|]. abstract set_solver+SR.
Qed.
Instance gset_SimpleCollection `{Countable K} : SimpleCollection K (gset K) := _.
Instance gset_Collection `{Countable K} : Collection K (gset K) := _.
Instance gset_SemiSet `{Countable K} : SemiSet K (gset K) := _.
Instance gset_Set_ `{Countable K} : Set_ K (gset K) := _.
Program Definition Pos2Qp (n: positive) : Qp := mk_Qp (Zpos n) _.
......
......@@ -65,7 +65,7 @@ Lemma rISet2_subseteq s:
rISet2 s rISet s.
Proof. by destruct s. Qed.
Definition tok s: set token
Definition tok s: propset token
:= {[ t | i, t = Change i i rISet2 s ]}.
Global Arguments tok !_ /.
......@@ -73,7 +73,7 @@ Global Arguments tok !_ /.
Canonical Structure rsl_sts := sts.Sts prim_step tok.
Definition i_states i : set state := {[ s | i rISet2 s ]}.
Definition i_states i : propset state := {[ s | i rISet2 s ]}.
Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
......
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