internlm/Lean-Github huggingface dataset:
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ
Tactic:
simp only [hasType_lambda] at h ⊢
Proof state after:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : ∃ σ_1, σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: Γ ⊢[T] a✝ ∶ σ_1)
⊢ ∃ σ_1, σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: (Γ ++ Δ) ⊢[T] a✝ ∶ σ_1)
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : ∃ σ_1, σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: Γ ⊢[T] a✝ ∶ σ_1)
⊢ ∃ σ_1, σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: (Γ ++ Δ) ⊢[T] a✝ ∶ σ_1)
Tactic:
obtain ⟨σ, rfl, h⟩ := h
Proof state after:
case intro.intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : a✝¹ :: Γ ⊢[T] a✝ ∶ σ
⊢ ∃ σ_1, LambdaType.lambda a✝² a✝¹ σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: (Γ ++ Δ) ⊢[T] a✝ ∶ σ_1)
Theorem: LambdaCalculi.append_hasType
Proof state before:
case intro.intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : a✝¹ :: Γ ⊢[T] a✝ ∶ σ
⊢ ∃ σ_1, LambdaType.lambda a✝² a✝¹ σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: (Γ ++ Δ) ⊢[T] a✝ ∶ σ_1)
Tactic:
exact ⟨σ, rfl, ih h⟩
Proof state after:
no goals
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C✝
ih₁ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝² ∶ σ) → (Γ ++ Δ ⊢[T] a✝² ∶ σ)
ih₂ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
Tactic:
simp only [hasType_case] at h ⊢
Proof state after:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C✝
ih₁ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝² ∶ σ) → (Γ ++ Δ ⊢[T] a✝² ∶ σ)
ih₂ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : ∃ τ₁ τ₂, (Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ σ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ σ)
⊢ ∃ τ₁ τ₂,
    (Γ ++ Δ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: (Γ ++ Δ) ⊢[T] a✝² ∶ σ) ∧ (τ₂ :: (Γ ++ Δ) ⊢[T] a✝¹ ∶ σ)
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C✝
ih₁ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝² ∶ σ) → (Γ ++ Δ ⊢[T] a✝² ∶ σ)
ih₂ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : ∃ τ₁ τ₂, (Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ σ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ σ)
⊢ ∃ τ₁ τ₂,
    (Γ ++ Δ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: (Γ ++ Δ) ⊢[T] a✝² ∶ σ) ∧ (τ₂ :: (Γ ++ Δ) ⊢[T] a✝¹ ∶ σ)
Tactic:
obtain ⟨σ₁, σ₂, h, h₁, h₂⟩ := h
Proof state after:
case intro.intro.intro.intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C✝
ih₁ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝² ∶ σ) → (Γ ++ Δ ⊢[T] a✝² ∶ σ)
ih₂ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ σ₁ σ₂ : LambdaType p U
h : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
h₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
h₂ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
⊢ ∃ τ₁ τ₂,
    (Γ ++ Δ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: (Γ ++ Δ) ⊢[T] a✝² ∶ σ) ∧ (τ₂ :: (Γ ++ Δ) ⊢[T] a✝¹ ∶ σ)
Theorem: LambdaCalculi.append_hasType
Proof state before:
case intro.intro.intro.intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C✝
ih₁ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝² ∶ σ) → (Γ ++ Δ ⊢[T] a✝² ∶ σ)
ih₂ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ σ₁ σ₂ : LambdaType p U
h : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
h₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
h₂ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
⊢ ∃ τ₁ τ₂,
    (Γ ++ Δ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: (Γ ++ Δ) ⊢[T] a✝² ∶ σ) ∧ (τ₂ :: (Γ ++ Δ) ⊢[T] a✝¹ ∶ σ)
Tactic:
exact ⟨σ₁, σ₂, ih h, ih₁ h₁, ih₂ h₂⟩
Proof state after:
no goals
Theorem: LambdaCalculi.append_hasType
Proof state before:
case elim
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.empty = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
a_ih✝ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
Tactic:
aesop
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_of_append_hasType
Proof state before:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.var a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var a✝ ∶ σ
Tactic:
case var =>
  simp only [hasType_var, List.length_append] at h ⊢
  obtain ⟨_, rfl⟩ := h
  rw [LambdaTerm.freeVarRange_var, Nat.add_one_le_iff] at ht
  refine ⟨ht, ?_⟩
  rw [List.get_append]
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_of_append_hasType
Proof state before:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.var a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var a✝ ∶ σ
Tactic:
simp only [hasType_var, List.length_append] at h ⊢
Proof state after:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
h :
  ∃ (h : a✝ < List.length Γ + List.length Δ),
    σ = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
