internlm/Lean-Github huggingface dataset:
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (forall_ x phi) → V v = V' v
⊢ Holds D I V (forall_ x phi) ↔ Holds D I V' (forall_ x phi)
Tactic:
simp only [occursFreeIn] at h1
Proof state after:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ Holds D I V (forall_ x phi) ↔ Holds D I V' (forall_ x phi)
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ Holds D I V (forall_ x phi) ↔ Holds D I V' (forall_ x phi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ (∀ (d : D), Holds D I (shift D V d) phi) ↔ ∀ (d : D), Holds D I (shift D V' d) phi
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ (∀ (d : D), Holds D I (shift D V d) phi) ↔ ∀ (d : D), Holds D I (shift D V' d) phi
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ ∀ (a : D), Holds D I (shift D V a) phi ↔ Holds D I (shift D V' a) phi
Theorem: LN.HoldsCoincideVar
Proof state before:
case h
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ ∀ (a : D), Holds D I (shift D V a) phi ↔ Holds D I (shift D V' a) phi
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ Holds D I (shift D V d) phi ↔ Holds D I (shift D V' d) phi
Theorem: LN.HoldsCoincideVar
Proof state before:
case h
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ Holds D I (shift D V d) phi ↔ Holds D I (shift D V' d) phi
Tactic:
apply phi_ih
Proof state after:
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ ∀ (v : Var), occursFreeIn v phi → shift D V d v = shift D V' d v
Theorem: LN.HoldsCoincideVar
Proof state before:
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ ∀ (v : Var), occursFreeIn v phi → shift D V d v = shift D V' d v
Tactic:
intro v a1
Proof state after:
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
v : Var
a1 : occursFreeIn v phi
⊢ shift D V d v = shift D V' d v
Theorem: LN.HoldsCoincideVar
Proof state before:
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
v : Var
a1 : occursFreeIn v phi
⊢ shift D V d v = shift D V' d v
Tactic:
cases v
Proof state after:
case h.h1.free_
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a✝ : String
a1 : occursFreeIn (free_ a✝) phi
⊢ shift D V d (free_ a✝) = shift D V' d (free_ a✝)

case h.h1.bound_
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a✝ : ℕ
a1 : occursFreeIn (bound_ a✝) phi
⊢ shift D V d (bound_ a✝) = shift D V' d (bound_ a✝)
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ shift D V d (free_ x) = shift D V' d (free_ x)
Tactic:
case free_ x =>
  simp only [shift]
  apply h1
  exact a1
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ i) phi
⊢ shift D V d (bound_ i) = shift D V' d (bound_ i)
Tactic:
case bound_ i =>
  cases i
  case zero =>
    simp only [shift]
  case succ i =>
    simp only [shift]
    apply h1
    simp only [lift]
    exact a1
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ shift D V d (free_ x) = shift D V' d (free_ x)
Tactic:
simp only [shift]
Proof state after:
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ V (free_ x) = V' (free_ x)
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ V (free_ x) = V' (free_ x)
Tactic:
apply h1
Proof state after:
case a
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ occursFreeIn (lift (free_ x)) phi
Theorem: LN.HoldsCoincideVar
Proof state before:
case a
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ occursFreeIn (lift (free_ x)) phi
Tactic:
exact a1
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ i) phi
⊢ shift D V d (bound_ i) = shift D V' d (bound_ i)
Tactic:
cases i
Proof state after:
case zero
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a1 : occursFreeIn (bound_ 0) phi
⊢ shift D V d (bound_ 0) = shift D V' d (bound_ 0)

case succ
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
n✝ : ℕ
a1 : occursFreeIn (bound_ (n✝ + 1)) phi
⊢ shift D V d (bound_ (n✝ + 1)) = shift D V' d (bound_ (n✝ + 1))
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a1 : occursFreeIn (bound_ 0) phi
⊢ shift D V d (bound_ 0) = shift D V' d (bound_ 0)
Tactic:
case zero =>
  simp only [shift]
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ shift D V d (bound_ (i + 1)) = shift D V' d (bound_ (i + 1))
Tactic:
case succ i =>
  simp only [shift]
  apply h1
  simp only [lift]
  exact a1
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a1 : occursFreeIn (bound_ 0) phi
⊢ shift D V d (bound_ 0) = shift D V' d (bound_ 0)
Tactic:
simp only [shift]
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ shift D V d (bound_ (i + 1)) = shift D V' d (bound_ (i + 1))
Tactic:
simp only [shift]
Proof state after:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ V (bound_ i) = V' (bound_ i)
Theorem: LN.HoldsCoincideVar
Proof state before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ V (bound_ i) = V' (bound_ i)
Tactic:
apply h1
Proof state after:
case a
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ occursFreeIn (lift (bound_ i)) phi
Theorem: LN.HoldsCoincideVar
Proof state before:
case a
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ occursFreeIn (lift (bound_ i)) phi
Tactic:
simp only [lift]
Proof state after:
case a
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ occursFreeIn (bound_ (i + 1)) phi
Theorem: LN.HoldsCoincideVar
Proof state before:
case a
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ occursFreeIn (bound_ (i + 1)) phi
Tactic:
exact a1
Proof state after:
no goals
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
⊢ (∀ (d : D), Holds D I (shift D V d) F) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) F
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
⊢ ∀ (a : D), Holds D I (shift D V a) F ↔ Holds D I (Function.updateITE V (free_ z) a ∘ Var.openList 0 [free_ z]) F
Theorem: LN.HoldsShift
Proof state before:
case h
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
⊢ ∀ (a : D), Holds D I (shift D V a) F ↔ Holds D I (Function.updateITE V (free_ z) a ∘ Var.openList 0 [free_ z]) F
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
⊢ Holds D I (shift D V d) F ↔ Holds D I (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) F
Theorem: LN.HoldsShift
Proof state before:
case h
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
⊢ Holds D I (shift D V d) F ↔ Holds D I (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) F
Tactic:
apply HoldsCoincideVar
Proof state after:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
⊢ ∀ (v : Var), occursFreeIn v F → shift D V d v = (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) v
Theorem: LN.HoldsShift
Proof state before:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
⊢ ∀ (v : Var), occursFreeIn v F → shift D V d v = (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) v
Tactic:
intro v a1
Proof state after:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) v
Theorem: LN.HoldsShift
Proof state before:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) v
Tactic:
simp
Proof state after:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = Function.updateITE V (free_ z) d (Var.openList 0 [free_ z] v)
Theorem: LN.HoldsShift
Proof state before:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = Function.updateITE V (free_ z) d (Var.openList 0 [free_ z] v)
Tactic:
simp only [Function.updateITE]
Proof state after:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = if Var.openList 0 [free_ z] v = free_ z then d else V (Var.openList 0 [free_ z] v)
Theorem: LN.HoldsShift
Proof state before:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = if Var.openList 0 [free_ z] v = free_ z then d else V (Var.openList 0 [free_ z] v)
Tactic:
cases v
Proof state after:
case h.h1.free_
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a✝ : String
a1 : occursFreeIn (free_ a✝) F
⊢ shift D V d (free_ a✝) =
    if Var.openList 0 [free_ z] (free_ a✝) = free_ z then d else V (Var.openList 0 [free_ z] (free_ a✝))

