Skip to content

Commit af39522

Browse files
author
twwar
committed
nj namespace
1 parent 4110032 commit af39522

File tree

1 file changed

+52
-43
lines changed
  • Cslib/Logics/Propositional/NaturalDeduction

1 file changed

+52
-43
lines changed

‎Cslib/Logics/Propositional/NaturalDeduction/Basic.lean‎

Lines changed: 52 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,8 @@ open Proposition Theory
5757

5858
variable {Atom : Type u} [DecidableEq Atom] {T : Theory Atom}
5959

60+
namespace NJ
61+
6062
/-- Contexts are finsets of propositions. -/
6163
abbrev Ctx (Atom) := Finset (Proposition Atom)
6264

@@ -68,7 +70,7 @@ abbrev Sequent (Atom) := Ctx Atom × Proposition Atom
6870

6971
/-- A `T`-derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ,
7072
possibly appealing to axioms from `T`. -/
71-
inductive Theory.Derivation : Sequent Atom → Type _ where
73+
inductive _root_.PL.Theory.Derivation : Sequent Atom → Type _ where
7274
/-- Axiom -/
7375
| ax {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ T) : Derivation ⟨Γ, A⟩
7476
/-- Assumption -/
@@ -95,18 +97,19 @@ inductive Theory.Derivation : Sequent Atom → Type _ where
9597
Derivation ⟨Γ, A ⟶ B⟩ → Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩
9698

9799
/-- A sequent is derivable if it has a derivation. -/
98-
def Theory.SDerivable (S : Sequent Atom) := Nonempty (T.Derivation S)
100+
def _root_.PL.Theory.SDerivable (S : Sequent Atom) := Nonempty (T.Derivation S)
99101

100102
/-- A proposition is derivable if it has a derivation from the empty context. -/
101-
def Theory.PDerivable (A : Proposition Atom) := T.SDerivable ⟨∅, A⟩
103+
@[reducible]
104+
def _root_.PL.Theory.PDerivable (A : Proposition Atom) := T.SDerivable ⟨∅, A⟩
102105

103106
@[inherit_doc]
104107
scoped notation Γ " ⊢[" T' "] " A:90 => Theory.SDerivable (T := T') ⟨Γ, A⟩
105108

106109
@[inherit_doc]
107110
scoped notation "⊢[" T' "] " A:90 => Theory.PDerivable (T := T') A
108111

109-
theorem Theory.Derivable.iff_sDerivable_empty {A : Proposition Atom} :
112+
theorem _root_.PL.Theory.Derivable.iff_sDerivable_empty {A : Proposition Atom} :
110113
⊢[T] A ↔ ∅ ⊢[T] A := by rfl
111114

112115
abbrev SDerivable (S : Sequent Atom) := MPL.SDerivable S
@@ -118,21 +121,22 @@ scoped notation Γ " ⊢ " A:90 => SDerivable ⟨Γ,A⟩
118121
scoped notation "⊢ " A:90 => PDerivable A
119122

120123
/-- An equivalence between A and B is a derivation of B from A and vice-versa. -/
121-
def Theory.equiv (A B : Proposition Atom) := T.Derivation ⟨{A},B⟩ × T.Derivation ⟨{B},A⟩
124+
def _root_.PL.Theory.equiv (A B : Proposition Atom) := T.Derivation ⟨{A},B⟩ × T.Derivation ⟨{B},A⟩
122125

123126
/-- `A` and `B` are T-equivalent if `T.equiv A B` is nonempty. -/
124-
def Theory.Equiv (A B : Proposition Atom) := Nonempty (T.equiv A B)
127+
def _root_.PL.Theory.Equiv (A B : Proposition Atom) := Nonempty (T.equiv A B)
125128

126129
@[inherit_doc]
127130
scoped notation A " ≡[" T' "] " B:29 => Theory.Equiv (T := T') A B
128131

129-
lemma Theory.Equiv.mp {A B : Proposition Atom} (h : A ≡[T] B) : {A} ⊢[T] B :=
132+
lemma _root_.PL.Theory.Equiv.mp {A B : Proposition Atom} (h : A ≡[T] B) : {A} ⊢[T] B :=
130133
let ⟨D,_⟩ := h; ⟨D⟩
131134

