Commit 3f93532c authored by Ralf Jung's avatar Ralf Jung

reestablish general adequacy

parent 20691a2e
......@@ -256,6 +256,8 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
- eapply HL. exact IHn.
Qed.
(* TODO RJ: show loeb under a context *)
Lemma later_true: (⊤:Props) == .
Proof.
move=> w n.
......@@ -349,6 +351,26 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
split; tauto.
Qed.
Lemma box_star P Q :
(P * Q) == P * Q.
Proof.
intros w n. split; (destruct n; first (intro; exact:bpred)); intros [[wP wQ] [Heq [HP HQ]]]; simpl in *.
- exists (1 w, w). split_conjs; simpl.
+ now rewrite ra_op_unit.
+ rewrite ra_unit_idem. eapply propsNE; first eexact Heq.
eapply propsMW, HP. eexists; now erewrite comm.
+ eapply propsNE; first eexact Heq.
eapply propsMW, HQ. eexists; now erewrite comm.
- exists (1 w, 1 w). split_conjs.
+ rewrite /fst /snd. rewrite -{1}(ra_unit_idem w). rewrite ra_op_unit. reflexivity.
+ simpl. eapply propsNE; first (eapply cmra_unit_dist; eexact Heq).
eapply propsMW, HP. apply ra_unit_proper_pord. exists wQ; now rewrite comm.
+ simpl. eapply propsNE; first (eapply cmra_unit_dist; eexact Heq).
eapply propsMW, HQ. apply ra_unit_proper_pord. exists wP; now rewrite comm.
Qed.
(* TODO RJ: show relation to implication *)
Lemma box_dup P :
P == P * P.
Proof.
......
This diff is collapsed.
......@@ -106,13 +106,13 @@ Notation "p ∧ q" := (and p q) (at level 39, right associativity) : bi_scope.
Notation "p ∨ q" := (or p q) (at level 51, right associativity) : bi_scope.
Notation "p * q" := (sc p q) (at level 40, left associativity) : bi_scope.
Notation "p → q" := (impl p q) (at level 55, right associativity) : bi_scope.
Notation "P ↔ Q" := ((P Q) (Q P))%bi (at level 95, no associativity) : bi_scope.
Notation "P ↔ Q" := ((P Q) (Q P))%bi (at level 57, no associativity) : bi_scope.
Notation "p '-*' q" := (si p q) (at level 55, right associativity) : bi_scope.
Notation "∀ x , p" := (all n[(fun x => p)]) (at level 60, x ident, right associativity) : bi_scope.
Notation "∃ x , p" := (xist n[(fun x => p)]) (at level 60, x ident, right associativity) : bi_scope.
Notation "∀ x : T , p" := (all n[(fun x : T => p)]) (at level 60, x ident, right associativity) : bi_scope.
Notation "∃ x : T , p" := (xist n[(fun x : T => p)]) (at level 60, x ident, right associativity) : bi_scope.
Notation "t1 '===' t2" := (intEq t1 t2) (at level 30) : bi_scope.
Notation "t1 '===' t2" := (intEq t1 t2) (at level 35) : bi_scope.
Local Open Scope bi_scope.
......@@ -322,7 +322,7 @@ Section EqBIProps.
Lemma intEq_rewrite_goal {T} `{cmetric T} (t1 t2: T) P (φ: _ -n> B):
P t1 === t2 -> P φ t1 -> P φ t2.
Proof.
move=>HEQ Hφ. transitivity ((t1 === t2) φ t1).
move=>HEQ Hφ. transitivity (t1 === t2 φ t1).
- apply and_R. split; assumption.
- move=>{P HEQ Hφ}. rewrite -/pord. apply and_impl. rewrite intEq_leibnitz /bi_leibnitz.
apply (all_L φ). simpl morph. reflexivity.
......
......@@ -317,7 +317,7 @@ Section MonotoneExtCBI.
fun P Q => mclose (lift_bin impl P Q).
Global Program Instance sc_mm : scBI (T -m> B) :=
fun P Q => m[(fun t:T => xist n[(fun ts:T*T => ((Mfst ts · Msnd ts) === t) (P (Mfst ts) * Q (Msnd ts)))])].
fun P Q => m[(fun t:T => xist n[(fun ts:T*T => (Mfst ts · Msnd ts) === t (P (Mfst ts) * Q (Msnd ts)))])].
Next Obligation.
move=>t1 t2 EQt. rewrite /= -/dist. eapply xist_dist. move=>[ts1 ts2] /=. rewrite -/dist.
rewrite EQt. reflexivity.
......@@ -396,7 +396,7 @@ Section MonotoneExtCBI.
lift_bin and (umconst ((u1 · u2) === t)) (lift_bin sc (umconst (f1 u1)) n[(fun ts => ((fst ts · snd ts) === u2) (f2 (fst ts) * f3 (snd ts)))]).
Program Definition sc_mm_assoc_f2 u1 u2 t (f1 f2 f3: T -n> B) :=
lift_bin and (umconst ((u1 · u2) === t)) (lift_bin sc n[(fun ts => ((fst ts · snd ts) === u1) (f1 (fst ts) * f2 (snd ts)))] (umconst (f3 u2))).
lift_bin and (umconst ((u1 · u2) === t)) (lift_bin sc n[(fun ts => (fst ts · snd ts) === u1 (f1 (fst ts) * f2 (snd ts)))] (umconst (f3 u2))).
Existing Instance sc_equiv.
......
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