Theorem: Lean4Lean.NormalEq.defeq (Lean4Lean/Theory/Typing/ParallelReduction.lean)

State before:
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
H : NormalEq TY Γ e1 e2
⊢ TY.IsDefEq Γ e1 e2
Tactic:
induction H with
| refl h => exact TY.refl h
| sortDF h1 h2 h3 => exact TY.sortDF h1 h2 h3
| appDF hf₁ _ ha₁ _ _ _ ih1 ih2 => exact TY.appDF hf₁ ih1 ha₁ ih2
| lamDF hA hA₁ _ _ ihA ihB =>
  have ⟨_, hB⟩ := TY.has_type ihB
  exact TY.trans (TY.symm <| TY.lamDF hA (TY.symm hA₁) (TY.refl hB))
    (TY.lamDF hA (TY.trans (TY.symm hA₁) ihA) ihB)
| forallEDF hA hA₁ _ hB₁ _ ihA ihB =>
  exact TY.trans (TY.symm <| TY.forallEDF hA (TY.symm hA₁) hB₁ (TY.refl hB₁))
    (TY.forallEDF hA (TY.trans (TY.symm hA₁) ihA) hB₁ ihB)
| etaL h1 _ ih =>
  have ⟨_, AB⟩ := TY.is_type h1
  have ⟨_, _, hA, _⟩ := TY.forallE_inv AB
  exact TY.trans (TY.lamDF hA (TY.refl hA) ih) (TY.eta h1)
| etaR h1 _ ih =>
  have ⟨_, AB⟩ := TY.is_type h1
  have ⟨_, _, hA, _⟩ := TY.forallE_inv AB
  exact TY.trans (TY.symm (TY.eta h1)) (TY.lamDF hA (TY.refl hA) ih)
| proofIrrel h1 h2 h3 => exact TY.proofIrrel h1 h2 h3
State after:
no goals

State before:
case refl
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ A✝ : VExpr
h : TY.HasType Γ✝ e✝ A✝
⊢ TY.IsDefEq Γ✝ e✝ e✝
Tactic:
exact TY.refl h
State after:
no goals

State before:
case sortDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
l₁✝ l₂✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF TY.univs l₁✝
h2 : VLevel.WF TY.univs l₂✝
h3 : l₁✝ ≈ l₂✝
⊢ TY.IsDefEq Γ✝ (sort l₁✝) (sort l₂✝)
Tactic:
exact TY.sortDF h1 h2 h3
State after:
no goals

State before:
case appDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
f₁✝ A✝ B✝ f₂✝ a₁✝ a₂✝ : VExpr
hf₁ : TY.HasType Γ✝ f₁✝ (forallE A✝ B✝)
a✝³ : TY.HasType Γ✝ f₂✝ (forallE A✝ B✝)
ha₁ : TY.HasType Γ✝ a₁✝ A✝
a✝² : TY.HasType Γ✝ a₂✝ A✝
a✝¹ : NormalEq TY Γ✝ f₁✝ f₂✝
a✝ : NormalEq TY Γ✝ a₁✝ a₂✝
ih1 : TY.IsDefEq Γ✝ f₁✝ f₂✝
ih2 : TY.IsDefEq Γ✝ a₁✝ a₂✝
⊢ TY.IsDefEq Γ✝ (app f₁✝ a₁✝) (app f₂✝ a₂✝)
Tactic:
exact TY.appDF hf₁ ih1 ha₁ ih2
State after:
no goals

State before:
case lamDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ body₁✝ body₂✝ : VExpr
hA : TY.HasType Γ✝ A✝ (sort u✝)
hA₁ : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
a✝ : NormalEq TY (A✝ :: Γ✝) body₁✝ body₂✝
ihA : TY.IsDefEq Γ✝ A₁✝ A₂✝
ihB : TY.IsDefEq (A✝ :: Γ✝) body₁✝ body₂✝
⊢ TY.IsDefEq Γ✝ (lam A₁✝ body₁✝) (lam A₂✝ body₂✝)
Tactic:
have ⟨_, hB⟩ := TY.has_type ihB
State after:
case lamDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ body₁✝ body₂✝ : VExpr
hA : TY.HasType Γ✝ A✝ (sort u✝)
hA₁ : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
a✝ : NormalEq TY (A✝ :: Γ✝) body₁✝ body₂✝
ihA : TY.IsDefEq Γ✝ A₁✝ A₂✝
ihB : TY.IsDefEq (A✝ :: Γ✝) body₁✝ body₂✝
w✝ : VExpr
hB : TY.HasType (A✝ :: Γ✝) body₁✝ w✝
⊢ TY.IsDefEq Γ✝ (lam A₁✝ body₁✝) (lam A₂✝ body₂✝)