case h.h1.bound_
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a✝ : ℕ
a1 : occursFreeIn (bound_ a✝) F
⊢ shift D V d (bound_ a✝) =
    if Var.openList 0 [free_ z] (bound_ a✝) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ a✝))
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ shift D V d (free_ x') =
    if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
Tactic:
case _ x' =>
  simp only [shift]
  simp only [Var.openList]
  split_ifs
  case _ c1 =>
    simp at c1
    simp only [← c1] at h1
    contradiction
  case _ c1 =>
    rfl
Proof state after:
no goals
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ i) F
⊢ shift D V d (bound_ i) =
    if Var.openList 0 [free_ z] (bound_ i) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ i))
Tactic:
case _ i =>
  cases i
  case zero =>
    simp only [shift]
    simp only [Var.openList]
    simp
  case succ i =>
    simp only [shift]
    simp only [Var.openList]
    simp
Proof state after:
no goals
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ shift D V d (free_ x') =
    if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
Tactic:
simp only [shift]
Proof state after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if free_ x' = free_ z then d else V (free_ x')
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if free_ x' = free_ z then d else V (free_ x')
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
h✝ : free_ x' = free_ z
⊢ V (free_ x') = d

case neg
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
h✝ : ¬free_ x' = free_ z
⊢ V (free_ x') = V (free_ x')
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : free_ x' = free_ z
⊢ V (free_ x') = d
Tactic:
case _ c1 =>
  simp at c1
  simp only [← c1] at h1
  contradiction
Proof state after:
no goals
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : ¬free_ x' = free_ z
⊢ V (free_ x') = V (free_ x')
Tactic:
case _ c1 =>
  rfl
Proof state after:
no goals
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : free_ x' = free_ z
⊢ V (free_ x') = d
Tactic:
simp at c1
Proof state after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
⊢ V (free_ x') = d
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
⊢ V (free_ x') = d
Tactic:
simp only [← c1] at h1
Proof state after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
h1 : ¬occursFreeIn (free_ x') F
⊢ V (free_ x') = d
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
h1 : ¬occursFreeIn (free_ x') F
⊢ V (free_ x') = d
Tactic:
contradiction
Proof state after:
no goals
Theorem: LN.HoldsShift
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : ¬free_ x' = free_ z
⊢ V (free_ x') = V (free_ x')
Tactic:
rfl
Proof state after:
no goals