internlm/Lean-Github huggingface dataset:
Theorem: ftr.toNth
Proof state before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
k : ℕ
IH :
  ∀ m_1 < k, ∀ {x : α} {x_1 : m_1 = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
x : α
k_is : k = m x
y z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ [z] ⊆ f x
Tactic:
simp
Proof state after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
k : ℕ
IH :
  ∀ m_1 < k, ∀ {x : α} {x_1 : m_1 = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
x : α
k_is : k = m x
y z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ z ∈ f x
Theorem: ftr.toNth
Proof state before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
k : ℕ
IH :
  ∀ m_1 < k, ∀ {x : α} {x_1 : m_1 = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
x : α
k_is : k = m x
y z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ z ∈ f x
Tactic:
assumption
Proof state after:
no goals
Theorem: ftr.iff_Nth
Proof state before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ y ∈ ftr f m isDec x ↔ ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
constructor
Proof state after:
case mp
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]

case mpr
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ (∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]) → y ∈ ftr f m isDec x
Theorem: ftr.iff_Nth
Proof state before:
case mp
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
Tactic:
apply ftr.toNth (m x)
Proof state after:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ m x = m x
Theorem: ftr.iff_Nth
Proof state before:
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ m x = m x
Tactic:
rfl
Proof state after:
no goals
Theorem: ftr.iff_Nth
Proof state before:
case mpr
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
⊢ (∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]) → y ∈ ftr f m isDec x
Tactic:
rintro ⟨i,claim⟩
Proof state after:
case mpr.intro
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
i : ℕ
claim : y ∈ (fun X => (List.map f X).join)^[i] [x]
⊢ y ∈ ftr f m isDec x
Theorem: ftr.iff_Nth
Proof state before:
case mpr.intro
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
x y : α
i : ℕ
claim : y ∈ (fun X => (List.map f X).join)^[i] [x]
⊢ y ∈ ftr f m isDec x
Tactic:
apply ftr.fromNth claim
Proof state after:
no goals
Theorem: ftr.Trans
Proof state before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : s ∈ ftr f m isDec t
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ s ∈ ftr f m isDec u
Tactic:
rw [ftr.iff_Nth]
Proof state after:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : s ∈ ftr f m isDec t
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Theorem: ftr.Trans
Proof state before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : s ∈ ftr f m isDec t
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
rw [ftr.iff_Nth] at s_in_ftr_t
Proof state after:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Theorem: ftr.Trans
Proof state before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
rw [ftr.iff_Nth] at t_in_ftr_u
Proof state after:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : ∃ i, t ∈ (fun X => (List.map f X).join)^[i] [u]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Theorem: ftr.Trans
Proof state before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : ∃ i, t ∈ (fun X => (List.map f X).join)^[i] [u]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
rcases s_in_ftr_t with ⟨i, s_in⟩
Proof state after:
case intro
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
t_in_ftr_u : ∃ i, t ∈ (fun X => (List.map f X).join)^[i] [u]
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Theorem: ftr.Trans
Proof state before:
case intro
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
t_in_ftr_u : ∃ i, t ∈ (fun X => (List.map f X).join)^[i] [u]
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
rcases t_in_ftr_u with ⟨j, t_in⟩
Proof state after:
case intro.intro
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Theorem: ftr.Trans
Proof state before:
case intro.intro
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
use i + j
Proof state after:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i + j] [u]
Theorem: ftr.Trans
Proof state before:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i + j] [u]
Tactic:
rw [Function.iterate_add]
Proof state after:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ ((fun X => (List.map f X).join)^[i] ∘ (fun X => (List.map f X).join)^[j]) [u]
Theorem: ftr.Trans
Proof state before:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ ((fun X => (List.map f X).join)^[i] ∘ (fun X => (List.map f X).join)^[j]) [u]
Tactic:
simp at *
Proof state after:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i] ((fun X => (List.map f X).join)^[j] [u])
Theorem: ftr.Trans
Proof state before:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i] ((fun X => (List.map f X).join)^[j] [u])
Tactic:
apply biUnion_subset f i [t] ((fun X => (X.map f).join)^[j] [u]) (by simp; aesop)
Proof state after:
case h.a
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i] [t]
Theorem: ftr.Trans
Proof state before:
case h.a
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i] [t]
Tactic:
assumption
Proof state after:
no goals
Theorem: ftr.Trans
Proof state before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ [t] ⊆ (fun X => (List.map f X).join)^[j] [u]
Tactic:
simp
Proof state after:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ t ∈ (fun X => (List.map f X).join)^[j] [u]
Theorem: ftr.Trans
Proof state before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ t ∈ (fun X => (List.map f X).join)^[j] [u]
Tactic:
aesop
Proof state after:
no goals
Theorem: interpolation
Proof state before:
⊢ ∀ (φ ψ : Formula), φ⊨ψ → ∃ θ, Interpolant φ ψ θ
Tactic:
intro φ ψ hyp
Proof state after:
φ ψ : Formula
hyp : φ⊨ψ
⊢ ∃ θ, Interpolant φ ψ θ
Theorem: interpolation
Proof state before:
φ ψ : Formula
hyp : φ⊨ψ
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
let X : TNode := ([φ], [~(ψ)], none)
Proof state after:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
⊢ ∃ θ, Interpolant φ ψ θ
Theorem: interpolation
Proof state before:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
have ctX : ClosedTableau ([],[]) X :=
  by
  rw [tautImp_iff_TNodeUnsat rfl] at hyp
  rw [← completeness] at hyp simp [consistent,inconsistent] at hyp
  exact Classical.choice hyp
