internlm/Lean-Github huggingface dataset:
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
γ : Program
v w : W✝
v_γ_w : relate M γ v w
⊢ ∃ Fδ ∈ H γ, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
cases γ
Proof state after:
case atom_prog
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
⊢ ∃ Fδ ∈ H (·a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case sequence
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹;'a✝) v w
⊢ ∃ Fδ ∈ H (a✝¹;'a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case union
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹⋓a✝) v w
⊢ ∃ Fδ ∈ H (a✝¹⋓a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case star
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Program
v_γ_w : relate M (∗a✝) v w
⊢ ∃ Fδ ∈ H (∗a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case test
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Formula
v_γ_w : relate M (?'a✝) v w
⊢ ∃ Fδ ∈ H (?'a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
⊢ ∃ Fδ ∈ H (·a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
case atom_prog =>
  simp [H, relateSeq] at *
  exact v_γ_w
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : relate M (?'τ) v w
⊢ ∃ Fδ ∈ H (?'τ), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
case test τ =>
  simp [H, relateSeq] at *
  aesop
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:
case union α β =>
  simp [H, relateSeq] at *
  cases v_γ_w
  case inl hyp =>
    have IHα := existsDiamondH hyp
    aesop
  case inr hyp =>
    have IHβ := existsDiamondH hyp
    aesop
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
⊢ ∃ Fδ ∈ H (·a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at *
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : M.Rel a✝ v w
⊢ M.Rel a✝ v w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : M.Rel a✝ v w
⊢ M.Rel a✝ v w
Tactic:
exact v_γ_w
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : relate M (?'τ) v w
⊢ ∃ Fδ ∈ H (?'τ), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at *
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : v = w ∧ evaluate M v τ
⊢ evaluate M v τ ∧ v = w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : v = w ∧ evaluate M v τ
⊢ evaluate M v τ ∧ v = w
Tactic:
aesop
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 [H, relateSeq] at *
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M α v w ∨ relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M α v w ∨ relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
cases v_γ_w
Proof state after:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
h✝ : relate M α v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w

case inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
h✝ : relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M α v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
case inl hyp =>
  have IHα := existsDiamondH hyp
  aesop
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
case inr hyp =>
  have IHβ := existsDiamondH hyp
  aesop
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M α v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
have IHα := existsDiamondH hyp
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M α v w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M α v w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
aesop
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
have IHβ := existsDiamondH hyp
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
aesop
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 : ∃ y, relate M α v y ∧ 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 : ∃ y, relate M α v y ∧ relate M β y w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases v_γ_w with ⟨u, v_α_u, u_β_w⟩
Proof state after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
have IHα := existsDiamondH v_α_u
Proof state after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at IHα
Proof state after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ a b, (a, b) ∈ H α ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ a b, (a, b) ∈ H α ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases IHα with ⟨Fs, δ, ⟨Fδ_in, u_Fs, v_δ_u⟩⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
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
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.intro.intro
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
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
cases em (δ = ε)
Proof state after:
case intro.intro.intro.intro.intro.intro.inl
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
h✝ : δ = ε
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case intro.intro.intro.intro.intro.intro.inr
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
h✝ : ¬δ = ε
⊢ ∃ 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
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:
subst hyp
Proof state after:
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
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_δ_u : relateSeq M ε v u
⊢ ∃ 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
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_δ_u : relateSeq M ε v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp only [relateSeq] at v_δ_u
Proof state after:
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
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_δ_u : v = u
⊢ ∃ 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
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_δ_u : v = u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
subst v_δ_u
Proof state after:
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
⊢ ∃ 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
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
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
have IHβ := existsDiamondH u_β_w
Proof state after:
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
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 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
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
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at IHβ
Proof state after:
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
IHβ : ∃ a b, (a, b) ∈ H β ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b 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
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
IHβ : ∃ a b, (a, b) ∈ H β ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases IHβ with ⟨Gs, η, ⟨Gη_in, v_Gs, v_η_w⟩⟩
Proof state after:
case intro.intro.intro.intro
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δ ∈ 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
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δ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
refine ⟨ ⟨Fs ∪ Gs, η⟩, ⟨?_, ?_, v_η_w⟩ ⟩
Proof state after:
case intro.intro.intro.intro.refine_1
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
⊢ (Fs ∪ Gs, η) ∈ H (α;'β)

case intro.intro.intro.intro.refine_2
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
⊢ (M, v)⊨(Fs ∪ Gs, η).1
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_1
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
⊢ (Fs ∪ Gs, η) ∈ H (α;'β)
Tactic:
simp_all [H]
Proof state after:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ 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 ∪ Gs, η) ∈ l
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ 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 ∪ Gs, η) ∈ l
Tactic:
refine ⟨_, ⟨⟨Fs, ε, ⟨Fδ_in, by rfl⟩⟩, ?_⟩⟩
Proof state after:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (Fs ∪ Gs, η) ∈ if ε = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, ε ++ [β])]
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (Fs ∪ Gs, η) ∈ if ε = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, ε ++ [β])]
Tactic:
simp
Proof state after:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = l) ∧ (Fs ∪ Gs, η) ∈ l
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = l) ∧ (Fs ∪ Gs, η) ∈ l
Tactic:
use [(Fs ∪ Gs, η)]
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = [(Fs ∪ Gs, η)]) ∧ (Fs ∪ Gs, η) ∈ [(Fs ∪ Gs, η)]
Theorem: existsDiamondH
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = [(Fs ∪ Gs, η)]) ∧ (Fs ∪ Gs, η) ∈ [(Fs ∪ Gs, η)]
Tactic:
aesop
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (if ε = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, ε ++ [β])]) = ?m.1356173
Tactic:
rfl
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_2
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
⊢ (M, v)⊨(Fs ∪ Gs, η).1
Tactic:
intro f f_in
Proof state after:
case intro.intro.intro.intro.refine_2
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
f_in : f ∈ (Fs ∪ Gs, η).1
⊢ evaluate M v f
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_2
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
f_in : f ∈ (Fs ∪ Gs, η).1
⊢ evaluate M v f
Tactic:
simp at f_in
Proof state after:
case intro.intro.intro.intro.refine_2
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
f_in : f ∈ Fs ∨ f ∈ Gs
⊢ evaluate M v f
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_2
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
f_in : f ∈ Fs ∨ f ∈ Gs
⊢ evaluate M v f
Tactic:
cases f_in
Proof state after:
case intro.intro.intro.intro.refine_2.inl
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 ∈ Fs
⊢ evaluate M v f

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
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_2.inl
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 ∈ Fs
⊢ evaluate M v f
Tactic:
specialize u_Fs f (by assumption)
Proof state after:
case intro.intro.intro.intro.refine_2.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
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 ∈ Fs
u_Fs : evaluate M v f
⊢ evaluate M v f
Theorem: existsDiamondH
Proof state before:
case intro.intro.intro.intro.refine_2.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
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 ∈ Fs
u_Fs : evaluate M v f
⊢ evaluate M v f
Tactic:
assumption
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
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 ∈ Fs
⊢ f ∈ Fs
Tactic:
assumption
Proof state after:
no goals