Theorem: inductionAxiom (Pdl/Examples.lean)

State before:
a : Program
φ : Formula
⊢ tautology (~(φ⋀⌈∗a⌉~φ⋀(~⌈a⌉φ))⋀(~⌈∗a⌉φ))
Tactic:
intro W M w
State after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(φ⋀⌈∗a⌉~φ⋀(~⌈a⌉φ))⋀(~⌈∗a⌉φ))

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(φ⋀⌈∗a⌉~φ⋀(~⌈a⌉φ))⋀(~⌈∗a⌉φ))
Tactic:
simp
State after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w φ →
    (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
      ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w φ →
    (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
      ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Tactic:
intro Mwφ
State after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
⊢ (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
    ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
⊢ (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
    ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Tactic:
intro MwStarImpHyp
State after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
⊢ ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
⊢ ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Tactic:
intro x w_starA_x
State after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
w_starA_x : Relation.ReflTransGen (relate M a) w x
⊢ evaluate M x φ

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
w_starA_x : Relation.ReflTransGen (relate M a) w x
⊢ evaluate M x φ
Tactic:
rw [starIffFinitelyManyStepsModel] at w_starA_x
State after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
w_starA_x : ∃ n ys, w = ys.head ∧ x = ys.last ∧ ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M x φ

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
w_starA_x : ∃ n ys, w = ys.head ∧ x = ys.last ∧ ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M x φ
Tactic:
rcases w_starA_x with ⟨n, ys, w_is_head, x_is_last, i_a_isucc⟩
State after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M x φ

State before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : ∀ (i : Fin n.succ), evaluate M (ys.get i) φ
⊢ evaluate M x φ
Tactic:
specialize claim n.succ
State after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M (ys.get ↑n.succ) φ
⊢ evaluate M x φ

State before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M (ys.get ↑n.succ) φ
⊢ evaluate M x φ
Tactic:
simp at claim
State after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ evaluate M x φ

State before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ evaluate M x φ
Tactic:
have x_is_ys_nsucc : x = ys.get (n + 1) :=
  by
  simp [Vector.last_def] at x_is_last
  sorry
State after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
x_is_ys_nsucc : x = ys.get (↑n + 1)
⊢ evaluate M x φ

State before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
x_is_ys_nsucc : x = ys.get (↑n + 1)
⊢ evaluate M x φ
Tactic:
rw [x_is_ys_nsucc]
State after:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
x_is_ys_nsucc : x = ys.get (↑n + 1)
⊢ evaluate M (ys.get (↑n + 1)) φ

State before:
case intro.intro.intro.intro
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
x_is_ys_nsucc : x = ys.get (↑n + 1)
⊢ evaluate M (ys.get (↑n + 1)) φ
Tactic:
sorry
State after:
no goals

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ ∀ (i : Fin n.succ), evaluate M (ys.get i) φ
Tactic:
apply Fin.induction
State after:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get 0) φ

case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ ∀ (i : Fin n), evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ

State before:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get 0) φ
Tactic:
simp
State after:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M ys.head φ

State before:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M ys.head φ
Tactic:
rw [← w_is_head]
State after:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M w φ

State before:
case zero
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M w φ
Tactic:
exact Mwφ
State after:
no goals

State before:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ ∀ (i : Fin n), evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Tactic:
intro i
State after:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
i : Fin n
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ

State before:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
i : Fin n
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Tactic:
specialize i_a_isucc i
State after:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ

State before:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
Tactic:
intro sat_phi
State after:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
sat_phi : evaluate M (ys.get i.castSucc) φ
⊢ evaluate M (ys.get i.succ) φ

State before:
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
sat_phi : evaluate M (ys.get i.castSucc) φ
⊢ evaluate M (ys.get i.succ) φ
Tactic:
sorry
State after:
no goals

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ x = ys.get (↑n + 1)
Tactic:
simp [Vector.last_def] at x_is_last
State after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.get (Fin.last n)
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ x = ys.get (↑n + 1)

State before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.get (Fin.last n)
i_a_isucc : ∀ (i : Fin n), relate M a (ys.get i.castSucc) (ys.get i.succ)
claim : evaluate M ys.head φ
⊢ x = ys.get (↑n + 1)
Tactic:
sorry
State after:
no goals