internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Completeness.Model.val
Proof state before:
case func
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 Γ)
n : ℕ
e : Fin n → SyntacticTerm L
ε : ℕ → Model T Γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ℕ n
a_ih✝ : ∀ (a : Fin arity✝), Semiterm.val (structure T Γ) e ε (a✝ a) = (Rew.bind e ε) (a✝ a)
⊢ (Structure.func a✝¹ fun i => (Rew.bind e ε) (a✝ i)) = Semiterm.func a✝¹ fun i => (Rew.bind e ε) (a✝ i)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
h : ⊤ ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) ⊤
Tactic:
by_contra
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 Γ)
h : ⊤ ∈ ⛓️
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) ⊤
⊢ False
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
h : ⊤ ∈ ⛓️
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) ⊤
⊢ False
Tactic:
exact chainSet_verum nwf h
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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✝ : ⊥ ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
rcases chainSet_axL nwf r v with (hr | hr)
Proof state after:
case inl
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : rel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)

case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inl
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : rel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)

case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
{ contradiction }
Proof state after:
case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
{ simpa[eval_rel] using hr }
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inl
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : rel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
simpa[eval_rel] using hr
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : nrel r v ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (nrel r v)
Tactic:
simpa[eval_nrel] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋏ q)
Tactic:
simp
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
⊢ (Evalf (Model.structure T Γ) Semiterm.fvar) p → ¬(Evalf (Model.structure T Γ) Semiterm.fvar) q
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
⊢ (Evalf (Model.structure T Γ) Semiterm.fvar) p → ¬(Evalf (Model.structure T Γ) Semiterm.fvar) q
Tactic:
intro _ _
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False
Tactic:
have : p ∈ ⛓️ ∨ q ∈ ⛓️ := chainSet_and nwf 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
this : p ∈ ⛓️ ∨ q ∈ ⛓️
⊢ False
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
this : p ∈ ⛓️ ∨ q ∈ ⛓️
⊢ False
Tactic:
rcases this with (h | h)
Proof state after:
case inl
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
⊢ False

case inr
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
⊢ False
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inl
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
⊢ False
Tactic:
have : ¬Evalf (Model.structure T Γ) Semiterm.fvar p := semanticMainLemma_val p h
Proof state after:
case inl
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
this : ¬(Evalf (Model.structure T Γ) Semiterm.fvar) p
⊢ False
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inl
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
this : ¬(Evalf (Model.structure T Γ) Semiterm.fvar) p
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inr
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
⊢ False
Tactic:
have : ¬Evalf (Model.structure T Γ) Semiterm.fvar q := semanticMainLemma_val q h
Proof state after:
case inr
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
this : ¬(Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inr
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
this : ¬(Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋎ q)
Tactic:
have hpq : p ∈ ⛓️ ∧ q ∈ ⛓️ := chainSet_or nwf 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 Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋎ q)
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋎ q)
Tactic:
simp only [LogicalConnective.HomClass.map_or, LogicalConnective.Prop.or_eq]
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 Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬((Evalf (Model.structure T Γ) Semiterm.fvar) p ∨ (Evalf (Model.structure T Γ) Semiterm.fvar) q)
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬((Evalf (Model.structure T Γ) Semiterm.fvar) p ∨ (Evalf (Model.structure T Γ) Semiterm.fvar) q)
Tactic:
rintro (h | h)
Proof state after:
case inl
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
h : (Evalf (Model.structure T Γ) Semiterm.fvar) p
⊢ False

case inr
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
h : (Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inl
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
h : (Evalf (Model.structure T Γ) Semiterm.fvar) p
⊢ False
Tactic:
exact semanticMainLemma_val p hpq.1 h
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
case inr
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 Γ)
p q : SyntacticFormula L
h✝ : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
h : (Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False
Tactic:
exact semanticMainLemma_val q hpq.2 h
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Tactic:
have : ∃ u, [→ u].hom p ∈ ⛓️ := chainSet_all nwf 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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
this : ∃ u, [→ u].hom p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
this : ∃ u, [→ u].hom p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Tactic:
rcases this with ⟨u, hu⟩
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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Tactic:
have : ¬Eval (Model.structure T Γ) ![u] Semiterm.fvar p := by
  simpa[eval_substs, Matrix.constant_eq_singleton] using semanticMainLemma_val ([→ u].hom p) hu
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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Tactic:
simp
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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ∃ x, ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ∃ x, ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p
Tactic:
exact ⟨u, this⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
simpa[eval_substs, Matrix.constant_eq_singleton] using semanticMainLemma_val ([→ u].hom p) hu
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∃' p)
Tactic:
simp
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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
⊢ ∀ (x : Model T Γ), ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p