Theorem: LoVe.RTC.head_induction_on (LoVe/LoVelib.lean)

State before:
α : Type
R : α → α → Prop
b : α
P : (a : α) → RTC R a b → Prop
a : α
h : RTC R a b
refl : P b (_ : RTC R b b)
head : ∀ (a c : α) (h' : R a c) (h : RTC R c b), P c h → P a (_ : RTC R a b)
⊢ P a h
Tactic:
induction h with
| refl =>
  exact refl
| tail b' c _ hb'c ih =>
  apply ih (P := fun a hab' ↦ P a (RTC.tail _ _ hab' hb'c))
  { exact head _ _ hb'c _ refl }
  { intro x y hxy hyb' hy
    exact head _ _ hxy _ hy }
State after:
no goals

State before:
case refl
α : Type
R : α → α → Prop
b a : α
P : (a_1 : α) → RTC R a_1 a → Prop
refl : P a (_ : RTC R a a)
head : ∀ (a_1 c : α) (h' : R a_1 c) (h : RTC R c a), P c h → P a_1 (_ : RTC R a_1 a)
⊢ P a (_ : RTC R a a)
Tactic:
exact refl
State after:
no goals

State before:
case tail
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ P a (_ : RTC R a c)
Tactic:
apply ih (P := fun a hab' ↦ P a (RTC.tail _ _ hab' hb'c))
State after:
case tail.refl
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ P b' (_ : RTC R b' c)

case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)

State before:
case tail.refl
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ P b' (_ : RTC R b' c)

case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)
Tactic:
{ exact head _ _ hb'c _ refl }
State after:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)

State before:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)
Tactic:
{ intro x y hxy hyb' hy
  exact head _ _ hxy _ hy }
State after:
no goals

State before:
case tail.refl
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ P b' (_ : RTC R b' c)
Tactic:
exact head _ _ hb'c _ refl
State after:
no goals

State before:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)
Tactic:
intro x y hxy hyb' hy
State after:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
x y : α
hxy : R x y
hyb' : RTC R y b'
hy : P y (_ : RTC R y c)
⊢ P x (_ : RTC R x c)

State before:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
x y : α
hxy : R x y
hyb' : RTC R y b'
hy : P y (_ : RTC R y c)
⊢ P x (_ : RTC R x c)
Tactic:
exact head _ _ hxy _ hy
State after:
no goals