internlm/Lean-Github huggingface dataset:
Theorem: localDiamondTruth
Proof state before:
case a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis
      (List.map
        (fun Fδ => if Fδ.2 = [] then repl_in_F x ρ Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)))
        (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ ∀ x_1 ∈ H β,
    (if x_1.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈x_1.2⌉⌉~·x) :: x_1.1))) =
      if x_1.2 = [] then Formula.bottom else Con ((~⌈⌈x_1.2⌉⌉~ρ) :: x_1.1)
Tactic:
intro Fδ Fδ_in_Hβ
Proof state after:
case a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis
      (List.map
        (fun Fδ => if Fδ.2 = [] then repl_in_F x ρ Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)))
        (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ : List Formula × List Program
Fδ_in_Hβ : Fδ ∈ H β
⊢ (if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) =
    if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Theorem: localDiamondTruth
Proof state before:
case a.inl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis
      (List.map
        (fun Fδ => if Fδ.2 = [] then repl_in_F x ρ Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)))
        (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ : List Formula × List Program
Fδ_in_Hβ : Fδ ∈ H β
h✝ : Fδ.2 = []
⊢ (if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) =
    if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Tactic:
simp_all
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case a.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis
      (List.map
        (fun Fδ => if Fδ.2 = [] then repl_in_F x ρ Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)))
        (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ : List Formula × List Program
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ (if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) =
    if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Tactic:
simp_all only [evaluate, relate, not_forall, exists_prop, repl_in_F, Formula.instBot, Prod.forall, ite_false]
Proof state after:
case a.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) = Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Theorem: localDiamondTruth
Proof state before:
case a.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) = Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Tactic:
rw [repl_in_Con]
Proof state after:
case a.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ Con (List.map (repl_in_F x ρ) ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) = Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Theorem: localDiamondTruth
Proof state before:
case a.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ Con (List.map (repl_in_F x ρ) ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) = Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Tactic:
simp only [List.map_cons, repl_in_F]
Proof state after:
case a.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ Con ((~repl_in_F x ρ (⌈⌈Fδ.2⌉⌉~·x)) :: List.map (repl_in_F x ρ) Fδ.1) = Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Theorem: localDiamondTruth
Proof state before:
case a.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ Con ((~repl_in_F x ρ (⌈⌈Fδ.2⌉⌉~·x)) :: List.map (repl_in_F x ρ) Fδ.1) = Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Tactic:
apply listEq_to_conEq
Proof state after:
case a.inr.a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ (~repl_in_F x ρ (⌈⌈Fδ.2⌉⌉~·x)) :: List.map (repl_in_F x ρ) Fδ.1 = (~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1
Theorem: localDiamondTruth
Proof state before:
case a.inr.a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ (~repl_in_F x ρ (⌈⌈Fδ.2⌉⌉~·x)) :: List.map (repl_in_F x ρ) Fδ.1 = (~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1
Tactic:
simp only [List.cons.injEq, Formula.neg.injEq]
Proof state after:
case a.inr.a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ (repl_in_F x ρ (⌈⌈Fδ.2⌉⌉~·x) = ⌈⌈Fδ.2⌉⌉~ρ) ∧ List.map (repl_in_F x ρ) Fδ.1 = Fδ.1
Theorem: localDiamondTruth
Proof state before:
case a.inr.a.left
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ repl_in_F x ρ (⌈⌈Fδ.2⌉⌉~·x) = ⌈⌈Fδ.2⌉⌉~ρ
Tactic:
exact repl_in_boxes_non_occ_eq _ ((myFresh _ _ (Fδ_in_Hβ)).2)
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case a.inr.a.right
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ List.map (repl_in_F x ρ) Fδ.1 = Fδ.1
Tactic:
exact repl_in_list_non_occ_eq _ ((myFresh _ _ (Fδ_in_Hβ)).1)
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
repl_w_ : evaluate M w (if (Fs, δ).2 = [] then Formula.bottom else Con ((~⌈⌈(Fs, δ).2⌉⌉~ρ) :: (Fs, δ).1))
hyp : δ = []
⊢ evaluate M w ρ
Tactic:
subst hyp
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
Fδ_in : (Fs, []) ∈ H β
repl_w_ : evaluate M w (if (Fs, []).2 = [] then Formula.bottom else Con ((~⌈⌈(Fs, []).2⌉⌉~ρ) :: (Fs, []).1))
⊢ evaluate M w ρ
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
Fδ_in : (Fs, []) ∈ H β
repl_w_ : evaluate M w (if (Fs, []).2 = [] then Formula.bottom else Con ((~⌈⌈(Fs, []).2⌉⌉~ρ) :: (Fs, []).1))
⊢ evaluate M w ρ
Tactic:
simp_all
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
repl_w_ : evaluate M w (if (Fs, δ).2 = [] then Formula.bottom else Con ((~⌈⌈(Fs, δ).2⌉⌉~ρ) :: (Fs, δ).1))
hyp : ¬δ = []
⊢ evaluate M w ρ
Tactic:
simp [hyp] at repl_w_
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : evaluate M w (Con ((~⌈⌈δ⌉⌉~ρ) :: Fs))
⊢ evaluate M w ρ
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : evaluate M w (Con ((~⌈⌈δ⌉⌉~ρ) :: Fs))
⊢ evaluate M w ρ
Tactic:
rw [conEval] at repl_w_
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
⊢ evaluate M w ρ