internlm/Lean-Github huggingface dataset:
Theorem: AlphaEquivPreservesType'
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h : (τ' →' σ') = σ
⊢ ∀ (y : V),
    (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
      ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')
Tactic:
introv
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h : (τ' →' σ') = σ
y : V
⊢ (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
    ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')
Theorem: AlphaEquivPreservesType'
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h : (τ' →' σ') = σ
y : V
⊢ (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
    ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')
Tactic:
by_cases h : y = x
Proof state after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h✝ : (τ' →' σ') = σ
y : V
h : y = x
⊢ (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
    ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
⊢ (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
    ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')
Theorem: AlphaEquivPreservesType'
Proof state before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h✝ : (τ' →' σ') = σ
y : V
h : y = x
⊢ (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
    ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')
Tactic:
simp [h, alpha_equiv.2]
Proof state after:
no goals
Theorem: AlphaEquivPreservesType'
Proof state before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
⊢ (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
    ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')
Tactic:
simp [h]
Proof state after:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
⊢ (var_map y = none ∧ getType y Γ = if y = x' then some τ' else getType y Γ') ∨
    ∃ z, var_map y = some z ∧ getType y Γ = if z = x' then some τ' else getType z Γ'
Theorem: AlphaEquivPreservesType'
Proof state before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
⊢ (var_map y = none ∧ getType y Γ = if y = x' then some τ' else getType y Γ') ∨
    ∃ z, var_map y = some z ∧ getType y Γ = if z = x' then some τ' else getType z Γ'
Tactic:
specialize ctxt_equiv y
Proof state after:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
ctxt_equiv : var_map y = none ∧ getType y Γ = getType y Γ' ∨ ∃ y_1, var_map y = some y_1 ∧ getType y Γ = getType y_1 Γ'
⊢ (var_map y = none ∧ getType y Γ = if y = x' then some τ' else getType y Γ') ∨
    ∃ z, var_map y = some z ∧ getType y Γ = if z = x' then some τ' else getType z Γ'
Theorem: AlphaEquivPreservesType'
Proof state before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
M' : Λ V 𝕍
ih :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M' : σ)
M✝ : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
ctxt_equiv : var_map y = none ∧ getType y Γ = getType y Γ' ∨ ∃ y_1, var_map y = some y_1 ∧ getType y Γ = getType y_1 Γ'
⊢ (var_map y = none ∧ getType y Γ = if y = x' then some τ' else getType y Γ') ∨
    ∃ z, var_map y = some z ∧ getType y Γ = if z = x' then some τ' else getType z Γ'
Tactic:
sorry
Proof state after:
no goals
Theorem: AlphaEquivPreservesType
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
⊢ ∀ {M M' : Λ V 𝕍} {Γ : TCtxt V 𝕍} {σ : 𝕋 𝕍}, (M =ₐ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)
Tactic:
introv
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
⊢ (M =ₐ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)
Theorem: AlphaEquivPreservesType
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
⊢ (M =ₐ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)
Tactic:
intro h h'
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
⊢ Γ ⊢ M' : σ
Theorem: AlphaEquivPreservesType
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
⊢ Γ ⊢ M' : σ
Tactic:
exact AlphaEquivPreservesType' h (by introv; simp) h'
Proof state after:
no goals
Theorem: AlphaEquivPreservesType
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
⊢ ∀ (x : V), none = none ∧ getType x Γ = getType x Γ ∨ ∃ y, none = some y ∧ getType x Γ = getType y Γ
Tactic:
introv
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
x : V
⊢ none = none ∧ getType x Γ = getType x Γ ∨ ∃ y, none = some y ∧ getType x Γ = getType y Γ
Theorem: AlphaEquivPreservesType
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
x : V
⊢ none = none ∧ getType x Γ = getType x Γ ∨ ∃ y, none = some y ∧ getType x Γ = getType y Γ
Tactic:
simp
Proof state after:
no goals
Theorem: varSubPreservesTypeVar
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
⊢ (Γ ⊢ N : σ) → typeOf (Γ;; x : σ) (Λ.Var y) = typeOf Γ (subVarInTerm x N (Λ.Var y))
Tactic:
intro h
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ typeOf (Γ;; x : σ) (Λ.Var y) = typeOf Γ (subVarInTerm x N (Λ.Var y))
Theorem: varSubPreservesTypeVar
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ typeOf (Γ;; x : σ) (Λ.Var y) = typeOf Γ (subVarInTerm x N (Λ.Var y))
Tactic:
simp
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ (if y = x then some σ else getType y Γ) = typeOf Γ (if x = y then N else Λ.Var y)
Theorem: varSubPreservesTypeVar
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ (if y = x then some σ else getType y Γ) = typeOf Γ (if x = y then N else Λ.Var y)
Tactic:
split_ifs with h' h'' h''
Proof state after:
case inl.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : x = y
⊢ some σ = typeOf Γ N

case inl.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : ¬x = y
⊢ some σ = typeOf Γ (Λ.Var y)

case inr.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : x = y
⊢ getType y Γ = typeOf Γ N

case inr.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : ¬x = y
⊢ getType y Γ = typeOf Γ (Λ.Var y)
Theorem: varSubPreservesTypeVar
Proof state before:
case inl.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : x = y
⊢ some σ = typeOf Γ N
Tactic:
rw [h]
Proof state after:
no goals
Theorem: varSubPreservesTypeVar
Proof state before:
case inl.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : ¬x = y
⊢ some σ = typeOf Γ (Λ.Var y)
Tactic:
exfalso
Proof state after:
case inl.inr.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : ¬x = y
⊢ False
Theorem: varSubPreservesTypeVar
Proof state before:
case inl.inr.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : ¬x = y
⊢ False
Tactic:
exact h'' (Eq.symm h')
Proof state after:
no goals
Theorem: varSubPreservesTypeVar
Proof state before:
case inr.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : x = y
⊢ getType y Γ = typeOf Γ N
Tactic:
exfalso
Proof state after:
case inr.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : x = y
⊢ False
Theorem: varSubPreservesTypeVar
Proof state before:
case inr.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : x = y
⊢ False
Tactic:
exact h' (Eq.symm h'')
Proof state after:
no goals
Theorem: varSubPreservesTypeVar
Proof state before:
case inr.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : ¬x = y
⊢ getType y Γ = typeOf Γ (Λ.Var y)
Tactic:
simp
Proof state after:
no goals
Theorem: varSubPreservesType
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
x : V
σ : 𝕋 𝕍
⊢ ∀ {Γ : TCtxt V 𝕍}, (Γ ⊢ N : σ) → typeOf (Γ;; x : σ) M = typeOf Γ (subVarInTerm x N M)
Tactic:
sorry
Proof state after:
no goals
Theorem: betaReductionPreservesType
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M M' : Λ V 𝕍
σ : 𝕋 𝕍
⊢ (M ↠ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.zero_add
Proof state before:
n : ℕ
⊢ 0 + n = n
Tactic:
induction n with 
| zero => rfl 
| succ n' ih => 
  rewrite [add_succ, ih] rfl
Proof state after:
no goals
Theorem: Tutorial.zero_add
Proof state before:
case zero

⊢ 0 + Nat.zero = Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Tutorial.zero_add
Proof state before:
case succ
n' : ℕ
ih : 0 + n' = n'
⊢ 0 + succ n' = succ n'
Tactic:
rewrite [add_succ, ih]
Proof state after:
case succ
n' : ℕ
ih : 0 + n' = n'
⊢ succ n' = succ n'
Theorem: Tutorial.zero_add
Proof state before:
case succ
n' : ℕ
ih : 0 + n' = n'
⊢ succ n' = succ n'
Tactic:
rfl
Proof state after:
no goals
Theorem: OrientableInvolutiveInv.no_fixed_points
Proof state before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
⊢ pos x ≠ pos x⁻¹
Tactic:
intro h
Proof state after:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = pos x⁻¹
⊢ False
Theorem: OrientableInvolutiveInv.no_fixed_points
Proof state before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = pos x⁻¹
⊢ False
Tactic:
have := h ▸ selection x
Proof state after:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = pos x⁻¹
this : xor (pos x⁻¹) (pos x⁻¹) = true
⊢ False
Theorem: OrientableInvolutiveInv.no_fixed_points
Proof state before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = pos x⁻¹
this : xor (pos x⁻¹) (pos x⁻¹) = true
⊢ False
Tactic:
simp_all only [Bool.xor_self]
Proof state after:
no goals
Theorem: OrientableInvolutiveInv.not_pos_inv_of_pos
Proof state before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = true
⊢ ¬pos x⁻¹ = true
Tactic:
have := h ▸ selection x
Proof state after:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = true
this : xor true (pos x⁻¹) = true
⊢ ¬pos x⁻¹ = true
Theorem: OrientableInvolutiveInv.not_pos_inv_of_pos
Proof state before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = true
this : xor true (pos x⁻¹) = true
⊢ ¬pos x⁻¹ = true
Tactic:
simp_all only [Bool.true_xor, Bool.not_eq_true', not_false_eq_true]
Proof state after:
no goals
Theorem: OrientableInvolutiveInv.pos_of_not_pos_inv
Proof state before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : ¬pos x⁻¹ = true
⊢ pos x = true
Tactic:
have := selection x
Proof state after:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : ¬pos x⁻¹ = true
this : xor (pos x) (pos x⁻¹) = true
⊢ pos x = true
Theorem: OrientableInvolutiveInv.pos_of_not_pos_inv
Proof state before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : ¬pos x⁻¹ = true
this : xor (pos x) (pos x⁻¹) = true
⊢ pos x = true
Tactic:
simp_all only [Bool.not_eq_true, Bool.xor_false]
Proof state after:
no goals
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
⊢ BddAbove c
Tactic:
dsimp [BddAbove, upperBounds]
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Tactic:
let sup := InvFreeSets.chainUnion c hcChain
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Tactic:
use sup
Proof state after:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
⊢ sup ∈ {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
⊢ sup ∈ {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Tactic:
intro A hAc
Proof state after:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
⊢ A ≤ sup
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
⊢ A ≤ sup
Tactic:
simp only [LE.le, chainUnion, Monad.join, joinM, Set.bind_def, Set.mem_image, exists_and_right,
  exists_eq_right, id_eq, Set.iUnion_exists]
Proof state after:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
⊢ Set.Subset (↑A) (⋃ i, ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i)
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
⊢ Set.Subset (↑A) (⋃ i, ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i)
Tactic:
intro x hxA
Proof state after:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ x ∈ ⋃ i, ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ x ∈ ⋃ i, ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i
Tactic:
use A
Proof state after:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ (↑A ∈ Set.range fun i => ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i) ∧ x ∈ ↑A
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ (↑A ∈ Set.range fun i => ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i) ∧ x ∈ ↑A
Tactic:
refine' ⟨_, hxA⟩
Proof state after:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ ↑A ∈ Set.range fun i => ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i