Proof state after:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
⊢ ∃ θ, Interpolant φ ψ θ
Theorem: interpolation
Proof state before:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
have partInt := tabToInt ctX
Proof state after:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
partInt : PartInterpolant X
⊢ ∃ θ, Interpolant φ ψ θ
Theorem: interpolation
Proof state before:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
partInt : PartInterpolant X
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
rcases partInt with ⟨θ, pI_prop⟩
Proof state after:
case mk
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : isPartInterpolant X θ
⊢ ∃ θ, Interpolant φ ψ θ
Theorem: interpolation
Proof state before:
case mk
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : isPartInterpolant X θ
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
unfold isPartInterpolant at pI_prop
Proof state after:
case mk
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ ∃ θ, Interpolant φ ψ θ
Theorem: interpolation
Proof state before:
case mk
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
use θ
Proof state after:
case h
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ Interpolant φ ψ θ
Theorem: interpolation
Proof state before:
case h
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ Interpolant φ ψ θ
Tactic:
constructor
Proof state after:
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ voc θ ⊆ voc φ ∩ voc ψ

case h.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ φ⊨θ ∧ θ⊨ψ
Theorem: interpolation
Proof state before:
case h.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ φ⊨θ ∧ θ⊨ψ
Tactic:
constructor
Proof state after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ φ⊨θ

case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ
Theorem: interpolation
Proof state before:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
Tactic:
rw [tautImp_iff_TNodeUnsat rfl] at hyp
Proof state after:
φ ψ : Formula
hyp : ¬satisfiable ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
Theorem: interpolation
Proof state before:
φ ψ : Formula
hyp : ¬satisfiable ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
Tactic:
rw [← completeness] at hyp
Proof state after:
φ ψ : Formula
hyp : ¬consistent ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
Theorem: interpolation
Proof state before:
φ ψ : Formula
hyp : ¬consistent ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
Tactic:
simp [consistent,inconsistent] at hyp
Proof state after:
φ ψ : Formula
X : TNode := ([φ], [~ψ], none)
hyp : Nonempty (ClosedTableau LoadHistory.nil ([φ], [~ψ], none))
⊢ ClosedTableau ([], []) X
Theorem: interpolation
Proof state before:
φ ψ : Formula
X : TNode := ([φ], [~ψ], none)
hyp : Nonempty (ClosedTableau LoadHistory.nil ([φ], [~ψ], none))
⊢ ClosedTableau ([], []) X
Tactic:
exact Classical.choice hyp
Proof state after:
no goals
Theorem: interpolation
Proof state before:
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ voc θ ⊆ voc φ ∩ voc ψ
Tactic:
intro f f_in
Proof state after:
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
f : ℕ
f_in : f ∈ voc θ
⊢ f ∈ voc φ ∩ voc ψ
Theorem: interpolation
Proof state before:
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
f : ℕ
f_in : f ∈ voc θ
⊢ f ∈ voc φ ∩ voc ψ
Tactic:
simp [voc,jvoc,vocabOfListFormula,vocabOfFormula] at pI_prop
Proof state after:
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
f : ℕ
f_in : f ∈ voc θ
pI_prop :
  vocabOfFormula θ ⊆ vocabOfFormula φ ∩ vocabOfFormula ψ ∧
    (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ¬evaluate x_1 x_2 θ → ¬evaluate x_1 x_2 φ) ∧
      ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
