internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Completeness.ReduxNat.toRedux
Proof state before:
case redux
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
h : decode ((encode c).pair i).unpair.1 = some c✝
r : Δ₂ ≺[c✝] Δ₁
⊢ Δ₂ ≺[c] Δ₁
Tactic:
simp at h
Proof state after:
case redux
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
r : Δ₂ ≺[c✝] Δ₁
h : c = c✝
⊢ Δ₂ ≺[c] Δ₁
Theorem: LO.FirstOrder.Completeness.ReduxNat.toRedux
Proof state before:
case redux
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
r : Δ₂ ≺[c✝] Δ₁
h : c = c✝
⊢ Δ₂ ≺[c] Δ₁
Tactic:
simpa[h] using r
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.ReduxNat.toRedux
Proof state before:
case refl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
c : Code L
i : ℕ
Δ₂ : Sequent L
h : decode ((encode c).pair i).unpair.1 = none
⊢ Δ₂ ≺[c] Δ₂
Tactic:
simp at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.SearchTree.rank_of_lt
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
τ₁ τ₂ : SearchTree T Γ
h : Lt T Γ τ₂ τ₁
⊢ τ₂.rank = τ₁.rank + 1
Tactic:
cases h
Proof state after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ rank ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ = rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩ + 1
Theorem: LO.FirstOrder.Completeness.SearchTree.rank_of_lt
Proof state before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ rank ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ = rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩ + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.SearchTree.seq_of_lt
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
τ₁ τ₂ : SearchTree T Γ
h : Lt T Γ τ₂ τ₁
⊢ τ₂.seq ≺⟨τ₁.rank⟩ τ₁.seq
Tactic:
cases h
Proof state after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ seq ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ ≺⟨rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩⟩ seq ⟨s✝, ⟨Δ₁✝, a✝⟩⟩
Theorem: LO.FirstOrder.Completeness.SearchTree.seq_of_lt
Proof state before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ seq ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ ≺⟨rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩⟩ seq ⟨s✝, ⟨Δ₁✝, a✝⟩⟩
Tactic:
simp[rank, seq]
Proof state after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ Δ₂✝ ≺⟨s✝⟩ Δ₁✝
Theorem: LO.FirstOrder.Completeness.SearchTree.seq_of_lt
Proof state before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ Δ₂✝ ≺⟨s✝⟩ Δ₁✝
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
⊢ ¬Acc (SearchTree.Lt T Γ) ⊤
Tactic:
intro A
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
⊢ False
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
⊢ False
Tactic:
have : WellFounded (SearchTree.Lt T Γ) := ⟨by
  rintro ⟨s, Δ, a⟩
  induction a
  case zero => exact A
  case succ s Δ₁ Δ₂ a r ih => exact ih.inv (SearchTree.Lt.intro a r)⟩
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
this : WellFounded (SearchTree.Lt T Γ)
⊢ False
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
this : WellFounded (SearchTree.Lt T Γ)
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
⊢ ∀ (a : SearchTree T Γ), Acc (SearchTree.Lt T Γ) a
Tactic:
rintro ⟨s, Δ, a⟩
Proof state after:
case mk.mk
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
a : SearchTreeAux T Γ s Δ
⊢ Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ, a⟩⟩
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
case mk.mk
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
a : SearchTreeAux T Γ s Δ
⊢ Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ, a⟩⟩
Tactic:
induction a
Proof state after:
case mk.mk.zero
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
⊢ Acc (SearchTree.Lt T Γ) ⟨0, ⟨Γ, SearchTreeAux.zero⟩⟩

case mk.mk.succ
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
s✝ : ℕ
Δ₁✝ Δ₂✝ : Sequent L
a✝¹ : SearchTreeAux T Γ s✝ Δ₁✝
a✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
a_ih✝ : Acc (SearchTree.Lt T Γ) ⟨s✝, ⟨Δ₁✝, a✝¹⟩⟩
⊢ Acc (SearchTree.Lt T Γ) ⟨s✝ + 1, ⟨Δ₂✝, a✝¹.succ a✝⟩⟩
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
⊢ Acc (SearchTree.Lt T Γ) ⟨0, ⟨Γ, SearchTreeAux.zero⟩⟩
Tactic:
case zero => exact A
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s✝ : ℕ
Δ : Sequent L
s : ℕ
Δ₁ Δ₂ : Sequent L
a : SearchTreeAux T Γ s Δ₁
r : Δ₂ ≺⟨s⟩ Δ₁
ih : Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ₁, a⟩⟩
⊢ Acc (SearchTree.Lt T Γ) ⟨s + 1, ⟨Δ₂, a.succ r⟩⟩
Tactic:
case succ s Δ₁ Δ₂ a r ih => exact ih.inv (SearchTree.Lt.intro a r)
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
⊢ Acc (SearchTree.Lt T Γ) ⟨0, ⟨Γ, SearchTreeAux.zero⟩⟩
Tactic:
exact A
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.top_inaccessible
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s✝ : ℕ
Δ : Sequent L
s : ℕ
Δ₁ Δ₂ : Sequent L
a : SearchTreeAux T Γ s Δ₁
r : Δ₂ ≺⟨s⟩ Δ₁
ih : Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ₁, a⟩⟩
⊢ Acc (SearchTree.Lt T Γ) ⟨s + 1, ⟨Δ₂, a.succ r⟩⟩
Tactic:
exact ih.inv (SearchTree.Lt.intro a r)
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainU_val_fst_eq
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
⊢ (chainU T Γ s).rank = s
Tactic:
induction' s with s ih <;> simp[SearchTree.rank]
Proof state after:
case zero
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
⊢ (chainU T Γ 0).fst = 0

