internlm/Lean-Github huggingface dataset:
Theorem: keepFreshH
Proof state before:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : F = [] ∧ δ = []
⊢ x ∉ vocabOfProgram y
Tactic:
exfalso
Proof state after:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : F = [] ∧ δ = []
⊢ False
Theorem: keepFreshH
Proof state before:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : F = [] ∧ δ = []
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
hyp : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram y
Tactic:
rcases hyp with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in_Hα, def_l⟩⟩, Fδ_in_l⟩⟩
Proof state after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] else [(F', δ' ++ [∗α])]) = l
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] else [(F', δ' ++ [∗α])]) = l
⊢ x ∉ vocabOfProgram y
Tactic:
subst def_l
Proof state after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
⊢ x ∉ vocabOfProgram y
Tactic:
have IHα := keepFreshH α x_notin F' δ' Fδ'_in_Hα
Proof state after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Tactic:
cases em (δ' = [])
Proof state after:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : δ' = []
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [∗α]
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [∗α]
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
cases Fδ_in_l
Proof state after:
case intro.intro.intro.intro.intro.inr.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
left✝ : F = F'
right✝ : δ = δ' ++ [∗α]
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
left✝ : F = F'
right✝ : δ = δ' ++ [∗α]
⊢ x ∉ vocabOfProgram y
Tactic:
subst_eqs
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram y
Tactic:
cases y_in
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y = (∗α)
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y
Tactic:
have := keepFreshH α x_notin F δ' Fδ'_in_Hα
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
this : x ∉ voc F ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
this : x ∉ voc F ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y = (∗α)
⊢ x ∉ vocabOfProgram y
Tactic:
subst_eqs
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
δ' : List Program
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram (∗α)
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
δ' : List Program
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram (∗α)
Tactic:
simp [vocabOfProgram]
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
δ' : List Program
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram α
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
δ' : List Program
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram α
Tactic:
exact x_notin
Proof state after:
no goals
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
⊢ (~⌈∗β⌉ψ)⊨ρ
Tactic:
intro W M
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ
Tactic:
have claim : ∀ u v, (M,v) ⊨ ρ → relate M β u v → (M,u) ⊨ ρ := by
  intro u v v_rho u_β_v
  have u_ : (M,u) ⊨ (~⌈β⌉~ρ) := by
    simp [modelCanSemImplyForm] at *
    use v
  have u_2 : (M, u) ⊨ (ρ ⋀ repl_in_F x ρ σ0) ⋁ (repl_in_F x ρ σ1) := by
    have repl_equiv := repl_in_F_equiv x ρ beta_equiv
    simp only [repl_in_F, beq_self_eq_true, reduceIte, Formula.or] at repl_equiv
    have nox : repl_in_P x ρ β = β := repl_in_P_non_occ_eq x_notin_beta
    rw [nox] at repl_equiv
    rw [equiv_iff _ _ repl_equiv] at u_
    simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
    tauto
  simp only [modelCanSemImplyForm, Formula.or, evaluatePoint, evaluate] at u_2
  rw [← @or_iff_not_and_not] at u_2
  specialize repl_imp_rho W M u
  aesop
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ
Tactic:
intro w hyp
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w : W
hyp : ∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ
⊢ ∀ ψ ∈ [ρ], evaluate M w ψ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w : W
hyp : ∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ
⊢ ∀ ψ ∈ [ρ], evaluate M w ψ
Tactic:
simp only [Formula.or, List.mem_singleton, forall_eq, evaluate, relate, not_forall, exists_prop] at *
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w : W
hyp : ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
⊢ evaluate M w ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w : W
hyp : ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
⊢ evaluate M w ρ
Tactic:
rcases hyp with ⟨v, w_bS_v, v_Psi⟩
Proof state after:
case intro.intro
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
v_Psi : ¬evaluate M v ψ
⊢ evaluate M w ρ
Theorem: guardToStarDiamond
Proof state before:
case intro.intro
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
v_Psi : ¬evaluate M v ψ
⊢ evaluate M w ρ
Tactic:
induction w_bS_v using Relation.ReflTransGen.head_induction_on
Proof state after:
case intro.intro.refl
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
⊢ evaluate M v ρ

case intro.intro.head
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
a✝¹ c✝ : W
h'✝ : relate M β a✝¹ c✝
h✝ : Relation.ReflTransGen (relate M β) c✝ v
a✝ : evaluate M c✝ ρ
⊢ evaluate M a✝¹ ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
⊢ evaluate M v ρ
Tactic:
case refl =>
  specialize notPsi_imp_rho W M v
  simp_all
Proof state after:
no goals
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
⊢ evaluate M u1 ρ
Tactic:
case head u1 u2 u1_b_u2 _ IH =>
  specialize claim u1 u2
  specialize notPsi_imp_rho W M u1
  simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
  simp_all
Proof state after:
no goals
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
⊢ ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
Tactic:
intro u v v_rho u_β_v
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
⊢ (M, u)⊨ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
⊢ (M, u)⊨ρ
Tactic:
have u_ : (M,u) ⊨ (~⌈β⌉~ρ) := by
  simp [modelCanSemImplyForm] at *
  use v
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
⊢ (M, u)⊨ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
⊢ (M, u)⊨ρ
Tactic:
have u_2 : (M, u) ⊨ (ρ ⋀ repl_in_F x ρ σ0) ⋁ (repl_in_F x ρ σ1) := by
  have repl_equiv := repl_in_F_equiv x ρ beta_equiv
  simp only [repl_in_F, beq_self_eq_true, reduceIte, Formula.or] at repl_equiv
  have nox : repl_in_P x ρ β = β := repl_in_P_non_occ_eq x_notin_beta
  rw [nox] at repl_equiv
  rw [equiv_iff _ _ repl_equiv] at u_
  simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
  tauto
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
⊢ (M, u)⊨ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
⊢ (M, u)⊨ρ
Tactic:
simp only [modelCanSemImplyForm, Formula.or, evaluatePoint, evaluate] at u_2
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : ¬(¬(evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0)) ∧ ¬evaluate M u (repl_in_F x ρ σ1))
⊢ (M, u)⊨ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : ¬(¬(evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0)) ∧ ¬evaluate M u (repl_in_F x ρ σ1))
⊢ (M, u)⊨ρ
Tactic:
rw [← @or_iff_not_and_not] at u_2
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0) ∨ evaluate M u (repl_in_F x ρ σ1)
⊢ (M, u)⊨ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0) ∨ evaluate M u (repl_in_F x ρ σ1)
⊢ (M, u)⊨ρ
Tactic:
specialize repl_imp_rho W M u
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0) ∨ evaluate M u (repl_in_F x ρ σ1)
repl_imp_rho : (∀ φ ∈ [repl_in_F x ρ σ1], evaluate M u φ) → ∀ ψ ∈ [ρ], evaluate M u ψ
⊢ (M, u)⊨ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0) ∨ evaluate M u (repl_in_F x ρ σ1)
repl_imp_rho : (∀ φ ∈ [repl_in_F x ρ σ1], evaluate M u φ) → ∀ ψ ∈ [ρ], evaluate M u ψ
⊢ (M, u)⊨ρ
Tactic:
aesop
Proof state after:
no goals
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
⊢ (M, u)⊨(~⌈β⌉~ρ)
Tactic:
simp [modelCanSemImplyForm] at *
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
⊢ ∃ x, relate M β u x ∧ evaluate M x ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
⊢ ∃ x, relate M β u x ∧ evaluate M x ρ
Tactic:
use v
Proof state after:
no goals