internlm/Lean-Github huggingface dataset:
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)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
have repl_equiv := repl_in_F_equiv x ρ beta_equiv
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)⊨(~⌈β⌉~ρ)
repl_equiv : repl_in_F x ρ (~⌈β⌉~·x)≡repl_in_F x ρ ((·x)⋀σ0⋁σ1)
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
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)⊨(~⌈β⌉~ρ)
repl_equiv : repl_in_F x ρ (~⌈β⌉~·x)≡repl_in_F x ρ ((·x)⋀σ0⋁σ1)
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
simp only [repl_in_F, beq_self_eq_true, reduceIte, Formula.or] at repl_equiv
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)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈repl_in_P x ρ β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
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)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈repl_in_P x ρ β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
have nox : repl_in_P x ρ β = β := repl_in_P_non_occ_eq x_notin_beta
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)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈repl_in_P x ρ β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
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)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈repl_in_P x ρ β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
rw [nox] at repl_equiv
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)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
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)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
rw [equiv_iff _ _ repl_equiv] at u_
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)⊨(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
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)⊨(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ψ → evaluate M w ρ
u_ : (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)
⊢ (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ψ → evaluate M w ρ
u_ : (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)
⊢ (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)
Tactic:
tauto
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 ψ
⊢ evaluate M v ρ
Tactic:
specialize notPsi_imp_rho W M 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⊨ρ
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 ψ
notPsi_imp_rho : (∀ φ ∈ [~ψ], evaluate M v φ) → ∀ ψ ∈ [ρ], evaluate M v ψ
⊢ evaluate M v ρ
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⊨ρ
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 ψ
notPsi_imp_rho : (∀ φ ∈ [~ψ], evaluate M v φ) → ∀ ψ ∈ [ρ], evaluate M v ψ
⊢ evaluate M v ρ
Tactic:
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:
specialize claim u1 u2
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 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 ρ
claim : (M, u2)⊨ρ → relate M β u1 u2 → (M, u1)⊨ρ
⊢ evaluate M u1 ρ
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 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 ρ
claim : (M, u2)⊨ρ → relate M β u1 u2 → (M, u1)⊨ρ
⊢ evaluate M u1 ρ
Tactic:
specialize notPsi_imp_rho W M u1
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⊨ρ
W : Type
M : KripkeModel W
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 ρ
claim : (M, u2)⊨ρ → relate M β u1 u2 → (M, u1)⊨ρ
notPsi_imp_rho : (∀ φ ∈ [~ψ], evaluate M u1 φ) → ∀ ψ ∈ [ρ], evaluate M u1 ψ
⊢ evaluate M u1 ρ
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⊨ρ
W : Type
M : KripkeModel W
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 ρ
claim : (M, u2)⊨ρ → relate M β u1 u2 → (M, u1)⊨ρ
notPsi_imp_rho : (∀ φ ∈ [~ψ], evaluate M u1 φ) → ∀ ψ ∈ [ρ], evaluate M u1 ψ
⊢ evaluate M u1 ρ
Tactic:
simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
Proof state after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
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 ρ
claim : evaluate M u2 ρ → relate M β u1 u2 → evaluate M u1 ρ
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ¬evaluate M u1 ψ → evaluate M u1 ρ
⊢ evaluate M u1 ρ
Theorem: guardToStarDiamond
Proof state before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
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 ρ
claim : evaluate M u2 ρ → relate M β u1 u2 → evaluate M u1 ρ
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ¬evaluate M u1 ψ → evaluate M u1 ρ
⊢ evaluate M u1 ρ
Tactic:
simp_all
Proof state after:
no goals
Theorem: helper
Proof state before:
W✝ : Type
M : KripkeModel W✝
w : W✝
⊢ ∀ (p : List Formula × List Program → Formula) (X : List (List Formula × List Program)),
    (∃ f ∈ List.map p X, evaluate M w f) ↔ ∃ Fδ ∈ X, evaluate M w (p Fδ)
Tactic:
aesop
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
γ : Program
ψ : Formula
⊢ (~⌈γ⌉ψ)≡dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H γ))
Tactic:
intro W M w
Proof state after:
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~⌈γ⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H γ)))
Theorem: localDiamondTruth
Proof state before:
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~⌈γ⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H γ)))
Tactic:
cases γ
Proof state after:
case atom_prog
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝ : ℕ
⊢ evaluate M w (~⌈·a✝⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (·a✝))))

