Theorem: interpolation (Pdl/Interpolation.lean)

State before:
⊢ ∀ (φ ψ : Formula), φ⊨ψ → ∃ θ, Interpolant φ ψ θ
Tactic:
intro φ ψ hyp
State after:
φ ψ : Formula
hyp : φ⊨ψ
⊢ ∃ θ, Interpolant φ ψ θ

State before:
φ ψ : Formula
hyp : φ⊨ψ
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
let X : TNode := ([φ], [~(ψ)], none)
State after:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
⊢ ∃ θ, Interpolant φ ψ θ

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
State after:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
⊢ ∃ θ, Interpolant φ ψ θ

State before:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
have partInt := tabToInt ctX
State after:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
partInt : PartInterpolant X
⊢ ∃ θ, Interpolant φ ψ θ

State before:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
partInt : PartInterpolant X
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
rcases partInt with ⟨θ, pI_prop⟩
State after:
case mk
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : isPartInterpolant X θ
⊢ ∃ θ, Interpolant φ ψ θ

State before:
case mk
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
pI_prop : isPartInterpolant X θ
⊢ ∃ θ, Interpolant φ ψ θ
Tactic:
unfold isPartInterpolant at pI_prop
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 φ ψ θ

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 θ
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 φ ψ θ

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
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)
⊢ φ⊨θ ∧ θ⊨ψ

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
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)
⊢ θ⊨ψ

State before:
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
Tactic:
rw [tautImp_iff_TNodeUnsat rfl] at hyp
State after:
φ ψ : Formula
hyp : ¬satisfiable ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X

State before:
φ ψ : Formula
hyp : ¬satisfiable ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
Tactic:
rw [← completeness] at hyp
State after:
φ ψ : Formula
hyp : ¬consistent ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X

State before:
φ ψ : Formula
hyp : ¬consistent ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
Tactic:
simp [consistent,inconsistent] at hyp
State after:
φ ψ : Formula
X : TNode := ([φ], [~ψ], none)
hyp : Nonempty (ClosedTableau LoadHistory.nil ([φ], [~ψ], none))
⊢ ClosedTableau ([], []) X

State before:
φ ψ : Formula
X : TNode := ([φ], [~ψ], none)
hyp : Nonempty (ClosedTableau LoadHistory.nil ([φ], [~ψ], none))
⊢ ClosedTableau ([], []) X
Tactic:
exact Classical.choice hyp
State after:
no goals

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
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 ψ

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
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 ψ

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
State after:
no goals

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
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)
⊢ φ⊨θ

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
State after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable ((~θ) :: X.left)
⊢ φ⊨θ

State before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable ((~θ) :: X.left)
⊢ φ⊨θ
Tactic:
rw [tautImp_iff_comboNotUnsat]
State after:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable ((~θ) :: X.left)
⊢ ¬satisfiable [φ, ~θ]

State before:
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable ((~θ) :: X.left)
⊢ ¬satisfiable [φ, ~θ]
Tactic:
simp [satisfiable] at *
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 θ

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
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 θ

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
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 θ

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
State after:
no goals

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
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)
⊢ θ⊨ψ

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
State after:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ

State before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ
Tactic:
rw [tautImp_iff_comboNotUnsat]
State after:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ ¬satisfiable [θ, ~ψ]

State before:
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ ¬satisfiable [θ, ~ψ]
Tactic:
simp [satisfiable] at *
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 ψ

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
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 ψ

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
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 ψ

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
State after:
no goals