Commit c9c90cf6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix issue #288.

parent d12506a1
...@@ -4,6 +4,7 @@ From iris.proofmode Require Import base modality_instances classes ltac_tactics. ...@@ -4,6 +4,7 @@ From iris.proofmode Require Import base modality_instances classes ltac_tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import bi. Import bi.
(* FIXME(Coq #6294): needs new unification *)
(** The lemma [from_assumption_exact is not an instance, but defined using (** The lemma [from_assumption_exact is not an instance, but defined using
[notypeclasses refine] through [Hint Extern] to enable the better unification [notypeclasses refine] through [Hint Extern] to enable the better unification
algorithm. We use [shelve] to avoid the creation of unshelved goals for evars algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
...@@ -15,6 +16,15 @@ Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed. ...@@ -15,6 +16,15 @@ Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
Hint Extern 0 (FromAssumption _ _ _) => Hint Extern 0 (FromAssumption _ _ _) =>
notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances. notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
(* FIXME(Coq #6294): needs new unification *)
(** Similarly, the lemma [from_exist_exist] is defined using a [Hint Extern] to
enable the better unification algorithm.
See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
Lemma from_exist_exist {PROP : bi} {A} (Φ : A PROP) : FromExist ( a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Hint Extern 0 (FromExist _ _) =>
notypeclasses refine (from_exist_exist _) : typeclass_instances.
Section bi_instances. Section bi_instances.
Context {PROP : bi}. Context {PROP : bi}.
Implicit Types P Q R : PROP. Implicit Types P Q R : PROP.
...@@ -871,8 +881,6 @@ Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 : ...@@ -871,8 +881,6 @@ Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
Proof. by rewrite /IntoOr -embed_or => <-. Qed. Proof. by rewrite /IntoOr -embed_or => <-. Qed.
(** FromExist *) (** FromExist *)
Global Instance from_exist_exist {A} (Φ : A PROP) : FromExist ( a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Global Instance from_exist_texist {A} (Φ : tele_arg A PROP) : Global Instance from_exist_texist {A} (Φ : tele_arg A PROP) :
FromExist (.. a, Φ a) Φ. FromExist (.. a, Φ a) Φ.
Proof. by rewrite /FromExist bi_texist_exist. Qed. Proof. by rewrite /FromExist bi_texist_exist. Qed.
......
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