Axiom _0: Prop.

From Coq Require Export Morphisms Setoid Utf8.

Class Equiv A := equiv: relation A.

Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
Reserved Notation "■ P" (at level 20, right associativity).

(** Define the scope *)
Declare Scope bi_scope.
Delimit Scope bi_scope with I.

Structure bi :=
  Bi { bi_car :> Type;
       bi_entails : bi_car → bi_car → Prop;
       bi_impl : bi_car → bi_car → bi_car;
       bi_forall : ∀ A, (A → bi_car) → bi_car; }.

Declare Instance bi_equiv `{PROP:bi} : Equiv (bi_car PROP).

Arguments bi_car : simpl never.
Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
Arguments bi_forall {PROP _} _%I : simpl never, rename.

Notation "P ⊢ Q" := (bi_entails P%I Q%I) .
Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) .

Infix "→" := bi_impl : bi_scope.
Notation "∀ x .. y , P" :=
  (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.

(* bug disappears if definitional class *)
Class Plainly (PROP : bi) := { plainly : PROP -> PROP; }.
Notation "■ P" := (plainly P) : bi_scope.

Section S.
  Context {I : Type} {PROP : bi} `(Plainly PROP).

  Lemma plainly_forall `{Plainly PROP} {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊣⊢ ■ (∀ a, Ψ a).
  Proof. Admitted.

  Global Instance entails_proper :
    Proper (equiv ==> equiv ==> iff) (bi_entails : relation PROP).
  Proof. Admitted.

  Global Instance impl_proper :
    Proper (equiv ==> equiv ==> equiv) (@bi_impl PROP).
  Proof. Admitted.

  Global Instance forall_proper A :
    Proper (pointwise_relation _ equiv ==> equiv) (@bi_forall PROP A).
  Proof. Admitted.

  Declare Instance PROP_Equivalence: Equivalence (@equiv PROP _).

  Set Mangle Names.
  Lemma foo (P : I -> PROP) K:
    K ⊢ ∀ (j : I)
          (_ : Prop) (* bug disappears if this is removed *)
      , (∀ i0, ■ P i0) → P j.
  Proof.
    setoid_rewrite plainly_forall.
    (* retype in case the tactic did some nonsense *)
    match goal with |- ?T => let _ := type of T in idtac end.
  Abort.
End S.