internlm/Lean-Github huggingface dataset:
Theorem: F_goes_down
Proof state before:
case atom_prog
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ F (·a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (·a✝)

case sequence
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
φ_in : φ ∈ F (a✝¹;'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (a✝¹;'a✝)

case union
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
φ_in : φ ∈ F (a✝¹⋓a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (a✝¹⋓a✝)

case star
φ : Formula
a✝ : Program
ℓ : TP (∗a✝)
φ_in : φ ∈ F (∗a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (∗a✝)

case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ F (?'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (?'a✝)
Tactic:
all_goals
  simp only [F, List.mem_union_iff, lengthOfProgram] at *
Proof state after:
case atom_prog
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ ∅
⊢ lengthOfFormula φ < 1

case sequence
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
φ_in : (φ ∈ F a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F a✝ fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case union
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
φ_in : (φ ∈ F a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F a✝ fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case star
φ : Formula
a✝ : Program
ℓ : TP (∗a✝)
φ_in : φ ∈ F a✝ fun x => ℓ ⟨↑x, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝

case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ if ℓ ⟨a✝, ⋯⟩ = true then ∅ else [~a✝]
⊢ lengthOfFormula φ < 2 + lengthOfFormula a✝
Theorem: F_goes_down
Proof state before:
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ ∅
⊢ lengthOfFormula φ < 1
Tactic:
case atom_prog =>
  simp only [List.empty_eq, List.not_mem_nil] at φ_in
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case sequence α β =>
  cases φ_in
  case inl φ_in_Fα =>
    have IHα := F_goes_down φ_in_Fα
    linarith
  case inr φ_in_Fβ =>
    have IHβ := F_goes_down φ_in_Fβ
    linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case union α β =>
  cases φ_in
  case inl φ_in_Fα =>
    have IHα := F_goes_down φ_in_Fα
    linarith
  case inr φ_in_Fβ =>
    have IHβ := F_goes_down φ_in_Fβ
    linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α
Tactic:
case star α =>
  have IHα := F_goes_down φ_in
  linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ F (?'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (?'a✝)
Tactic:
simp only [F, List.mem_union_iff, lengthOfProgram] at *
Proof state after:
case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ if ℓ ⟨a✝, ⋯⟩ = true then ∅ else [~a✝]
⊢ lengthOfFormula φ < 2 + lengthOfFormula a✝
Theorem: F_goes_down
Proof state before:
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ ∅
⊢ lengthOfFormula φ < 1
Tactic:
simp only [List.empty_eq, List.not_mem_nil] at φ_in
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases φ_in
Proof state after:
case inl
φ : Formula
α β : Program
ℓ : TP (α;'β)
h✝ : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
φ : Formula
α β : Program
ℓ : TP (α;'β)
h✝ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl φ_in_Fα =>
  have IHα := F_goes_down φ_in_Fα
  linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inr φ_in_Fβ =>
  have IHβ := F_goes_down φ_in_Fβ
  linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IHα := F_goes_down φ_in_Fα
Proof state after:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IHβ := F_goes_down φ_in_Fβ
Proof state after:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases φ_in
Proof state after:
case inl
φ : Formula
α β : Program
ℓ : TP (α⋓β)
h✝ : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
φ : Formula
α β : Program
ℓ : TP (α⋓β)
h✝ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl φ_in_Fα =>
  have IHα := F_goes_down φ_in_Fα
  linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inr φ_in_Fβ =>
  have IHβ := F_goes_down φ_in_Fβ
  linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IHα := F_goes_down φ_in_Fα
Proof state after:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IHβ := F_goes_down φ_in_Fβ
Proof state after:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: F_goes_down
Proof state before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α
Tactic:
have IHα := F_goes_down φ_in
Proof state after:
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α
Theorem: F_goes_down
Proof state before:
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α
Tactic:
linarith
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ
Tactic:
cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩)
Proof state after:
case inl
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ

case inr
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ
Theorem: F_goes_down
Proof state before:
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
⊢ τ ∈ testsOfProgram (?'τ)
Tactic:
simp [testsOfProgram]
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
case inl
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ
Tactic:
simp_all
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
case inr
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ
Tactic:
simp_all
Proof state after:
no goals
Theorem: boxHelperTermination
Proof state before:
n : ℕ
a γ : Program
ℓ : TP γ
ψ : Formula
⊢ (∀ δ ∈ P γ ℓ,
      (∀ α ∈ δ, α ∈ subprograms γ) ∧
        (∀ (h : δ.length > 0), isAtomic (δ.get (Fin.ofNat' 0 h)) = true) ∧
          ∀ iα ∈ δ.enum, iα.2 = γ ↔ isAtomic γ = true ∧ iα.1 = n ∧ iα.1 = 1 ∨ isStar γ = true ∧ iα.1 = n) ∧
    ∀ φ ∈ (unfoldBox γ ψ).join,
      φ ∈ fischerLadner (⌈γ⌉ψ) ∧
        (φ = ψ ∨ (∃ τ ∈ testsOfProgram γ, φ = (~τ)) ∨ ∃ δ, (φ = ⌈a⌉⌈⌈δ⌉⌉ψ) ∧ ∀ α ∈ δ, α ∈ subprograms γ)
Tactic:
sorry
Proof state after:
no goals
Theorem: boxHelperTP
Proof state before:
α : Program
ℓ : TP α
⊢ (∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false) ∧
    Con (F α ℓ)⋀signature α ℓ≡signature α ℓ ∧
      ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
Tactic:
refine ⟨?_, ?_, ?_⟩
Proof state after:
case refine_1
α : Program
ℓ : TP α
⊢ ∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false

case refine_2
α : Program
ℓ : TP α
⊢ Con (F α ℓ)⋀signature α ℓ≡signature α ℓ

case refine_3
α : Program
ℓ : TP α
⊢ ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
Theorem: boxHelperTP
Proof state before:
case refine_1
α : Program
ℓ : TP α
⊢ ∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false
Tactic:
intro τ τ_in
Proof state after:
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in : (~↑τ) ∈ F α ℓ
⊢ ℓ τ = false
Theorem: boxHelperTP
Proof state before:
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in : (~↑τ) ∈ F α ℓ
⊢ ℓ τ = false
Tactic:
unfold F at *
Proof state after:
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in :
  (~↑τ) ∈
    match α, ℓ with
    | ·a, x => ∅
    | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
    | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
    | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
    | ∗α, l =>
      F α fun x =>
        match x with
        | ⟨f, f_in⟩ => l ⟨f, ⋯⟩
⊢ ℓ τ = false
Theorem: boxHelperTP
Proof state before:
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in :
  (~↑τ) ∈
    match α, ℓ with
    | ·a, x => ∅
    | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
    | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
    | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
    | ∗α, l =>
      F α fun x =>
        match x with
        | ⟨f, f_in⟩ => l ⟨f, ⋯⟩
⊢ ℓ τ = false
Tactic:
sorry
Proof state after:
no goals
Theorem: boxHelperTP
Proof state before:
case refine_2
α : Program
ℓ : TP α
⊢ Con (F α ℓ)⋀signature α ℓ≡signature α ℓ
Tactic:
intro W M w
Proof state after:
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (F α ℓ)⋀signature α ℓ) ↔ evaluate M w (signature α ℓ)
Theorem: boxHelperTP
Proof state before:
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (F α ℓ)⋀signature α ℓ) ↔ evaluate M w (signature α ℓ)
Tactic:
simp [conEval, signature, F]
Proof state after:
case refine_2
α : 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) →
    ∀ f ∈ F α ℓ, evaluate M w f
Theorem: boxHelperTP
Proof state before:
case refine_2
α : 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) →
    ∀ f ∈ F α ℓ, evaluate M w f
Tactic:
unfold F at *
Proof state after:
case refine_2
α : 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) →
    ∀
      f ∈
        match α, ℓ with
        | ·a, x => ∅
        | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
        | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | ∗α, l =>
          F α fun x =>
            match x with
            | ⟨f, f_in⟩ => l ⟨f, ⋯⟩,
      evaluate M w f
Theorem: boxHelperTP
Proof state before:
case refine_2
α : 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) →
    ∀
      f ∈
        match α, ℓ with
        | ·a, x => ∅
        | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
        | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | ∗α, l =>
          F α fun x =>
            match x with
            | ⟨f, f_in⟩ => l ⟨f, ⋯⟩,
      evaluate M w f
Tactic:
sorry
Proof state after:
no goals
Theorem: boxHelperTP
Proof state before:
case refine_3
α : Program
ℓ : TP α
⊢ ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
Tactic:
intro ψ
Proof state after:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
⊢ Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
Theorem: boxHelperTP
Proof state before:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
⊢ Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
Tactic:
intro W M w
Proof state after:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (Xset α ℓ ψ)⋀signature α ℓ) ↔
    evaluate M w (Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ)
Theorem: boxHelperTP
Proof state before:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (Xset α ℓ ψ)⋀signature α ℓ) ↔
    evaluate M w (Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ)
Tactic:
simp [conEval, Xset]
Proof state after:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (signature α ℓ) →
    ((∀ (f : Formula), (f ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉ψ) = f) → evaluate M w f) ↔ ∀ a ∈ P α ℓ, evaluate M w (⌈⌈a⌉⌉ψ))
Theorem: boxHelperTP
Proof state before:
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (signature α ℓ) →
    ((∀ (f : Formula), (f ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉ψ) = f) → evaluate M w f) ↔ ∀ a ∈ P α ℓ, evaluate M w (⌈⌈a⌉⌉ψ))
