internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (def_ X xs) →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn]
Proof state after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    False →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    False →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (pred_const_ X xs) → V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_const_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  simp only [isFreeIn] at h1
  simp only [subAux]
  simp only [Holds]
  simp only [I']
  simp only [Interpretation.usingPred]
  simp
  congr! 1
  simp only [List.map_eq_map_iff]
  intro x a1
  simp
  exact h1 x a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), isFreeIn x_1 (eq_ x y) → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (eq_ x y) ↔ Holds D I V E (subAux c τ σ (eq_ x y))
Tactic:
case eq_ x y =>
  simp only [isFreeIn] at h1
  simp only [subAux]
  simp only [Holds]
  have s1 : V' x = V (σ x)
  apply h1
  simp
  simp only [s1]
  have s2 : V' y = V (σ y)
  apply h1
  simp
  simp only [s2]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x false_ → V' x = V (σ x)
h2 : ∀ x ∈ false_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E false_ ↔ Holds D I V E (subAux c τ σ false_)
Tactic:
case true_ | false_ =>
  simp only [subAux]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi.not_ → V' x = V (σ x)
h2 : ∀ x ∈ phi.not_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi.not_ ↔ Holds D I V E (subAux c τ σ phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [isFreeIn] at h1
  simp only [predVarSet] at h2
  simp only [subAux]
  simp only [Holds]
  congr! 1
  exact phi_ih V V' σ h1 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (pred_const_ X xs) → V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_const_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_const_ X xs))
Tactic:
simp only [isFreeIn] at h1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_const_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_const_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_const_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_const_ X xs))
Tactic:
simp only [subAux]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_const_ X xs) ↔ Holds D I V E (pred_const_ X (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_const_ X xs) ↔ Holds D I V E (pred_const_ X (List.map σ xs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ (I' D I V'' E τ).pred_const_ X (List.map V' xs) ↔ I.pred_const_ X (List.map V (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ (I' D I V'' E τ).pred_const_ X (List.map V' xs) ↔ I.pred_const_ X (List.map V (List.map σ xs))
Tactic:
simp only [I']
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ (Interpretation.usingPred D I fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V'' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds).pred_const_
      X (List.map V' xs) ↔
    I.pred_const_ X (List.map V (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ (Interpretation.usingPred D I fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V'' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds).pred_const_
      X (List.map V' xs) ↔
    I.pred_const_ X (List.map V (List.map σ xs))
Tactic:
simp only [Interpretation.usingPred]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ I.pred_const_ X (List.map V' xs) ↔ I.pred_const_ X (List.map V (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ I.pred_const_ X (List.map V' xs) ↔ I.pred_const_ X (List.map V (List.map σ xs))
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ I.pred_const_ X (List.map V' xs) ↔ I.pred_const_ X (List.map (V ∘ σ) xs)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ I.pred_const_ X (List.map V' xs) ↔ I.pred_const_ X (List.map (V ∘ σ) xs)
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ List.map V' xs = List.map (V ∘ σ) xs
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ List.map V' xs = List.map (V ∘ σ) xs
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ x ∈ xs, V' x = (V ∘ σ) x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ x ∈ xs, V' x = (V ∘ σ) x
Tactic:
intro x a1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : x ∈ xs
⊢ V' x = (V ∘ σ) x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : x ∈ xs
⊢ V' x = (V ∘ σ) x
Tactic:
simp
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : x ∈ xs
⊢ V' x = V (σ x)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : x ∈ xs
⊢ V' x = V (σ x)
Tactic:
exact h1 x a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (pred_var_ X xs) → V' x = V (σ x)
h2 : ∀ x ∈ (pred_var_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Tactic:
simp only [isFreeIn] at h1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_var_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_var_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Tactic:
simp only [predVarSet] at h2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ {(X, xs.length)}.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ {(X, xs.length)}.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Tactic:
simp at h2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ predVarFreeVarSet τ (X, xs.length), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ predVarFreeVarSet τ (X, xs.length), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Tactic:
simp only [predVarFreeVarSet] at h2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔ Holds D I V E (subAux c τ σ (pred_var_ X xs))
Tactic:
simp only [subAux]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ X xs) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (I' D I V'' E τ).pred_var_ X (List.map V' xs) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))