internlm/Lean-Github huggingface dataset:
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M α w v ∧ ¬evaluate M v ψ
this : ∃ x, relate M α w x ∧ ¬evaluate M x ψ
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Tactic:
rw [IHα] at this
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M α w v ∧ ¬evaluate M v ψ
this : ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M α w v ∧ ¬evaluate M v ψ
this : ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Tactic:
rcases this with ⟨f, ⟨⟨a, b, ⟨ab_in, def_f⟩⟩, w_f⟩⟩
Proof state after:
case intro.intro.intro.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M α w v ∧ ¬evaluate M v ψ
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ H α
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case intro.intro.intro.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M α w v ∧ ¬evaluate M v ψ
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ H α
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Tactic:
exact ⟨f, ⟨⟨a, b, ⟨Or.inl ab_in, def_f⟩⟩, w_f⟩⟩
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Tactic:
have : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) := ⟨v, hyp⟩
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
this : ∃ x, relate M β w x ∧ ¬evaluate M x ψ
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
this : ∃ x, relate M β w x ∧ ¬evaluate M x ψ
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Tactic:
rw [IHβ] at this
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
this : ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
this : ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Tactic:
rcases this with ⟨f, ⟨⟨a, b, ⟨ab_in, def_f⟩⟩, w_f⟩⟩
Proof state after:
case intro.intro.intro.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ H β
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case intro.intro.intro.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ H β
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Tactic:
exact ⟨f, ⟨⟨a, b, ⟨Or.inr ab_in, def_f⟩⟩, w_f⟩⟩
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case mpr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ (∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f) →
    ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
rintro ⟨f, ⟨a, b, ⟨(ab_in_Hα|ab_in_Hβ), def_f⟩⟩, w_f⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hα : (a, b) ∈ H α
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ

case mpr.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.intro.intro.intro.intro.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hα : (a, b) ∈ H α
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
have : ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f :=
  ⟨f, ⟨⟨a, b, ⟨ab_in_Hα, def_f⟩⟩, w_f⟩⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hα : (a, b) ∈ H α
this : ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.intro.intro.intro.intro.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hα : (a, b) ∈ H α
this : ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
rw [← IHα] at this
Proof state after:
case mpr.intro.intro.intro.intro.intro.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hα : (a, b) ∈ H α
this : ∃ x, relate M α w x ∧ ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.intro.intro.intro.intro.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hα : (a, b) ∈ H α
this : ∃ x, relate M α w x ∧ ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
rcases this with ⟨x, ⟨w_α_x, x_Psi⟩⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.inl.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hα : (a, b) ∈ H α
x : W
w_α_x : relate M α w x
x_Psi : ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.intro.intro.intro.intro.inl.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hα : (a, b) ∈ H α
x : W
w_α_x : relate M α w x
x_Psi : ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
exact ⟨x, ⟨Or.inl w_α_x, x_Psi⟩⟩
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
have : ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f :=
  ⟨f, ⟨⟨a, b, ⟨ab_in_Hβ, def_f⟩⟩, w_f⟩⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
this : ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
this : ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
rw [← IHβ] at this
Proof state after:
case mpr.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
this : ∃ x, relate M β w x ∧ ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
this : ∃ x, relate M β w x ∧ ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
rcases this with ⟨x, ⟨w_β_x, x_Psi⟩⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.inr.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
x : W
w_β_x : relate M β w x
x_Psi : ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.intro.intro.intro.intro.inr.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
x : W
w_β_x : relate M β w x
x_Psi : ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
Tactic:
exact ⟨x, ⟨Or.inr w_β_x, x_Psi⟩⟩
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Tactic:
have : evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (~⌈α⌉⌈β⌉ψ) := by aesop
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
this : evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (~⌈α⌉⌈β⌉ψ)
⊢ evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
this : evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (~⌈α⌉⌈β⌉ψ)
⊢ evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Tactic:
rw [this]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
this : evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (~⌈α⌉⌈β⌉ψ)
⊢ evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
this : evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (~⌈α⌉⌈β⌉ψ)
⊢ evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Tactic:
clear this
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Tactic:
have IHα := localDiamondTruth α (⌈β⌉ψ) W M w
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α)))
⊢ evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α)))
⊢ evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Tactic:
rw [IHα]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α)))
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α))) ↔
    evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : evaluate M w (~⌈α⌉⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α)))
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α))) ↔
    evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Tactic:
clear IHα
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α))) ↔
    evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α))) ↔
    evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Tactic:
rw [disEval]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α), evaluate M w f) ↔
    evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α), evaluate M w f) ↔
    evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β))))
Tactic:
rw [disEval]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α), evaluate M w f) ↔
    ∃ f ∈ List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β)), evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ (⌈β⌉ψ))) (H α), evaluate M w f) ↔
    ∃ f ∈ List.map (fun Fδ => Con (Yset Fδ ψ)) (H (α;'β)), evaluate M w f
Tactic:
rw [helper, helper]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))) ↔ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))) ↔ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
constructor
Proof state after:
case mp
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))) → ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))

case mpr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))) → ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ evaluate M w (~⌈α;'β⌉ψ) ↔ evaluate M w (~⌈α⌉⌈β⌉ψ)
Tactic:
aesop
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case mp
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))) → ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
rintro ⟨⟨Fs,δ⟩, ⟨Fδ_in, w_Con⟩⟩
Proof state after:
case mp.intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))