case sequence
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝¹ a✝ : Program
⊢ evaluate M w (~⌈a✝¹;'a✝⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (a✝¹;'a✝))))

case union
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝¹ a✝ : Program
⊢ evaluate M w (~⌈a✝¹⋓a✝⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (a✝¹⋓a✝))))

case star
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝ : Program
⊢ evaluate M w (~⌈∗a✝⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗a✝))))

case test
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝ : Formula
⊢ evaluate M w (~⌈?'a✝⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (?'a✝))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
a : ℕ
⊢ evaluate M w (~⌈·a⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (·a))))
Tactic:
case atom_prog a =>
  simp [H]
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w (~⌈?'τ⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (?'τ))))
Tactic:
case test τ =>
  simp [evaluate, H, Yset]
  rw [conEval]
  simp
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
a : ℕ
⊢ evaluate M w (~⌈·a⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (·a))))
Tactic:
simp [H]
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w (~⌈?'τ⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (?'τ))))
Tactic:
simp [evaluate, H, Yset]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w τ ∧ ¬evaluate M w ψ ↔ evaluate M w (Con (List.insert τ [~ψ]))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w τ ∧ ¬evaluate M w ψ ↔ evaluate M w (Con (List.insert τ [~ψ]))
Tactic:
rw [conEval]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w τ ∧ ¬evaluate M w ψ ↔ ∀ f ∈ List.insert τ [~ψ], evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w τ ∧ ¬evaluate M w ψ ↔ ∀ f ∈ List.insert τ [~ψ], evaluate M w f
Tactic:
simp
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 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:
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 α)))
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 α)))
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:
simp [evaluate, H, Yset, disEval] at *
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
⊢ (∃ x, (relate M α w 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
⊢ (∃ x, (relate M α w 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:
constructor
Proof state after:
case mp
ψ : 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
⊢ (∃ x, (relate M α w 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

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 ψ
Theorem: localDiamondTruth
Proof state before:
case mp
ψ : 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
⊢ (∃ x, (relate M α w 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:
rintro ⟨v, v_claim⟩
Proof state after:
case mp.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
v_claim : (relate M α w v ∨ relate M β w v) ∧ ¬evaluate M v ψ
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case mp.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
v_claim : (relate M α w v ∨ 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:
rw [or_and_right] at v_claim
Proof state after:
case mp.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
v_claim : relate M α w v ∧ ¬evaluate M v ψ ∨ relate M β w v ∧ ¬evaluate M v ψ
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case mp.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
v_claim : relate M α w v ∧ ¬evaluate M v ψ ∨ 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:
cases v_claim
Proof state after:
case mp.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
v : W
h✝ : relate M α w v ∧ ¬evaluate M v ψ
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f

case mp.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
v : W
h✝ : relate M β w v ∧ ¬evaluate M v ψ
⊢ ∃ 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 ψ
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
Tactic:
case inl hyp =>
  have : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) := ⟨v, hyp⟩
  rw [IHα] at this
  rcases this with ⟨f, ⟨⟨a, b, ⟨ab_in, def_f⟩⟩, w_f⟩⟩
  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:
case inr hyp =>
  have : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) := ⟨v, hyp⟩
  rw [IHβ] at this
  rcases this with ⟨f, ⟨⟨a, b, ⟨ab_in, def_f⟩⟩, w_f⟩⟩
  exact ⟨f, ⟨⟨a, b, ⟨Or.inr 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