internlm/Lean-Github huggingface dataset:
Theorem: existsWitnessPath_rtl
Proof state before:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
Tactic:
use v1
Proof state after:
case h
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v1 ∧ ¬evaluate M v1 (⌈⌈γs⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
case h
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v1 ∧ ¬evaluate M v1 (⌈⌈γs⌉⌉ξ)
Tactic:
constructor
Proof state after:
case h.left
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v1

case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v1 (⌈⌈γs⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
case h.left
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v1
Tactic:
sorry
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v1 (⌈⌈γs⌉⌉ξ)
Tactic:
specialize IH v1 (ηs++γs) ξ wit_v1_ηγs ?_
Proof state after:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ wit_v1_ηγs.length = n

case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ¬evaluate M v1 (⌈⌈ηs ++ γs⌉⌉ξ)
⊢ ¬evaluate M v1 (⌈⌈γs⌉⌉ξ)
Theorem: existsWitnessPath_rtl
Proof state before:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ wit_v1_ηγs.length = n
Tactic:
sorry
Proof state after:
no goals
Theorem: existsWitnessPath_rtl
Proof state before:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγs.length = n + 1
IH : ¬evaluate M v1 (⌈⌈ηs ++ γs⌉⌉ξ)
⊢ ¬evaluate M v1 (⌈⌈γs⌉⌉ξ)
Tactic:
sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
v : W
δ : List Program
ξ : Formula
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Tactic:
induction δ generalizing v
Proof state after:
case nil
W : Type
M : KripkeModel W
ξ : Formula
v : W
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ) → Nonempty (witness M v [] ξ)

case cons
W : Type
M : KripkeModel W
ξ : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : ∀ (v : W), evaluate M v (~⌈⌈tail✝⌉⌉ξ) → Nonempty (witness M v tail✝ ξ)
v : W
⊢ evaluate M v (~⌈⌈head✝ :: tail✝⌉⌉ξ) → Nonempty (witness M v (head✝ :: tail✝) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
v : W
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ) → Nonempty (witness M v [] ξ)
Tactic:
case nil =>
  intro v_ξ
  constructor
  apply witness.nil
  simp at *
  exact v_ξ
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ) → Nonempty (witness M v (α :: γs) ξ)
Tactic:
case cons α γs IH =>
  intro v_
  simp at *
  rcases v_ with ⟨w, v_α_w, w_⟩
  rcases IH w w_ with ⟨w_wit⟩
  cases α case atom_prog a =>
    simp at v_α_w
    constructor
    apply witness.consAtom v_α_w w_wit
  case sequence α β =>
    simp at *
    rcases v_α_w with ⟨u, v_u, u_w⟩
    rcases IH w w_ with ⟨w_wit⟩
    constructor
    sorry
  case union α β =>
    constructor
    sorry
  case test τ =>
    constructor
    sorry
  case star β =>
    constructor
    sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
