Skip to content

Commit d5b2038

Browse files
iehalityiehality
committed
bump
1 parent 60583d6 commit d5b2038

2 files changed

Lines changed: 290 additions & 51 deletions

File tree

‎Foundation/FirstOrder/Basic/Calculus2Alt.lean‎

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
module
2+
public import Foundation.FirstOrder.Basic.Calculus
3+
@[expose] public section
4+
5+
/-! # Alternative definition of proof -/
6+
7+
namespace LO.FirstOrder
8+
9+
variable {L : Language} [L.DecidableEq]
10+
11+
section derivation2
12+
13+
inductive Derivation2 (T : Theory L) : Finset (Proposition L) → Type _
14+
| closed (Γ) (φ : Proposition L) : φ ∈ Γ → ∼φ ∈ Γ → Derivation2 T Γ
15+
| axm {Γ} (φ : Sentence L) : φ ∈ T → (φ : Proposition L) ∈ Γ → Derivation2 T Γ
16+
| verum {Γ} : ⊤ ∈ Γ → Derivation2 T Γ
17+
| and {Γ} {φ ψ : Proposition L} : φ ⋏ ψ ∈ Γ → Derivation2 T (insert φ Γ) → Derivation2 T (insert ψ Γ) → Derivation2 T Γ
18+
| or {Γ} {φ ψ : Proposition L} : φ ⋎ ψ ∈ Γ → Derivation2 T (insert φ (insert ψ Γ)) → Derivation2 T Γ
19+
| all {Γ} {φ : Semiproposition L 1} : ∀⁰ φ ∈ Γ → Derivation2 T (insert (Rewriting.free φ) (Γ.image Rewriting.shift)) → Derivation2 T Γ
20+
| exs {Γ} {φ : Semiproposition L 1} : ∃⁰ φ ∈ Γ → (t : SyntacticTerm L) → Derivation2 T (insert (φ/[t]) Γ) → Derivation2 T Γ
21+
| wk {Δ Γ} : Derivation2 T Δ → Δ ⊆ Γ → Derivation2 T Γ
22+
| shift {Γ} : Derivation2 T Γ → Derivation2 T (Γ.image Rewriting.shift)
23+
| cut {Γ φ} : Derivation2 T (insert φ Γ) → Derivation2 T (insert (∼φ) Γ) → Derivation2 T Γ
24+
25+
scoped infix:45 " ⟹₂" => Derivation2
26+
27+
abbrev Derivable2 (T : Theory L) (Γ : Finset (Proposition L)) := Nonempty (T ⟹₂ Γ)
28+
29+
scoped infix:45 " ⟹₂! " => Derivable2
30+
31+
abbrev Derivable2SingleConseq (T : Theory L) (φ : Proposition L) : Prop := T ⟹₂! {φ}
32+
33+
scoped infix: 45 " ⊢!₂! " => Derivable2SingleConseq
34+
35+
variable {T : Theory L}
36+
37+
omit [L.DecidableEq] in
38+
@[simp] lemma Sequent.embed_append (A B : List (Sentence L)) :
39+
Sequent.embed (A ++ B) = Sequent.embed A ++ Sequent.embed B := by
40+
simp [Sequent.embed]
41+
42+
lemma shifts_toFinset_eq_image_shift (Γ : Sequent L) :
43+
(Rewriting.shifts Γ).toFinset = Γ.toFinset.image Rewriting.shift := by ext φ; simp [Rewriting.shifts]
44+
45+
set_option linter.flexible false in
46+
def Derivation.toDerivation2 (T) {Γ : Sequent L} : ⊢ᴸᴷ¹ Γ → T ⟹₂ Γ.toFinset
47+
| Derivation.identity R v => Derivation2.closed _ (Semiformula.rel R v) (by simp) (by simp)
48+
| Derivation.verum => Derivation2.verum (by simp)
49+
| Derivation.and (Γ := Γ) (φ := φ) (ψ := ψ) dp dq =>
50+
Derivation2.and (φ := φ) (ψ := ψ) (by simp)
51+
(Derivation2.wk (Derivation.toDerivation2 T dp) (by simp))
52+
(Derivation2.wk (Derivation.toDerivation2 T dq) (by simp))
53+
| Derivation.or (Γ := Γ) (φ := φ) (ψ := ψ) dpq =>
54+
Derivation2.or (φ := φ) (ψ := ψ) (by simp)
55+
(Derivation2.wk (Derivation.toDerivation2 T dpq)
56+
(by simp))
57+
| Derivation.all (Γ := Γ) (φ := φ) dp =>
58+
Derivation2.all (φ := φ) (by simp)
59+
(Derivation2.wk (Derivation.toDerivation2 T dp)
60+
(by
61+
intro x hx
62+
simp [shifts_toFinset_eq_image_shift] at hx ⊢
63+
grind))
64+
| Derivation.exs (Γ := Γ) (φ := φ) (t := t) dp =>
65+
Derivation2.exs (φ := φ) (by simp) t
66+
(Derivation2.wk (Derivation.toDerivation2 T dp) (by simp))
67+
| Derivation.contraction d h =>
68+
Derivation2.wk (Derivation.toDerivation2 T d) (List.toFinset_mono h)
69+
| Derivation.cut (Γ := Γ) (Δ := Δ) (φ := φ) d₁ d₂ =>
70+
Derivation2.cut (φ := φ)
71+
(Derivation2.wk (Derivation.toDerivation2 T d₁) (by intro x hx; simp at hx ⊢; grind))
72+
(Derivation2.wk (Derivation.toDerivation2 T d₂) (by intro x hx; simp at hx ⊢; grind))
73+
74+
namespace Derivation2
75+
76+
noncomputable def cast {Γ Δ : Finset (Proposition L)} (d : T ⟹₂ Γ) (h : Γ = Δ := by simp) : T ⟹₂ Δ := by
77+
rcases h; exact d
78+
79+
noncomputable def contra {Γ Δ : Finset (Proposition L)} (d : T ⟹₂ Δ) (h : Δ ⊆ Γ := by simp) : T ⟹₂ Γ :=
80+
d.wk h
81+
82+
omit [L.DecidableEq] in
83+
lemma mem_theory_append {A B : List (Sentence L)} (hA : ∀ ψ ∈ A, ψ ∈ T) (hB : ∀ ψ ∈ B, ψ ∈ T) :
84+
∀ ψ ∈ A ++ B, ψ ∈ T := by
85+
intro ψ hψ
86+
rcases List.mem_append.mp hψ with hψ | hψ
87+
· exact hA ψ hψ
88+
· exact hB ψ hψ
89+
90+
@[reducible] noncomputable def cutMany : (A : List (Sentence L)) → (∀ ψ ∈ A, ψ ∈ T) →
91+
T ⟹₂! (insert (φ : Proposition L) (∼Sequent.embed A).toFinset) → T ⟹₂! {φ}
92+
| [], _, d => d
93+
| ψ :: A, hA, ⟨d⟩ =>
94+
have ax : T ⟹₂ insert (ψ : Proposition L) (insert φ (∼Sequent.embed A).toFinset) :=
95+
Derivation2.axm ψ (hA ψ (by simp)) (by simp)
96+
have dn : T ⟹₂ insert (∼(ψ : Proposition L)) (insert φ (∼Sequent.embed A).toFinset) := by
97+
refine Derivation2.cast d ?_
98+
ext x; simp [List.toFinset_cons]; grind
99+
have c : T ⟹₂ insert φ (∼Sequent.embed A).toFinset := by
100+
refine Derivation2.cast (Derivation2.cut ax dn) ?_
101+
ext x; simp
102+
cutMany A (by intro θ hθ; exact hA θ (by simp [hθ])) ⟨c⟩
103+
104+
set_option linter.flexible false in
105+
noncomputable def toProof : {Γ : Finset (Proposition L)} → T ⟹₂ Γ →
106+
∃ A : List (Sentence L), (∀ ψ ∈ A, ψ ∈ T) ∧ Nonempty (⊢ᴸᴷ¹ Γ.toList ++ ∼Sequent.embed A)
107+
| Γ, closed _ φ hp hn =>
108+
⟨[], by simp, ⟨(Derivation.eta φ).contra (by intro x hx; simp at hx ⊢; grind)⟩⟩
109+
| Γ, axm φ hT hΓ =>
110+
⟨[φ], by simp [hT], ⟨(Derivation.eta (φ : Proposition L)).contra (by intro x hx; simp at hx ⊢; grind)⟩⟩
111+
| Γ, verum h =>
112+
⟨[], by simp, ⟨Derivation.verum.contra (by intro x hx; simp at hx ⊢; grind)⟩⟩
113+
| Γ, and (φ := φ) (ψ := ψ) h dφ dψ => by
114+
rcases toProof dφ with ⟨A, hA, ⟨bφ⟩⟩
115+
rcases toProof dψ with ⟨B, hB, ⟨bψ⟩⟩
116+
refine ⟨A ++ B, mem_theory_append hA hB, ⟨?_⟩⟩
117+
have bφ' : ⊢ᴸᴷ¹ φ :: Γ.toList ++ ∼Sequent.embed (A ++ B) :=
118+
bφ.contra (by intro x hx; simp at hx ⊢; grind)
119+
have bψ' : ⊢ᴸᴷ¹ ψ :: Γ.toList ++ ∼Sequent.embed (A ++ B) :=
120+
bψ.contra (by intro x hx; simp at hx ⊢; grind)
121+
exact (Derivation.and bφ' bψ').contra (by intro x hx; simp at hx ⊢; grind)
122+
| Γ, or (φ := φ) (ψ := ψ) h d => by
123+
rcases toProof d with ⟨A, hA, ⟨b⟩⟩
124+
refine ⟨A, hA, ⟨?_⟩⟩
125+
have b' : ⊢ᴸᴷ¹ φ :: ψ :: Γ.toList ++ ∼Sequent.embed A :=
126+
b.contra (by intro x hx; simp at hx ⊢; grind)
127+
exact (Derivation.or b').contra (by intro x hx; simp at hx ⊢; grind)
128+
| Γ, all (φ := φ) h d => by
129+
rcases toProof d with ⟨A, hA, ⟨b⟩⟩
130+
refine ⟨A, hA, ⟨?_⟩⟩
131+
have b' : ⊢ᴸᴷ¹ Rewriting.free φ :: (Γ.toList ++ ∼Sequent.embed A)⁺ :=
132+
b.contra (by
133+
intro x hx
134+
suffices x = Rewriting.free φ ∨ (∃ a ∈ Γ, Rewriting.shift a = x) ∨
135+
∃ a ∈ Sequent.embed A, Rewriting.shift a = ∼x by
136+
simpa [Rewriting.shifts] using this
137+
have hx' : (x = Rewriting.free φ ∨ ∃ a ∈ Γ, Rewriting.shift a = x) ∨
138+
∼x ∈ Sequent.embed A := by
139+
simpa [Rewriting.shifts] using hx
140+
rcases hx' with (rfl | hx) | hx
141+
· exact Or.inl rfl
142+
· exact Or.inr <| Or.inl hx
143+
· rw [Sequent.embed] at hx
144+
rcases List.mem_map.mp hx with ⟨θ, hθ, hθx⟩
145+
exact Or.inr <| Or.inr ⟨Rewriting.emb θ,
146+
by rw [Sequent.embed]; exact List.mem_map.mpr ⟨θ, hθ, rfl⟩,
147+
by rw [←hθx]; simp⟩)
148+
exact (Derivation.all b').contra (by intro x hx; simp at hx ⊢; grind)
149+
| Γ, exs (φ := φ) h t d => by
150+
rcases toProof d with ⟨A, hA, ⟨b⟩⟩
151+
refine ⟨A, hA, ⟨?_⟩⟩
152+
have b' : ⊢ᴸᴷ¹ φ/[t] :: Γ.toList ++ ∼Sequent.embed A :=
153+
b.contra (by intro x hx; simp at hx ⊢; grind)
154+
exact (Derivation.exs (t := t) b').contra (by intro x hx; simp at hx ⊢; grind)
155+
| Γ, wk d h => by
156+
rcases toProof d with ⟨A, hA, ⟨b⟩⟩
157+
refine ⟨A, hA, ⟨b.contra ?_⟩⟩
158+
intro x hx
159+
simp at hx ⊢
160+
grind
161+
| _, shift (Γ := Γ) d => by
162+
rcases toProof d with ⟨A, hA, ⟨b⟩⟩
163+
refine ⟨A, hA, ⟨?_⟩⟩
164+
exact b.shift.contra (by
165+
intro x hx
166+
suffices (∃ a ∈ Γ, Rewriting.shift a = x) ∨ ∼x ∈ Sequent.embed A by
167+
simpa [Rewriting.shifts] using this
168+
have hx' : (∃ a ∈ Γ, Rewriting.shift a = x) ∨
169+
∃ a ∈ Sequent.embed A, Rewriting.shift a = ∼x := by
170+
simpa [Rewriting.shifts] using hx
171+
rcases hx' with hx | ⟨a, ha, hax⟩
172+
· exact Or.inl hx
173+
· right
174+
rw [Sequent.embed] at ha
175+
rcases List.mem_map.mp ha with ⟨θ, hθ, rfl⟩
176+
rw [←hax]
177+
rw [Sequent.embed]
178+
exact List.mem_map.mpr ⟨θ, hθ, by simp⟩)
179+
| Γ, cut (φ := φ) d dn => by
180+
rcases toProof d with ⟨A, hA, ⟨b⟩⟩
181+
rcases toProof dn with ⟨B, hB, ⟨bn⟩⟩
182+
refine ⟨A ++ B, mem_theory_append hA hB, ⟨?_⟩⟩
183+
have b' : ⊢ᴸᴷ¹ φ :: Γ.toList ++ ∼Sequent.embed (A ++ B) :=
184+
b.contra (by intro x hx; simp at hx ⊢; grind)
185+
have bn' : ⊢ᴸᴷ¹ ∼φ :: Γ.toList ++ ∼Sequent.embed (A ++ B) :=
186+
bn.contra (by intro x hx; simp at hx ⊢; grind)
187+
exact (Derivation.cut
188+
b' bn').contra (by intro x hx; simp at hx ⊢; grind)
189+
190+
end Derivation2
191+
192+
set_option linter.flexible false in
193+
lemma provable_iff_derivable2 {φ : Sentence L} : T ⊢ φ ↔ T ⊢!₂! (φ : Proposition L) := by
194+
constructor
195+
· rintro ⟨A, hA, d⟩
196+
exact Derivation2.cutMany A hA ⟨Derivation2.cast (Derivation.toDerivation2 T d) (by ext x; simp [Sequent.embed])⟩
197+
· rintro ⟨d⟩
198+
rcases d.toProof with ⟨A, hA, ⟨b⟩⟩
199+
exact ⟨A, hA, b.contra (by
200+
intro x hx
201+
simp at hx ⊢
202+
rcases hx with rfl | hx
203+
· exact Or.inl rfl
204+
· right
205+
rw [Sequent.embed] at hx
206+
exact List.mem_map.mp hx)⟩
207+
208+
end derivation2
209+
210+
end LO.FirstOrder

0 commit comments

Comments
 (0)