internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (sub τ phi)) ↔
    ∃ d,
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x d) (head✝ :: tail✝) phi
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x a) (head✝ :: tail✝) phi
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tl (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tl F
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds] at ih
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
simp at ih
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V tl (def_ X xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V tl (def_ X xs)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

case neg
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
case _ c1 =>
  specialize ih (Function.updateListITE V hd.args (List.map V xs)) hd.q
  simp only [sub_no_predVar hd.q τ hd.h2] at ih
  apply ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Tactic:
case _ c1 =>
  specialize ih V (def_ X xs)
  simp only [sub] at ih
  exact ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
specialize ih (Function.updateListITE V hd.args (List.map V xs)) hd.q
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl (sub τ hd.q) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl (sub τ hd.q) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
simp only [sub_no_predVar hd.q τ hd.h2] at ih
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
apply ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Tactic:
specialize ih V (def_ X xs)
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
ih :
  Holds D I V tl (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
ih :
  Holds D I V tl (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Tactic:
simp only [sub] at ih
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
ih :
  Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
ih :
  Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Tactic:
exact ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → PredName
h1 : F.IsValid
⊢ (sub τ F).IsValid
Tactic:
simp only [IsValid] at h1
Proof state after:
F : Formula
τ : PredName → PredName
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (sub τ F).IsValid
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → PredName
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (sub τ F).IsValid
Tactic:
simp only [IsValid]
Proof state after:
F : Formula
τ : PredName → PredName
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (sub τ F)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → PredName
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (sub τ F)
Tactic:
intro D I V E
Proof state after:
F : Formula
τ : PredName → PredName
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (sub τ F)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → PredName
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (sub τ F)
Tactic:
simp only [substitution_theorem D I V E τ F]
Proof state after:
F : Formula
τ : PredName → PredName
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D
    { nonempty := ⋯, pred_const_ := I.pred_const_,
      pred_var_ := fun P ds => if ds = [] then Holds D I V E (pred_var_ (τ P) []) else I.pred_var_ P ds }
    V E F