Theorem: top_equiv_disj_TP (Pdl/Unfold.lean)

State before:
L : List Formula
⊢ ∀ (α : Program), L = testsOfProgram α → tautology (dis (List.map (signature α) (allTP α)))
Tactic:
intro α
State after:
L : List Formula
α : Program
⊢ L = testsOfProgram α → tautology (dis (List.map (signature α) (allTP α)))

State before:
L : List Formula
α : Program
⊢ L = testsOfProgram α → tautology (dis (List.map (signature α) (allTP α)))
Tactic:
intro L_def
State after:
L : List Formula
α : Program
L_def : L = testsOfProgram α
⊢ tautology (dis (List.map (signature α) (allTP α)))

State before:
L : List Formula
α : Program
L_def : L = testsOfProgram α
⊢ tautology (dis (List.map (signature α) (allTP α)))
Tactic:
intro W M w
State after:
L : List Formula
α : Program
L_def : L = testsOfProgram α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (signature α) (allTP α)))

State before:
L : List Formula
α : Program
L_def : L = testsOfProgram α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (signature α) (allTP α)))
Tactic:
rw [disEval]
State after:
L : List Formula
α : Program
L_def : L = testsOfProgram α
W : Type
M : KripkeModel W
w : W
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f

State before:
L : List Formula
α : Program
L_def : L = testsOfProgram α
W : Type
M : KripkeModel W
w : W
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
Tactic:
induction L generalizing α
State after:
case nil
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f

case cons
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : ∀ (α : Program), tail✝ = testsOfProgram α → ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
α : Program
L_def : head✝ :: tail✝ = testsOfProgram α
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f

State before:
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
Tactic:
case nil =>
  simp [TP,signature,allTP]
  rw [← L_def]
  simp
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
Tactic:
simp [TP,signature,allTP]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ a,
    a.Sublist (testsOfProgram α) ∧
      evaluate M w (Con (List.map (fun τ => if ↑τ ∈ a then ↑τ else ~↑τ) (testsOfProgram α).attach))

State before:
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ a,
    a.Sublist (testsOfProgram α) ∧
      evaluate M w (Con (List.map (fun τ => if ↑τ ∈ a then ↑τ else ~↑τ) (testsOfProgram α).attach))
Tactic:
rw [← L_def]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ a, a.Sublist [] ∧ evaluate M w (Con (List.map (fun τ => if ↑τ ∈ a then ↑τ else ~↑τ) [].attach))

State before:
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ a, a.Sublist [] ∧ evaluate M w (Con (List.map (fun τ => if ↑τ ∈ a then ↑τ else ~↑τ) [].attach))
Tactic:
simp
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
IH : ∀ (α : Program), L = testsOfProgram α → ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
α : Program
L_def : τ :: L = testsOfProgram α
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
Tactic:
simp [TP,signature,allTP,conEval] at *
State after:
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
⊢ ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)

State before:
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
⊢ ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
Tactic:
rw [← L_def]
State after:
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)

State before:
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
Tactic:
cases em (evaluate M w τ)
State after:
case inl
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
h✝ : evaluate M w τ
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)

case inr
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
h✝ : ¬evaluate M w τ
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)

State before:
case inl
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
h✝ : evaluate M w τ
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
Tactic:
sorry
State after:
no goals

State before:
case inr
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
h✝ : ¬evaluate M w τ
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
Tactic:
sorry
State after:
no goals