Commit 825e7e74 authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Switched back to having ucmra with discrete unit; more WIP updating.

parent df6f2669
-Q . iris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
prelude/list.v
algebra/irelations.v
algebra/relations.v
algebra/step.v
......
......@@ -194,6 +194,7 @@ Proof.
split; simpl.
- apply (@ucmra_unit_valid A).
- by intros x; constructor; rewrite /= left_id.
- apply discrete. apply _.
- do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure authUR :=
......
......@@ -186,9 +186,7 @@ Arguments core' _ _ _ /.
Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
mixin_ucmra_unit_valid : ;
mixin_ucmra_unit_left_id : LeftId () ();
(*
mixin_ucmra_unit_timeless : Discrete ;
*)
mixin_ucmra_unit_timeless : y : A, {0} y y;
mixin_ucmra_pcore_unit : pcore Some
}.
......@@ -238,7 +236,9 @@ Section ucmra_mixin.
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_left_id : LeftId () (@op A _).
Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
Lemma ucmra_pcore_unit : pcore (:A) Some .
Global Instance ucmra_unit_timeless : Discrete ( : A).
Proof. intros y. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
Lemma ucmra_pcore_unit : pcore (:A) Some .
Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
End ucmra_mixin.
......@@ -1084,6 +1084,7 @@ Section prod_unit.
split.
- split; apply ucmra_unit_valid.
- by split; rewrite /=left_id.
- by intros ? [??]; split; apply (discrete _).
- rewrite prod_pcore_Some'; split; apply (persistent _).
Qed.
Canonical Structure prodUR := UcmraT (prod A B) prod_ucmra_mixin.
......@@ -1250,7 +1251,7 @@ Section option.
Instance option_empty : Empty (option A) := None.
Lemma option_ucmra_mixin : UCMRAMixin optionR.
Proof. split. done. by intros []. done. Qed.
Proof. split. done. by intros []. by inversion_clear 1. done. Qed.
Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
(** Misc *)
......
......@@ -162,6 +162,7 @@ Proof.
split.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- apply gmap_empty_timeless.
- constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
Canonical Structure gmapUR :=
......
......@@ -130,34 +130,12 @@ Section iprod_cmra.
split.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite iprod_lookup_op left_id.
- intros f Hf x. rewrite //=. specialize (Hf x). rewrite //= in Hf. by apply: discrete.
- constructor=> x. apply persistent_core, _.
Qed.
Canonical Structure iprodUR :=
UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
(*
Global Instance iprod_empty_discrete : Discrete ( : iprod B).
Proof.
intros f Hf x. apply: timeless.
intros ? Heq i. specialize (Heq i).
rewrite iprod_lookup_empty in Heq |- *.
rewrite //= in Heq.
rewrite /equiv. destruct (B i). rewrite /ofe_equiv//=.
inversion Heq.
specialize (Heq).
destruct (y i).
rewrite /equiv.
intros k.
inversion Hm.
inversion_clear Heq.
specialize (h
apply _.
*)
(** Internalized properties *)
Lemma iprod_equivI {M} g1 g2 : g1 g2 ⊣⊢ ( i, g1 i g2 i : uPred M).
......@@ -213,24 +191,8 @@ Section iprod_singleton.
x x' (iprod_singleton x y) x' = .
Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
(*
Global Instance iprod_singleton_timeless x (y : B x) :
Discrete y Discrete (iprod_singleton x y).
Proof.
rewrite /iprod_singleton. intros. apply iprod_insert_timeless; auto.
intros ??? => //=.
intros i.
specialize (H1 x).
Hdist.
rewrite /dist//=. rewrite /iprodC //= /ofe_dist //=.
rewrite /iprod //=.
rewrite /iprod_cofe_mixin.
rewrite /OfeT.
rewrite /ofe_dist//=. intros Hiprod. rewrite / rewrite //=. inversion 1. apply _.
Defined.
Next Obligation.
*)
Discrete y Discrete (iprod_singleton x y) := _.
Lemma iprod_singleton_validN n x (y : B x) : {n} iprod_singleton x y {n} y.
Proof.
......
......@@ -197,6 +197,7 @@ Section cmra.
split.
- constructor.
- by intros l.
- by inversion_clear 1.
- by constructor.
Qed.
Canonical Structure listUR :=
......
This diff is collapsed.
From stdpp Require Export irelations.
From iris.algebra Require Export irelations.
From iris.prelude Require Import list.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import wsat ownership.
......
From stdpp Require Export irelations.
From iris.algebra Require Export irelations.
From iris.prelude Require Import list.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import wsat ownership.
From iris.program_logic Require Import adequacy.
......@@ -502,7 +503,7 @@ Section bounded_nondet_hom2.
invariant *)
Implicit Types rw: gmap positive (iRes Λ Σ).
Context (B: cofeT).
Context (B: ofeT).
Context (B_idx_step: nat relation (option B)).
Context (F: nat list (iRes Λ Σ) option B).
Context (F_proper: forall n, Proper (() ==> ()) (F n)).
......
From iris.program_logic Require Import language.
From stdpp Require Import set irelations.
From stdpp Require Import set.
From iris.algebra Require Import irelations.
Section delayed_lang.
......@@ -100,7 +101,7 @@ Section delayed_lang.
induction v.
- simpl. unfold delayed_to_val. simpl.
rewrite to_of_val. destruct (minimal_dec p); first exfalso; eauto.
repeat f_equal. apply proof_irrelevance.
repeat f_equal. eapply Classical_Prop.proof_irrelevance.
Qed.
Lemma delayed_of_to_val: e v, delayed_to_val e = Some v delayed_of_val v = e.
......
......@@ -66,7 +66,7 @@ Lemma own_valid_r γ a : own γ a ⊢ (own γ a ★ ⧆✓ a).
Proof. apply: uPred.relevant_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a (⧆✓ a own γ a).
Proof. by rewrite comm -own_valid_r. Qed.
Global Instance own_atimeless γ a : Timeless a ATimelessP (own γ a).
Global Instance own_atimeless γ a : Discrete a ATimelessP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Global Instance own_affine γ a : AffineP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
......@@ -182,7 +182,7 @@ Lemma owne_valid_r a : owne a ⊢ (owne a ★ ⧆✓ a).
Proof. apply: uPred.relevant_entails_r. apply owne_valid. Qed.
Lemma owne_valid_l a : owne a (⧆✓ a owne a).
Proof. by rewrite comm -owne_valid_r. Qed.
Global Instance owne_atimeless a : Timeless a ATimelessP (owne a).
Global Instance owne_atimeless a : Discrete a ATimelessP (owne a).
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
Global Instance owne_affine a : AffineP (owne a).
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
......
......@@ -53,7 +53,7 @@ Proof.
by rewrite /to_globalF iprod_op_singleton -ucmra_transport_op op_singleton.
Qed.
Global Instance to_globalF_timeless γ a : Discrete a Discrete (to_globalF γ a).
Proof. rewrite /to_globalF. apply _. Qed.
Proof. rewrite /to_globalF; apply _. Qed.
Global Instance to_globalF_persistent γ a :
Persistent a Persistent (to_globalF γ a).
Proof. rewrite /to_globalF; apply _. Qed.
......@@ -71,7 +71,7 @@ Lemma to_globalFe_op a1 a2 :
Proof.
by rewrite /to_globalFe iprod_op_singleton -ucmra_transport_op.
Qed.
Global Instance to_globalFe_timeless a: Timeless a Timeless (to_globalFe a).
Global Instance to_globalFe_timeless a: Discrete a Discrete (to_globalFe a).
Proof. rewrite /to_globalFe; apply _. Qed.
Global Instance to_globalFe_persistent a :
Persistent a Persistent (to_globalFe a).
......
......@@ -29,14 +29,14 @@ Proof.
uPred.unseal; split=> n r rl ?? Hvs; constructor; auto. intros k Ef σ1' rf rfl ???.
destruct (Hvs (S k) Ef σ1' rf rfl) as
(r'&(σ1&r1&r2&rl1&rl2&?&Hrl&((Hsafe&HP)&Haff)&Hwp)&Hws);
auto; clear Hvs; cofe_subst r'; cofe_subst rl1.
auto; clear Hvs; ofe_subst r'; ofe_subst rl1.
rewrite left_id in Hrl *=>Hrl.
destruct (wsat_update_pst k (E2 Ef) σ1 σ1' r1 (rl2 rfl) (r2 rf)) as [-> Hws'].
{ apply equiv_dist. rewrite -(ownP_spec' k); auto. }
{ rewrite -(dist_le _ _ _ _ Hrl); auto. by rewrite assoc. }
constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
destruct (λ H1 H2 H3 H4, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 H4 k Ef σ2 rf rfl)
as (r'&rl'&(r1'&r2'&rl1'&rl2'&?&?&?&Hfork)&?&Hs); auto; cofe_subst r'; cofe_subst rl'.
as (r'&rl'&(r1'&r2'&rl1'&rl2'&?&?&?&Hfork)&?&Hs); auto; ofe_subst r'; ofe_subst rl'.
{ split. done. apply ownP_spec; auto. }
{ rewrite ?right_id. rewrite (comm _ r2) -assoc; eauto using wsat_le. }
exists r1', r2', rl1', rl2'; split_and?; try done.
......@@ -57,7 +57,7 @@ Proof.
intros k Ef σ1 rf rfl ???; split; [done|]. destruct n as [|n]; first lia.
intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
destruct (λ H1 H2 H3 H4, Hwp e2 ef σ1 k H1 H2 H3 H4 k Ef σ1 rf rfl)
as (r'&rl'&(r1'&r2'&rl1'&rl2'&?&?&?&Hfork)&?&Hs); auto; cofe_subst r'; cofe_subst rl'.
as (r'&rl'&(r1'&r2'&rl1'&rl2'&?&?&?&Hfork)&?&Hs); auto; ofe_subst r'; ofe_subst rl'.
{ split; auto. }
{ rewrite ?right_id. eauto using wsat_le. }
exists r1', r2', rl1', rl2'; split_and?; try done.
......
From iris.program_logic Require Import language.
From stdpp Require Import set irelations.
From stdpp Require Import set.
From iris.algebra Require Import irelations.
Section delayed_lang.
......
......@@ -41,16 +41,8 @@ Proof.
Qed.
Global Instance ownP_affine σ : AffineP (@ownP Λ Σ σ).
Proof. rewrite /ownP. apply _. Qed.
(* TODO: FIX ME *)
(*
Global Instance ownP_atimeless σ : ATimelessP (@ownP Λ Σ σ).
Proof. Print Instances TimelessP. Print ATimelessP. rewrite /ownP. apply uPred.affine_atimeless.
apply uPred.ownM_atimeless.
apply res_timeless => //=. apply _. Print UCMRAT. apply _.
apply _.
rewrite /uPred_ownM //=.
rewrite /ownP; apply _. Qed.
*)
Proof. rewrite /ownP. apply _. Qed.
(* ghost state *)
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
......
This diff is collapsed.
This diff is collapsed.
......@@ -127,6 +127,7 @@ Proof.
split.
- split_and!; apply ucmra_unit_valid.
- by split; rewrite /= left_id.
- apply discrete. apply _.
- do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure resUR :=
......
......@@ -41,7 +41,7 @@ Section saved_prop.
{ intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
rewrite -{2}[x]help -{2}[y]help. apply affine_mono. apply later_mono.
apply (eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) G2 z))%I;
first solve_proper; auto with I.
apply (eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) G2 z))%I; auto with I.
{ intros ? ?? ->. auto. }
Qed.
End saved_prop.
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