internlm/Lean-Github huggingface dataset:
Theorem: evalBoxes
Proof state before:
case nil
W✝ : Type
M : KripkeModel W✝
φ : Formula
w : W✝
⊢ evaluate M w (⌈⌈[]⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M [] w v → evaluate M v φ
Tactic:
simp [relateSeq]
Proof state after:
no goals
Theorem: evalBoxes
Proof state before:
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ evaluate M w (⌈⌈α :: δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Tactic:
simp only [Formula.boxes, evaluate]
Proof state after:
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)) ↔ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Theorem: evalBoxes
Proof state before:
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)) ↔ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Tactic:
constructor
Proof state after:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)) → ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ

case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ) → ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
Theorem: evalBoxes
Proof state before:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)) → ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Tactic:
intro lhs
Proof state after:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
⊢ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Theorem: evalBoxes
Proof state before:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
⊢ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Tactic:
intro v v_αδ_w
Proof state after:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : relateSeq M (α :: δ) w v
⊢ evaluate M v φ
Theorem: evalBoxes
Proof state before:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : relateSeq M (α :: δ) w v
⊢ evaluate M v φ
Tactic:
simp [relateSeq] at *
Proof state after:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : ∃ u, relate M α w u ∧ relateSeq M δ u v
⊢ evaluate M v φ
Theorem: evalBoxes
Proof state before:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : ∃ u, relate M α w u ∧ relateSeq M δ u v
⊢ evaluate M v φ
Tactic:
rcases v_αδ_w with ⟨u, w_α_u, u_δ_v⟩
Proof state after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ
Theorem: evalBoxes
Proof state before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ
Tactic:
specialize @IH u
Proof state after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
IH : evaluate M u (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
⊢ evaluate M v φ
Theorem: evalBoxes
Proof state before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
IH : evaluate M u (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
⊢ evaluate M v φ
Tactic:
refine IH.1 ?_ v u_δ_v
Proof state after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
IH : evaluate M u (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
⊢ evaluate M u (⌈⌈δ⌉⌉φ)
Theorem: evalBoxes
Proof state before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
IH : evaluate M u (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
⊢ evaluate M u (⌈⌈δ⌉⌉φ)
Tactic:
simp_all only [true_iff]
Proof state after:
no goals
Theorem: evalBoxes
Proof state before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ) → ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
Tactic:
intro rhs
Proof state after:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
⊢ ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
Theorem: evalBoxes
Proof state before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
⊢ ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
Tactic:
intro u w_α_u
Proof state after:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ evaluate M u (⌈⌈δ⌉⌉φ)
Theorem: evalBoxes
Proof state before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ evaluate M u (⌈⌈δ⌉⌉φ)
Tactic:
apply IH.2
Proof state after:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
Theorem: evalBoxes
Proof state before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
Tactic:
intro v u_δ_v
Proof state after:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ
Theorem: evalBoxes
Proof state before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ
Tactic:
apply rhs
Proof state after:
case mpr.a
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ relateSeq M (α :: δ) w v
Theorem: evalBoxes
Proof state before:
case mpr.a
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ relateSeq M (α :: δ) w v
Tactic:
simp only [relateSeq]
Proof state after:
case mpr.a
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ ∃ u, relate M α w u ∧ relateSeq M δ u v
Theorem: evalBoxes
Proof state before:
case mpr.a
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ ∃ u, relate M α w u ∧ relateSeq M δ u v
Tactic:
use u
Proof state after:
no goals
Theorem: truthImply_then_satImply
Proof state before:
X Y : List Formula
⊢ X⊨Y → satisfiable X → satisfiable Y
Tactic:
intro X_Y
Proof state after:
X Y : List Formula
X_Y : X⊨Y
⊢ satisfiable X → satisfiable Y
Theorem: truthImply_then_satImply
Proof state before:
X Y : List Formula
X_Y : X⊨Y
⊢ satisfiable X → satisfiable Y
Tactic:
intro satX
Proof state after:
X Y : List Formula
X_Y : X⊨Y
satX : satisfiable X
⊢ satisfiable Y
Theorem: truthImply_then_satImply
Proof state before:
X Y : List Formula
X_Y : X⊨Y
satX : satisfiable X
⊢ satisfiable Y
Tactic:
rcases satX with ⟨W,M,w,v_X⟩
Proof state after:
case intro.intro.intro
X Y : List Formula
X_Y : X⊨Y
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
⊢ satisfiable Y
Theorem: truthImply_then_satImply
Proof state before:
case intro.intro.intro
X Y : List Formula
X_Y : X⊨Y
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
⊢ satisfiable Y
Tactic:
specialize X_Y W M w v_X
Proof state after:
case intro.intro.intro
X Y : List Formula
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
X_Y : ∀ ψ ∈ Y, evaluate M w ψ
⊢ satisfiable Y
Theorem: truthImply_then_satImply
Proof state before:
case intro.intro.intro
X Y : List Formula
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
X_Y : ∀ ψ ∈ Y, evaluate M w ψ
⊢ satisfiable Y
Tactic:
use W, M, w
Proof state after:
no goals
Theorem: getTypeRebind
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
⊢ ∀ (x : V), getType x ((Γ;; y : σ);; y : σ') = getType x (Γ;; y : σ')
Tactic:
introv
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ getType x ((Γ;; y : σ);; y : σ') = getType x (Γ;; y : σ')
Theorem: getTypeRebind
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ getType x ((Γ;; y : σ);; y : σ') = getType x (Γ;; y : σ')
Tactic:
simp
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ (if x = y then some σ' else if x = y then some σ else getType x Γ) = if x = y then some σ' else getType x Γ
Theorem: getTypeRebind
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ (if x = y then some σ' else if x = y then some σ else getType x Γ) = if x = y then some σ' else getType x Γ
Tactic:
split_ifs <;> rfl
Proof state after:
no goals
Theorem: getTypeReorder
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
⊢ x ≠ y → ∀ {z : V}, getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
intro h z
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Theorem: getTypeReorder
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
by_cases h' : z = x
Proof state after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Theorem: getTypeReorder
Proof state before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
simp [h, h']
Proof state after:
no goals
Theorem: getTypeReorder
Proof state before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
by_cases h'' : z = y
Proof state after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : ¬z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Theorem: getTypeReorder
Proof state before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
simp [h', h'']
Proof state after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ some σ' = if y = x then some σ else some σ'
Theorem: getTypeReorder
Proof state before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ some σ' = if y = x then some σ else some σ'
Tactic:
split_ifs with h
Proof state after:
case pos.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ some σ' = some σ

case pos.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : ¬y = x
⊢ some σ' = some σ'
Theorem: getTypeReorder
Proof state before:
case pos.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ some σ' = some σ
Tactic:
exfalso
Proof state after:
case pos.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ False
Theorem: getTypeReorder
Proof state before:
case pos.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ False
Tactic:
rw [h''] at h'
Proof state after:
case pos.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬y = x
h'' : z = y
h : y = x
⊢ False
Theorem: getTypeReorder
Proof state before:
case pos.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬y = x
h'' : z = y
h : y = x
⊢ False
Tactic:
exact h' h
Proof state after:
no goals
Theorem: getTypeReorder
Proof state before:
case pos.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : ¬y = x
⊢ some σ' = some σ'
Tactic:
rfl
Proof state after:
no goals
Theorem: getTypeReorder
Proof state before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : ¬z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
simp [h', h'']
Proof state after:
no goals
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
⊢ ∀ (Γ : TCtxt V 𝕍) (x : V), x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
Tactic:
intros Γ x
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x : V
⊢ x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x : V
⊢ x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
Tactic:
induction' Γ
Proof state after:
case Empty
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
⊢ x ∈ DomTCtxt TCtxt.Empty → ∃ σ, getType x TCtxt.Empty = some σ

case VarCtxt
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x a✝² : V
a✝¹ : 𝕋 𝕍
a✝ : TCtxt V 𝕍
a_ih✝ : x ∈ DomTCtxt a✝ → ∃ σ, getType x a✝ = some σ
⊢ x ∈ DomTCtxt (a✝;; a✝² : a✝¹) → ∃ σ, getType x (a✝;; a✝² : a✝¹) = some σ
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
case Empty
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
⊢ x ∈ DomTCtxt TCtxt.Empty → ∃ σ, getType x TCtxt.Empty = some σ
Tactic:
simp
Proof state after:
no goals
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
⊢ x ∈ DomTCtxt (Γ;; x' : σ) → ∃ σ_1, getType x (Γ;; x' : σ) = some σ_1
Tactic:
simp only [DomTCtxt, Finset.mem_union, Finset.mem_singleton, getType]
Proof state after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Tactic:
by_cases h' : x = x'
Proof state after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Tactic:
. simp [h']
Proof state after:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Tactic:
simp [h']
Proof state after:
no goals
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Tactic:
simp only [h', or_false, ite_false]
Proof state after:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
Theorem: typeOfDefinedOfInTCtxt
Proof state before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
Tactic:
assumption
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M : Λ V 𝕍
⊢ ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Tactic:
induction M with
| Var x => intro Γ Γ' h; apply h; simp
| App M N ih₁ ih₂ =>
  intro Γ Γ' h
  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])
  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])
  simp [ih₁ h₁, ih₂ h₂]
| Lam y σ M ih => 
  intro Γ Γ' h
  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')
  simp [ih h]
Proof state after:
no goals
Theorem: ctxtTypeOfPreservation
Proof state before:
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
⊢ ∀ {Γ Γ' : TCtxt V 𝕍},
    (∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ') →
      typeOf Γ (Λ.Var x) = typeOf Γ' (Λ.Var x)
Tactic:
intro Γ Γ' h
Proof state after:
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)