Theorem: LN.ShiftVarOpenList (FOL/LN/Paper.lean)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d = shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)
Tactic:
funext v
State after:
case h
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
v : Var
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d v = (shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)) v

State before:
case h
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
v : Var
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d v = (shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)) v
Tactic:
simp
State after:
case h
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
v : Var
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d v = shift D V d (Var.openList (j + 1) (List.map free_ zs) v)

State before:
case h
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
v : Var
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d v = shift D V d (Var.openList (j + 1) (List.map free_ zs) v)
Tactic:
cases v
State after:
case h.free_
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
a✝ : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ a✝) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (free_ a✝))

case h.bound_
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
a✝ : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ a✝) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ a✝))

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (free_ x))
Tactic:
case _ x =>
  simp only [Var.openList]
  simp only [shift]
  simp
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ V (Var.openList j (List.map free_ zs) (free_ x)) = V (free_ x)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ i) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (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
      split
      case _ c1 =>
        have s1 : i + 1 < j + 1
        linarith
        simp only [if_pos s1]
      case _ c1 =>
        have s1 : ¬ i + 1 < j + 1
        linarith
        simp only [if_neg s1]
        split
        case _ c2 =>
          simp
        case _ c2 =>
          simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (free_ x))
Tactic:
simp only [Var.openList]
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) = shift D V d (free_ x)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) = shift D V d (free_ x)
Tactic:
simp only [shift]
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ (V ∘ Var.openList j (List.map free_ zs)) (free_ x) = V (free_ x)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ (V ∘ Var.openList j (List.map free_ zs)) (free_ x) = V (free_ x)
Tactic:
simp
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ V (Var.openList j (List.map free_ zs) (free_ x)) = V (free_ x)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ i) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ i))
Tactic:
cases i
State after:
case zero
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ 0) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ 0))

case succ
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
n✝ : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ (n✝ + 1)) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ (n✝ + 1)))

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ 0) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ 0))
Tactic:
case zero =>
  simp only [shift]
  simp only [Var.openList]
  simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ (i + 1)) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)))
Tactic:
case succ i =>
    simp only [shift]
    simp only [Var.openList]
    simp
    split
    case _ c1 =>
      have s1 : i + 1 < j + 1
      linarith
      simp only [if_pos s1]
    case _ c1 =>
      have s1 : ¬ i + 1 < j + 1
      linarith
      simp only [if_neg s1]
      split
      case _ c2 =>
        simp
      case _ c2 =>
        simp
State after:
case h_3
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
i✝ : ℕ
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ i✝.succ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (bound_ i✝)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ 0) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ 0))
Tactic:
simp only [shift]
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ d =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ 0) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ d =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ 0) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
simp only [Var.openList]
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ d =
    match
      if 0 < j + 1 then bound_ 0
      else
        if x : 0 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[0 - (j + 1)]
        else bound_ (0 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ d =
    match
      if 0 < j + 1 then bound_ 0
      else
        if x : 0 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[0 - (j + 1)]
        else bound_ (0 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ (i + 1)) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)))
Tactic:
simp only [shift]
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
simp only [Var.openList]
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match
      if i + 1 < j + 1 then bound_ (i + 1)
      else
        if x : i + 1 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - (j + 1)]
        else bound_ (i + 1 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match
      if i + 1 < j + 1 then bound_ (i + 1)
      else
        if x : i + 1 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - (j + 1)]
        else bound_ (i + 1 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
simp
State after:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) =
    match
      if i < j then bound_ (i + 1)
      else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) =
    match
      if i < j then bound_ (i + 1)
      else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
Tactic:
split
State after:
case h_1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)

case h_2
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d

case h_3
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
i✝ : ℕ
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ i✝.succ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (bound_ i✝)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)
Tactic:
case _ c1 =>
  have s1 : i + 1 < j + 1
  linarith
  simp only [if_pos s1]
State after:
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
s1 : i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d
Tactic:
case _ c1 =>
  have s1 : ¬ i + 1 < j + 1
  linarith
  simp only [if_neg s1]
  split
  case _ c2 =>
    simp
  case _ c2 =>
    simp
State after:
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ ¬i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
s1 : ¬i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)
Tactic:
have s1 : i + 1 < j + 1
State after:
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
s1 : i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)

State before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d
Tactic:
have s1 : ¬ i + 1 < j + 1
State after:
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ ¬i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
s1 : ¬i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d