internlm/Lean-Github huggingface dataset:
Theorem: completeness
Proof state before:
case mp
X : TNode
X_is_consistent : consistent X
⊢ satisfiable X
Tactic:
rcases X with ⟨L, R, O⟩
Proof state after:
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
⊢ satisfiable (L, R, O)
Theorem: completeness
Proof state before:
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
⊢ satisfiable (L, R, O)
Tactic:
have ⟨WS, M, w, h⟩ := modelExistence X_is_consistent
Proof state after:
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ satisfiable (L, R, O)
Theorem: completeness
Proof state before:
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ satisfiable (L, R, O)
Tactic:
use WS, M.val, w
Proof state after:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ (↑M, w)⊨(L, R, O)
Theorem: completeness
Proof state before:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ (↑M, w)⊨(L, R, O)
Tactic:
simp [modelCanSemImplyTNode, TNode.toFinset] at *
Proof state after:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
⊢ ∀ (f : Formula),
    ((f ∈ L ∨ f ∈ R) ∨
        (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f) →
      evaluate (↑M) w f
Theorem: completeness
Proof state before:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
⊢ ∀ (f : Formula),
    ((f ∈ L ∨ f ∈ R) ∨
        (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f) →
      evaluate (↑M) w f
Tactic:
intro f f_in
Proof state after:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ evaluate (↑M) w f
Theorem: completeness
Proof state before:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ evaluate (↑M) w f
Tactic:
apply truthLemma M w f
Proof state after:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ ↑w
Theorem: completeness
Proof state before:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ ↑w
Tactic:
apply h
Proof state after:
case h.a
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset)
Theorem: completeness
Proof state before:
case h.a
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset)
Tactic:
aesop
Proof state after:
no goals
Theorem: completeness
Proof state before:
case mpr
X : TNode
⊢ satisfiable X → consistent X
Tactic:
exact correctness X
Proof state after:
no goals
Theorem: singletonCompleteness
Proof state before:
⊢ ∀ (φ : Formula), consistent ([φ], [], none) ↔ satisfiable φ
Tactic:
intro φ
Proof state after:
φ : Formula
⊢ consistent ([φ], [], none) ↔ satisfiable φ
Theorem: singletonCompleteness
Proof state before:
φ : Formula
⊢ consistent ([φ], [], none) ↔ satisfiable φ
Tactic:
have := completeness ⟨[φ], [], none⟩
Proof state after:
φ : Formula
this : consistent ([φ], [], none) ↔ satisfiable ([φ], [], none)
⊢ consistent ([φ], [], none) ↔ satisfiable φ
Theorem: singletonCompleteness
Proof state before:
φ : Formula
this : consistent ([φ], [], none) ↔ satisfiable ([φ], [], none)
⊢ consistent ([φ], [], none) ↔ satisfiable φ
Tactic:
simp [this,tNodeHasSat,modelCanSemImplyTNode]
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
induction n
Proof state after:
case zero
W : Type
M : KripkeModel W
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = 0 → evaluate M v (~⌈⌈δ⌉⌉ξ)

case succ
W : Type
M : KripkeModel W
n✝ : ℕ
a✝ : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n✝ → evaluate M v (~⌈⌈δ⌉⌉ξ)
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n✝ + 1 → evaluate M v (~⌈⌈δ⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = 0 → evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
case zero =>
  intro v δ ξ wit def_n
  subst_eqs
  cases wit
  case nil =>
    subst_eqs
    simp [Formula.boxes, evaluate] at *
    assumption
  all_goals
    exfalso
    simp [witness.length] at *
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = 0 → evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
intro v δ ξ wit def_n
Proof state after:
W : Type
M : KripkeModel W
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = 0
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = 0
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
cases wit
Proof state after:
case nil
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = 0
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)

case consAtom
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝¹ : ℕ
v1✝ : W
γs✝ : List Program
v0_a_v1✝ : M.Rel a✝¹ v v1✝
a✝ : witness M v1✝ γs✝ ξ
def_n : (witness.consAtom v0_a_v1✝ a✝).length = 0
⊢ evaluate M v (~⌈⌈(·a✝¹) :: γs✝⌉⌉ξ)

