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

State before:
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
k : Nat
Γ₁ Γ : List VExpr
e1 e2 : VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ₁ Γ
H : ParRed E Γ₁ e1 e2
⊢ ParRed E Γ (inst e1 a1 k) (inst e2 a2 k)
Tactic:
induction H generalizing Γ k with
| @bvar _ i =>
  dsimp [inst]
  induction W generalizing i with
  | zero =>
    cases i with simp [inst_lift]
    | zero => exact H0
    | succ h => exact rfl
  | succ _ ih =>
    cases i with simp
    | zero => exact rfl
    | succ h => exact ih.weakN HE.1 .one
| 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 [inst, inst0_inst_hi]
  exact .beta (ih1 W.succ) (ih2 W)
| extra _ ih =>
  refine .extra fun a a' h => ?_
  obtain ⟨_, _, h', rfl, rfl⟩ := HE.2 W h
  exact ih _ _ h' W
State after:
no goals

State before:
case bvar
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
i k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.bvar i) a1 k) (inst (VExpr.bvar i) a2 k)
Tactic:
dsimp [inst]
State after:
case bvar
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
i k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (instVar i a1 k) (instVar i a2 k)

State before:
case bvar
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
i k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (instVar i a1 k) (instVar i a2 k)
Tactic:
induction W generalizing i with
| zero =>
  cases i with simp [inst_lift]
  | zero => exact H0
  | succ h => exact rfl
| succ _ ih =>
  cases i with simp
  | zero => exact rfl
  | succ h => exact ih.weakN HE.1 .one
State after:
no goals

State before:
case bvar.zero
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
i : Nat
⊢ ParRed E Γ₀ (instVar i a1) (instVar i a2)
Tactic:
cases i with simp [inst_lift]
| zero => exact H0
| succ h => exact rfl
State after:
no goals

State before:
case bvar.zero.zero
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
⊢ ParRed E Γ₀ a1 a2
Tactic:
exact H0
State after:
no goals

State before:
case bvar.zero.succ
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
h : Nat
⊢ ParRed E Γ₀ (VExpr.bvar h) (VExpr.bvar h)
Tactic:
exact rfl
State after:
no goals

State before:
case bvar.succ
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ a1 A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat}, ParRed E Γ'✝ (instVar i a1 k✝) (instVar i a2 k✝)
i : Nat
⊢ ParRed E (inst A✝ a1 k✝ :: Γ'✝) (instVar i a1 (k✝ + 1)) (instVar i a2 (k✝ + 1))
Tactic:
cases i with simp
| zero => exact rfl
| succ h => exact ih.weakN HE.1 .one
State after:
no goals

State before:
case bvar.succ.zero
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ a1 A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat}, ParRed E Γ'✝ (instVar i a1 k✝) (instVar i a2 k✝)
⊢ ParRed E (inst A✝ a1 k✝ :: Γ'✝) (VExpr.bvar 0) (VExpr.bvar 0)
Tactic:
exact rfl
State after:
no goals

State before:
case bvar.succ.succ
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ a1 A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat}, ParRed E Γ'✝ (instVar i a1 k✝) (instVar i a2 k✝)
h : Nat
⊢ ParRed E (inst A✝ a1 k✝ :: Γ'✝) (lift (instVar h a1 k✝)) (lift (instVar h a2 k✝))
Tactic:
exact ih.weakN HE.1 .one
State after:
no goals

State before:
case const
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
c✝ : Name
ls✝ : List VLevel
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.const c✝ ls✝) a1 k) (inst (VExpr.const c✝ ls✝) a2 k)
Tactic:
exact rfl
State after:
no goals

State before:
case app
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst f✝ a1 k) (inst f'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a✝² a1 k) (inst a'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.app f✝ a✝²) a1 k) (inst (VExpr.app f'✝ a'✝) a2 k)
Tactic:
exact .app (ih1 W) (ih2 W)
State after:
no goals

State before:
case lam
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst A✝ a1 k) (inst A'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst body✝ a1 k) (inst body'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.lam A✝ body✝) a1 k) (inst (VExpr.lam A'✝ body'✝) a2 k)
Tactic:
exact .lam (ih1 W) (ih2 W.succ)
State after:
no goals

State before:
case forallE
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst A✝ a1 k) (inst A'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst B✝ a1 k) (inst B'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.forallE A✝ B✝) a1 k) (inst (VExpr.forallE A'✝ B'✝) a2 k)
Tactic:
exact .forallE (ih1 W) (ih2 W.succ)
State after:
no goals

State before:
case beta
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst e₁✝ a1 k) (inst e₁'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst e₂✝ a1 k) (inst e₂'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.app (VExpr.lam A✝ e₁✝) e₂✝) a1 k) (inst (inst e₁'✝ e₂'✝) a2 k)
Tactic:
simp [inst, inst0_inst_hi]
State after:
case beta
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst e₁✝ a1 k) (inst e₁'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst e₂✝ a1 k) (inst e₂'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (VExpr.app (VExpr.lam (inst A✝ a1 k) (inst e₁✝ a1 (k + 1))) (inst e₂✝ a1 k))
    (inst (inst e₁'✝ a2 (k + 1)) (inst e₂'✝ a2 k))

State before:
case beta
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst e₁✝ a1 k) (inst e₁'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst e₂✝ a1 k) (inst e₂'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (VExpr.app (VExpr.lam (inst A✝ a1 k) (inst e₁✝ a1 (k + 1))) (inst e₂✝ a1 k))
    (inst (inst e₁'✝ a2 (k + 1)) (inst e₂'✝ a2 k))
Tactic:
exact .beta (ih1 W.succ) (ih2 W)
State after:
no goals

State before:
case extra
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst e✝ a1 k) (inst e'✝ a2 k)
Tactic:
refine .extra fun a a' h => ?_
State after:
case extra
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
a a' : VExpr
h : E Γ (inst e✝ a1 k) (inst e'✝ a2 k) a a'
⊢ ParRed E Γ a a'

State before:
case extra
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
a a' : VExpr
h : E Γ (inst e✝ a1 k) (inst e'✝ a2 k) a a'
⊢ ParRed E Γ a a'
Tactic:
obtain ⟨_, _, h', rfl, rfl⟩ := HE.2 W h
State after:
case extra.intro.intro.intro.intro
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
w✝¹ w✝ : VExpr
h' : E Γ✝ e✝ e'✝ w✝¹ w✝
h : E Γ (inst e✝ a1 k) (inst e'✝ a2 k) (inst w✝¹ a1 k) (inst w✝ a2 k)
⊢ ParRed E Γ (inst w✝¹ a1 k) (inst w✝ a2 k)

State before:
case extra.intro.intro.intro.intro
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : 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.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
w✝¹ w✝ : VExpr
h' : E Γ✝ e✝ e'✝ w✝¹ w✝
h : E Γ (inst e✝ a1 k) (inst e'✝ a2 k) (inst w✝¹ a1 k) (inst w✝ a2 k)
⊢ ParRed E Γ (inst w✝¹ a1 k) (inst w✝ a2 k)
Tactic:
exact ih _ _ h' W
State after:
no goals