Theorem: ReflTransGen.to_finitelyManySteps (Pdl/Star.lean)

State before:
α : Type u_1
x z : α
r : α → α → Prop
h : Relation.ReflTransGen r x z
⊢ ∃ n ys, x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
induction h using Relation.ReflTransGen.head_induction_on
State after:
case refl
α : Type u_1
x z : α
r : α → α → Prop
⊢ ∃ n ys, z = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)

case head
α : Type u_1
x z : α
r : α → α → Prop
a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : Relation.ReflTransGen r c✝ z
a✝ : ∃ n ys, c✝ = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
⊢ ∃ n ys, a✝¹ = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)

State before:
α : Type u_1
x z : α
r : α → α → Prop
⊢ ∃ n ys, z = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
case refl =>
  use 0, Vector.cons z Vector.nil
  aesop
State after:
no goals

State before:
α : Type u_1
x z : α
r : α → α → Prop
⊢ ∃ n ys, z = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
use 0, Vector.cons z Vector.nil
State after:
case h
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = (z ::ᵥ Vector.nil).head ∧
    z = (z ::ᵥ Vector.nil).last ∧ ∀ (i : Fin 0), r ((z ::ᵥ Vector.nil).get i.castSucc) ((z ::ᵥ Vector.nil).get i.succ)

State before:
case h
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = (z ::ᵥ Vector.nil).head ∧
    z = (z ::ᵥ Vector.nil).last ∧ ∀ (i : Fin 0), r ((z ::ᵥ Vector.nil).get i.castSucc) ((z ::ᵥ Vector.nil).get i.succ)
Tactic:
aesop
State after:
no goals

State before:
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
IH_b_z : ∃ n ys, b = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
⊢ ∃ n ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
rcases IH_b_z with ⟨m, zs, b_is_head_zs, z_is_last_zs, zs_steps⟩
State after:
case intro.intro.intro.intro
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∃ n ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)

State before:
case intro.intro.intro.intro
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∃ n ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
use m + 1
State after:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∃ ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin (m + 1)), r (ys.get i.castSucc) (ys.get i.succ)

State before:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∃ ys, a = ys.head ∧ z = ys.last ∧ ∀ (i : Fin (m + 1)), r (ys.get i.castSucc) (ys.get i.succ)
Tactic:
use a ::ᵥ zs
State after:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ a = (a ::ᵥ zs).head ∧ z = (a ::ᵥ zs).last ∧ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) ((a ::ᵥ zs).get i.succ)

State before:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ a = (a ::ᵥ zs).head ∧ z = (a ::ᵥ zs).last ∧ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) ((a ::ᵥ zs).get i.succ)
Tactic:
simp only [Vector.head_cons, Vector.get_cons_succ, true_and]
State after:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ z = (a ::ᵥ zs).last ∧ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) (zs.get i)

State before:
case h
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ z = (a ::ᵥ zs).last ∧ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) (zs.get i)
Tactic:
constructor
State after:
case h.left
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ z = (a ::ᵥ zs).last

case h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) (zs.get i)

State before:
case h.left
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ z = (a ::ᵥ zs).last
Tactic:
aesop
State after:
no goals

State before:
case h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ ∀ (i : Fin (m + 1)), r ((a ::ᵥ zs).get i.castSucc) (zs.get i)
Tactic:
intro i
State after:
case h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i : Fin (m + 1)
⊢ r ((a ::ᵥ zs).get i.castSucc) (zs.get i)

State before:
case h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i : Fin (m + 1)
⊢ r ((a ::ᵥ zs).get i.castSucc) (zs.get i)
Tactic:
induction i using Fin.induction
State after:
case h.right.zero
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ r ((a ::ᵥ zs).get (Fin.castSucc 0)) (zs.get 0)

case h.right.succ
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i✝ : Fin m
a✝ : r ((a ::ᵥ zs).get i✝.castSucc.castSucc) (zs.get i✝.castSucc)
⊢ r ((a ::ᵥ zs).get i✝.succ.castSucc) (zs.get i✝.succ)

State before:
case h.right.zero
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ r ((a ::ᵥ zs).get (Fin.castSucc 0)) (zs.get 0)

case h.right.succ
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i✝ : Fin m
a✝ : r ((a ::ᵥ zs).get i✝.castSucc.castSucc) (zs.get i✝.castSucc)
⊢ r ((a ::ᵥ zs).get i✝.succ.castSucc) (zs.get i✝.succ)
Tactic:
all_goals aesop
State after:
no goals

State before:
case h.right.succ
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i✝ : Fin m
a✝ : r ((a ::ᵥ zs).get i✝.castSucc.castSucc) (zs.get i✝.castSucc)
⊢ r ((a ::ᵥ zs).get i✝.succ.castSucc) (zs.get i✝.succ)
Tactic:
aesop
State after:
no goals