internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi.not_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H 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.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (exists_ x phi)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (exists_ x phi) ↔ Holds D I V E_ref (replace P zs H (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.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_const_ X xs))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ X xs) ↔ Holds D I V E_ref (pred_const_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ X xs) ↔ Holds D I V E_ref (pred_const_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (I' D I V' E_ref P zs H).pred_const_ X (List.map V xs) ↔ I.pred_const_ X (List.map V xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (I' D I V' E_ref P zs H).pred_const_ X (List.map V xs) ↔ I.pred_const_ X (List.map V xs)
Tactic:
simp only [I']
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Interpretation.usingPred D I fun Q ds =>
          if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E_ref H
          else I.pred_var_ Q ds).pred_const_
      X (List.map V xs) ↔
    I.pred_const_ X (List.map V xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Interpretation.usingPred D I fun Q ds =>
          if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E_ref H
          else I.pred_var_ Q ds).pred_const_
      X (List.map V xs) ↔
    I.pred_const_ X (List.map V xs)
Tactic:
simp only [Interpretation.usingPred]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_var_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_var_ X xs))
Tactic:
simp only [admitsAux] at h1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_var_ X xs))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (I' D I V' E_ref P zs H).pred_var_ X (List.map V xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (I' D I V' E_ref P zs H).pred_var_ X (List.map V xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [I']
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Interpretation.usingPred D I fun Q ds =>
          if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E_ref H
          else I.pred_var_ Q ds).pred_var_
      X (List.map V xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Interpretation.usingPred D I fun Q ds =>
          if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E_ref H
          else I.pred_var_ Q ds).pred_var_
      X (List.map V xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [Interpretation.usingPred]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = P ∧ (List.map V xs).length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = P ∧ (List.map V xs).length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
split_ifs at h1
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h✝ : X = P ∧ xs.length = zs.length
h1 : Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h✝ : ¬(X = P ∧ xs.length = zs.length)
h1 : True
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
case neg c1 =>
  split_ifs
  case pos c2 =>
    contradiction
  case neg c2 =>
    simp only [Holds]
Proof state after:
no goals