Theorem: signature_iff (Pdl/Unfold.lean)

State before:
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (signature α ℓ) ↔ ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = true ↔ evaluate M w ↑τ
Tactic:
simp [signature, conEval]
State after:
α : 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) ↔
    ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a

State before:
α : 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) ↔
    ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a
Tactic:
constructor
State after:
case mp
α : 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) →
    ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a

case mpr
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ (∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a) →
    ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f

State before:
case mp
α : 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) →
    ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a
Tactic:
intro w_ℓ
State after:
case mp
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
w_ℓ : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
⊢ ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a

State before:
case mp
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
w_ℓ : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
⊢ ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a
Tactic:
intro τ τ_in
State after:
case mp
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
w_ℓ : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
τ : Formula
τ_in : τ ∈ testsOfProgram α
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ

State before:
case mp
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
w_ℓ : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
τ : Formula
τ_in : τ ∈ testsOfProgram α
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ
Tactic:
cases em (ℓ ⟨τ, τ_in⟩)
State after:
case mp.inl
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
w_ℓ : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ℓ ⟨τ, τ_in⟩ = true
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ

case mp.inr
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
w_ℓ : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ

State before:
case mp.inl
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
w_ℓ : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ℓ ⟨τ, τ_in⟩ = true
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ
Tactic:
specialize w_ℓ τ τ τ_in
State after:
case mp.inl
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ℓ ⟨τ, τ_in⟩ = true
w_ℓ : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = τ → evaluate M w τ
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ

State before:
case mp.inl
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ℓ ⟨τ, τ_in⟩ = true
w_ℓ : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = τ → evaluate M w τ
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ
Tactic:
aesop
State after:
no goals

State before:
case mp.inr
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
w_ℓ : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ
Tactic:
specialize w_ℓ (~τ) τ τ_in
State after:
case mp.inr
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
w_ℓ : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ) → evaluate M w (~τ)
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ

State before:
case mp.inr
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
w_ℓ : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ) → evaluate M w (~τ)
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ
Tactic:
aesop
State after:
no goals

State before:
case mpr
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ (∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a) →
    ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
Tactic:
aesop
State after:
no goals