-
Notifications
You must be signed in to change notification settings - Fork 30
/
IMSELL.v
148 lines (104 loc) · 5.25 KB
/
IMSELL.v
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)
Require Import List Permutation.
Set Implicit Arguments.
(* * Intuitionistic Multiplicative Sub-Exponential Linear Logic
derived from https://doi.org/10.1017/S0960129516000293 *)
Local Infix "~p" := (@Permutation _) (at level 70).
Reserved Notation "A ⊸ B" (at level 51, right associativity, format "A ⊸ B").
Reserved Notation "'![' m ']' x" (at level 52, format "![ m ] x").
Reserved Notation "‼ x" (at level 60, format "‼ x").
Section IMSELL.
Variables (var bang : Type)
(bang_le : bang -> bang -> Prop) (* a pre-order on modalities *)
(bang_U : bang -> Prop) (* universal modalities have structural rules *)
.
Notation Λ := bang.
Inductive imsell_form : Type :=
| imsell_var : var -> imsell_form
| imsell_ban : Λ -> imsell_form -> imsell_form
| imsell_imp : imsell_form -> imsell_form -> imsell_form.
Infix "⊸" := imsell_imp.
Notation "![ m ] x" := (imsell_ban m x).
Notation "£" := imsell_var.
Definition imsell_lban := map (fun '(m,A) => ![m]A).
Notation "‼ Γ" := (imsell_lban Γ).
Notation "u ≼ l" := (forall '(v,A), In (v,A) l -> bang_le u v) (at level 70).
Notation U := bang_U.
Reserved Notation "l ⊢ x" (at level 70, no associativity).
(* We consider the (![.],-o) fragment of IMSELL without cut *)
Inductive S_imsell : list imsell_form -> imsell_form -> Prop :=
| in_imsell_ax A : A::nil ⊢ A (* [identity] *)
| in_imsell_perm Γ Δ A : Γ ~p Δ -> Γ ⊢ A
(*----------------------------- [permutation] *)
-> Δ ⊢ A
| in_imsell_limp_l Γ Δ A B C : Γ ⊢ A -> B::Δ ⊢ C
(*----------------------------- [⊸L] *)
-> A⊸B::Γ++Δ ⊢ C
| in_imsell_limp_r Γ A B : A::Γ ⊢ B
(*----------------------------- [⊸R] *)
-> Γ ⊢ A⊸B
| in_imsell_bang_l Γ m A B : A::Γ ⊢ B
(*----------------------------- [!L] *)
-> ![m]A::Γ ⊢ B
| in_imsell_bang_r Γ m A : m ≼ Γ -> ‼Γ ⊢ A
(*----------------------------- [!R] *)
-> ‼Γ ⊢ ![m]A
| in_imsell_weak Γ u A B : U u -> Γ ⊢ B
(*----------------------------- [weakening] *)
-> ![u]A::Γ ⊢ B
| in_imsell_cntr Γ u A B : U u -> ![u]A::![u]A::Γ ⊢ B
(*----------------------------- [contraction] *)
-> ![u]A::Γ ⊢ B
where "Γ ⊢ A" := (S_imsell Γ A).
End IMSELL.
Infix "⊸" := imsell_imp.
Notation "![ m ] x" := (imsell_ban m x).
Notation "£" := imsell_var.
Notation "‼ Γ" := (imsell_lban Γ).
(* An IMSELL signature is a type of modalities pre-ordered
and an upper-closed subset of exponentials *)
Record IMSELL_sig : Type :=
{ IMSELL_Λ :> Type;
IMSELL_le : IMSELL_Λ -> IMSELL_Λ -> Prop;
IMSELL_refl : forall m, IMSELL_le m m;
IMSELL_trans : forall u v w, IMSELL_le u v -> IMSELL_le v w -> IMSELL_le u w;
IMSELL_U : IMSELL_Λ -> Prop;
IMSELL_clos : forall u v, IMSELL_U u -> IMSELL_le u v -> IMSELL_U v
}.
Section imsell3.
(* The minimal signature for this undecidability proof
3 modalities {a,b,∞} with a,b < ∞ and ∞ is the only
universal modality *)
Let bang := option bool.
Let bang_le (u v : bang) :=
match v with
| None => True
| Some _ => u = v
end.
Let bang_U := @eq bang None.
Definition imsell3 : IMSELL_sig.
Proof.
exists bang bang_le bang_U; trivial.
all: repeat intros [[]|]; now simpl.
Defined.
End imsell3.
Local Infix "≤" := (@IMSELL_le _) (at level 70).
Local Notation "u ≰ v" := (~ u ≤ v) (at level 70).
Local Notation U := (@IMSELL_U _).
Definition IMSELL_sig3 :=
{ S : IMSELL_sig | exists a b i : S, a ≤ i /\ b ≤ i /\ a ≰ b /\ b ≰ a
/\ ~ U a /\ ~ U b /\ U i }.
Definition IMSELL_problem (S : IMSELL_sig) :=
let F := imsell_form nat (IMSELL_Λ S) in (list F * F)%type.
Definition IMSELL_problem3 (S : IMSELL_sig3) := IMSELL_problem (proj1_sig S).
(* Cut-free provability over an IMSELL signature *)
Definition IMSELL_cf_PROVABILITY S (P : IMSELL_problem S) :=
let (Γ,A) := P in S_imsell (IMSELL_le S) (IMSELL_U S) Γ A.
Definition IMSELL_cf_PROVABILITY3 S (P : IMSELL_problem3 S) := IMSELL_cf_PROVABILITY P.