Theorem: boxHelperTP (Pdl/Unfold.lean)

State before:
α : Program
ℓ : TP α
⊢ (∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false) ∧
    Con (F α ℓ)⋀signature α ℓ≡signature α ℓ ∧
      ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
Tactic:
refine ⟨?_, ?_, ?_⟩
State after:
case refine_1
α : Program
ℓ : TP α
⊢ ∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false

case refine_2
α : Program
ℓ : TP α
⊢ Con (F α ℓ)⋀signature α ℓ≡signature α ℓ

case refine_3
α : Program
ℓ : TP α
⊢ ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ

State before:
case refine_1
α : Program
ℓ : TP α
⊢ ∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false
Tactic:
intro τ τ_in
State after:
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in : (~↑τ) ∈ F α ℓ
⊢ ℓ τ = false

State before:
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in : (~↑τ) ∈ F α ℓ
⊢ ℓ τ = false
Tactic:
unfold F at *
State after:
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in :
  (~↑τ) ∈
    match α, ℓ with
    | ·a, x => ∅
    | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
    | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
    | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
    | ∗α, l =>
      F α fun x =>
        match x with
        | ⟨f, f_in⟩ => l ⟨f, ⋯⟩
⊢ ℓ τ = false

State before:
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in :
  (~↑τ) ∈
    match α, ℓ with
    | ·a, x => ∅
    | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
    | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
    | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
    | ∗α, l =>
      F α fun x =>
        match x with
        | ⟨f, f_in⟩ => l ⟨f, ⋯⟩
⊢ ℓ τ = false
Tactic:
sorry
State after:
no goals

State before:
case refine_2
α : Program
ℓ : TP α
⊢ Con (F α ℓ)⋀signature α ℓ≡signature α ℓ
Tactic:
intro W M w
State after:
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (F α ℓ)⋀signature α ℓ) ↔ evaluate M w (signature α ℓ)

State before:
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (F α ℓ)⋀signature α ℓ) ↔ evaluate M w (signature α ℓ)
Tactic:
simp [conEval, signature, F]
State after:
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∀ f ∈ F α ℓ, evaluate M w f

State before:
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∀ f ∈ F α ℓ, evaluate M w f
Tactic:
unfold F at *
State after:
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∀
      f ∈
        match α, ℓ with
        | ·a, x => ∅
        | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
        | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | ∗α, l =>
          F α fun x =>
            match x with
            | ⟨f, f_in⟩ => l ⟨f, ⋯⟩,
      evaluate M w f

State before:
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∀
      f ∈
        match α, ℓ with
        | ·a, x => ∅
        | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
        | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | ∗α, l =>
          F α fun x =>
            match x with
            | ⟨f, f_in⟩ => l ⟨f, ⋯⟩,
      evaluate M w f
Tactic:
sorry
State after:
no goals

State before:
case refine_3
α : Program
ℓ : TP α
⊢ ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
Tactic:
intro ψ
State after:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
⊢ Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ

State before:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
⊢ Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
Tactic:
intro W M w
State after:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (Xset α ℓ ψ)⋀signature α ℓ) ↔
    evaluate M w (Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ)

State before:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (Xset α ℓ ψ)⋀signature α ℓ) ↔
    evaluate M w (Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ)
Tactic:
simp [conEval, Xset]
State after:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (signature α ℓ) →
    ((∀ (f : Formula), (f ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉ψ) = f) → evaluate M w f) ↔ ∀ a ∈ P α ℓ, evaluate M w (⌈⌈a⌉⌉ψ))

State before:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (signature α ℓ) →
    ((∀ (f : Formula), (f ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉ψ) = f) → evaluate M w f) ↔ ∀ a ∈ P α ℓ, evaluate M w (⌈⌈a⌉⌉ψ))
Tactic:
sorry
State after:
no goals