Theorem: existsWitnessPath_rtl (Pdl/Paths.lean)

State before:
W : Type
M : KripkeModel W
n : ℕ
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
induction n
State after:
case zero
W : Type
M : KripkeModel W
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = 0 → evaluate M v (~⌈⌈δ⌉⌉ξ)

case succ
W : Type
M : KripkeModel W
n✝ : ℕ
a✝ : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n✝ → evaluate M v (~⌈⌈δ⌉⌉ξ)
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n✝ + 1 → evaluate M v (~⌈⌈δ⌉⌉ξ)

State before:
W : Type
M : KripkeModel W
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = 0 → evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
case zero =>
  intro v δ ξ wit def_n
  subst_eqs
  cases wit
  case nil =>
    subst_eqs
    simp [Formula.boxes, evaluate] at *
    assumption
  all_goals
    exfalso
    simp [witness.length] at *
State after:
no goals

State before:
W : Type
M : KripkeModel W
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = 0 → evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
intro v δ ξ wit def_n
State after:
W : Type
M : KripkeModel W
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = 0
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)

State before:
W : Type
M : KripkeModel W
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = 0
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
cases wit
State after:
case nil
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = 0
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)

case consAtom
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝¹ : ℕ
v1✝ : W
γs✝ : List Program
v0_a_v1✝ : M.Rel a✝¹ v v1✝
a✝ : witness M v1✝ γs✝ ξ
def_n : (witness.consAtom v0_a_v1✝ a✝).length = 0
⊢ evaluate M v (~⌈⌈(·a✝¹) :: γs✝⌉⌉ξ)

case consEmpty
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
γs✝ : List Program
Fs✝ : List Formula
a✝² : (Fs✝, ε) ∈ H α✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v γs✝ ξ
def_n : (witness.consEmpty Fs✝ a✝² a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

State before:
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = 0
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
case nil =>
  subst_eqs
  simp [Formula.boxes, evaluate] at *
  assumption
State after:
no goals

State before:
case consAtom
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝¹ : ℕ
v1✝ : W
γs✝ : List Program
v0_a_v1✝ : M.Rel a✝¹ v v1✝
a✝ : witness M v1✝ γs✝ ξ
def_n : (witness.consAtom v0_a_v1✝ a✝).length = 0
⊢ evaluate M v (~⌈⌈(·a✝¹) :: γs✝⌉⌉ξ)

case consEmpty
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
γs✝ : List Program
Fs✝ : List Formula
a✝² : (Fs✝, ε) ∈ H α✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v γs✝ ξ
def_n : (witness.consEmpty Fs✝ a✝² a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)
Tactic:
all_goals
  exfalso
  simp [witness.length] at *
State after:
no goals

State before:
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = 0
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
subst_eqs
State after:
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)

State before:
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
simp [Formula.boxes, evaluate] at *
State after:
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ

State before:
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ
Tactic:
assumption
State after:
no goals

State before:
case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)
Tactic:
exfalso
State after:
case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ False

State before:
case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ False
Tactic:
simp [witness.length] at *
State after:
no goals

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n + 1 → evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
intro v δ ξ wit def_n
State after:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = n + 1
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = n + 1
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)
Tactic:
cases wit
State after:
case nil
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)

case consAtom
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝¹ : ℕ
v1✝ : W
γs✝ : List Program
v0_a_v1✝ : M.Rel a✝¹ v v1✝
a✝ : witness M v1✝ γs✝ ξ
def_n : (witness.consAtom v0_a_v1✝ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈(·a✝¹) :: γs✝⌉⌉ξ)

case consEmpty
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
α✝ : Program
γs✝ : List Program
Fs✝ : List Formula
a✝² : (Fs✝, ε) ∈ H α✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v γs✝ ξ
def_n : (witness.consEmpty Fs✝ a✝² a✝¹ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

case consComp
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
case nil =>
  exfalso
  subst_eqs
State after:
no goals

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : (witness.consAtom v0_a_v1 wit_v1_γs).length = n + 1
⊢ evaluate M v (~⌈⌈(·a) :: γs⌉⌉ξ)
Tactic:
case consAtom a v1 γs v0_a_v1 wit_v1_γs =>
  simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
  refine ⟨v1, v0_a_v1, IH v1 γs ξ wit_v1_γs ?_⟩
  linarith
State after:
no goals

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
Tactic:
exfalso
State after:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ False

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ False
Tactic:
subst_eqs
State after:
no goals

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : (witness.consAtom v0_a_v1 wit_v1_γs).length = n + 1
⊢ evaluate M v (~⌈⌈(·a) :: γs⌉⌉ξ)
Tactic:
simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
State after:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γ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, M.Rel a v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)

State before:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γ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, M.Rel a v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
Tactic:
refine ⟨v1, v0_a_v1, IH v1 γs ξ wit_v1_γs ?_⟩
State after:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γ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

State before:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γ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:
linarith
State after:
no goals

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : (witness.consEmpty Fs Fε_in_Hα v_Fs wit_γs).length = n + 1
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
Tactic:
simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
State after:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γ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⌉⌉ξ)

State before:
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γ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 v
State after:
case h
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v ∧ ¬evaluate M v (⌈⌈γs⌉⌉ξ)

State before:
case h
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v ∧ ¬evaluate M v (⌈⌈γs⌉⌉ξ)
Tactic:
constructor
State after:
case h.left
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v

case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v (⌈⌈γs⌉⌉ξ)

State before:
case h.left
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ relate M α v v
Tactic:
sorry
State after:
no goals

State before:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v (⌈⌈γs⌉⌉ξ)
Tactic:
apply IH v γs ξ wit_γs
State after:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ wit_γs.length = n

State before:
case h.right
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ wit_γs.length = n
Tactic:
linarith
State after:
no goals

State before:
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
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 : (witness.consComp v_a_v1 Fsaηs_in_Hα four wit_v1_ηγs).length = n + 1
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
Tactic:
simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
State after:
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⌉⌉ξ)

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
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⌉⌉ξ)

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
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⌉⌉ξ)

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
State after:
no goals

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 ?_
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⌉⌉ξ)

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
State after:
no goals

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
State after:
no goals