1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
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; }.
#[export] 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.
|