132-
lemma Theory.Equiv.mpr {A B : Proposition Atom} (h : A ≡[T] B) : {B} ⊢[T] A :=
135+
lemma _root_.PL.Theory.Equiv.mpr {A B : Proposition Atom} (h : A ≡[T] B) : {B} ⊢[T] A :=
133136
let ⟨_,D⟩ := h; ⟨D⟩
134137

135-
theorem Theory.equiv_iff {A B : Proposition Atom} : A ≡[T] B ↔ {A} ⊢[T] B ∧ {B} ⊢[T] A := by
138+
theorem _root_.PL.Theory.equiv_iff {A B : Proposition Atom} :
139+
A ≡[T] B ↔ {A} ⊢[T] B ∧ {B} ⊢[T] A := by
136140
constructor
137141
· intro h
138142
exact ⟨h.mp, h.mpr⟩
@@ -148,7 +152,7 @@ open Derivation
148152
/-! ### Operations on derivations -/
149153

150154
/-- Weakening is a derived rule. -/
151-
def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom}
155+
def _root_.PL.Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom}
152156
(hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : T.Derivation ⟨Γ, A⟩ → T'.Derivation ⟨Δ, A⟩
153157
| ax hA => ax <| hTheory hA
154158
| ass hA => ass <| hCtx hA
@@ -165,48 +169,48 @@ def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposit
165169
| implE D D' => implE (D.weak hTheory hCtx) (D'.weak hTheory hCtx)
166170

