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

State before:
D : Type
V : VarAssignment D
xs : List String
⊢ V ∘ Var.openList 0 (List.map free_ xs) = shiftList D V (List.map (V ∘ free_) xs)
Tactic:
induction xs
State after:
case nil
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])

case cons
D : Type
V : VarAssignment D
head✝ : String
tail✝ : List String
tail_ih✝ : V ∘ Var.openList 0 (List.map free_ tail✝) = shiftList D V (List.map (V ∘ free_) tail✝)
⊢ V ∘ Var.openList 0 (List.map free_ (head✝ :: tail✝)) = shiftList D V (List.map (V ∘ free_) (head✝ :: tail✝))

State before:
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])
Tactic:
case nil =>
  funext v
  simp
  simp only [shiftList]
  cases v
  case _ x =>
    simp only [Var.openList]
  case _ i =>
    simp only [Var.openList]
    split
    case _ c1 =>
      rfl
    case _ c1 =>
      simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V ∘ Var.openList 0 (List.map free_ (hd :: tl)) = shiftList D V (List.map (V ∘ free_) (hd :: tl))
Tactic:
case _ hd tl ih =>
  funext v
  simp
  simp only [shiftList]
  cases v
  case _ x =>
    simp only [shift]
    simp only [← ih]
    simp only [Var.openList]
    simp
  case _ i =>
    cases i
    case zero =>
      simp only [shift]
      simp only [Var.openList]
      simp
    case succ i =>
      simp only [shift]
      simp only [← ih]
      simp
      simp only [Var.openList]
      simp
      split
      case _ c1 =>
        have s1 : i < tl.length
        linarith
        simp only [s1]
        simp
      case _ c1 =>
        have s1 : ¬ i < tl.length
        linarith
        simp only [s1]
        simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])
Tactic:
funext v
State after:
case h
D : Type
V : VarAssignment D
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ [])) v = shiftList D V (List.map (V ∘ free_) []) v

State before:
case h
D : Type
V : VarAssignment D
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ [])) v = shiftList D V (List.map (V ∘ free_) []) v
Tactic:
simp
State after:
case h
D : Type
V : VarAssignment D
v : Var
⊢ V (Var.openList 0 [] v) = shiftList D V [] v

State before:
case h
D : Type
V : VarAssignment D
v : Var
⊢ V (Var.openList 0 [] v) = shiftList D V [] v
Tactic:
simp only [shiftList]
State after:
case h
D : Type
V : VarAssignment D
v : Var
⊢ V (Var.openList 0 [] v) = V v

State before:
case h
D : Type
V : VarAssignment D
v : Var
⊢ V (Var.openList 0 [] v) = V v
Tactic:
cases v
State after:
case h.free_
D : Type
V : VarAssignment D
a✝ : String
⊢ V (Var.openList 0 [] (free_ a✝)) = V (free_ a✝)

case h.bound_
D : Type
V : VarAssignment D
a✝ : ℕ
⊢ V (Var.openList 0 [] (bound_ a✝)) = V (bound_ a✝)

State before:
D : Type
V : VarAssignment D
x : String
⊢ V (Var.openList 0 [] (free_ x)) = V (free_ x)
Tactic:
case _ x =>
  simp only [Var.openList]
State after:
no goals

State before:
D : Type
V : VarAssignment D
i : ℕ
⊢ V (Var.openList 0 [] (bound_ i)) = V (bound_ i)
Tactic:
case _ i =>
  simp only [Var.openList]
  split
  case _ c1 =>
    rfl
  case _ c1 =>
    simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
x : String
⊢ V (Var.openList 0 [] (free_ x)) = V (free_ x)
Tactic:
simp only [Var.openList]
State after:
no goals

State before:
D : Type
V : VarAssignment D
i : ℕ
⊢ V (Var.openList 0 [] (bound_ i)) = V (bound_ i)
Tactic:
simp only [Var.openList]
State after:
D : Type
V : VarAssignment D
i : ℕ
⊢ V (if i < 0 then bound_ i else if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) =
    V (bound_ i)

State before:
D : Type
V : VarAssignment D
i : ℕ
⊢ V (if i < 0 then bound_ i else if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) =
    V (bound_ i)
Tactic:
split
State after:
case inl
D : Type
V : VarAssignment D
i : ℕ
h✝ : i < 0
⊢ V (bound_ i) = V (bound_ i)

case inr
D : Type
V : VarAssignment D
i : ℕ
h✝ : ¬i < 0
⊢ V (if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) = V (bound_ i)

State before:
D : Type
V : VarAssignment D
i : ℕ
c1 : i < 0
⊢ V (bound_ i) = V (bound_ i)
Tactic:
case _ c1 =>
  rfl
State after:
no goals

State before:
D : Type
V : VarAssignment D
i : ℕ
c1 : ¬i < 0
⊢ V (if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) = V (bound_ i)
Tactic:
case _ c1 =>
  simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
i : ℕ
c1 : i < 0
⊢ V (bound_ i) = V (bound_ i)
Tactic:
rfl
State after:
no goals

