internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs)) tl hd.q
Tactic:
apply Holds_coincide_Var
Proof state after:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
          (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v =
        Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
          (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v =
        Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v
Tactic:
intro v' a1
Proof state after:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
have s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun (x : VarName) => if h1_v = x then h1_t else x) h1_xs
Proof state after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ ∀ x ∈ h1_xs, Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ ∀ x ∈ h1_xs, Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
intro x _
Proof state after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if x = h1_v then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp only [eq_comm]
Proof state after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp
Proof state after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = V (if h1_v = x then h1_t else x)

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
c3 : h1_v = x
⊢ V h1_t = V h1_t
Tactic:
case _ c3 =>
  simp only [if_pos c3]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
c3 : ¬h1_v = x
⊢ V x = V x
Tactic:
case _ c3 =>
  simp only [if_neg c3]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp only [s1]
Proof state after:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
apply Function.updateListITE_mem_eq_len
Proof state after:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ v' ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ hd.args.length = (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs).length