internlm/Lean-Github huggingface dataset:
Theorem: repl_in_model_rel_iff
Proof state before:
case mp
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v → Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v

case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v → Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v
Tactic:
all_goals
  apply Relation.ReflTransGen.mono
  intro w v
  rw [IHα w v]
  tauto
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof state before:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v → Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v
Tactic:
apply Relation.ReflTransGen.mono
Proof state after:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ ∀ (a b : W), relate (repl_in_model x ψ M) α a b → relate M (repl_in_P x ψ α) a b
Theorem: repl_in_model_rel_iff
Proof state before:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ ∀ (a b : W), relate (repl_in_model x ψ M) α a b → relate M (repl_in_P x ψ α) a b
Tactic:
intro w v
Proof state after:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
w v : W
⊢ relate (repl_in_model x ψ M) α w v → relate M (repl_in_P x ψ α) w v
Theorem: repl_in_model_rel_iff
Proof state before:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
w v : W
⊢ relate (repl_in_model x ψ M) α w v → relate M (repl_in_P x ψ α) w v
Tactic:
rw [IHα w v]
Proof state after:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
w v : W
⊢ relate (repl_in_model x ψ M) α w v → relate (repl_in_model x ψ M) α w v
Theorem: repl_in_model_rel_iff
Proof state before:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
w v : W
⊢ relate (repl_in_model x ψ M) α w v → relate (repl_in_model x ψ M) α w v
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v
Tactic:
have IHφ := repl_in_model_sat_iff x ψ φ M v
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v
Theorem: repl_in_model_rel_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v
Tactic:
simp only [repl_in_P, relate, and_congr_right_iff, evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
⊢ w = v → (evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ)
Theorem: repl_in_model_rel_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
⊢ w = v → (evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ)
Tactic:
intro w_is_v
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
w_is_v : w = v
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
Theorem: repl_in_model_rel_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
w_is_v : w = v
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
Tactic:
subst w_is_v
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
IHφ : evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
Theorem: repl_in_model_rel_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
IHφ : evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
Tactic:
exact IHφ
Proof state after:
no goals
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
⊢ φ1≡φ2 → repl_in_F x ψ φ1≡repl_in_F x ψ φ2
Tactic:
intro hyp
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
⊢ repl_in_F x ψ φ1≡repl_in_F x ψ φ2
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
⊢ repl_in_F x ψ φ1≡repl_in_F x ψ φ2
Tactic:
intro W M w
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
have claim1 := repl_in_model_sat_iff x ψ φ1 M w
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
have claim2 := repl_in_model_sat_iff x ψ φ2 M w
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
claim2 : (M, w)⊨repl_in_F x ψ φ2 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
claim2 : (M, w)⊨repl_in_F x ψ φ2 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
simp only [evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
rw [claim1]
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate M w (repl_in_F x ψ φ2)
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
rw [claim2]
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Tactic:
have := @equiv_iff φ1 φ2 hyp W (repl_in_model x ψ M) w
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : (repl_in_model x ψ M, w)⊨φ1 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : (repl_in_model x ψ M, w)⊨φ1 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Tactic:
simp only [evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Theorem: repl_in_F_equiv
Proof state before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Tactic:
exact this
Proof state after:
no goals
Theorem: repl_in_P_equiv
Proof state before:
α1 α2 : Program
x : ℕ
ψ : Formula
⊢ α1≡ᵣα2 → repl_in_P x ψ α1≡ᵣrepl_in_P x ψ α2
Tactic:
intro hyp
Proof state after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
⊢ repl_in_P x ψ α1≡ᵣrepl_in_P x ψ α2
Theorem: repl_in_P_equiv
Proof state before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
⊢ repl_in_P x ψ α1≡ᵣrepl_in_P x ψ α2
Tactic:
intro W M w v
Proof state after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Theorem: repl_in_P_equiv
Proof state before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Tactic:
have claim1 := repl_in_model_rel_iff x ψ α1 M w v
Proof state after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Theorem: repl_in_P_equiv
Proof state before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Tactic:
have claim2 := repl_in_model_rel_iff x ψ α2 M w v
Proof state after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Theorem: repl_in_P_equiv
Proof state before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Tactic:
rw [claim1]
Proof state after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate (repl_in_model x ψ M) α1 w v ↔ relate M (repl_in_P x ψ α2) w v
Theorem: repl_in_P_equiv
Proof state before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate (repl_in_model x ψ M) α1 w v ↔ relate M (repl_in_P x ψ α2) w v
Tactic:
rw [claim2]
Proof state after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate (repl_in_model x ψ M) α1 w v ↔ relate (repl_in_model x ψ M) α2 w v
Theorem: repl_in_P_equiv
Proof state before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate (repl_in_model x ψ M) α1 w v ↔ relate (repl_in_model x ψ M) α2 w v
Tactic:
apply hyp
Proof state after:
no goals
Theorem: repl_in_disMap
Proof state before:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ repl_in_F x ρ (dis (List.map (fun Fδ => if p Fδ then Formula.bottom else f Fδ) L)) =
    dis (List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L)
Tactic:
rw [repl_in_dis, listEq_to_disEq]
Proof state after:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ) (List.map (fun Fδ => if p Fδ then Formula.bottom else f Fδ) L) =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L
Theorem: repl_in_disMap
Proof state before:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ) (List.map (fun Fδ => if p Fδ then Formula.bottom else f Fδ) L) =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L
Tactic:
simp only [List.map_map]
Proof state after:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ ∘ fun Fδ => if p Fδ then Formula.bottom else f Fδ) L =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L
Theorem: repl_in_disMap
Proof state before:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ ∘ fun Fδ => if p Fδ then Formula.bottom else f Fδ) L =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L
Tactic:
aesop
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ φ ↔ (subst_in_model σ M, w)⊨φ
Tactic:
cases φ
Proof state after:
case bottom
σ : Substitution
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ Formula.bottom ↔ (subst_in_model σ M, w)⊨Formula.bottom

