Theorem: signature_conbot_iff_neq (Pdl/Unfold.lean)

State before:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ℓ ≠ ℓ'
Tactic:
simp only [ne_eq]
State after:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬ℓ = ℓ'

State before:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬ℓ = ℓ'
Tactic:
rw [TP_eq_iff]
State after:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ

State before:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
constructor
State after:
case mp
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') → ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ

case mpr
α : Program
ℓ ℓ' : TP α
⊢ (¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ) → contradiction (signature α ℓ⋀signature α ℓ')

State before:
case mp
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') → ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
intro contrasign
State after:
case mp
α : Program
ℓ ℓ' : TP α
contrasign : contradiction (signature α ℓ⋀signature α ℓ')
⊢ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ

State before:
case mp
α : Program
ℓ ℓ' : TP α
contrasign : contradiction (signature α ℓ⋀signature α ℓ')
⊢ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
simp_all [TP, contradiction, signature_iff]
State after:
case mp
α : Program
ℓ ℓ' : TP α
contrasign :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    (∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a) →
      ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬(ℓ' ⟨x, x_1⟩ = true ↔ evaluate M w x)
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬ℓ ⟨x, x_1⟩ = ℓ' ⟨x, x_1⟩

State before:
case mp
α : Program
ℓ ℓ' : TP α
contrasign :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    (∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a) →
      ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬(ℓ' ⟨x, x_1⟩ = true ↔ evaluate M w x)
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬ℓ ⟨x, x_1⟩ = ℓ' ⟨x, x_1⟩
Tactic:
sorry
State after:
no goals

State before:
case mpr
α : Program
ℓ ℓ' : TP α
⊢ (¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ) → contradiction (signature α ℓ⋀signature α ℓ')
Tactic:
intro ldiff
State after:
case mpr
α : Program
ℓ ℓ' : TP α
ldiff : ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
⊢ contradiction (signature α ℓ⋀signature α ℓ')

State before:
case mpr
α : Program
ℓ ℓ' : TP α
ldiff : ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
⊢ contradiction (signature α ℓ⋀signature α ℓ')
Tactic:
intro W M w
State after:
case mpr
α : Program
ℓ ℓ' : TP α
ldiff : ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
W : Type
M : KripkeModel W
w : W
⊢ ¬evaluate M w (signature α ℓ⋀signature α ℓ')

State before:
case mpr
α : Program
ℓ ℓ' : TP α
ldiff : ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
W : Type
M : KripkeModel W
w : W
⊢ ¬evaluate M w (signature α ℓ⋀signature α ℓ')
Tactic:
simp_all only [List.mem_attach, forall_true_left, Subtype.forall, not_forall, evaluate, not_and]
State after:
case mpr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
ldiff : ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬ℓ ⟨x, x_1⟩ = ℓ' ⟨x, x_1⟩
⊢ evaluate M w (signature α ℓ) → ¬evaluate M w (signature α ℓ')

State before:
case mpr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
ldiff : ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬ℓ ⟨x, x_1⟩ = ℓ' ⟨x, x_1⟩
⊢ evaluate M w (signature α ℓ) → ¬evaluate M w (signature α ℓ')
Tactic:
rcases ldiff with ⟨τ, τ_in, disagree⟩
State after:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
⊢ evaluate M w (signature α ℓ) → ¬evaluate M w (signature α ℓ')

State before:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
⊢ evaluate M w (signature α ℓ) → ¬evaluate M w (signature α ℓ')
Tactic:
simp_all [signature, conEval]
State after:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x

State before:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
intro ℓ_conform
State after:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x

State before:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
cases em (ℓ ⟨τ,τ_in⟩)
State after:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
h✝ : ℓ ⟨τ, τ_in⟩ = true
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x

case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x

State before:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
h✝ : ℓ ⟨τ, τ_in⟩ = true
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
specialize ℓ_conform τ τ τ_in
State after:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = τ → evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x

State before:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = τ → evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
simp_all only [ite_true, forall_true_left]
State after:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x

State before:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
use (~τ)
State after:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = (~τ)) ∧ ¬evaluate M w (~τ)

State before:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = (~τ)) ∧ ¬evaluate M w (~τ)
Tactic:
constructor
State after:
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = (~τ)

case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ¬evaluate M w (~τ)

State before:
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = (~τ)
Tactic:
use τ, τ_in
State after:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ)

State before:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ)
Tactic:
simp_all
State after:
no goals

State before:
case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ¬evaluate M w (~τ)
Tactic:
simp
State after:
case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ evaluate M w τ

State before:
case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ evaluate M w τ
Tactic:
assumption
State after:
no goals

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

State before:
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ) → evaluate M w (~τ)
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
simp_all only [Bool.not_eq_true, ite_false, evaluate, forall_true_left]
State after:
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x

State before:
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
use τ
State after:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ) ∧ ¬evaluate M w τ

State before:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ) ∧ ¬evaluate M w τ
Tactic:
constructor
State after:
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ

case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ¬evaluate M w τ

State before:
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ
Tactic:
use τ, τ_in
State after:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = τ

State before:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = τ
Tactic:
simp_all
State after:
no goals

State before:
case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ¬evaluate M w τ
Tactic:
assumption
State after:
no goals