Tactic:
sorry
Proof state after:
no goals
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
⊢ ρ⊨⌈∗β⌉ψ
Tactic:
intro W M w
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w : W
⊢ (∀ φ ∈ [ρ], evaluate M w φ) → ∀ ψ_1 ∈ [⌈∗β⌉ψ], evaluate M w ψ_1
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w : W
⊢ (∀ φ ∈ [ρ], evaluate M w φ) → ∀ ψ_1 ∈ [⌈∗β⌉ψ], evaluate M w ψ_1
Tactic:
simp only [List.mem_singleton, forall_eq, evaluate, relate]
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w ρ → ∀ (v : W), Relation.ReflTransGen (relate M β) w v → evaluate M v ψ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w ρ → ∀ (v : W), Relation.ReflTransGen (relate M β) w v → evaluate M v ψ
Tactic:
intro w_rho v w_bS_v
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w : W
w_rho : evaluate M w ρ
v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
⊢ evaluate M v ψ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w : W
w_rho : evaluate M w ρ
v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
⊢ evaluate M v ψ
Tactic:
induction w_bS_v using Relation.ReflTransGen.head_induction_on
Proof state after:
case refl
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ evaluate M v ψ

case head
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v a✝¹ c✝ : W
h'✝ : relate M β a✝¹ c✝
h✝ : Relation.ReflTransGen (relate M β) c✝ v
a✝ : evaluate M c✝ ρ → evaluate M v ψ
w_rho : evaluate M a✝¹ ρ
⊢ evaluate M v ψ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ → evaluate M v ψ
w_rho : evaluate M u1 ρ
⊢ evaluate M v ψ
Tactic:
case head u1 u2 u1_b_u2 _ IH =>
  apply IH
  exact fortysix W M u1 u2 w_rho u1_b_u2
Proof state after:
no goals
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
⊢ ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
Tactic:
intro W M w v w_rho w_β_v
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ (M, v)⊨ρ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
this : (M, w)⊨⌈β⌉ρ
⊢ (M, v)⊨ρ
Tactic:
simp [evaluate,relate,modelCanSemImplyForm] at this
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
this : ∀ (v : W), relate M β w v → evaluate M v ρ
⊢ (M, v)⊨ρ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
this : ∀ (v : W), relate M β w v → evaluate M v ρ
⊢ (M, v)⊨ρ
Tactic:
exact this v w_β_v
Proof state after:
no goals
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ (M, w)⊨⌈β⌉ρ
Tactic:
have by_ass : (M,w) ⊨ (repl_in_F x ρ) (χ0 ⋁ χ1) := by apply rho_imp_repl; simp; exact w_rho; simp
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
⊢ (M, w)⊨⌈β⌉ρ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
⊢ (M, w)⊨⌈β⌉ρ
Tactic:
have := repl_in_F_equiv x ρ beta_equiv
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : repl_in_F x ρ (⌈β⌉·x)≡repl_in_F x ρ ((·x)⋀χ0⋁χ1)
⊢ (M, w)⊨⌈β⌉ρ