Commit d157edcc authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ci/ralf/pair_core_id' into 'master'

Use apply: for pair_core_id

Closes #255

See merge request iris/iris!395
parents 287cfd91 9c47194e
From iris.algebra Require Import auth excl.
From iris.base_logic.lib Require Import invariants.
(** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
......@@ -34,3 +35,16 @@ Proof.
- apply _.
- reflexivity.
Qed.
(** Regression test for <https://gitlab.mpi-sws.org/iris/iris/issues/255>. *)
Definition testR := authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optionUR (exclR unitO)))
(optionUR (agreeR (boolO)))).
Section test_prod.
Context `{!inG Σ testR}.
Lemma test_prod_persistent γ :
Persistent (PROP:=iPropI Σ) (own γ (((None, None), Some (to_agree true)))).
Proof. apply _. Qed.
End test_prod.
......@@ -1170,7 +1170,9 @@ Section prod.
CmraDiscrete A CmraDiscrete B CmraDiscrete prodR.
Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
Global Instance pair_core_id x y :
(* FIXME(Coq #6294): This is not an instance because we need it to use the new
unification. *)
Lemma pair_core_id x y :
CoreId x CoreId y CoreId (x,y).
Proof. by rewrite /CoreId prod_pcore_Some'. Qed.
......@@ -1189,6 +1191,9 @@ Section prod.
Proof. move=>? [??] [_ ?] [_ /=?]. eauto. Qed.
End prod.
(* Registering as [Hint Extern] with new unification. *)
Hint Extern 4 (CoreId _) => notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
Arguments prodR : clear implicits.
Section prod_unit.
......
......@@ -324,4 +324,4 @@ End sbi_embed.
[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [monPred_objectively_plain]
for an example where it would fail with a regular [Instance].*)
Hint Extern 4 (Plain _) => eapply @embed_plain : typeclass_instances.
Hint Extern 4 (Plain _) => notypeclasses refine (embed_plain _ _) : typeclass_instances.
......@@ -633,4 +633,4 @@ Hint Immediate plain_persistent : typeclass_instances.
[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [coreP_persistent] for an
example where it would fail with a regular [Instance].*)
Hint Extern 4 (Persistent (_ _)) => eapply @impl_persistent : typeclass_instances.
Hint Extern 4 (Persistent _) => notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances.
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