internlm/Lean-Github huggingface dataset:
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
IHβ : ∃ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
rcases IHβ with ⟨η, ⟨η_in, v_η_w⟩⟩
Proof state after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
η : List Program
η_in : η ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
v_η_w : relateSeq M η v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Theorem: existsBoxFP
Proof state before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
η : List Program
η_in : η ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
v_η_w : relateSeq M η v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
use η
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
η : List Program
η_in : η ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
v_η_w : relateSeq M η v w
⊢ η ∈ P (α;'β) ℓ ∧ relateSeq M η v w
Theorem: existsBoxFP
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
η : List Program
η_in : η ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
v_η_w : relateSeq M η v w
⊢ η ∈ P (α;'β) ℓ ∧ relateSeq M η v w
Tactic:
simp_all [P]
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
⊢ evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
Tactic:
simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
use δ ++ [β]
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ++ [β] ∈ P (α;'β) ℓ ∧ relateSeq M (δ ++ [β]) v w
Theorem: existsBoxFP
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ++ [β] ∈ P (α;'β) ℓ ∧ relateSeq M (δ ++ [β]) v w
Tactic:
simp_all [P, relateSeq]
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ (δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨
      δ ++ [β] ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []) ∧
    relateSeq M (δ ++ [β]) v w
Theorem: existsBoxFP
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ (δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨
      δ ++ [β] ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []) ∧
    relateSeq M (δ ++ [β]) v w
Tactic:
constructor
Proof state after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨
    δ ++ [β] ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []

case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ relateSeq M (δ ++ [β]) v w
Theorem: existsBoxFP
Proof state before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨
    δ ++ [β] ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
Tactic:
left
Proof state after:
case h.left.h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
Theorem: existsBoxFP
Proof state before:
case h.left.h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
Tactic:
apply List.mem_filter_of_mem δ_in (by aesop)
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ (δ != []) = true
Tactic:
aesop
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ relateSeq M (δ ++ [β]) v w
Tactic:
simp [relateSeq_append]
Proof state after:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ ∃ u, relateSeq M δ v u ∧ relate M β u w
Theorem: existsBoxFP
Proof state before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ ∃ u, relateSeq M δ v u ∧ relate M β u w
Tactic:
use u
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : relate M (∗β) v w
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
simp only [relate] at v_γ_w
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
cases ReflTransGen.cases_tail_eq_neq v_γ_w
Proof state after:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v = w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

case inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_is_w : v = w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
case inl v_is_w =>
  subst v_is_w
  use []
  simp_all [P,relateSeq]
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_is_w : v = w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
subst v_is_w
Proof state after:
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v v
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v v
Tactic:
use []
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ [] ∈ P (∗β) ℓ ∧ relateSeq M [] v v
Theorem: existsBoxFP
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ [] ∈ P (∗β) ℓ ∧ relateSeq M [] v v
Tactic:
simp_all [P,relateSeq]
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
hyp : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
rcases hyp with ⟨v_neq_w, ⟨u, v_neq_u, v_β_u, u_βS_w⟩⟩
Proof state after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Theorem: existsBoxFP
Proof state before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
Proof state after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Theorem: existsBoxFP
Proof state before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
have IHβ := existsBoxFP β v_β_u ℓ v_Fℓβ
Proof state after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
IHβ :
  ∃
    δ ∈
      P β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩,
    relateSeq M δ v u
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Theorem: existsBoxFP
Proof state before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
IHβ :
  ∃
    δ ∈
      P β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩,
    relateSeq M δ v u
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
rcases IHβ with ⟨δ, ⟨δ_in, v_δ_w⟩⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Theorem: existsBoxFP
Proof state before:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
have claim : δ ≠ [] := by by_contra hyp; subst hyp; simp_all [relateSeq];
Proof state after:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : δ ≠ []
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Theorem: existsBoxFP
Proof state before:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : δ ≠ []
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
use δ ++ [∗β]
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : δ ≠ []
⊢ δ ++ [∗β] ∈ P (∗β) ℓ ∧ relateSeq M (δ ++ [∗β]) v w
Theorem: existsBoxFP
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : δ ≠ []
⊢ δ ++ [∗β] ∈ P (∗β) ℓ ∧ relateSeq M (δ ++ [∗β]) v w
Tactic:
simp_all [P, relateSeq]
Proof state after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩) ∧ relateSeq M (δ ++ [∗β]) v w
Theorem: existsBoxFP
Proof state before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩) ∧ relateSeq M (δ ++ [∗β]) v w
Tactic:
constructor
Proof state after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩)

case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ relateSeq M (δ ++ [∗β]) v w
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
⊢ evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
Tactic:
simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
⊢ δ ≠ []
Tactic:
by_contra hyp
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
hyp : δ = []
⊢ False
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
hyp : δ = []
⊢ False
Tactic:
subst hyp
Proof state after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M [] v u
⊢ False
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M [] v u
⊢ False
Tactic:
simp_all [relateSeq]
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩)
Tactic:
apply List.mem_filter_of_mem δ_in (by aesop)
Proof state after:
no goals