case atom_prop
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝ : ℕ
⊢ (M, w)⊨subst_in_F σ (·a✝) ↔ (subst_in_model σ M, w)⊨·a✝

case neg
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (~a✝) ↔ (subst_in_model σ M, w)⊨(~a✝)

case and
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝¹ a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (a✝¹⋀a✝) ↔ (subst_in_model σ M, w)⊨a✝¹⋀a✝

case box
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝¹ : Program
a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈a✝¹⌉a✝) ↔ (subst_in_model σ M, w)⊨⌈a✝¹⌉a✝
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ Formula.bottom ↔ (subst_in_model σ M, w)⊨Formula.bottom
Tactic:
case bottom =>
  simp [evaluatePoint, modelCanSemImplyForm]
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨subst_in_F σ (·c) ↔ (subst_in_model σ M, w)⊨·c
Tactic:
case atom_prop c =>
  simp [evaluatePoint, modelCanSemImplyForm, evaluate, subst_in_model]
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)
Tactic:
case neg φ =>
  have IH := substitutionLemma σ φ M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  tauto
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Tactic:
case and φ1 φ2 =>
  have IH1 := substitutionLemma σ φ1 M w
  have IH2 := substitutionLemma σ φ2 M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  rw [IH1, IH2]
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
Tactic:
case box α φ =>
  have IHα := substitutionLemmaRel σ α M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  constructor
  all_goals
    intro hyp v rel
    have IHφ := substitutionLemma σ φ M v
    specialize IHα v
    specialize hyp v
    tauto
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ Formula.bottom ↔ (subst_in_model σ M, w)⊨Formula.bottom
Tactic:
simp [evaluatePoint, modelCanSemImplyForm]
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨subst_in_F σ (·c) ↔ (subst_in_model σ M, w)⊨·c
Tactic:
simp [evaluatePoint, modelCanSemImplyForm, evaluate, subst_in_model]
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)
Tactic:
have IH := substitutionLemma σ φ M w
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : (M, w)⊨subst_in_F σ φ ↔ (subst_in_model σ M, w)⊨φ
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : (M, w)⊨subst_in_F σ φ ↔ (subst_in_model σ M, w)⊨φ
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ
⊢ ¬evaluate M w (subst_in_F σ φ) ↔ ¬evaluate (subst_in_model σ M) w φ
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ
⊢ ¬evaluate M w (subst_in_F σ φ) ↔ ¬evaluate (subst_in_model σ M) w φ
Tactic:
tauto
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Tactic:
have IH1 := substitutionLemma σ φ1 M w
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Tactic:
have IH2 := substitutionLemma σ φ2 M w
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
IH2 : (M, w)⊨subst_in_F σ φ2 ↔ (subst_in_model σ M, w)⊨φ2
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
IH2 : (M, w)⊨subst_in_F σ φ2 ↔ (subst_in_model σ M, w)⊨φ2
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : evaluate M w (subst_in_F σ φ1) ↔ evaluate (subst_in_model σ M) w φ1
IH2 : evaluate M w (subst_in_F σ φ2) ↔ evaluate (subst_in_model σ M) w φ2
⊢ evaluate M w (subst_in_F σ φ1) ∧ evaluate M w (subst_in_F σ φ2) ↔
    evaluate (subst_in_model σ M) w φ1 ∧ evaluate (subst_in_model σ M) w φ2
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : evaluate M w (subst_in_F σ φ1) ↔ evaluate (subst_in_model σ M) w φ1
IH2 : evaluate M w (subst_in_F σ φ2) ↔ evaluate (subst_in_model σ M) w φ2
⊢ evaluate M w (subst_in_F σ φ1) ∧ evaluate M w (subst_in_F σ φ2) ↔
    evaluate (subst_in_model σ M) w φ1 ∧ evaluate (subst_in_model σ M) w φ2
Tactic:
rw [IH1, IH2]
Proof state after:
no goals
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
Tactic:
have IHα := substitutionLemmaRel σ α M w
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
Theorem: substitutionLemma
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)) ↔
    ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