Verified Commit 954e2ea7 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Mode for Equiv

Include workaround for Coq bug #14441.
parent a78b08fa
Pipeline #48975 canceled with stage
in 46 seconds
......@@ -33,6 +33,13 @@ Coq 8.11 is no longer supported in this version of Iris.
algorithm.
* Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`,
`rFunctorContractive`, `urFunctorContractive`.
* Also set `Hint Mode` for the stdpp class `Equiv`.
This might require few spurious type annotations until
https://github.com/coq/coq/issues/14441 is fixed.
This `Hint Mode` is not in stdpp due to Coq bugs
https://github.com/coq/coq/issues/5735 and
https://github.com/coq/coq/issues/9058, only fixed in Coq >= 8.12, which stdpp
supports and Iris does not.
* Add `max_prefix_list` RA on lists whose composition is only defined when one
operand is a prefix of the other. The result is the longer list.
......
......@@ -171,7 +171,8 @@ Section list.
([^o list] k y l1, f k y) ([^o list] k y l2, g k y).
Proof.
intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
intros k. assert (l1 !! k l2 !! k) as Hlk by (by f_equiv).
(* FIXME (Coq #14441) unnecessary type annotation *)
intros k. assert (l1 !! k @{option A} l2 !! k) as Hlk by (by f_equiv).
destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
......@@ -324,7 +325,8 @@ Section gmap.
([^o map] k y m1, f k y) ([^o map] k y m2, g k y).
Proof.
intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
intros k. assert (m1 !! k m2 !! k) as Hlk by (by f_equiv).
(* FIXME (Coq #14441) unnecessary type annotation *)
intros k. assert (m1 !! k @{option A} m2 !! k) as Hlk by (by f_equiv).
destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
......
......@@ -7,3 +7,7 @@ Ltac done := stdpp.tactics.done.
(** Iris itself and many dependencies still rely on this coercion. *)
Coercion Z.of_nat : nat >-> Z.
(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12, which Iris depends on. *)
Global Hint Mode Equiv ! : typeclass_instances.
......@@ -13,9 +13,6 @@ Section test_dist_equiv_mode.
Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
l1 l2 i, l1 !! i l2 !! i.
Abort.
Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
l1 l2 i, l1 !! i l2 !! i.
Abort.
End test_dist_equiv_mode.
(** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
......
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