internlm/Lean-Github huggingface dataset:
Theorem: ctxtTypeOfPreservation
Proof state before:
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
Γ Γ' : TCtxt V 𝕍
h : ∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ'
⊢ typeOf Γ (Λ.Var x) = typeOf Γ' (Λ.Var x)
Tactic:
apply h
Proof state after:
case Var.a
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
Γ Γ' : TCtxt V 𝕍
h : ∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ'
⊢ x ∈ freeVarsOfTerm (Λ.Var x)
Theorem: ctxtTypeOfPreservation
Proof state before:
case Var.a
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
Γ Γ' : TCtxt V 𝕍
h : ∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ'
⊢ x ∈ freeVarsOfTerm (Λ.Var x)
Tactic:
simp
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
⊢ ∀ {Γ Γ' : TCtxt V 𝕍},
    (∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ') →
      typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Tactic:
intro Γ Γ' h
Proof state after:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Theorem: ctxtTypeOfPreservation
Proof state before:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Tactic:
have h₁ (x : V) (h' : x ∈ freeVarsOfTerm M) : getType x Γ = getType x Γ' := by
  exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', true_or])
Proof state after:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Theorem: ctxtTypeOfPreservation
Proof state before:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Tactic:
have h₂ (x : V) (h' : x ∈ freeVarsOfTerm N) : getType x Γ = getType x Γ' := by
  exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', or_true])
Proof state after:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
h₂ : ∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Theorem: ctxtTypeOfPreservation
Proof state before:
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
h₂ : ∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
Tactic:
simp [ih₁ h₁, ih₂ h₂]
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
⊢ getType x Γ = getType x Γ'
Tactic:
exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', true_or])
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
⊢ x ∈ freeVarsOfTerm (Λ.App M N)
Tactic:
simp only [freeVarsOfTerm, Finset.mem_union, h', true_or]
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm N
⊢ getType x Γ = getType x Γ'
Tactic:
exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', or_true])
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm N
⊢ x ∈ freeVarsOfTerm (Λ.App M N)
Tactic:
simp only [freeVarsOfTerm, Finset.mem_union, h', or_true]
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
⊢ ∀ {Γ Γ' : TCtxt V 𝕍},
    (∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ') →
      typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
Tactic:
intro Γ Γ' h
Proof state after:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
Theorem: ctxtTypeOfPreservation
Proof state before:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
Tactic:
have h (x : V) (h' : x ∈ freeVarsOfTerm M) : getType x (Γ;; y : σ) = getType x (Γ';; y : σ) := by
  by_cases h'' : x = y <;> simp[h'']
  exact h x (Finset.mem_erase_of_ne_of_mem h'' h')
Proof state after:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h✝ : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
h : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x (Γ;; y : σ) = getType x (Γ';; y : σ)
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
Theorem: ctxtTypeOfPreservation
Proof state before:
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h✝ : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
h : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x (Γ;; y : σ) = getType x (Γ';; y : σ)
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
Tactic:
simp [ih h]
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
⊢ getType x (Γ;; y : σ) = getType x (Γ';; y : σ)
Tactic:
by_cases h'' : x = y <;> simp[h'']
Proof state after:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
h'' : ¬x = y
⊢ getType x Γ = getType x Γ'
Theorem: ctxtTypeOfPreservation
Proof state before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm M
h'' : ¬x = y
⊢ getType x Γ = getType x Γ'
Tactic:
exact h x (Finset.mem_erase_of_ne_of_mem h'' h')
Proof state after:
no goals
Theorem: var_rule
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x : V
σ : 𝕋 𝕍
⊢ getType x Γ = some σ ↔ (Γ ⊢ Λ.Var x : σ)
Tactic:
simp
Proof state after:
no goals
Theorem: appl_rule
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
⊢ (∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)) ↔ (Γ ⊢ Λ.App M N : τ)
Tactic:
apply Iff.intro
Proof state after:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
⊢ (∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)) → (Γ ⊢ Λ.App M N : τ)

case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
⊢ (Γ ⊢ Λ.App M N : τ) → ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
⊢ (∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)) → (Γ ⊢ Λ.App M N : τ)
Tactic:
rintro ⟨σ, h, h'⟩
Proof state after:
case mp.intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ σ : 𝕋 𝕍
h : Γ ⊢ M : σ →' τ
h' : Γ ⊢ N : σ
⊢ Γ ⊢ Λ.App M N : τ
Theorem: appl_rule
Proof state before:
case mp.intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ σ : 𝕋 𝕍
h : Γ ⊢ M : σ →' τ
h' : Γ ⊢ N : σ
⊢ Γ ⊢ Λ.App M N : τ
Tactic:
unfold typingJudgement at *
Proof state after:
case mp.intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ σ : 𝕋 𝕍
h : typeOf Γ M = some (σ →' τ)
h' : typeOf Γ N = some σ
⊢ typeOf Γ (Λ.App M N) = some τ
Theorem: appl_rule
Proof state before:
case mp.intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ σ : 𝕋 𝕍
h : typeOf Γ M = some (σ →' τ)
h' : typeOf Γ N = some σ
⊢ typeOf Γ (Λ.App M N) = some τ
Tactic:
simp [h, h']
Proof state after:
no goals
Theorem: appl_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
⊢ (Γ ⊢ Λ.App M N : τ) → ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
intro h
Proof state after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h : Γ ⊢ Λ.App M N : τ
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h : Γ ⊢ Λ.App M N : τ
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
simp only [typingJudgement, typeOf] at h
Proof state after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h :
  (match typeOf Γ M with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h :
  (match typeOf Γ M with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
generalize h' : typeOf Γ M = x
Proof state after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h :
  (match typeOf Γ M with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
x : Option (𝕋 𝕍)
h' : typeOf Γ M = x
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h :
  (match typeOf Γ M with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
x : Option (𝕋 𝕍)
h' : typeOf Γ M = x
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
rw [h'] at h
Proof state after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
h :
  (match x with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = x
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
h :
  (match x with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = x
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
match x with
  | none => simp at h
  | some val => 
    match val with
    | .To σ τ' => 
      use σ
      simp only at h 
      split_ifs at h with h''
      simp only [Option.some.injEq] at h 
      rw [h] at h'
      exact ⟨h', h''⟩
Proof state after:
no goals
Theorem: appl_rule
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
h :
  (match none with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = none
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
simp at h
Proof state after:
no goals
Theorem: appl_rule
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val : 𝕋 𝕍
h :
  (match some val with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = some val
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
match val with
| .To σ τ' => 
  use σ
  simp only at h 
  split_ifs at h with h''
  simp only [Option.some.injEq] at h 
  rw [h] at h'
  exact ⟨h', h''⟩
Proof state after:
no goals
Theorem: appl_rule
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h :
  (match some (σ →' τ') with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
use σ
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h :
  (match some (σ →' τ') with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h :
  (match some (σ →' τ') with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
simp only at h
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h : (if typeOf Γ N = some σ then some τ' else none) = some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h : (if typeOf Γ N = some σ then some τ' else none) = some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
split_ifs at h with h''
Proof state after:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : some τ' = some τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : some τ' = some τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
simp only [Option.some.injEq] at h
Proof state after:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : τ' = τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : τ' = τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
rw [h] at h'
Proof state after:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ)
h'' : typeOf Γ N = some σ
h : τ' = τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Theorem: appl_rule
Proof state before:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ)
h'' : typeOf Γ N = some σ
h : τ' = τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
Tactic:
exact ⟨h', h''⟩
Proof state after:
no goals
Theorem: abst_rule
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ ((Γ;; x : σ) ⊢ M : τ) ↔ (Γ ⊢ λ' x : σ, M : σ →' τ)
Tactic:
apply Iff.intro
Proof state after:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ ((Γ;; x : σ) ⊢ M : τ) → (Γ ⊢ λ' x : σ, M : σ →' τ)

case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ (Γ ⊢ λ' x : σ, M : σ →' τ) → ((Γ;; x : σ) ⊢ M : τ)
Theorem: abst_rule
Proof state before:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ ((Γ;; x : σ) ⊢ M : τ) → (Γ ⊢ λ' x : σ, M : σ →' τ)
Tactic:
intros h
Proof state after:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : (Γ;; x : σ) ⊢ M : τ
⊢ Γ ⊢ λ' x : σ, M : σ →' τ
Theorem: abst_rule
Proof state before:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : (Γ;; x : σ) ⊢ M : τ
⊢ Γ ⊢ λ' x : σ, M : σ →' τ
Tactic:
unfold typingJudgement at *
Proof state after:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : typeOf (Γ;; x : σ) M = some τ
⊢ typeOf Γ (λ' x : σ, M) = some (σ →' τ)
Theorem: abst_rule
Proof state before:
case mp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : typeOf (Γ;; x : σ) M = some τ
⊢ typeOf Γ (λ' x : σ, M) = some (σ →' τ)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: abst_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
⊢ (Γ ⊢ λ' x : σ, M : σ →' τ) → ((Γ;; x : σ) ⊢ M : τ)
Tactic:
intros h
Proof state after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : Γ ⊢ λ' x : σ, M : σ →' τ
⊢ (Γ;; x : σ) ⊢ M : τ
Theorem: abst_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h : Γ ⊢ λ' x : σ, M : σ →' τ
⊢ (Γ;; x : σ) ⊢ M : τ
Tactic:
simp at *
Proof state after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h :
  (match typeOf (Γ;; x : σ) M with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
⊢ typeOf (Γ;; x : σ) M = some τ
Theorem: abst_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h :
  (match typeOf (Γ;; x : σ) M with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
⊢ typeOf (Γ;; x : σ) M = some τ
Tactic:
generalize h' : typeOf (Γ;; x : σ) M = aux
Proof state after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h :
  (match typeOf (Γ;; x : σ) M with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
aux : Option (𝕋 𝕍)
h' : typeOf (Γ;; x : σ) M = aux
⊢ aux = some τ
Theorem: abst_rule
Proof state before:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
h :
  (match typeOf (Γ;; x : σ) M with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
aux : Option (𝕋 𝕍)
h' : typeOf (Γ;; x : σ) M = aux
⊢ aux = some τ
Tactic:
rw [h'] at h
Proof state after:
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
aux : Option (𝕋 𝕍)
h :
  (match aux with
    | some τ => some (σ →' τ)
    | x => none) =
    some (σ →' τ)
h' : typeOf (Γ;; x : σ) M = aux
⊢ aux = some τ