Theorem: Lean4Lean.ParRed.weakN (Lean4Lean/Theory/Typing/ParallelReduction.lean)

State before:
E : Extra
HE : Extra.IsWeakN E
n k : Nat
Γ Γ' : List VExpr
e1 e2 : VExpr
W : Ctx.LiftN n k Γ Γ'
H : ParRed E Γ e1 e2
⊢ ParRed E Γ' (liftN n e1 k) (liftN n e2 k)
Tactic:
induction H generalizing k Γ' with
| bvar | sort | const => exact rfl
| app _ _ ih1 ih2 => exact .app (ih1 W) (ih2 W)
| lam _ _ ih1 ih2 => exact .lam (ih1 W) (ih2 W.succ)
| forallE _ _ ih1 ih2 => exact .forallE (ih1 W) (ih2 W.succ)
| beta _ _ ih1 ih2 =>
  simp [liftN, liftN_inst_hi]
  exact .beta (ih1 W.succ) (ih2 W)
| extra _ ih =>
  refine .extra fun a a' h => ?_
  obtain ⟨_, _, h', rfl, rfl⟩ := HE W h
  exact ih _ _ h' W
State after:
no goals

State before:
case const
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
c✝ : Name
ls✝ : List VLevel
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.const c✝ ls✝) k) (liftN n (VExpr.const c✝ ls✝) k)
Tactic:
exact rfl
State after:
no goals

State before:
case app
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
f✝ f'✝ a✝² a'✝ : VExpr
a✝¹ : ParRed E Γ✝ f✝ f'✝
a✝ : ParRed E Γ✝ a✝² a'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n f✝ k) (liftN n f'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a✝² k) (liftN n a'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.app f✝ a✝²) k) (liftN n (VExpr.app f'✝ a'✝) k)
Tactic:
exact .app (ih1 W) (ih2 W)
State after:
no goals

State before:
case lam
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ A'✝ body✝ body'✝ : VExpr
a✝¹ : ParRed E Γ✝ A✝ A'✝
a✝ : ParRed E (A✝ :: Γ✝) body✝ body'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n A✝ k) (liftN n A'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n body✝ k) (liftN n body'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.lam A✝ body✝) k) (liftN n (VExpr.lam A'✝ body'✝) k)
Tactic:
exact .lam (ih1 W) (ih2 W.succ)
State after:
no goals

State before:
case forallE
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ A'✝ B✝ B'✝ : VExpr
a✝¹ : ParRed E Γ✝ A✝ A'✝
a✝ : ParRed E (A✝ :: Γ✝) B✝ B'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n A✝ k) (liftN n A'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n B✝ k) (liftN n B'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.forallE A✝ B✝) k) (liftN n (VExpr.forallE A'✝ B'✝) k)
Tactic:
exact .forallE (ih1 W) (ih2 W.succ)
State after:
no goals

State before:
case beta
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n e₁✝ k) (liftN n e₁'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n e₂✝ k) (liftN n e₂'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.app (VExpr.lam A✝ e₁✝) e₂✝) k) (liftN n (inst e₁'✝ e₂'✝) k)
Tactic:
simp [liftN, liftN_inst_hi]
State after:
case beta
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n e₁✝ k) (liftN n e₁'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n e₂✝ k) (liftN n e₂'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (VExpr.app (VExpr.lam (liftN n A✝ k) (liftN n e₁✝ (k + 1))) (liftN n e₂✝ k))
    (inst (liftN n e₁'✝ (k + 1)) (liftN n e₂'✝ k))

State before:
case beta
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n e₁✝ k) (liftN n e₁'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n e₂✝ k) (liftN n e₂'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (VExpr.app (VExpr.lam (liftN n A✝ k) (liftN n e₁✝ (k + 1))) (liftN n e₂✝ k))
    (inst (liftN n e₁'✝ (k + 1)) (liftN n e₂'✝ k))
Tactic:
exact .beta (ih1 W.succ) (ih2 W)
State after:
no goals

State before:
case extra
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n e✝ k) (liftN n e'✝ k)
Tactic:
refine .extra fun a a' h => ?_
State after:
case extra
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
a a' : VExpr
h : E Γ' (liftN n e✝ k) (liftN n e'✝ k) a a'
⊢ ParRed E Γ' a a'

State before:
case extra
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
a a' : VExpr
h : E Γ' (liftN n e✝ k) (liftN n e'✝ k) a a'
⊢ ParRed E Γ' a a'
Tactic:
obtain ⟨_, _, h', rfl, rfl⟩ := HE W h
State after:
case extra.intro.intro.intro.intro
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
w✝¹ w✝ : VExpr
h' : E Γ✝ e✝ e'✝ w✝¹ w✝
h : E Γ' (liftN n e✝ k) (liftN n e'✝ k) (liftN n w✝¹ k) (liftN n w✝ k)
⊢ ParRed E Γ' (liftN n w✝¹ k) (liftN n w✝ k)

State before:
case extra.intro.intro.intro.intro
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
w✝¹ w✝ : VExpr
h' : E Γ✝ e✝ e'✝ w✝¹ w✝
h : E Γ' (liftN n e✝ k) (liftN n e'✝ k) (liftN n w✝¹ k) (liftN n w✝ k)
⊢ ParRed E Γ' (liftN n w✝¹ k) (liftN n w✝ k)
Tactic:
exact ih _ _ h' W
State after:
no goals