v : W
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ) → Nonempty (witness M v [] ξ)
Tactic:
intro v_ξ
Proof state after:
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ Nonempty (witness M v [] ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ Nonempty (witness M v [] ξ)
Tactic:
constructor
Proof state after:
case val
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ witness M v [] ξ
Theorem: existsWitnessPath_ltr
Proof state before:
case val
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ witness M v [] ξ
Tactic:
apply witness.nil
Proof state after:
case val.a
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ evaluate M v (~ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
case val.a
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ evaluate M v (~ξ)
Tactic:
simp at *
Proof state after:
case val.a
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ
Theorem: existsWitnessPath_ltr
Proof state before:
case val.a
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ
Tactic:
exact v_ξ
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ) → Nonempty (witness M v (α :: γs) ξ)
Tactic:
intro v_
Proof state after:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
v_ : evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
v_ : evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Tactic:
simp at *
Proof state after:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v_ : ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v_ : ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Tactic:
rcases v_ with ⟨w, v_α_w, w_⟩
Proof state after:
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Tactic:
rcases IH w w_ with ⟨w_wit⟩
Proof state after:
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v (α :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v (α :: γs) ξ)
Tactic:
cases α
Proof state after:
case intro.intro.intro.atom_prog
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝ : ℕ
v_α_w : relate M (·a✝) v w
⊢ Nonempty (witness M v ((·a✝) :: γs) ξ)

case intro.intro.intro.sequence
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝¹ a✝ : Program
v_α_w : relate M (a✝¹;'a✝) v w
⊢ Nonempty (witness M v ((a✝¹;'a✝) :: γs) ξ)

case intro.intro.intro.union
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝¹ a✝ : Program
v_α_w : relate M (a✝¹⋓a✝) v w
⊢ Nonempty (witness M v ((a✝¹⋓a✝) :: γs) ξ)

case intro.intro.intro.star
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝ : Program
v_α_w : relate M (∗a✝) v w
⊢ Nonempty (witness M v ((∗a✝) :: γs) ξ)

case intro.intro.intro.test
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝ : Formula
v_α_w : relate M (?'a✝) v w
⊢ Nonempty (witness M v ((?'a✝) :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : relate M (·a) v w
⊢ Nonempty (witness M v ((·a) :: γs) ξ)
Tactic:
case atom_prog a =>
  simp at v_α_w
  constructor
  apply witness.consAtom v_α_w w_wit
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α;'β) v w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
case sequence α β =>
  simp at *
  rcases v_α_w with ⟨u, v_u, u_w⟩
  rcases IH w w_ with ⟨w_wit⟩
  constructor
  sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α⋓β) v w
⊢ Nonempty (witness M v ((α⋓β) :: γs) ξ)
Tactic:
case union α β =>
  constructor
  sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
τ : Formula
v_α_w : relate M (?'τ) v w
⊢ Nonempty (witness M v ((?'τ) :: γs) ξ)
Tactic:
case test τ =>
  constructor
  sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
β : Program
v_α_w : relate M (∗β) v w
⊢ Nonempty (witness M v ((∗β) :: γs) ξ)
Tactic:
case star β =>
  constructor
  sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : relate M (·a) v w
⊢ Nonempty (witness M v ((·a) :: γs) ξ)
Tactic:
simp at v_α_w
Proof state after:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : M.Rel a v w
⊢ Nonempty (witness M v ((·a) :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : M.Rel a v w
⊢ Nonempty (witness M v ((·a) :: γs) ξ)
Tactic:
constructor
Proof state after:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : M.Rel a v w
⊢ witness M v ((·a) :: γs) ξ
Theorem: existsWitnessPath_ltr
Proof state before:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : M.Rel a v w
⊢ witness M v ((·a) :: γs) ξ
Tactic:
apply witness.consAtom v_α_w w_wit
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α;'β) v w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
simp at *
Proof state after:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
rcases v_α_w with ⟨u, v_u, u_w⟩
Proof state after:
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
rcases IH w w_ with ⟨w_wit⟩
Proof state after:
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit✝ : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Theorem: existsWitnessPath_ltr
Proof state before:
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit✝ : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
constructor
Proof state after:
case intro.intro.intro.val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit✝ : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
w_wit : witness M w γs ξ
⊢ witness M v ((α;'β) :: γs) ξ
Theorem: existsWitnessPath_ltr
Proof state before:
case intro.intro.intro.val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit✝ : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
w_wit : witness M w γs ξ
⊢ witness M v ((α;'β) :: γs) ξ
Tactic:
sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α⋓β) v w
⊢ Nonempty (witness M v ((α⋓β) :: γs) ξ)
Tactic:
constructor
Proof state after:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α⋓β) v w
⊢ witness M v ((α⋓β) :: γs) ξ
Theorem: existsWitnessPath_ltr
Proof state before:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α⋓β) v w
⊢ witness M v ((α⋓β) :: γs) ξ
Tactic:
sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
τ : Formula
v_α_w : relate M (?'τ) v w
⊢ Nonempty (witness M v ((?'τ) :: γs) ξ)
Tactic:
constructor
Proof state after:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
τ : Formula
v_α_w : relate M (?'τ) v w
⊢ witness M v ((?'τ) :: γs) ξ
Theorem: existsWitnessPath_ltr
Proof state before:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
τ : Formula
v_α_w : relate M (?'τ) v w
⊢ witness M v ((?'τ) :: γs) ξ
Tactic:
sorry
Proof state after:
no goals
Theorem: existsWitnessPath_ltr
Proof state before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
β : Program
v_α_w : relate M (∗β) v w
⊢ Nonempty (witness M v ((∗β) :: γs) ξ)
Tactic:
constructor
Proof state after:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
β : Program
v_α_w : relate M (∗β) v w
⊢ witness M v ((∗β) :: γs) ξ
Theorem: existsWitnessPath_ltr
Proof state before:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
β : Program
v_α_w : relate M (∗β) v w
⊢ witness M v ((∗β) :: γs) ξ
Tactic:
sorry
Proof state after:
no goals
Theorem: existsWitnessPath
Proof state before:
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) ↔ Nonempty (witness M v δ ξ)
Tactic:
constructor
Proof state after:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)

case mpr
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ Nonempty (witness M v δ ξ) → (M, v)⊨(~⌈⌈δ⌉⌉ξ)
Theorem: existsWitnessPath
Proof state before:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Tactic:
simp [modelCanSemImplyForm, evaluatePoint] at *
Proof state after:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Theorem: existsWitnessPath
Proof state before:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Tactic:
have := existsWitnessPath_ltr M v δ ξ
Proof state after:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
this : evaluate M v (~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Theorem: existsWitnessPath
Proof state before:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
this : evaluate M v (~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Tactic:
simp_all
Proof state after:
no goals
Theorem: existsWitnessPath
Proof state before:
case mpr
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ Nonempty (witness M v δ ξ) → (M, v)⊨(~⌈⌈δ⌉⌉ξ)
Tactic:
rintro ⟨wit⟩
Proof state after:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ)