@@ -12,41 +12,21 @@ public import Cslib.Foundations.Logic.InferenceSystem
1212/-! # Multiplicative Classical Linear Logic (MLL)
1313
1414Multiplicative classical linear logic, defined as a fragment of classical linear logic by means of
15- `Subtype`.
15+ a predicate (unbundled style) and `Subtype` (bundled style) .
1616
17- This file also serves as the reference example of how to define a fragment of an inference system
18- through `Subtype`, following the next recipe.
17+ This file serves as the reference example of how to define a fragment of an inference system
18+ through tagging of `InferenceSystem` and `Subtype`, following the next recipe. It is a work in
19+ progress: the recipe will evolve together with how the Lean and CSLib ecosystems can
20+ deal with this general problem.
1921
20221. Define predicates for restricting relevant types to the fragment, here `IsMLL` for propositions
2123
22- system (here `Cslib.Logic.CLL`).
23- 2. Define the types in the fragment -- here `MLL.Proposition` and `MLL.Proof` -- as abbreviations of
24-
24+ system (here `Cslib.Logic.CLL`). Custom recursors can be defined for convenient case analysis that
25+ automatically discharges irrelevant cases (those not in the fragment).
26+ 2. Define the inference system in the fragment -- here `MLL.Proof` -- as an abbreviation of
27+
2528
2629We also call the first part the 'unbundled part' and the second the 'bundled part'.
27-
28- This recipe has the advantage that any value (propositions, proofs, etc.) in the fragment is
29- coerciable into the original system for free through `Subtype`.
30-
31- The main disadvantage is that the fragment does not have its own inductives, so case analysis
32- requires carrying around the restricting predicate(s) as parameters to discharge irrelevant cases
33- from the original system.
34- This can be elegantly managed by unbundling the predicate right away, so that `match` (or similar)
35- can automatically eliminate irrelevant cases.
36- For example, the following definition checks that an MLL proof is cut-free:
37-
38- ```
39- /-- A proof is cut-free if it does not contain any applications of rule cut. -/
40- def Proof.cutFree {Γ : Sequent Atom} (p : ⇓Γ) : Bool :=
41- go p.val p.property
42- where go {Γ : CLL.Sequent Atom} (p : ⇓Γ) (hp : p.IsMLL) : Bool :=
43- match p, hp with
44- | .ax, _ => true
45- | .bot p, hp | .parr p, hp => go p hp
46- | .one, _ => true
47- | .cut _ _, _ => false
48- | .tensor p q, hp => go p hp.left && go q hp.right
49- ```
5030-/
5131
5232@[expose] public section
@@ -60,12 +40,39 @@ def Proposition.IsMLL : Proposition Atom → Prop
6040 | tensor a b | parr a b => a.IsMLL ∧ b.IsMLL
6141 | _ => False
6242
43+ /-- Recursor for MLL propositions. -/
44+ @ [induction_eliminator, cases_eliminator, elab_as_elim]
45+ def Proposition.IsMLL.rec
46+ {motive : {a : Proposition Atom} → (h : a.IsMLL) → Sort u}
47+ (atom : ∀ x : Atom, motive (a := .atom x) (by simp))
48+ (atomDual : ∀ x : Atom, motive (a := .atomDual x) (by simp))
49+ (one : motive (a := .one) (by simp))
50+ (bot : motive (a := .bot) (by simp))
51+ (tensor : ∀ (a b : Proposition Atom) {ha : a.IsMLL} {hb : b.IsMLL},
52+ motive ha → motive hb → motive (a :=.tensor a b) (by simp [ha,hb]))
53+ (parr : ∀ (a b : Proposition Atom) {ha : a.IsMLL} {hb : b.IsMLL},
54+ motive ha → motive hb → motive (a := .parr a b) (by simp [ha,hb]))
55+ {a : Proposition Atom} (h : a.IsMLL) : motive (a := a) h :=
56+ match a, h with
57+ | .atom x, _ => atom x
58+ | .atomDual x, _ => atomDual x
59+ | .one, _ => one
60+ | .bot, _ => bot
61+ | .tensor a b, ⟨ha, hb⟩ =>
62+ tensor a b (ha := ha) (hb := hb)
63+ (Proposition.IsMLL.rec atom atomDual one bot tensor parr ha)
64+ (Proposition.IsMLL.rec atom atomDual one bot tensor parr hb)
65+ | .parr a b, ⟨ha, hb⟩ =>
66+ parr a b
67+ (Proposition.IsMLL.rec atom atomDual one bot tensor parr ha)
68+ (Proposition.IsMLL.rec atom atomDual one bot tensor parr hb)
69+ | .zero, h | .top, h | .oplus _ _, h | .with _ _, h
70+ | .bang _, h | .quest _, h => nomatch h
71+
6372/-- Duality in MLL stays in MLL. -/
6473@ [scoped grind →]
6574theorem Proposition.isMLL_dual {a : Proposition Atom} (ha : a.IsMLL) : a⫠.IsMLL := by
66- induction a with
67- | atom | atomDual | one | bot | tensor | parr => grind [dual, IsMLL]
68- | _ => grind [IsMLL]
75+ induction ha <;> grind [dual, IsMLL]
6976
7077/-- A multiplicative propositional context. -/
7178@[simp]
@@ -97,11 +104,47 @@ def Proof.IsMLL {Γ : Sequent Atom} : ⇓Γ → Prop
97104 | one => True
98105 | _ => False
99106
107+ /-- Recursor for MLL derivations. -/
108+ @ [induction_eliminator, cases_eliminator, elab_as_elim]
109+ def Proof.IsMLL.rec
110+ {motive : {Γ : Sequent Atom} → {p : Proof Γ} → (h : p.IsMLL) → Sort u}
111+ (ax : ∀ {a : Proposition Atom} {ha : a.IsMLL}, @motive {a, a⫠} .ax (by simp [ha]))
112+ (one : @motive {Proposition.one} .one (by simp))
113+ (bot : ∀ {Γ : Sequent Atom} (p : Proof Γ) {hp : p.IsMLL},
114+ @motive Γ p hp → @motive (.bot ::ₘ Γ) (.bot p) (by simp [hp]))
115+ (tensor : ∀ {a b : Proposition Atom} {Γ Δ : Sequent Atom}
116+ (p : Proof (a ::ₘ Γ)) (q : Proof (b ::ₘ Δ)) {hp : p.IsMLL} {hq : q.IsMLL},
117+ @motive (a ::ₘ Γ) p hp → @motive (b ::ₘ Δ) q hq →
118+ @motive ((a ⊗ b) ::ₘ (Γ + Δ)) (.tensor p q) (by simp [hp, hq]))
119+ (parr : ∀ {a b : Proposition Atom} {Γ : Sequent Atom}
120+ (p : Proof (a ::ₘ b ::ₘ Γ)) {hp : p.IsMLL},
121+ @motive (a ::ₘ b ::ₘ Γ) p hp → @motive ((a ⅋ b) ::ₘ Γ) (.parr p) (by simp [hp]))
122+ (cut : ∀ {a : Proposition Atom} {Γ Δ : Sequent Atom}
123+ (p : Proof (a ::ₘ Γ)) (q : Proof (a⫠ ::ₘ Δ)) {hp : p.IsMLL} {hq : q.IsMLL},
124+ @motive (a ::ₘ Γ) p hp → @motive (a⫠ ::ₘ Δ) q hq →
125+ @motive (Γ + Δ) (.cut p q) (by simp [hp, hq]))
126+ {Γ : Sequent Atom} {p : Proof Γ} (h : p.IsMLL) : @motive Γ p h :=
127+ match p, h with
128+ | .ax (a := a), hp => @ax a (by simpa)
129+ | .one, _ => one
130+ | .bot p (Γ := Γ), hp => @bot Γ p hp (IsMLL.rec ax one bot tensor parr cut (p := p) hp)
131+ | .tensor (a := a) (b := b) (Γ := Γ) (Δ := Δ) p q, h =>
132+ @tensor a b Γ Δ p q h.left h.right
133+ (IsMLL.rec ax one bot tensor parr cut h.left)
134+ (IsMLL.rec ax one bot tensor parr cut h.right)
135+ | .parr (a := a) (b := b) (Γ := Γ) p, hp =>
136+ @parr a b Γ p hp
137+ (IsMLL.rec ax one bot tensor parr cut (p := p) hp)
138+ | .cut (a := a) (Γ := Γ) (Δ := Δ) p q, h =>
139+ @cut a Γ Δ p q h.left h.right
140+ (IsMLL.rec ax one bot tensor parr cut h.left)
141+ (IsMLL.rec ax one bot tensor parr cut h.right)
142+
100143open scoped Sequent Proposition in
101- /-- An MLL proof can only prove MLL sequents. -/
102- theorem Proof.isMLL_sequent {Γ : Sequent Atom} ( p : ⇓Γ) (hp : p.IsMLL) : Γ.IsMLL := by
144+ /-- A proof in the MLL fragment can only prove MLL sequents. -/
145+ theorem Proof.isMLL_sequent {Γ : Sequent Atom} { p : ⇓Γ} (h : p.IsMLL) : Γ.IsMLL := by
103146 -- This should be simpler, grind seems to have some trouble.
104- induction p
147+ induction h
105148 case ax =>
106149 grind [Proof.IsMLL, Multiset.insert_eq_cons, Multiset.mem_singleton]
107150 case one =>
@@ -110,31 +153,52 @@ theorem Proof.isMLL_sequent {Γ : Sequent Atom} (p : ⇓Γ) (hp : p.IsMLL) : Γ.
110153 case bot Γ p ih =>
111154 simp
112155 grind [Proof.IsMLL]
113- case oplus₁ | oplus₂ | «with » | top | quest | weaken | contract | bang => contradiction
114156
115- end Cslib.Logic.CLL
157+ /-- If a CLL derivation is cut-free and concludes an MLL sequent, then it is an MLL derivation. -/
158+ theorem Proof.isMLL_cutFree {Γ : Sequent Atom} (p : ⇓Γ) (hΓ : Γ.IsMLL)
159+ (hp : p.cutFree) : p.IsMLL := by
160+ induction p
161+ case ax => simp_all
162+ case one => simp
163+ case bot _ _ ih =>
164+ refine ih ?_ hp
165+ simpa using hΓ
166+ case parr a b Γ p ih =>
167+ refine ih ?_ hp
168+ simp at hΓ
169+ grind [Sequent.IsMLL]
170+ case tensor a b Γ Δ p q ihp ihq =>
171+ simp at hΓ
172+ refine ⟨ihp ?mll.p ?cut.p, ihq ?mll.q ?cut.q⟩
173+ case mll | mll => grind [Sequent.IsMLL]
174+ case cut | cut => grind [cutFree]
175+ case oplus₁ | oplus₂ | «with » | top | quest | contract | weaken | bang => simp at hΓ
176+ case cut => simp [cutFree] at hp
116177
117- namespace Cslib.Logic.MLL
178+ /-- MLL derivations. -/
179+ abbrev MLL.Proof (Γ : CLL.Sequent Atom) := {p : ⇓Γ // p.IsMLL}
118180
119- /-- MLL propositions . -/
120- abbrev Proposition (Atom : Type u) := {a : CLL.Proposition Atom // a.IsMLL}
181+ /-- Tag for the MLL inference system . -/
182+ opaque MLL : Type := Empty
121183
122- /-- MLL propositional contexts . -/
123- abbrev Proposition.Context (Atom : Type u ) := {c : CLL.Proposition.Context Atom // c.IsMLL}
184+ /-- MLL inference system . -/
185+ instance : InferenceSystem MLL (Sequent Atom ) := ⟨MLL.Proof⟩
124186
125- /-- Filling of an MLL propositional context. -/
126- def Proposition.Context.fill (c : Proposition.Context Atom) (a : Proposition Atom) :
127- Proposition Atom where
128- val := CLL.Proposition.Context.fill c a
129- property := (CLL.Proposition.Context.isMLL_fill c.property).mpr a.property
187+ namespace MLL
130188
131- /-- MLL sequents. -/
132- abbrev Sequent (Atom : Type u) := {Γ : CLL.Sequent Atom // Γ.IsMLL}
189+ open InferenceSystem
133190
134- /-- MLL derivations. -/
135- abbrev Proof {Atom : Type u} (Γ : Sequent Atom) := {p : CLL.Proof (Atom := Atom) Γ // p.IsMLL}
191+ /-- MLL proofs derive only MLL sequents. -/
192+ theorem Proof.isMLL_sequent {Γ : Sequent Atom} (p : MLL⇓Γ) : Γ.IsMLL :=
193+ CLL.Proof.isMLL_sequent p.property
136194
137- /-- The sequent calculus of MLL. -/
138- instance : Logic.InferenceSystem (Sequent Atom) := ⟨Proof⟩
195+ end MLL
139196
140- end Cslib.Logic.MLL
197+ /-- Downcasting of cut-free CLL proofs of multiplicative sequents into MLL proofs. -/
198+ def Proof.cutFreeToMLL {Γ : Sequent Atom} (p : ⇓Γ) (hΓ : Γ.IsMLL) (hp : p.cutFree) : MLL⇓Γ :=
199+ ⟨p, CLL.Proof.isMLL_cutFree p hΓ hp⟩
200+
201+ instance {Γ : Sequent Atom} : Coe (MLL⇓Γ) (⇓Γ) where
202+ coe p := p.val
203+
204+ end Cslib.Logic.CLL
0 commit comments