Skip to content

GitLab

Commit 83b90e1d authored by Ralf Jung's avatar Ralf Jung
Browse files

make "\checkmark u" a proposition

parent f0d016bf
Hide whitespace changes
Inline Side-by-side
iris_core.v
View file @ 83b90e1d
......@@ -14,7 +14,7 @@ Module IrisRes (RL : RA_T) (C : CORE_LANG) <: RA_T.
(* The order on (ra_pos res) is inferred correctly, but this one is not *)
Instance res_pord: preoType res := ra_preo res.
End IrisRes.
Module IrisCore (RL : RA_T) (C : CORE_LANG).
Export C.
Module Export R := IrisRes RL C.
......@@ -188,8 +188,8 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Proof.
intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
- destruct Hut as [s Heq]. rewrite assoc in Heq.
assert (VALu:✓(s · u) = true). { eapply ra_op_pos_valid. eassumption. }
assert (VALt:✓t = true). { eapply ra_op_pos_valid2. eassumption. }
assert (VALu:✓(s · u) ). { eapply ra_op_pos_valid. eassumption. }
assert (VALt:✓t ). { eapply ra_op_pos_valid2. eassumption. }
exists (ra_mk_pos (s · u) (VAL:=VALu)). exists (ra_mk_pos t (VAL:=VALt)).
split; [|split].
+ rewrite <-Heq. reflexivity.
......@@ -201,12 +201,11 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
rewrite <-assoc, (comm _ u), assoc. reflexivity.
Qed.
Lemma ownR_valid u (INVAL: ✓u = false):
Lemma ownR_valid u (INVAL: ~✓u):
ownR u ⊑ ⊥.
Proof.
intros w n [r VAL] [v Heq]. hnf. unfold ra_proj, proj1_sig in Heq.
rewrite <-Heq in VAL. apply ra_op_valid2 in VAL. rewrite INVAL in VAL.
discriminate.
rewrite <-Heq in VAL. apply ra_op_valid2 in VAL. contradiction.
Qed.
(** Proper physical state: ownership of the machine state **)
......@@ -345,7 +344,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
rewrite !assoc, (comm (_ r2)); reflexivity.
Qed.
Definition state_sat (r: res) σ: Prop := ✓r = true /\
Definition state_sat (r: res) σ: Prop := ✓r /\
match r with
| (ex_own s, _) => s = σ
| _ => True
......@@ -402,12 +401,12 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
apply HR; [reflexivity | assumption].
Qed.
Lemma wsat_not_empty σ m (r: res) w k (HN : ✓r = false) :
Lemma wsat_not_empty σ m (r: res) w k (HN : ~✓r) :
~ wsat σ m r w (S k) tt.
Proof.
intros [rs [HD _] ]. destruct HD as [VAL _].
assert(VALr:✓r = true).
{ eapply ra_op_valid. eassumption. }
assert(VALr:✓r).
{ eapply ra_op_valid; [now apply _|]. eassumption. }
congruence.
Qed.
......
lib/ModuRes/BI.v
View file @ 83b90e1d
......@@ -178,7 +178,7 @@ Section UPredBI.
Next Obligation.
intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]].
rewrite <- HEq', assoc in HEq; setoid_rewrite HLe.
assert(VAL: ✓ (rd · ra_proj r11) = true).
assert(VAL: ✓ (rd · ra_proj r11) ).
{ eapply ra_op_pos_valid; eassumption. }
exists (ra_cr_pos VAL) r12.
split; [|split;[|assumption] ].
......@@ -193,7 +193,7 @@ Section UPredBI.
Next Obligation.
intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP.
rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'.
assert (VAL: ✓ (r12 · ra_proj r) = true).
assert (VAL: ✓ (r12 · ra_proj r) ).
{ eapply ra_op_pos_valid. erewrite comm. eassumption. }
pose (rc := ra_cr_pos VAL).
eapply HSI with (r':=rc); [| etransitivity; eassumption |].
......@@ -369,14 +369,14 @@ Section UPredBI.
intros P Q R n r; split.
- intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]].
rewrite <- EQrr, assoc in EQr. unfold sc.
assert(VAL: ✓ (ra_proj r1 · ra_proj r2) = true).
assert(VAL: ✓ (ra_proj r1 · ra_proj r2) ).
{ eapply ra_op_pos_valid; eassumption. }
pose (r12 := ra_cr_pos VAL).
exists r12 r3; split; [assumption | split; [| assumption] ].
exists r1 r2; split; [reflexivity | split; assumption].
- intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]].
rewrite <- EQrr, <- assoc in EQr; clear EQrr.
assert(VAL: ✓ (ra_proj r2 · ra_proj r3) = true).
assert(VAL: ✓ (ra_proj r2 · ra_proj r3) ).
{ eapply ra_op_pos_valid. rewrite comm. eassumption. }
pose (r23 := ra_cr_pos VAL).
exists r1 r23; split; [assumption | split; [assumption |] ].
......@@ -729,7 +729,7 @@ Section MComplUP.
End MComplUP.
(* The above suffice for showing that the eqn used in Rose actually forms a Complete BI.
(* The above suffice for showing that the eqn used in Iris actually forms a Complete BI.
The following would allow for further monotone morphisms to be added. *)
Section MComplMM.
......
lib/ModuRes/RA.v
View file @ 83b90e1d
......@@ -24,13 +24,17 @@ Section Definitions.
ra_op_unit t : ra_op ra_unit t == t;
ra_valid_proper :> Proper (equiv ==> eq) ra_valid;
ra_valid_unit : ra_valid ra_unit = true;
ra_op_invalid t1 t2: ra_valid t1 = false -> ra_valid (ra_op t1 t2) = false
ra_op_valid t1 t2 : ra_valid (ra_op t1 t2) = true -> ra_valid t1 = true
}.
End Definitions.
Arguments ra_valid {T} {_} t.
Notation "1" := (ra_unit _) : ra_scope.
Notation "p · q" := (ra_op _ p q) (at level 40, left associativity) : ra_scope.
Notation "'✓' p" := (ra_valid _ p) (at level 35) : ra_scope.
Notation "'✓' p" := (ra_valid p = true) (at level 35) : ra_scope.
Notation "'~' '✓' p" := (ra_valid p <> true) (at level 35) : ra_scope.
Tactic Notation "decide✓" ident(t1) "eqn:" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H].
Delimit Scope ra_scope with ra.
......@@ -43,22 +47,22 @@ Section RAs.
Proof.
rewrite comm. now eapply ra_op_unit.
Qed.
Lemma ra_op_invalid2 t1 t2: ✓ t2 = false -> ✓ (t1 · t2) = false.
Lemma ra_op_valid2 t1 t2: ✓ (t1 · t2) -> ✓ t2.
Proof.
rewrite comm. now eapply ra_op_invalid.
rewrite comm. now eapply ra_op_valid.
Qed.
Lemma ra_op_valid t1 t2: ✓ (t1 · t2) = true -> ✓ t1 = true.
Lemma ra_op_invalid t1 t2: ~✓t1 -> ~✓(t1 · t2).
Proof.
intros Hval.
destruct (✓ t1) eqn:Heq; [reflexivity|].
rewrite <-Hval. symmetry. now eapply ra_op_invalid.
intros Hinval Hval.
apply Hinval.
eapply ra_op_valid; now eauto.
Qed.
Lemma ra_op_valid2 t1 t2: ✓ (t1 · t2) = true -> ✓ t2 = true.
Lemma ra_op_invalid2 t1 t2: ~✓t2 -> ~✓(t1 · t2).
Proof.
rewrite comm. now eapply ra_op_valid.
rewrite comm. now eapply ra_op_invalid.
Qed.
End RAs.
......@@ -74,7 +78,7 @@ Section Products.
| (s1, t1), (s2, t2) => (s1 · s2, t1 · t2)
end.
Global Instance ra_valid_prod : RA_valid (S * T) :=
fun st => match st with (s, t) => ✓ s && ✓ t
fun st => match st with (s, t) => ra_valid s && ra_valid t
end.
Global Instance ra_prod : RA (S * T).
Proof.
......@@ -87,9 +91,9 @@ Section Products.
- intros [s1 t1] [s2 t2] [Heqs Heqt]. unfold ra_valid; simpl in *.
rewrite Heqs, Heqt. reflexivity.
- unfold ra_unit, ra_valid; simpl. erewrite !ra_valid_unit by apply _. reflexivity.
- intros [s1 t1] [s2 t2]. unfold ra_valid; simpl. rewrite !andb_false_iff. intros [Hv|Hv].
+ left. now eapply ra_op_invalid.
+ right. now eapply ra_op_invalid.
- intros [s1 t1] [s2 t2]. unfold ra_valid; simpl. rewrite !andb_true_iff. intros [H1 H2]. split.
+ eapply ra_op_valid; now eauto.
+ eapply ra_op_valid; now eauto.
Qed.
End Products.
......@@ -98,11 +102,11 @@ Section PositiveCarrier.
Context {T} `{raT : RA T}.
Local Open Scope ra_scope.
Definition ra_pos: Type := { r | ✓ r = true }.
Definition ra_pos: Type := { r | ✓ r }.
Coercion ra_proj (t:ra_pos): T := proj1_sig t.
Definition ra_mk_pos t {VAL: ✓ t = true}: ra_pos := exist _ t VAL.
Definition ra_cr_pos {t} (VAL: ✓ t = true) := ra_mk_pos t (VAL:=VAL).
Definition ra_mk_pos t {VAL: ✓ t}: ra_pos := exist _ t VAL.
Definition ra_cr_pos {t} (VAL: ✓ t) := ra_mk_pos t (VAL:=VAL).
Program Definition ra_pos_unit: ra_pos := exist _ 1 _.
Next Obligation.
......@@ -110,14 +114,14 @@ Section PositiveCarrier.
Qed.
Lemma ra_op_pos_valid t1 t2 t:
t1 · t2 == ra_proj t -> ✓ t1 = true.
t1 · t2 == ra_proj t -> ✓ t1.
Proof.
destruct t as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
eapply ra_op_valid. eassumption.
eapply ra_op_valid; eassumption.
Qed.
Lemma ra_op_pos_valid2 t1 t2 t:
t1 · t2 == ra_proj t -> ✓ t2 = true.
t1 · t2 == ra_proj t -> ✓ t2.
Proof.
rewrite comm. now eapply ra_op_pos_valid.
Qed.
......
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