State before:
case lamDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ body₁✝ body₂✝ : VExpr
hA : TY.HasType Γ✝ A✝ (sort u✝)
hA₁ : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
a✝ : NormalEq TY (A✝ :: Γ✝) body₁✝ body₂✝
ihA : TY.IsDefEq Γ✝ A₁✝ A₂✝
ihB : TY.IsDefEq (A✝ :: Γ✝) body₁✝ body₂✝
w✝ : VExpr
hB : TY.HasType (A✝ :: Γ✝) body₁✝ w✝
⊢ TY.IsDefEq Γ✝ (lam A₁✝ body₁✝) (lam A₂✝ body₂✝)
Tactic:
exact TY.trans (TY.symm <| TY.lamDF hA (TY.symm hA₁) (TY.refl hB))
  (TY.lamDF hA (TY.trans (TY.symm hA₁) ihA) ihB)
State after:
no goals

State before:
case forallEDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ B₁✝ : VExpr
v✝ : VLevel
B₂✝ : VExpr
hA : TY.HasType Γ✝ A✝ (sort u✝)
hA₁ : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
hB₁ : TY.HasType (A✝ :: Γ✝) B₁✝ (sort v✝)
a✝ : NormalEq TY (A✝ :: Γ✝) B₁✝ B₂✝
ihA : TY.IsDefEq Γ✝ A₁✝ A₂✝
ihB : TY.IsDefEq (A✝ :: Γ✝) B₁✝ B₂✝
⊢ TY.IsDefEq Γ✝ (forallE A₁✝ B₁✝) (forallE A₂✝ B₂✝)
Tactic:
exact TY.trans (TY.symm <| TY.forallEDF hA (TY.symm hA₁) hB₁ (TY.refl hB₁))
  (TY.forallEDF hA (TY.trans (TY.symm hA₁) ihA) hB₁ ihB)
State after:
no goals

State before:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝
Tactic:
have ⟨_, AB⟩ := TY.is_type h1
State after:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
w✝ : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝)
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝

State before:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
w✝ : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝)
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝
Tactic:
have ⟨_, _, hA, _⟩ := TY.forallE_inv AB
State after:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
w✝² : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝²)
w✝¹ w✝ : VLevel
hA : TY.HasType Γ✝ A✝ (sort w✝¹)
right✝ : TY.HasType (A✝ :: Γ✝) A✝ (sort w✝)
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝

State before:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : TY.IsDefEq (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
w✝² : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝²)
w✝¹ w✝ : VLevel
hA : TY.HasType Γ✝ A✝ (sort w✝¹)
right✝ : TY.HasType (A✝ :: Γ✝) A✝ (sort w✝)
⊢ TY.IsDefEq Γ✝ (lam A✝ e✝) e'✝
Tactic:
exact TY.trans (TY.lamDF hA (TY.refl hA) ih) (TY.eta h1)
State after:
no goals

State before:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)
Tactic:
have ⟨_, AB⟩ := TY.is_type h1
State after:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
w✝ : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝)
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)

State before:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
w✝ : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝)
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)
Tactic:
have ⟨_, _, hA, _⟩ := TY.forallE_inv AB
State after:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
w✝² : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝²)
w✝¹ w✝ : VLevel
hA : TY.HasType Γ✝ A✝ (sort w✝¹)
right✝ : TY.HasType (A✝ :: Γ✝) A✝ (sort w✝)
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)

State before:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : TY.IsDefEq (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
w✝² : VLevel
AB : TY.HasType Γ✝ (forallE A✝ B✝) (sort w✝²)
w✝¹ w✝ : VLevel
hA : TY.HasType Γ✝ A✝ (sort w✝¹)
right✝ : TY.HasType (A✝ :: Γ✝) A✝ (sort w✝)
⊢ TY.IsDefEq Γ✝ e'✝ (lam A✝ e✝)
Tactic:
exact TY.trans (TY.symm (TY.eta h1)) (TY.lamDF hA (TY.refl hA) ih)
State after:
no goals

State before:
case proofIrrel
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
h1 : TY.HasType Γ✝ p✝ (sort VLevel.zero)
h2 : TY.HasType Γ✝ h✝ p✝
h3 : TY.HasType Γ✝ h'✝ p✝
⊢ TY.IsDefEq Γ✝ h✝ h'✝
Tactic:
exact TY.proofIrrel h1 h2 h3
State after:
no goals