⊢ ∃ (h : a✝ < List.length Γ), σ = List.get Γ { val := a✝, isLt := h }
Theorem: LambdaCalculi.hasType_of_append_hasType
Proof state before:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
h :
  ∃ (h : a✝ < List.length Γ + List.length Δ),
    σ = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
⊢ ∃ (h : a✝ < List.length Γ), σ = List.get Γ { val := a✝, isLt := h }
Tactic:
obtain ⟨_, rfl⟩ := h
Proof state after:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ ∃ (h : a✝ < List.length Γ),
    List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := h }
Theorem: LambdaCalculi.hasType_of_append_hasType
Proof state before:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ ∃ (h : a✝ < List.length Γ),
    List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := h }
Tactic:
rw [LambdaTerm.freeVarRange_var, Nat.add_one_le_iff] at ht
Proof state after:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : a✝ < List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ ∃ (h : a✝ < List.length Γ),
    List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := h }
Theorem: LambdaCalculi.hasType_of_append_hasType
Proof state before:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : a✝ < List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ ∃ (h : a✝ < List.length Γ),
    List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := h }
Tactic:
refine ⟨ht, ?_⟩
Proof state after:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : a✝ < List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := ht }
Theorem: LambdaCalculi.hasType_of_append_hasType
Proof state before:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : a✝ < List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := ht }
Tactic:
rw [List.get_append]
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_of_append_hasType
Proof state before:
case elim
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.empty = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.elim a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
Tactic:
aesop
Proof state after:
no goals
Theorem: LambdaCalculi.concat_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.1008396
C✝ : Type u_1
T : C✝ → LambdaType p U
Γ : Context p U
t : LambdaTerm p U C✝
σ : LambdaType p U
h : Γ ⊢[T] t ∶ σ
τ : LambdaType p U
⊢ List.concat Γ τ ⊢[T] t ∶ σ
Tactic:
rw [List.concat_eq_append]
Proof state after:
p : LambdaParams
U : Type u_2
C : Type ?u.1008396
C✝ : Type u_1
T : C✝ → LambdaType p U
Γ : Context p U
t : LambdaTerm p U C✝
σ : LambdaType p U
h : Γ ⊢[T] t ∶ σ
τ : LambdaType p U
⊢ Γ ++ [τ] ⊢[T] t ∶ σ
Theorem: LambdaCalculi.concat_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.1008396
C✝ : Type u_1
T : C✝ → LambdaType p U
Γ : Context p U
t : LambdaTerm p U C✝
σ : LambdaType p U
h : Γ ⊢[T] t ∶ σ
τ : LambdaType p U
⊢ Γ ++ [τ] ⊢[T] t ∶ σ
Tactic:
exact append_hasType h [τ]
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_of_concat_hasType
Proof state before:
p : LambdaParams
U : Type ?u.1008576
C : Type ?u.1008579
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : List.concat Γ τ ⊢[T] t ∶ σ
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ Γ ⊢[T] t ∶ σ
Tactic:
rw [List.concat_eq_append] at h
Proof state after:
p : LambdaParams
U : Type ?u.1008576
C : Type ?u.1008579
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ++ [τ] ⊢[T] t ∶ σ
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ Γ ⊢[T] t ∶ σ
Theorem: LambdaCalculi.hasType_of_concat_hasType
Proof state before:
p : LambdaParams
U : Type ?u.1008576
C : Type ?u.1008579
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ++ [τ] ⊢[T] t ∶ σ
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ Γ ⊢[T] t ∶ σ
Tactic:
exact hasType_of_append_hasType h ht
Proof state after:
no goals
Theorem: LambdaCalculi.concat_hasType_iff
Proof state before:
p : LambdaParams
U : Type ?u.1008897
C : Type ?u.1008900
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ (List.concat Γ τ ⊢[T] t ∶ σ) ↔ (Γ ⊢[T] t ∶ σ)
Tactic:
rw [List.concat_eq_append]
Proof state after:
p : LambdaParams
U : Type ?u.1008897
C : Type ?u.1008900
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ (Γ ++ [τ] ⊢[T] t ∶ σ) ↔ (Γ ⊢[T] t ∶ σ)
Theorem: LambdaCalculi.concat_hasType_iff
Proof state before:
p : LambdaParams
U : Type ?u.1008897
C : Type ?u.1008900
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ (Γ ++ [τ] ⊢[T] t ∶ σ) ↔ (Γ ⊢[T] t ∶ σ)
Tactic:
exact append_hasType_iff ht
Proof state after:
no goals
Theorem: free_subst_of_not_free
Proof state before:
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free t
⊢ free (t[v := s]) = free t
Tactic:
rw [subst_eq_of_not_free h]
Proof state after:
no goals
Theorem: free_subst_eq
Proof state before:
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Tactic:
by_cases h : v ∈ free t
Proof state after:
case pos
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∈ free t
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}

