Commit 4cba2266 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename cofe_subst -> ofe_subst.

parent d1ec2aec
......@@ -152,7 +152,7 @@ Proof.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- intros n [x a] [y b] [Hx Ha]; simpl in *. rewrite !auth_validN_eq.
destruct Hx as [?? Hx|]; first destruct Hx; intros ?; cofe_subst; auto.
destruct Hx as [?? Hx|]; first destruct Hx; intros ?; ofe_subst; auto.
- intros [[[?|]|] ?]; rewrite /= ?auth_valid_eq
?auth_validN_eq /= ?cmra_included_includedN ?cmra_valid_validN;
naive_solver eauto using O.
......
......@@ -309,7 +309,7 @@ Proof.
by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
Global Instance cmra_opM_ne : NonExpansive2 (@opM A).
Proof. destruct 2; by cofe_subst. Qed.
Proof. destruct 2; by ofe_subst. Qed.
Global Instance cmra_opM_proper : Proper (() ==> () ==> ()) (@opM A).
Proof. destruct 2; by setoid_subst. Qed.
......@@ -383,7 +383,7 @@ Qed.
Lemma cmra_valid_included x y : y x y x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_valid_op_l. Qed.
Lemma cmra_validN_includedN n x y : {n} y x {n} y {n} x.
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_included n x y : {n} y x y {n} x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
......@@ -1269,9 +1269,9 @@ Section option.
Proof.
apply cmra_total_mixin.
- eauto.
- by intros [x|] n; destruct 1; constructor; cofe_subst.
- destruct 1; by cofe_subst.
- by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
- by intros [x|] n; destruct 1; constructor; ofe_subst.
- destruct 1; by ofe_subst.
- by destruct 1; rewrite /validN /option_validN //=; ofe_subst.
- intros [x|]; [apply cmra_valid_validN|done].
- intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
- intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
......
......@@ -205,7 +205,7 @@ Qed.
Lemma csum_cmra_mixin : CMRAMixin (csum A B).
Proof.
split.
- intros [] n; destruct 1; constructor; by cofe_subst.
- intros [] n; destruct 1; constructor; by ofe_subst.
- intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto.
......@@ -213,7 +213,7 @@ Proof.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto.
exists (Cinr cb'); by repeat constructor.
- intros ? [a|b|] [a'|b'|] H; inversion_clear H; cofe_subst; done.
- intros ? [a|b|] [a'|b'|] H; inversion_clear H; ofe_subst; done.
- intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
- intros n [a|b|]; simpl; auto using cmra_validN_S.
- intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc.
......
......@@ -79,7 +79,7 @@ Global Instance gmap_lookup_timeless m i : Timeless m → Timeless (m !! i).
Proof.
intros ? [x|] Hx; [|by symmetry; apply: timeless].
assert (m {0} <[i:=x]> m)
by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
by (by symmetry in Hx; inversion Hx; ofe_subst; rewrite insert_id).
by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
Qed.
Global Instance gmap_insert_timeless m i x :
......
......@@ -20,13 +20,13 @@ Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption.
Notation NonExpansive f := ( n, Proper (dist n ==> dist n) f).
Notation NonExpansive2 f := ( n, Proper (dist n ==> dist n ==> dist n) f).
Tactic Notation "cofe_subst" ident(x) :=
Tactic Notation "ofe_subst" ident(x) :=
repeat match goal with
| _ => progress simplify_eq/=
| H:@dist ?A ?d ?n x _ |- _ => setoid_subst_aux (@dist A d n) x
| H:@dist ?A ?d ?n _ x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
end.
Tactic Notation "cofe_subst" :=
Tactic Notation "ofe_subst" :=
repeat match goal with
| _ => progress simplify_eq/=
| H:@dist ?A ?d ?n ?x _ |- _ => setoid_subst_aux (@dist A d n) x
......@@ -130,7 +130,7 @@ Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
(** General properties *)
Section cofe.
Section ofe.
Context {A : ofeT}.
Implicit Types x y : A.
Global Instance ofe_equivalence : Equivalence (() : relation A).
......@@ -176,7 +176,7 @@ Section cofe.
Proof.
split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
Qed.
End cofe.
End ofe.
(** Contractive functions *)
Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop :=
......@@ -764,7 +764,7 @@ Section sum.
Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
Global Instance inr_timeless (y : B) : Timeless y Timeless (inr y).
Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
Global Instance sum_discrete_cofe : Discrete A Discrete B Discrete sumC.
Global Instance sum_discrete_ofe : Discrete A Discrete B Discrete sumC.
Proof. intros ?? [?|?]; apply _. Qed.
End sum.
......@@ -806,8 +806,8 @@ Proof.
by apply sumC_map_ne; apply cFunctor_contractive.
Qed.
(** Discrete cofe *)
Section discrete_cofe.
(** Discrete OFE *)
Section discrete_ofe.
Context `{Equiv A} (Heq : @Equivalence A ()).
Instance discrete_dist : Dist A := λ n x y, x y.
......@@ -828,7 +828,7 @@ Section discrete_cofe.
intros n c. rewrite /compl /=;
symmetry; apply (chain_cauchy c 0 n). omega.
Qed.
End discrete_cofe.
End discrete_ofe.
Notation discreteC A := (OfeT A (discrete_ofe_mixin _)).
Notation leibnizC A := (OfeT A (@discrete_ofe_mixin _ equivL _)).
......@@ -1112,7 +1112,7 @@ Section sigma.
rewrite /dist /ofe_dist /= /sig_dist /equiv /ofe_equiv /= /sig_equiv /=.
apply (timeless _).
Qed.
Global Instance sig_discrete_cofe : Discrete A Discrete sigC.
Global Instance sig_discrete_ofe : Discrete A Discrete sigC.
Proof. intros ??. apply _. Qed.
End sigma.
......
......@@ -37,7 +37,7 @@ Section cmra.
Definition uPred_cmra_mixin : CMRAMixin (uPred M).
Proof.
apply cmra_total_mixin; try apply _ || by eauto.
- intros n P Q ??. by cofe_subst.
- intros n P Q ??. by ofe_subst.
- intros P; split.
+ intros HP n n' x ?. apply HP.
+ intros HP n x. by apply (HP n).
......
......@@ -76,7 +76,7 @@ Next Obligation.
Qed.
Next Obligation.
intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?; rewrite {1}(dist_le _ _ _ _ Hx) // =>?.
exists x1, x2; cofe_subst; split_and!;
exists x1, x2; ofe_subst; split_and!;
eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
Qed.
Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. Qed.
......@@ -238,7 +238,7 @@ Global Instance impl_proper :
Global Instance sep_ne : NonExpansive2 (@uPred_sep M).
Proof.
intros n P P' HP Q Q' HQ; split=> n' x ??.
unseal; split; intros (x1&x2&?&?&?); cofe_subst x;
unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
exists x1, x2; split_and!; try (apply HP || apply HQ);
eauto using cmra_validN_op_l, cmra_validN_op_r.
Qed.
......@@ -381,7 +381,7 @@ Qed.
Lemma sep_mono P P' Q Q' : (P Q) (P' Q') P P' Q Q'.
Proof.
intros HQ HQ'; unseal.
split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
Qed.
Lemma True_sep_1 P : P True P.
......@@ -390,7 +390,7 @@ Proof.
Qed.
Lemma True_sep_2 P : True P P.
Proof.
unseal; split; intros n x ? (x1&x2&?&_&?); cofe_subst;
unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst;
eauto using uPred_mono, cmra_includedN_r.
Qed.
Lemma sep_comm' P Q : P Q Q P.
......@@ -412,7 +412,7 @@ Proof.
Qed.
Lemma wand_elim_l' P Q R : (P Q - R) P Q R.
Proof.
unseal =>HPQR. split; intros n x ? (?&?&?&?&?). cofe_subst.
unseal =>HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
eapply HPQR; eauto using cmra_validN_op_l.
Qed.
......@@ -508,7 +508,7 @@ Qed.
(* Valid *)
Lemma ownM_valid (a : M) : uPred_ownM a a.
Proof.
unseal; split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
Qed.
Lemma cmra_valid_intro {A : cmraT} (a : A) : a uPred_valid (M:=M) ( a).
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. 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