internlm/Lean-Github huggingface dataset:
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_2.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Gs
⊢ evaluate M v f
Tactic:
apply v_Gs f
Proof state after:
case intro.intro.intro.intro.refine_2.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Gs
⊢ f ∈ Gs
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_2.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Gs
⊢ f ∈ Gs
Tactic:
assumption
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
refine ⟨⟨Fs, δ ++ [β]⟩, ⟨?_, ?_, ?_⟩⟩
Proof state after:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈ H (α;'β)

case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ (M, v)⊨(Fs, δ ++ [β]).1

case refine_3
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ relateSeq M (Fs, δ ++ [β]).2 v w
Theorem: existsDiamondH
Proof state before:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈ H (α;'β)
Tactic:
simp_all [H]
Proof state after:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs, δ ++ [β]) ∈ l
Theorem: existsDiamondH
Proof state before:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs, δ ++ [β]) ∈ l
Tactic:
refine ⟨_, ⟨⟨Fs, δ, ⟨ Fδ_in , by rfl⟩⟩, ?_⟩⟩
Proof state after:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ (Fs, δ ++ [β]) ∈ if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]
Theorem: existsDiamondH
Proof state before:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ (Fs, δ ++ [β]) ∈ if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]
Tactic:
simp_all
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ (if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]) = ?m.1382731
Tactic:
rfl
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ (M, v)⊨(Fs, δ ++ [β]).1
Tactic:
intro f f_in
Proof state after:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ (Fs, δ ++ [β]).1
⊢ evaluate M v f
Theorem: existsDiamondH
Proof state before:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ (Fs, δ ++ [β]).1
⊢ evaluate M v f
Tactic:
simp at f_in
Proof state after:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ Fs
⊢ evaluate M v f
Theorem: existsDiamondH
Proof state before:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ Fs
⊢ evaluate M v f
Tactic:
specialize u_Fs f f_in
Proof state after:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ Fs
u_Fs : evaluate M v f
⊢ evaluate M v f
Theorem: existsDiamondH
Proof state before:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ Fs
u_Fs : evaluate M v f
⊢ evaluate M v f
Tactic:
assumption
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
case refine_3
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ relateSeq M (Fs, δ ++ [β]).2 v w
Tactic:
simp [relateSeq_append]
Proof state after:
case refine_3
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ ∃ u, relateSeq M δ v u ∧ relate M β u w
Theorem: existsDiamondH
Proof state before:
case refine_3
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ ∃ u, relateSeq M δ v u ∧ relate M β u w
Tactic:
use u
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : relate M (∗β) v w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp only [relate] at v_γ_w
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
have := ReflTransGen.cases_tail_eq_neq v_γ_w
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
this : v = w ∨ v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
this : v = w ∨ v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
cases this
Proof state after:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v = w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v = w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
subst_eqs
Proof state after:
case inl.refl
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v v
Theorem: existsDiamondH
Proof state before:
case inl.refl
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v v
Tactic:
use ⟨∅, ε⟩
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ (∅, ε) ∈ H (∗β) ∧ (M, v)⊨(∅, ε).1 ∧ relateSeq M (∅, ε).2 v v
Theorem: existsDiamondH
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ (∅, ε) ∈ H (∗β) ∧ (M, v)⊨(∅, ε).1 ∧ relateSeq M (∅, ε).2 v v
Tactic:
simp [H, relateSeq]
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
hyp : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases hyp with ⟨_, ⟨v1, v_neq_v1, v_β_v1, v1_βS_w⟩⟩
Proof state after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
have IHβ := existsDiamondH v_β_v1
Proof state after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v v1
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v v1
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases IHβ with ⟨⟨Fs,δ⟩, Fδ_in, v_Fs, v_δ_v1⟩
Proof state after:
case intro.intro.intro.intro.intro.mk.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.intro.mk.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
use ⟨Fs, δ ++ [∗β]⟩
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (Fs, δ ++ [∗β]) ∈ H (∗β) ∧ (M, v)⊨(Fs, δ ++ [∗β]).1 ∧ relateSeq M (Fs, δ ++ [∗β]).2 v w
Theorem: existsDiamondH
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (Fs, δ ++ [∗β]) ∈ H (∗β) ∧ (M, v)⊨(Fs, δ ++ [∗β]).1 ∧ relateSeq M (Fs, δ ++ [∗β]).2 v w
Tactic:
constructor
Proof state after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (Fs, δ ++ [∗β]) ∈ H (∗β)

case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (M, v)⊨(Fs, δ ++ [∗β]).1 ∧ relateSeq M (Fs, δ ++ [∗β]).2 v w
Theorem: existsDiamondH
Proof state before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (Fs, δ ++ [∗β]) ∈ H (∗β)
Tactic:
simp [H] at *
Proof state after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l
Theorem: existsDiamondH
Proof state before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l
Tactic:
have claim : δ ≠ ε := by
  by_contra hyp
  subst_eqs
  simp [relateSeq] at v_δ_v1
  tauto
Proof state after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l
Theorem: existsDiamondH
Proof state before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l
Tactic:
refine ⟨_, ⟨⟨Fs, δ, ⟨Fδ_in, by rfl⟩⟩, ?_⟩⟩
Proof state after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ (Fs, δ ++ [∗β]) ∈ if δ = [] then [] else [(Fs, δ ++ [∗β])]
Theorem: existsDiamondH
Proof state before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ (Fs, δ ++ [∗β]) ∈ if δ = [] then [] else [(Fs, δ ++ [∗β])]
Tactic:
simp_all
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ δ ≠ ε
Tactic:
by_contra hyp
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
hyp : δ = ε
⊢ False
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
hyp : δ = ε
⊢ False
Tactic:
subst_eqs
Proof state after:
case refl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
v_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H β
v_δ_v1 : relateSeq M ε v v1
⊢ False
Theorem: existsDiamondH
Proof state before:
case refl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
v_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H β
v_δ_v1 : relateSeq M ε v v1
⊢ False
Tactic:
simp [relateSeq] at v_δ_v1
Proof state after:
case refl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
v_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H β
v_δ_v1 : v = v1
⊢ False
Theorem: existsDiamondH
Proof state before:
case refl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
v_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H β
v_δ_v1 : v = v1
⊢ False
Tactic:
tauto
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ (if δ = [] then [] else [(Fs, δ ++ [∗β])]) = ?m.1478336
Tactic:
rfl
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (M, v)⊨(Fs, δ ++ [∗β]).1 ∧ relateSeq M (Fs, δ ++ [∗β]).2 v w
Tactic:
constructor
Proof state after:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (M, v)⊨(Fs, δ ++ [∗β]).1

case h.right.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M (Fs, δ ++ [∗β]).2 v w
Theorem: existsDiamondH
Proof state before:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (M, v)⊨(Fs, δ ++ [∗β]).1
Tactic:
intro f f_in
Proof state after:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
f : Formula
f_in : f ∈ (Fs, δ ++ [∗β]).1
⊢ evaluate M v f