case neg
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free t
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Theorem: free_subst_eq
Proof state before:
case pos
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∈ free t
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Tactic:
simp [free_subst_of_free, h]
Proof state after:
no goals
Theorem: free_subst_eq
Proof state before:
case neg
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free t
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Tactic:
simp [subst_eq_of_not_free, h]
Proof state after:
no goals
Theorem: not_mem_free_of_subst
Proof state before:
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free s
⊢ v ∉ free (t[v := s])
Tactic:
rw [free_subst_eq]
Proof state after:
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free s
⊢ v ∉ free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Theorem: not_mem_free_of_subst
Proof state before:
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free s
⊢ v ∉ free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Tactic:
simp_all
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_some
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
t u : LambdaTerm p U C
h : f n t = some u
⊢ replace' f n t = u
Tactic:
cases t <;> simp only [h, replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_const
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
c : C
⊢ replace' f n (const c) =
    match f n (const c) with
    | some u => u
    | none => const c
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_var
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n m : ℕ
⊢ replace' f n (var m) =
    match f n (var m) with
    | some u => u
    | none => var m
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_lambda
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.lambda = true
τ : LambdaType p U
t : LambdaTerm p U C
⊢ replace' f n (lambda h τ t) =
    match f n (lambda h τ t) with
    | some u => u
    | none => lambda h τ (replace' f (n + 1) t)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_app
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.lambda = true
l r : LambdaTerm p U C
⊢ replace' f n (app h l r) =
    match f n (app h l r) with
    | some u => u
    | none => app h (replace' f n l) (replace' f n r)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_pair
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.prod = true
l r : LambdaTerm p U C
⊢ replace' f n (pair h l r) =
    match f n (pair h l r) with
    | some u => u
    | none => pair h (replace' f n l) (replace' f n r)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_fst
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.prod = true
t : LambdaTerm p U C
⊢ replace' f n (fst h t) =
    match f n (fst h t) with
    | some u => u
    | none => fst h (replace' f n t)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_snd
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.prod = true
t : LambdaTerm p U C
⊢ replace' f n (snd h t) =
    match f n (snd h t) with
    | some u => u
    | none => snd h (replace' f n t)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_inl
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.coprod = true
τ : LambdaType p U
l : LambdaTerm p U C
⊢ replace' f n (inl h τ l) =
    match f n (inl h τ l) with
    | some u => u
    | none => inl h τ (replace' f n l)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_inr
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.coprod = true
τ : LambdaType p U
r : LambdaTerm p U C
⊢ replace' f n (inr h τ r) =
    match f n (inr h τ r) with
    | some u => u
    | none => inr h τ (replace' f n r)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_case
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.coprod = true
l r t : LambdaTerm p U C
⊢ replace' f n (case h l r t) =
    match f n (case h l r t) with
    | some u => u
    | none => case h (replace' f (n + 1) l) (replace' f (n + 1) r) (replace' f n t)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_star
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.unit = true
⊢ replace' f n (star h) =
    match f n (star h) with
    | some u => u
    | none => star h
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.replace'_elim
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.empty = true
τ : LambdaType p U
t : LambdaTerm p U C
⊢ replace' f n (elim h τ t) =
    match f n (elim h τ t) with
    | some u => u
    | none => elim h τ (replace' f n t)
Tactic:
simp only [replace']
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.instantiate'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
m n : ℕ
h : m + 1 ≤ n
⊢ replace' (instantiateFun t) n (var m) = var m
Tactic:
case var m =>
  rw [Nat.add_one_le_iff] at h
  rw [replace'_var, instantiateFun]
  aesop
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.instantiate'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
m n : ℕ
h : m + 1 ≤ n
⊢ replace' (instantiateFun t) n (var m) = var m
Tactic:
rw [Nat.add_one_le_iff] at h
Proof state after:
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
m n : ℕ
h : m < n
⊢ replace' (instantiateFun t) n (var m) = var m
Theorem: LambdaCalculi.LambdaTerm.instantiate'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
m n : ℕ
h : m < n
⊢ replace' (instantiateFun t) n (var m) = var m
Tactic:
rw [replace'_var, instantiateFun]
Proof state after:
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
m n : ℕ
h : m < n
⊢ (match
      match var m with
      | var m => some (if m = n then t else if m < n then var m else var (m - 1))
      | x => none with
    | some u => u
    | none => var m) =
    var m