Commit 766dbcd2 authored by Robbert Krebbers's avatar Robbert Krebbers

Use different module structuring of uPred.

This fixes the following issue by JH Jourdan:

  The fact of including uPred_[...] in the module uPred (in base_logic.v),
  implies that typeclasses instances are declared twice. Once in module
  uPred and once in module uPred_[...]. This has the unfortunate
  consequence that it has to backtrack to both instances each time the
  first one fails, making failure of type class search for e.g.
  PersistentP potentially exponential.

  Goal ((□ ∀ (x1 x2 x3 x4 x5: nat), True -∗ True) -∗ True : iProp Σ).
    Time iIntros "#H".
    Undo.
    Remove Hints uPred_derived.forall_persistent : typeclass_instances.
    Time iIntros "#H".

Thanks to Jason Gross @ Coq club for suggesting this fix.
parent b212b3fa
Pipeline #3336 passed with stage
in 11 minutes and 12 seconds
From iris.base_logic Require Export derived.
Module uPred.
Include uPred_entails.
Include uPred_primitive.
Include uPred_derived.
Module Import uPred.
Export upred.uPred.
Export primitive.uPred.
Export derived.uPred.
End uPred.
(* Hint DB for the logic *)
Import uPred.
Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
......
From iris.base_logic Require Export primitive.
Import uPred_entails uPred_primitive.
Import upred.uPred primitive.uPred.
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P Q) (Q P))%I.
Instance: Params (@uPred_iff) 1.
......@@ -34,7 +34,7 @@ Arguments timelessP {_} _ {_}.
Class PersistentP {M} (P : uPred M) := persistentP : P P.
Arguments persistentP {_} _ {_}.
Module uPred_derived.
Module uPred.
Section derived.
Context {M : ucmraT}.
Implicit Types φ : Prop.
......@@ -858,5 +858,4 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
Lemma always_entails_r P Q `{!PersistentP Q} : (P Q) P P Q.
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End derived.
End uPred_derived.
End uPred.
From iris.base_logic Require Import base_logic.
Import upred.
(* In this file we show that the bupd can be thought of a kind of
step-indexed double-negation when our meta-logic is classical *)
......
......@@ -40,7 +40,7 @@ Section fractional.
(** Fractional and logical connectives *)
Global Instance persistent_fractional P :
PersistentP P Fractional (λ _, P).
Proof. intros HP q q'. by apply uPred_derived.always_sep_dup. Qed.
Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
Global Instance fractional_sep Φ Ψ :
Fractional Φ Fractional Ψ Fractional (λ q, Φ q Ψ q)%I.
......
......@@ -192,7 +192,7 @@ Coercion uPred_valid {M} (P : uPred M) : Prop := True%I ⊢ P.
Notation "P -∗ Q" := (P Q)
(at level 99, Q at level 200, right associativity) : C_scope.
Module uPred_primitive.
Module uPred.
Definition unseal :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
......@@ -596,4 +596,4 @@ Proof. by unseal. Qed.
Lemma cofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f g ⊣⊢ x, f x g x.
Proof. by unseal. Qed.
End primitive.
End uPred_primitive.
End uPred.
From iris.base_logic Require Export primitive derived.
Import uPred_entails uPred_primitive.
From iris.base_logic Require Export base_logic.
Import uPred.
Section adequacy.
Context {M : ucmraT}.
......
......@@ -138,7 +138,7 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
(at level 95, no associativity) : C_scope.
Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
Module uPred_entails.
Module uPred.
Section entails.
Context {M : ucmraT}.
Implicit Types P Q : uPred M.
......@@ -173,4 +173,4 @@ Proof. by intros ->. Qed.
Lemma entails_equiv_r (P Q R : uPred M) : (P Q) (Q ⊣⊢ R) (P R).
Proof. by intros ? <-. Qed.
End entails.
End uPred_entails.
End uPred.
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