167171
/-- Weakening the theory only. -/
168-
def Theory.Derivation.weak_theory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom}
169-
(hTheory : T ⊆ T') : T.Derivation ⟨Γ, A⟩ → T'.Derivation ⟨Γ, A⟩ :=
172+
def _root_.PL.Theory.Derivation.weak_theory {T T' : Theory Atom} {Γ : Ctx Atom}
173+
{A : Proposition Atom} (hTheory : T ⊆ T') : T.Derivation ⟨Γ, A⟩ → T'.Derivation ⟨Γ, A⟩ :=
170174
Theory.Derivation.weak hTheory (by rfl)
171175

172176
/-- Weakening the context only. -/
173-
def Theory.Derivation.weak_ctx {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom}
177+
def _root_.PL.Theory.Derivation.weak_ctx {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom}
174178
(hCtx : Γ ⊆ Δ) : T.Derivation ⟨Γ, A⟩ → T.Derivation ⟨Δ, A⟩ :=
175179
Theory.Derivation.weak (by rfl) hCtx
176180

177181
/-- Proof irrelevant weakening. -/
178-
theorem Theory.SDerivable.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom}
179-
(hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : Γ ⊢[T] A → (T'.SDerivable ⟨Δ, A⟩)
182+
theorem _root_.PL.Theory.SDerivable.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom}
183+
{A : Proposition Atom} (hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : Γ ⊢[T] A → (T'.SDerivable ⟨Δ, A⟩)
180184
| ⟨D⟩ => ⟨D.weak hTheory hCtx⟩
181185

182186
/-- Proof irrelevant weakening of the theory. -/
183-
theorem Theory.SDerivable.weak_theory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom}
184-
(hTheory : T ⊆ T') : Γ ⊢[T] A → Γ ⊢[T'] A
187+
theorem _root_.PL.Theory.SDerivable.weak_theory {T T' : Theory Atom} {Γ : Ctx Atom}
188+
{A : Proposition Atom} (hTheory : T ⊆ T') : Γ ⊢[T] A → Γ ⊢[T'] A
185189
| ⟨D⟩ => ⟨D.weak_theory hTheory⟩
186190

187191
/-- Proof irrelevant weakening of the context. -/
188-
theorem Theory.SDerivable.weak_ctx {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom}
189-
(hCtx : Γ ⊆ Δ) : Γ ⊢[T] A → Δ ⊢[T] A
192+
theorem _root_.PL.Theory.SDerivable.weak_ctx {T : Theory Atom} {Γ Δ : Ctx Atom}
193+
{A : Proposition Atom} (hCtx : Γ ⊆ Δ) : Γ ⊢[T] A → Δ ⊢[T] A
190194
| ⟨D⟩ => ⟨D.weak_ctx hCtx⟩
191195

192196
/--
193197
Implement the cut rule, removing a hypothesis `A` from `E` using a derivation `D`. This is *not*
194198
substitution, which would replace appeals to `A` in `E` by the whole derivation `D`.
195199
-/
196-
def Theory.Derivation.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom}
200+
def _root_.PL.Theory.Derivation.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom}
197201
(D : T.Derivation ⟨Γ, A⟩) (E : T.Derivation ⟨insert A Δ, B⟩) : T.Derivation ⟨Γ ∪ Δ, B⟩ := by
198202
refine implE ?_ (D.weak_ctx Finset.subset_union_left)
199203
have : insert A Δ ⊆ insert A (Γ ∪ Δ) := by grind
200204
exact implI (Γ ∪ Δ) <| E.weak_ctx this
201205

202206
/-- Proof irrelevant cut rule. -/
203-
theorem Theory.SDerivable.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} :
207+
theorem _root_.PL.Theory.SDerivable.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} :
204208
Γ ⊢[T] A → (insert A Δ) ⊢[T] B → (Γ ∪ Δ) ⊢[T] B
205209
| ⟨D⟩, ⟨E⟩ => ⟨D.cut E⟩
206210

207211
/-- Remove unnecessary hypotheses. This can't be computable because it requires picking an order
208212
on the finset `Δ`. -/
209-
theorem Theory.SDerivable.cut_away {Γ Δ : Ctx Atom} {B : Proposition Atom}
213+
theorem _root_.PL.Theory.SDerivable.cut_away {Γ Δ : Ctx Atom} {B : Proposition Atom}
210214
(hΔ : ∀ A ∈ Δ, Γ ⊢[T] A) (hDer : (Γ ∪ Δ) ⊢[T] B) : Γ ⊢[T] B := by
211215
induction Δ using Finset.induction with
212216
| empty => exact hDer.weak_ctx (by grind)
@@ -219,7 +223,7 @@ theorem Theory.SDerivable.cut_away {Γ Δ : Ctx Atom} {B : Proposition Atom}
219223
· rwa [← Finset.union_insert A Γ Δ]
220224

221225
/-- Substitution of a derivation `D` for one of the hypotheses in the context `Δ` of `E`. -/
222-
def Theory.Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom}
226+
def _root_.PL.Theory.Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom}
223227
(D : T.Derivation ⟨Γ, A⟩) (E : T.Derivation ⟨Δ, B⟩) : T.Derivation ⟨Γ ∪ (Δ \ {A}), B⟩ := by
224228
match E with
225229
| ax hB => exact ax hB
@@ -268,7 +272,7 @@ def Theory.Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom}
268272
| implE E E' => exact implE (D.subs E) (D.subs E')
269273