case consEmpty
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
γs✝ : List Program
Fs✝ : List Formula
a✝² : (Fs✝, ε) ∈ H α✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v γs✝ ξ
def_n : (witness.consEmpty Fs✝ a✝² a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = 0
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
case nil =>
  subst_eqs
  simp [Formula.boxes, evaluate] at *
  assumption
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
case consAtom
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝¹ : ℕ
v1✝ : W
γs✝ : List Program
v0_a_v1✝ : M.Rel a✝¹ v v1✝
a✝ : witness M v1✝ γs✝ ξ
def_n : (witness.consAtom v0_a_v1✝ a✝).length = 0
⊢ evaluate M v (~⌈⌈(·a✝¹) :: γs✝⌉⌉ξ)

case consEmpty
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
γs✝ : List Program
Fs✝ : List Formula
a✝² : (Fs✝, ε) ∈ H α✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v γs✝ ξ
def_n : (witness.consEmpty Fs✝ a✝² a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)
Tactic:
all_goals
  exfalso
  simp [witness.length] at *
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = 0
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
subst_eqs
Proof state after:
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
simp [Formula.boxes, evaluate] at *
Proof state after:
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ
Theorem: existsWitnessPath_rtl
Proof state before:
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ
Tactic:
assumption
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)
Tactic:
exfalso
Proof state after:
case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ False
Theorem: existsWitnessPath_rtl
Proof state before:
case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ False
Tactic:
simp [witness.length] at *
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n + 1 → evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
intro v δ ξ wit def_n
Proof state after:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = n + 1
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = n + 1
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
cases wit
Proof state after:
case nil
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)

case consAtom
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝¹ : ℕ
v1✝ : W
γs✝ : List Program
v0_a_v1✝ : M.Rel a✝¹ v v1✝
a✝ : witness M v1✝ γs✝ ξ
def_n : (witness.consAtom v0_a_v1✝ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈(·a✝¹) :: γs✝⌉⌉ξ)

case consEmpty
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
α✝ : Program
γs✝ : List Program
Fs✝ : List Formula
a✝² : (Fs✝, ε) ∈ H α✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v γs✝ ξ
def_n : (witness.consEmpty Fs✝ a✝² a✝¹ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

case consComp
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
case nil =>
  exfalso
  subst_eqs
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : (witness.consAtom v0_a_v1 wit_v1_γs).length = n + 1
⊢ evaluate M v (~⌈⌈(·a) :: γs⌉⌉ξ)
Tactic:
case consAtom a v1 γs v0_a_v1 wit_v1_γs =>
  simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
  refine ⟨v1, v0_a_v1, IH v1 γs ξ wit_v1_γs ?_⟩
  linarith
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
exfalso
Proof state after:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ False
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ False
Tactic:
subst_eqs
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : (witness.consAtom v0_a_v1 wit_v1_γs).length = n + 1
⊢ evaluate M v (~⌈⌈(·a) :: γs⌉⌉ξ)
Tactic:
simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
Proof state after:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : 1 + wit_v1_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ∃ x, M.Rel a v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : 1 + wit_v1_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ∃ x, M.Rel a v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
Tactic:
refine ⟨v1, v0_a_v1, IH v1 γs ξ wit_v1_γs ?_⟩
Proof state after:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : 1 + wit_v1_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ wit_v1_γs.length = n
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : 1 + wit_v1_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ wit_v1_γs.length = n
Tactic:
linarith
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : (witness.consEmpty Fs Fε_in_Hα v_Fs wit_γs).length = n + 1
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
Tactic:
simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
Proof state after:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
Tactic:
use v
Proof state after:
case h
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v ∧ ¬evaluate M v (⌈⌈γs⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
case h
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v ∧ ¬evaluate M v (⌈⌈γs⌉⌉ξ)
Tactic:
constructor
Proof state after:
case h.left
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v

case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v (⌈⌈γs⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
case h.left
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v
Tactic:
sorry
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v (⌈⌈γs⌉⌉ξ)
Tactic:
apply IH v γs ξ wit_γs
Proof state after:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ wit_γs.length = n
Theorem: existsWitnessPath_rtl
Proof state before:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ wit_γs.length = n
Tactic:
linarith
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : (witness.consComp v_a_v1 Fsaηs_in_Hα four wit_v1_ηγs).length = n + 1
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
Tactic:
simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
Proof state after:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)