Commit 97dc4393 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Use projections in the instance of Timeless for pairs

parent 8c77aa2f
Pipeline #1445 passed with stage
......@@ -323,9 +323,9 @@ Section product.
apply (conv_compl n (chain_map snd c)).
Qed.
Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
Global Instance pair_timeless (x : A) (y : B) :
Timeless x Timeless y Timeless (x,y).
Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
Global Instance prod_timeless (x : A * B) :
Timeless (x.1) Timeless (x.2) Timeless x.
Proof. by intros ???[??]; split; apply (timeless _). Qed.
Global Instance prod_discrete_cofe : Discrete A Discrete B Discrete prodC.
Proof. intros ?? [??]; apply _. Qed.
End product.
......
......@@ -57,11 +57,6 @@ Proof. solve_proper. Qed.
Global Instance slice_persistent γ P : PersistentP (slice N γ P).
Proof. apply _. Qed.
(* This should go automatic *)
Instance box_own_auth_timeless γ
(a : auth (option (excl bool))) : TimelessP (box_own_auth γ a).
Proof. apply own_timeless, pair_timeless; apply _. Qed.
Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) b1 = b2.
Proof.
......
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