internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.isFreeIn_imp_occursIn
Proof state before:
v : VarName
F : Formula
h1 : isFreeIn v F
⊢ occursIn v F
Tactic:
induction F
Proof state after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isFreeIn v (pred_const_ a✝¹ a✝)
⊢ occursIn v (pred_const_ a✝¹ a✝)

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isFreeIn v (pred_var_ a✝¹ a✝)
⊢ occursIn v (pred_var_ a✝¹ a✝)

case eq_
v a✝¹ a✝ : VarName
h1 : isFreeIn v (eq_ a✝¹ a✝)
⊢ occursIn v (eq_ a✝¹ a✝)

case true_
v : VarName
h1 : isFreeIn v true_
⊢ occursIn v true_

case false_
v : VarName
h1 : isFreeIn v false_
⊢ occursIn v false_

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v a✝.not_
⊢ occursIn v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v (a✝¹.imp_ a✝)
⊢ occursIn v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v (a✝¹.and_ a✝)
⊢ occursIn v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v (a✝¹.or_ a✝)
⊢ occursIn v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v (a✝¹.iff_ a✝)
⊢ occursIn v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v (forall_ a✝¹ a✝)
⊢ occursIn v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v (exists_ a✝¹ a✝)
⊢ occursIn v (exists_ a✝¹ a✝)

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isFreeIn v (def_ a✝¹ a✝)
⊢ occursIn v (def_ a✝¹ a✝)
Theorem: FOL.NV.isFreeIn_imp_occursIn
Proof state before:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : v ∈ a✝
⊢ occursIn v (pred_const_ a✝¹ a✝)

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : v ∈ a✝
⊢ occursIn v (pred_var_ a✝¹ a✝)

case eq_
v a✝¹ a✝ : VarName
h1 : v = a✝¹ ∨ v = a✝
⊢ occursIn v (eq_ a✝¹ a✝)

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v a✝
⊢ occursIn v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
⊢ occursIn v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
⊢ occursIn v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
⊢ occursIn v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : isFreeIn v a✝¹ ∨ isFreeIn v a✝
⊢ occursIn v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : ¬v = a✝¹ ∧ isFreeIn v a✝
⊢ occursIn v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → occursIn v a✝
h1 : ¬v = a✝¹ ∧ isFreeIn v a✝
⊢ occursIn v (exists_ a✝¹ a✝)

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ occursIn v (def_ a✝¹ a✝)
Tactic:
all_goals
  simp only [occursIn]
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_occursIn
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isFreeIn v (def_ a✝¹ a✝)
⊢ occursIn v (def_ a✝¹ a✝)
Tactic:
simp only [isFreeIn] at h1
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ occursIn v (def_ a✝¹ a✝)
Theorem: FOL.NV.isFreeIn_imp_occursIn
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ occursIn v (def_ a✝¹ a✝)
Tactic:
simp only [occursIn]
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ v ∈ a✝
Theorem: FOL.NV.isFreeIn_imp_occursIn
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ v ∈ a✝
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (replace τ (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  simp only [replace]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (replace τ (eq_ x y))
Tactic:
case eq_ x y =>
  simp only [replace]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E (replace τ false_)
Tactic:
case true_ | false_ =>
  simp only [replace]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi.not_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace τ phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  congr! 1
  exact phi_ih V binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (exists_ x phi)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (replace τ (exists_ x phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
  intro v a1
  simp only [Function.updateITE]
  simp at a1
  push_neg at a1
  cases a1
  case h.intro a1_left a1_right =>
    simp only [if_neg a1_right]
    exact h2 v a1_left
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (replace τ (pred_const_ X xs))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (pred_const_ X xs)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (pred_const_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_var_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [admitsAux] at h1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2 ∧
    (∀ x ∈ binders, ¬(isFreeIn x (τ X xs.length).2 ∧ x ∉ (τ X xs.length).1)) ∧ xs.length = (τ X xs.length).1.length
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2 ∧
    (∀ x ∈ binders, ¬(isFreeIn x (τ X xs.length).2 ∧ x ∉ (τ X xs.length).1)) ∧ xs.length = (τ X xs.length).1.length
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp at h1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1 :
  Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2 ∧
    (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1 :
  Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2 ∧
    (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
cases h1
Proof state after:
case intro
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
left✝ : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
right✝ : (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right : (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
cases h1_right
Proof state after:
case intro
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
left✝ : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
right✝ : xs.length = (τ X xs.length).1.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
obtain s1 :=
Sub.Var.All.Rec.substitution_theorem D I V E (Function.updateListITE id (τ X xs.length).fst xs)
  (τ X xs.length).snd h1_left
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (V ∘ Function.updateListITE id (τ X xs.length).1 xs) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (V ∘ Function.updateListITE id (τ X xs.length).1 xs) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [Function.updateListITE_comp] at s1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE (V ∘ id) (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE (V ∘ id) (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp at s1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))