internlm/Lean-Github huggingface dataset:
Theorem: existsDiamondH
Proof state before:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
f : Formula
f_in : f ∈ (Fs, δ ++ [∗β]).1
⊢ evaluate M v f
Tactic:
simp at f_in
Proof state after:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
f : Formula
f_in : f ∈ Fs
⊢ evaluate M v f
Theorem: existsDiamondH
Proof state before:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
f : Formula
f_in : f ∈ Fs
⊢ evaluate M v f
Tactic:
exact v_Fs f f_in
Proof state after:
no goals
Theorem: existsDiamondH
Proof state before:
case h.right.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M (Fs, δ ++ [∗β]).2 v w
Tactic:
rw [relateSeq_append]
Proof state after:
case h.right.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ u, relateSeq M δ v u ∧ relateSeq M [∗β] u w
Theorem: existsDiamondH
Proof state before:
case h.right.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ u, relateSeq M δ v u ∧ relateSeq M [∗β] u w
Tactic:
use v1
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M δ v v1 ∧ relateSeq M [∗β] v1 w
Theorem: existsDiamondH
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M δ v v1 ∧ relateSeq M [∗β] v1 w
Tactic:
simp [relateSeq] at *
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ relateSeq M δ v v1 ∧ Relation.ReflTransGen (relate M β) v1 w
Theorem: existsDiamondH
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ relateSeq M δ v v1 ∧ Relation.ReflTransGen (relate M β) v1 w
Tactic:
tauto
Proof state after:
no goals
Theorem: TP_eq_iff
Proof state before:
α : Program
ℓ ℓ' : TP α
⊢ ℓ = ℓ' ↔ ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
constructor
Proof state after:
case mp
α : Program
ℓ ℓ' : TP α
⊢ ℓ = ℓ' → ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ

case mpr
α : Program
ℓ ℓ' : TP α
⊢ (∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ) → ℓ = ℓ'
Theorem: TP_eq_iff
Proof state before:
case mp
α : Program
ℓ ℓ' : TP α
⊢ ℓ = ℓ' → ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
intro ℓ_eq_ℓ _ _
Proof state after:
case mp
α : Program
ℓ ℓ' : TP α
ℓ_eq_ℓ : ℓ = ℓ'
τ✝ : { x // x ∈ testsOfProgram α }
a✝ : τ✝ ∈ (testsOfProgram α).attach
⊢ ℓ τ✝ = ℓ' τ✝
Theorem: TP_eq_iff
Proof state before:
case mp
α : Program
ℓ ℓ' : TP α
ℓ_eq_ℓ : ℓ = ℓ'
τ✝ : { x // x ∈ testsOfProgram α }
a✝ : τ✝ ∈ (testsOfProgram α).attach
⊢ ℓ τ✝ = ℓ' τ✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: TP_eq_iff
Proof state before:
case mpr
α : Program
ℓ ℓ' : TP α
⊢ (∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ) → ℓ = ℓ'
Tactic:
intro rhs
Proof state after:
case mpr
α : Program
ℓ ℓ' : TP α
rhs : ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
⊢ ℓ = ℓ'
Theorem: TP_eq_iff
Proof state before:
case mpr
α : Program
ℓ ℓ' : TP α
rhs : ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
⊢ ℓ = ℓ'
Tactic:
simp_all
Proof state after:
case mpr
α : Program
ℓ ℓ' : TP α
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
⊢ ℓ = ℓ'
Theorem: TP_eq_iff
Proof state before:
case mpr
α : Program
ℓ ℓ' : TP α
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
⊢ ℓ = ℓ'
Tactic:
unfold TP at *
Proof state after:
case mpr
α : Program
ℓ ℓ' : { τ // τ ∈ testsOfProgram α } → Bool
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
⊢ ℓ = ℓ'
Theorem: TP_eq_iff
Proof state before:
case mpr
α : Program
ℓ ℓ' : { τ // τ ∈ testsOfProgram α } → Bool
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
⊢ ℓ = ℓ'
Tactic:
ext τ
Proof state after:
case mpr.h
α : Program
ℓ ℓ' : { τ // τ ∈ testsOfProgram α } → Bool
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
τ : { τ // τ ∈ testsOfProgram α }
⊢ ℓ τ = ℓ' τ
Theorem: TP_eq_iff
Proof state before:
case mpr.h
α : Program
ℓ ℓ' : { τ // τ ∈ testsOfProgram α } → Bool
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
τ : { τ // τ ∈ testsOfProgram α }
⊢ ℓ τ = ℓ' τ
Tactic:
apply rhs
Proof state after:
no goals
Theorem: signature_iff
Proof 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]
Proof 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
Theorem: signature_iff
Proof 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
Proof 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
Theorem: signature_iff
Proof 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_ℓ
Proof 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
Theorem: signature_iff
Proof 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
Proof 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 τ
Theorem: signature_iff
Proof 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⟩)
Proof 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 τ
Theorem: signature_iff
Proof 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
Proof 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 τ
Theorem: signature_iff
Proof 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
Proof state after:
no goals
Theorem: signature_iff
Proof 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
Proof 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 τ
Theorem: signature_iff
Proof 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
Proof state after:
no goals
Theorem: signature_iff
Proof 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
Proof state after:
no goals
Theorem: top_equiv_disj_TP
Proof state before:
L : List Formula
⊢ ∀ (α : Program), L = testsOfProgram α → tautology (dis (List.map (signature α) (allTP α)))
Tactic:
intro α
Proof state after:
L : List Formula
α : Program
⊢ L = testsOfProgram α → tautology (dis (List.map (signature α) (allTP α)))
Theorem: top_equiv_disj_TP
Proof state before:
L : List Formula
α : Program
⊢ L = testsOfProgram α → tautology (dis (List.map (signature α) (allTP α)))
Tactic:
intro L_def
Proof state after:
L : List Formula
α : Program
L_def : L = testsOfProgram α
⊢ tautology (dis (List.map (signature α) (allTP α)))
Theorem: top_equiv_disj_TP
Proof state before:
L : List Formula
α : Program
L_def : L = testsOfProgram α
⊢ tautology (dis (List.map (signature α) (allTP α)))
Tactic:
intro W M w
Proof 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 α)))
Theorem: top_equiv_disj_TP
Proof 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]
Proof 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
Theorem: top_equiv_disj_TP
Proof 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 α
Proof 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
Theorem: top_equiv_disj_TP
Proof 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
Proof state after:
no goals
Theorem: top_equiv_disj_TP
Proof 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]
Proof 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))
Theorem: top_equiv_disj_TP
Proof 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]
Proof 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))
Theorem: top_equiv_disj_TP
Proof 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
Proof state after:
no goals
Theorem: top_equiv_disj_TP
Proof 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 *
Proof 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)
Theorem: top_equiv_disj_TP
Proof 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]
Proof 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)
Theorem: top_equiv_disj_TP
Proof 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 τ)
Proof 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)
Theorem: top_equiv_disj_TP
Proof 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
Proof state after:
no goals
Theorem: top_equiv_disj_TP
Proof 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
Proof state after:
no goals
Theorem: signature_conbot_iff_neq
Proof state before:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ℓ ≠ ℓ'
Tactic:
simp only [ne_eq]
Proof state after:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬ℓ = ℓ'
Theorem: signature_conbot_iff_neq
Proof state before:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬ℓ = ℓ'
Tactic:
rw [TP_eq_iff]
Proof state after:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Theorem: signature_conbot_iff_neq
Proof state before:
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
constructor
Proof state after:
case mp
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') → ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ

case mpr
α : Program
ℓ ℓ' : TP α
⊢ (¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ) → contradiction (signature α ℓ⋀signature α ℓ')
Theorem: signature_conbot_iff_neq
Proof state before:
case mp
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') → ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
intro contrasign
Proof state after:
case mp
α : Program
ℓ ℓ' : TP α
contrasign : contradiction (signature α ℓ⋀signature α ℓ')
⊢ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Theorem: signature_conbot_iff_neq
Proof state before:
case mp
α : Program
ℓ ℓ' : TP α
contrasign : contradiction (signature α ℓ⋀signature α ℓ')
⊢ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
simp_all [TP, contradiction, signature_iff]
Proof 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⟩
Theorem: signature_conbot_iff_neq
Proof 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
Proof state after:
no goals
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr
α : Program
ℓ ℓ' : TP α
⊢ (¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ) → contradiction (signature α ℓ⋀signature α ℓ')
Tactic:
intro ldiff
Proof state after:
case mpr
α : Program
ℓ ℓ' : TP α
ldiff : ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
⊢ contradiction (signature α ℓ⋀signature α ℓ')
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr
α : Program
ℓ ℓ' : TP α
ldiff : ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
⊢ contradiction (signature α ℓ⋀signature α ℓ')
Tactic:
intro W M w
Proof state after:
case mpr
α : Program
ℓ ℓ' : TP α
ldiff : ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
W : Type
M : KripkeModel W
w : W
⊢ ¬evaluate M w (signature α ℓ⋀signature α ℓ')
Theorem: signature_conbot_iff_neq
Proof 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]
Proof 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 α ℓ')
Theorem: signature_conbot_iff_neq
Proof 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⟩
Proof 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 α ℓ')