270274
/-- Transport a derivation along a map of atoms. -/
271-
def Theory.Derivation.map {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
275+
def _root_.PL.Theory.Derivation.map {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
272276
{T : Theory Atom} (f : Atom → Atom') {Γ : Ctx Atom} {B : Proposition Atom} :
273277
T.Derivation ⟨Γ, B⟩ → (T.map f).Derivation ⟨Γ.map f, B.map f⟩
274278
| ax h => ax <| Set.mem_image_of_mem (Proposition.map f) h
@@ -284,35 +288,36 @@ def Theory.Derivation.map {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq
284288
| implI _ D => implI _ <| (Finset.image_insert (Proposition.map f) _ _) ▸ (D.map f)
285289
| implE D E => implE (D.map f) (E.map f)
286290

287-
theorem Theory.Derivable.image {Atom' : Type u} [DecidableEq Atom'] {T : Theory Atom}
291+
theorem _root_.PL.Theory.Derivable.image {Atom' : Type u} [DecidableEq Atom'] {T : Theory Atom}
288292
(f : Atom → Atom') {Γ : Ctx Atom} {B : Proposition Atom} :
289293
Γ ⊢[T] B → (Γ.map f) ⊢[T.map f] (B.map f) := by
290294
intro ⟨D⟩
291295
exact ⟨D.map f⟩
292296

293297
/-! ### Properties of equivalence -/
294298

295-
def Theory.derivationTop [Inhabited Atom] : T.Derivation ⟨∅, ⊤⟩ :=
299+
def _root_.PL.Theory.derivationTop [Inhabited Atom] : T.Derivation ⟨∅, ⊤⟩ :=
296300
implI ∅ <| ass <| by grind
297301

298-
theorem Theory.pDerivable_top [Inhabited Atom] : ⊢[T] ⊤ := ⟨T.derivationTop⟩
302+
theorem _root_.PL.Theory.pDerivable_top [Inhabited Atom] : ⊢[T] ⊤ := ⟨T.derivationTop⟩
299303

300-
theorem Theory.pDerivable_iff_equiv_top [Inhabited Atom] (A : Proposition Atom) :
304+
theorem _root_.PL.Theory.pDerivable_iff_equiv_top [Inhabited Atom] (A : Proposition Atom) :
301305
⊢[T] A ↔ A ≡[T] ⊤ := by
302306
constructor <;> intro h
303307
· refine ⟨T.derivationTop.weak_ctx <| by grind, ?_⟩
304308
let D := Classical.choice h
305309
exact D.weak_ctx <| by grind
306310
· have : (∅ : Ctx Atom) = ∅ ∪ ∅ := rfl
307-
rw [PDerivable, this]
308-
refine Theory.SDerivable.cut T.pDerivable_top h.mpr
311+
change Theory.SDerivable ⟨∅, A⟩
312+
refine this ▸ Theory.SDerivable.cut T.pDerivable_top h.mpr
309313

310314
/-- Change the conclusion along an equivalence. -/
311315
def mapEquivConclusion (Γ : Ctx Atom) {A B : Proposition Atom} (e : T.equiv A B)
312316
(D : T.Derivation ⟨Γ, A⟩) : T.Derivation ⟨Γ, B⟩ :=
313-
Γ.union_empty ▸ Theory.Derivation.cut (Δ := ∅) D e.1
317+
Γ.union_empty ▸ cut (Δ := ∅) D e.1
314318

315-
theorem Theory.equiv_iff_equiv_sDerivable {A B : Proposition Atom} :
319+
/-- `A` and `B` are equivalent iff they are proved by the same contexts. -/
320+
theorem _root_.PL.Theory.equiv_iff_equiv_sDerivable {A B : Proposition Atom} :
316321
A ≡[T] B ↔ ∀ Γ : Ctx Atom, Γ ⊢[T] A ↔ Γ ⊢[T] B := by
317322
constructor
318323
· intro ⟨D,E⟩ Γ
@@ -331,7 +336,8 @@ def mapEquivHypothesis (Γ : Ctx Atom) {A B : Proposition Atom} (e : T.equiv A B
331336
have : insert B Γ = {B} ∪ Γ := rfl
332337
exact this ▸ Theory.Derivation.cut e.2 D
333338

334-
theorem Theory.equiv_iff_equiv_hypothesis {A B : Proposition Atom} :
339+
/-- `A` and `B` are equivalent iff they have equivalent strength as hypotheses. -/
340+
theorem _root_.PL.Theory.equiv_iff_equiv_hypothesis {A B : Proposition Atom} :
335341
A ≡[T] B ↔
336342
∀ (Γ : Ctx Atom) (C : Proposition Atom), (insert A Γ) ⊢[T] C ↔ (insert B Γ) ⊢[T] C := by
337343
constructor
@@ -371,7 +377,8 @@ theorem equivalent_trans {T : Theory Atom} {A B C : Proposition Atom} :
371377
| ⟨e⟩, ⟨e'⟩ => ⟨transEquiv e e'⟩
372378

373379
/-- Equivalence is indeed an equivalence relation. -/
374-
theorem Theory.equiv_equivalence (T : Theory Atom) : Equivalence (T.Equiv (Atom := Atom)) :=
380+
theorem _root_.PL.Theory.equiv_equivalence (T : Theory Atom) :
381+
Equivalence (T.Equiv (Atom := Atom)) :=
375382
⟨equivalent_refl, equivalent_comm, equivalent_trans⟩
376383

377384
protected def Theory.propositionSetoid (T : Theory Atom) : Setoid (Proposition Atom) :=
@@ -385,15 +392,15 @@ ought also to generalise.
385392
-/
386393

387394
/-- A theory `T` is weaker than `T'` if all its axioms are `T'`-derivable. -/
388-
def Theory.WeakerThan (T T' : Theory Atom) : Prop :=
395+
def _root_.PL.Theory.WeakerThan (T T' : Theory Atom) : Prop :=
389396
∀ A ∈ T, T'.PDerivable A
390397

391398
instance instLETheory : LE (Theory Atom) where
392399
le := Theory.WeakerThan
393400

394401
/-- Replace appeals to axioms in `T` by `T'`-derivations. -/
395-
noncomputable def Theory.Derivation.mapLE {T T' : Theory Atom} {S : Sequent Atom} (h : T ≤ T') :
396-
T.Derivation S → T'.Derivation S
402+
noncomputable def _root_.PL.Theory.Derivation.mapLE {T T' : Theory Atom} {S : Sequent Atom}
403+
(h : T ≤ T') : T.Derivation S → T'.Derivation S
397404
| ax hB => Classical.choice (h _ hB) |>.weak_ctx (by grind)
398405
| ass hB => ass hB
399406
| conjI D E => conjI (D.mapLE h) (E.mapLE h)
@@ -406,13 +413,13 @@ noncomputable def Theory.Derivation.mapLE {T T' : Theory Atom} {S : Sequent Atom
406413
| implE D E => implE (D.mapLE h) (E.mapLE h)
407414

408415
/-- Proof irrelevant substitution of `T`-axioms. -/
409-
theorem Theory.Derivable.map_LE {T T' : Theory Atom} {S : Sequent Atom} (h : T ≤ T') :
416+
theorem _root_.PL.Theory.Derivable.map_LE {T T' : Theory Atom} {S : Sequent Atom} (h : T ≤ T') :
410417
T.SDerivable S → T'.SDerivable S
411418
| ⟨D⟩ => ⟨D.mapLE h⟩
412419

413420
/-- `T ≤ T'` is in fact equivalent to the stronger condition in the conclusion of
414421
`Theory.Derivation.mapLE`. -/
415-
theorem Theory.LE_iff_map {T T' : Theory Atom} :
422+
theorem _root_.PL.Theory.LE_iff_map {T T' : Theory Atom} :
416423
T ≤ T' ↔ ∀ S : Sequent Atom, T.SDerivable S → T'.SDerivable S := by
417424
constructor
418425
· intro h _
@@ -427,15 +434,17 @@ instance instPreorderTheory : Preorder (Theory Atom) where
427434

428435
/-- An extension `T'` of a theory `T` generalises `Theory.WeakerThan` to allow a change of the
429436
atomic language. -/
430-
structure Extension {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] (T : Theory Atom)
431-
(T' : Theory Atom') where
437+
structure _root_.PL.Theory.Extension {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
438+
(T : Theory Atom) (T' : Theory Atom') where
432439
f : Atom → Atom'
433440
h : T.map f ≤ T'
434441

435442
/-- An extension of theories is conservative if it doesn't add any new theorems, when restricted
436443
to the domain language `Atom`. -/
437-
def IsConservative {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] (T : Theory Atom)
438-
(T' : Theory Atom') : Extension T T' → Prop
444+
def Extension.IsConservative {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
445+
(T : Theory Atom) (T' : Theory Atom') : Extension T T' → Prop
439446
| ⟨f, _⟩ => ∀ (A : Proposition Atom), ⊢[T'] (A.map f) → ⊢[T] A
440447

448+
end NJ
449+
441450
end PL

0 commit comments

Comments
 (0)