case succ
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
ih : (chainU T Γ s).rank = s
⊢ (chainU T Γ (s + 1)).fst = s + 1
Theorem: LO.FirstOrder.Completeness.chainU_val_fst_eq
Proof state before:
case zero
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
⊢ (chainU T Γ 0).fst = 0
Tactic:
exact rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainU_val_fst_eq
Proof state before:
case succ
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
ih : (chainU T Γ s).rank = s
⊢ (chainU T Γ (s + 1)).fst = s + 1
Tactic:
simpa[ih] using SearchTree.rank_of_lt (chainU_spec nwf s)
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chain_spec
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
⊢ ⛓️[s + 1] ≺⟨s⟩ ⛓️[s]
Tactic:
simpa[chainU_val_fst_eq nwf s] using SearchTree.seq_of_lt (chainU_spec nwf s)
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chain_monotone
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ⛓️[s] ⊆ ⛓️[u]
Tactic:
suffices ∀ d, ⛓️[s] ⊆ ⛓️[s + d] by
  simpa[Nat.add_sub_of_le h] using this (u - s)
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ∀ (d : ℕ), ⛓️[s] ⊆ ⛓️[s + d]
Theorem: LO.FirstOrder.Completeness.chain_monotone
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ∀ (d : ℕ), ⛓️[s] ⊆ ⛓️[s + d]
Tactic:
intro d
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
d : ℕ
⊢ ⛓️[s] ⊆ ⛓️[s + d]
Theorem: LO.FirstOrder.Completeness.chain_monotone
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
d : ℕ
⊢ ⛓️[s] ⊆ ⛓️[s + d]
Tactic:
induction' d with d ih
Proof state after:
case zero
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ⛓️[s] ⊆ ⛓️[s + 0]

case succ
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
d : ℕ
ih : ⛓️[s] ⊆ ⛓️[s + d]
⊢ ⛓️[s] ⊆ ⛓️[s + (d + 1)]
Theorem: LO.FirstOrder.Completeness.chain_monotone
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
this : ∀ (d : ℕ), ⛓️[s] ⊆ ⛓️[s + d]
⊢ ⛓️[s] ⊆ ⛓️[u]
Tactic:
simpa[Nat.add_sub_of_le h] using this (u - s)
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chain_monotone
Proof state before:
case zero
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ⛓️[s] ⊆ ⛓️[s + 0]
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chain_monotone
Proof state before:
case succ
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
d : ℕ
ih : ⛓️[s] ⊆ ⛓️[s + d]
⊢ ⛓️[s] ⊆ ⛓️[s + (d + 1)]
Tactic:
simpa only [Nat.add_succ] using subset_trans ih <| ReduxNat.antimonotone (chain_spec nwf (s + d))
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
⊢ ⊤ ∉ ⛓️
Tactic:
simp[chainSet]
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
⊢ ∀ (x : ℕ), ⊤ ∉ ⛓️[x]
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
⊢ ∀ (x : ℕ), ⊤ ∉ ⛓️[x]
Tactic:
intro s h
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
⊢ False
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
⊢ False
Tactic:
have : ⊤ ∈ ⛓️[(encode (Code.verum : Code L)).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) h
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
⊢ False
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
⊢ False
Tactic:
have : ¬⊤ ∈ ⛓️[(encode (Code.verum : Code L)).pair s] := by
  have : ⛓️[(encode Code.verum).pair s + 1] ≺[Code.verum] ⛓️[(encode Code.verum).pair s] := chain_spec' nwf _ _
  generalize ⛓️[(encode (Code.verum : Code L)).pair s + 1] = Δ' at this
  rcases this; assumption
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
this : ⊤ ∉ ⛓️[(encode Code.verum).pair s]
⊢ False
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
this : ⊤ ∉ ⛓️[(encode Code.verum).pair s]
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Tactic:
have : ⛓️[(encode Code.verum).pair s + 1] ≺[Code.verum] ⛓️[(encode Code.verum).pair s] := chain_spec' nwf _ _
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
this : ⛓️[(encode Code.verum).pair s + 1] ≺[Code.verum] ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
this : ⛓️[(encode Code.verum).pair s + 1] ≺[Code.verum] ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Tactic:
generalize ⛓️[(encode (Code.verum : Code L)).pair s + 1] = Δ' at this
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
Δ' : Sequent L
this : Δ' ≺[Code.verum] ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
Δ' : Sequent L
this : Δ' ≺[Code.verum] ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Tactic:
rcases this
Proof state after:
case verumRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
a✝ : ⊤ ∉ ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Theorem: LO.FirstOrder.Completeness.chainSet_verum
Proof state before:
case verumRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
a✝ : ⊤ ∉ ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Tactic:
assumption
Proof state after:
no goals