⊢ f ∈ voc φ ∩ voc ψ
Theorem: interpolation
Proof state before:
case h.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
f : ℕ
f_in : f ∈ voc θ
pI_prop :
  vocabOfFormula θ ⊆ vocabOfFormula φ ∩ vocabOfFormula ψ ∧
    (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ¬evaluate x_1 x_2 θ → ¬evaluate x_1 x_2 φ) ∧
      ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
⊢ f ∈ voc φ ∩ voc ψ
Tactic:
exact pI_prop.1 f_in
Proof state after:
no goals
Theorem: interpolation
Proof state before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ φ⊨θ
Tactic:
have := pI_prop.2.1
Proof state after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
this : ¬satisfiable ((~θ) :: X.left)
⊢ φ⊨θ
Theorem: interpolation
Proof state before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
this : ¬satisfiable ((~θ) :: X.left)
⊢ φ⊨θ
Tactic:
clear pI_prop
Proof state after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable ((~θ) :: X.left)
⊢ φ⊨θ
Theorem: interpolation
Proof state before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable ((~θ) :: X.left)
⊢ φ⊨θ
Tactic:
rw [tautImp_iff_comboNotUnsat]
Proof state after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable ((~θ) :: X.left)
⊢ ¬satisfiable [φ, ~θ]
Theorem: interpolation
Proof state before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable ((~θ) :: X.left)
⊢ ¬satisfiable [φ, ~θ]
Tactic:
simp [satisfiable] at *
Proof state after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ¬evaluate x_1 x_2 θ → ¬evaluate x_1 x_2 φ
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 φ → evaluate x_1 x_2 θ
Theorem: interpolation
Proof state before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ¬evaluate x_1 x_2 θ → ¬evaluate x_1 x_2 φ
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 φ → evaluate x_1 x_2 θ
Tactic:
intro W M w
Proof state after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ¬evaluate x_1 x_2 θ → ¬evaluate x_1 x_2 φ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w φ → evaluate M w θ
Theorem: interpolation
Proof state before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ¬evaluate x_1 x_2 θ → ¬evaluate x_1 x_2 φ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w φ → evaluate M w θ
Tactic:
specialize this W M w
Proof state after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
W : Type
M : KripkeModel W
w : W
this : ¬evaluate M w θ → ¬evaluate M w φ
⊢ evaluate M w φ → evaluate M w θ
Theorem: interpolation
Proof state before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
W : Type
M : KripkeModel W
w : W
this : ¬evaluate M w θ → ¬evaluate M w φ
⊢ evaluate M w φ → evaluate M w θ
Tactic:
tauto
Proof state after:
no goals
Theorem: interpolation
Proof state before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ
Tactic:
have := pI_prop.2.2
Proof state after:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
this : ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ
Theorem: interpolation
Proof state before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : voc θ ⊆ jvoc X ∧ ¬satisfiable ((~θ) :: X.left) ∧ ¬satisfiable (θ :: X.right)
this : ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ
Tactic:
clear pI_prop
Proof state after:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ
Theorem: interpolation
Proof state before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ
Tactic:
rw [tautImp_iff_comboNotUnsat]
Proof state after:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ ¬satisfiable [θ, ~ψ]
Theorem: interpolation
Proof state before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ ¬satisfiable [θ, ~ψ]
Tactic:
simp [satisfiable] at *
Proof state after:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
Theorem: interpolation
Proof state before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
Tactic:
intro W M w
Proof state after:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w θ → evaluate M w ψ
Theorem: interpolation
Proof state before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w θ → evaluate M w ψ
Tactic:
specialize this W M w
Proof state after:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
W : Type
M : KripkeModel W
w : W
this : evaluate M w θ → evaluate M w ψ
⊢ evaluate M w θ → evaluate M w ψ
Theorem: interpolation
Proof state before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
W : Type
M : KripkeModel W
w : W
this : evaluate M w θ → evaluate M w ψ
⊢ evaluate M w θ → evaluate M w ψ
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_Con
Proof state before:
x : ℕ
ψ : Formula
l : List Formula
⊢ repl_in_F x ψ (Con l) = Con (List.map (repl_in_F x ψ) l)
Tactic:
cases l
Proof state after:
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (Con []) = Con (List.map (repl_in_F x ψ) [])

case cons
x : ℕ
ψ head✝ : Formula
tail✝ : List Formula
⊢ repl_in_F x ψ (Con (head✝ :: tail✝)) = Con (List.map (repl_in_F x ψ) (head✝ :: tail✝))
Theorem: repl_in_Con
Proof state before:
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (Con []) = Con (List.map (repl_in_F x ψ) [])
Tactic:
simp
Proof state after:
no goals