State before:
D : Type
V : VarAssignment D
i : ℕ
c1 : ¬i < 0
⊢ V (if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) = V (bound_ i)
Tactic:
simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V ∘ Var.openList 0 (List.map free_ (hd :: tl)) = shiftList D V (List.map (V ∘ free_) (hd :: tl))
Tactic:
funext v
State after:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ (hd :: tl))) v = shiftList D V (List.map (V ∘ free_) (hd :: tl)) v

State before:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ (hd :: tl))) v = shiftList D V (List.map (V ∘ free_) (hd :: tl)) v
Tactic:
simp
State after:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) = shiftList D V (V (free_ hd) :: List.map (V ∘ free_) tl) v

State before:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) = shiftList D V (V (free_ hd) :: List.map (V ∘ free_) tl) v
Tactic:
simp only [shiftList]
State after:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) v

State before:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) v
Tactic:
cases v
State after:
case h.free_
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
a✝ : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ a✝)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (free_ a✝)

case h.bound_
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
a✝ : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ a✝)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ a✝)

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (free_ x)
Tactic:
case _ x =>
  simp only [shift]
  simp only [← ih]
  simp only [Var.openList]
  simp
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (free_ x) = V (Var.openList 0 (List.map free_ tl) (free_ x))

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ i)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (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 [← ih]
    simp
    simp only [Var.openList]
    simp
    split
    case _ c1 =>
      have s1 : i < tl.length
      linarith
      simp only [s1]
      simp
    case _ c1 =>
      have s1 : ¬ i < tl.length
      linarith
      simp only [s1]
      simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (free_ x)
Tactic:
simp only [shift]
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) = shiftList D V (List.map (V ∘ free_) tl) (free_ x)

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) = shiftList D V (List.map (V ∘ free_) tl) (free_ x)
Tactic:
simp only [← ih]
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) = (V ∘ Var.openList 0 (List.map free_ tl)) (free_ x)

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) = (V ∘ Var.openList 0 (List.map free_ tl)) (free_ x)
Tactic:
simp only [Var.openList]
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (free_ x) = (V ∘ Var.openList 0 (List.map free_ tl)) (free_ x)

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (free_ x) = (V ∘ Var.openList 0 (List.map free_ tl)) (free_ x)
Tactic:
simp
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (free_ x) = V (Var.openList 0 (List.map free_ tl) (free_ x))

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ i)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ i)
Tactic:
cases i
State after:
case zero
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ 0)

case succ
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
n✝ : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (n✝ + 1))) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ (n✝ + 1))

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ 0)
Tactic:
case zero =>
  simp only [shift]
  simp only [Var.openList]
  simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ (i + 1))
Tactic:
case succ i =>
  simp only [shift]
  simp only [← ih]
  simp
  simp only [Var.openList]
  simp
  split
  case _ c1 =>
    have s1 : i < tl.length
    linarith
    simp only [s1]
    simp
  case _ c1 =>
    have s1 : ¬ i < tl.length
    linarith
    simp only [s1]
    simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ 0)
Tactic:
simp only [shift]
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) = V (free_ hd)

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) = V (free_ hd)
Tactic:
simp only [Var.openList]
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V
      (if 0 < 0 then bound_ 0
      else
        if x : 0 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[0 - 0]
        else bound_ (0 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V (free_ hd)

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V
      (if 0 < 0 then bound_ 0
      else
        if x : 0 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[0 - 0]
        else bound_ (0 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V (free_ hd)
Tactic:
simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ (i + 1))
Tactic:
simp only [shift]
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shiftList D V (List.map (V ∘ free_) tl) (bound_ i)

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shiftList D V (List.map (V ∘ free_) tl) (bound_ i)
Tactic:
simp only [← ih]
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    (V ∘ Var.openList 0 (List.map free_ tl)) (bound_ i)

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    (V ∘ Var.openList 0 (List.map free_ tl)) (bound_ i)
Tactic:
simp
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    V (Var.openList 0 (List.map free_ tl) (bound_ i))

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    V (Var.openList 0 (List.map free_ tl) (bound_ i))
Tactic:
simp only [Var.openList]
State after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V
      (if i + 1 < 0 then bound_ (i + 1)
      else
        if x : i + 1 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[i + 1 - 0]
        else bound_ (i + 1 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V
      (if i < 0 then bound_ i
      else
        if x : i - 0 < (List.map free_ tl).length then (List.map free_ tl)[i - 0]
        else bound_ (i - 0 - (List.map free_ tl).length + 0))

State before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V
      (if i + 1 < 0 then bound_ (i + 1)
      else
        if x : i + 1 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[i + 1 - 0]
        else bound_ (i + 1 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V
      (if i < 0 then bound_ i
      else
        if x : i - 0 < (List.map free_ tl).length then (List.map free_ tl)[i - 0]
        else bound_ (i - 0 - (List.map free_ tl).length + 0))
Tactic:
simp
State after:
no goals