Commit 011e9bbb authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Change the tactic for resolving typeclass instances from canonical structures.

Example include Equiv, Dist, Op, Core, Valid, ValidN and Unit.

The previous hints used eapply. The new hint now use refine. These two
tactic use a different unification algorithm, which result in
different behavior with respect to canonical structures.

The refine tactic is followed by shelving all the remaining goals,
which correspond actually to existential variables.

In particular, in RustHornBelt, the version using apply is unable to
find the canonical structure of heterogeneous lists.
parent 59e3a162
......@@ -27,6 +27,10 @@ Coq 8.11 is no longer supported in this version of Iris.
* Demote the Camera structure on `list` to `iris_staging` since its composition
is not very well-behaved.
* Extend `gmap_view` with lemmas for "big" operations on maps.
* Typeclasses instances triggering a canonical structure search such as `Equiv`,
`Dist`, `Op`, `Valid`, `ValidN`, `Unit`, `PCore` now use an `Hint Extern`
based on `refine` instead of `apply`, in order to use Coq's newer unification
algorithm.
**Changes in `bi`:**
......
......@@ -93,10 +93,11 @@ Global Arguments cmra_validN : simpl never.
Global Arguments cmra_ofe_mixin : simpl never.
Global Arguments cmra_mixin : simpl never.
Add Printing Constructor cmra.
Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
Global Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
Global Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.
Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
Coercion cmra_ofeO (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeO.
......@@ -215,7 +216,8 @@ Global Arguments ucmra_ofe_mixin : simpl never.
Global Arguments ucmra_cmra_mixin : simpl never.
Global Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmra.
Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.
Coercion ucmra_ofeO (A : ucmra) : ofe := Ofe A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeO.
Coercion ucmra_cmraR (A : ucmra) : cmra :=
......@@ -1543,7 +1545,7 @@ Section option_prod.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
End option_prod.
Lemma option_fmap_mono {A B : cmra} (f : A B) ma mb :
Lemma option_fmap_mono {A B : cmra} (f : A B) (ma mb : option A) :
Proper (() ==> ()) f
( a b, a b f a f b)
ma mb f <$> ma f <$> mb.
......
......@@ -56,8 +56,9 @@ Structure ofe := Ofe {
}.
Global Arguments Ofe _ {_ _} _.
Add Printing Constructor ofe.
Global Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
Global Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
Global Hint Extern 0 (Equiv _) => refine (ofe_equiv _); shelve : typeclass_instances.
Global Hint Extern 0 (Dist _) => refine (ofe_dist _); shelve : typeclass_instances.
Global Arguments ofe_car : simpl never.
Global Arguments ofe_equiv : simpl never.
Global Arguments ofe_dist : simpl never.
......
Supports Markdown
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