internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      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) (hd :: tl) (τ X ds.length).2
            else I.pred_var_ X 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 X ds =>
            if ds.length = (τ X ds.length).1.length then
              Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) (hd :: tl) (τ X ds.length).2
            else I.pred_var_ X ds }
        V tl (def_ X xs)) ↔
    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)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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
h✝ : X = hd.name ∧ xs.length = hd.args.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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X 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

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      V tl (def_ X xs) ↔
    Holds D I V tl (def_ X xs)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X 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
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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
⊢ { 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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 hd.q →
      ({ 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) (hd :: tl) (τ X ds.length).2
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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
⊢ { 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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 hd.q →
      ({ 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) (hd :: tl) (τ X ds.length).2
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet]
Proof state after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp only [hd.h2]
Proof state after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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),
    (P, ds.length) ∈ ∅ →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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),
    (P, ds.length) ∈ ∅ →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        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.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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)
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      V tl (def_ X xs) ↔
    Holds D I V tl (def_ X xs)
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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)
⊢ { 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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 ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) (hd :: tl) (τ X ds.length).2
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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)
⊢ { 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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 ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) (hd :: tl) (τ X ds.length).2
                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
τ : PredName → ℕ → 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 ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → 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 ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        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.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let zs := (τ X ds.length).1;
          let H := (τ X ds.length).2;
          if ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ X ds }
      V E F ↔
    Holds D I V E (replace τ F)
Tactic:
apply substitution_theorem_aux D I V V E τ ∅ F
Proof state after:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ admitsAux τ ∅ F

case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ ∀ x ∉ ∅, V x = V x
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ admitsAux τ ∅ F
Tactic:
simp only [admits] at h1
Proof state after:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admitsAux τ ∅ F
⊢ admitsAux τ ∅ F
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admitsAux τ ∅ F
⊢ admitsAux τ ∅ F
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem
Proof state before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ ∀ x ∉ ∅, V x = V x
Tactic:
intro X _
Proof state after:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
X : VarName
a✝ : X ∉ ∅
⊢ V X = V X
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem
Proof state before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
X : VarName
a✝ : X ∉ ∅
⊢ V X = V X
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : F.IsValid
⊢ (replace τ F).IsValid
Tactic:
simp only [IsValid] at h2
Proof state after:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (replace τ F).IsValid
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (replace τ F).IsValid
Tactic:
simp only [IsValid]
Proof state after:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (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 (replace τ F)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (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 (replace τ F)
Tactic:
intro D I V E
Proof state after:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (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 (replace τ F)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (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 (replace τ F)
Tactic:
obtain s1 := substitution_theorem D I V E τ F h1
Proof state after:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (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
s1 :
  Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let zs := (τ X ds.length).1;
          let H := (τ X ds.length).2;
          if ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ X ds }
      V E F ↔
    Holds D I V E (replace τ F)
⊢ Holds D I V E (replace τ F)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (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
s1 :
  Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let zs := (τ X ds.length).1;
          let H := (τ X ds.length).2;
          if ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ X ds }
      V E F ↔
    Holds D I V E (replace τ F)
⊢ Holds D I V E (replace τ F)
Tactic:
simp only [← s1]
Proof state after:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (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
s1 :
  Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let zs := (τ X ds.length).1;
          let H := (τ X ds.length).2;
          if ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ X ds }
      V E F ↔
    Holds D I V E (replace τ F)
⊢ 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 F
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_is_valid
Proof state before:
F : Formula
τ : PredName → ℕ → List VarName × Formula
h1 : admits τ F
h2 : ∀ (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
s1 :
  Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let zs := (τ X ds.length).1;
          let H := (τ X ds.length).2;
          if ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ X ds }
      V E F ↔
    Holds D I V E (replace τ F)
⊢ 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 F
Tactic:
apply h2
Proof state after:
no goals
Theorem: List.map_eq_self_iff
Proof state before:
α : Type
f : α → α
xs : List α
⊢ map f xs = xs ↔ ∀ x ∈ xs, f x = x
Tactic:
induction xs
Proof state after:
case nil
α : Type
f : α → α
⊢ map f [] = [] ↔ ∀ x ∈ [], f x = x

case cons
α : Type
f : α → α
head✝ : α
tail✝ : List α
tail_ih✝ : map f tail✝ = tail✝ ↔ ∀ x ∈ tail✝, f x = x
⊢ map f (head✝ :: tail✝) = head✝ :: tail✝ ↔ ∀ x ∈ head✝ :: tail✝, f x = x
Theorem: List.map_eq_self_iff
Proof state before:
α : Type
f : α → α
⊢ map f [] = [] ↔ ∀ x ∈ [], f x = x
Tactic:
case nil =>
  simp
Proof state after:
no goals
Theorem: List.map_eq_self_iff
Proof state before:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
⊢ map f (hd :: tl) = hd :: tl ↔ ∀ x ∈ hd :: tl, f x = x
Tactic:
case cons hd tl ih =>
  simp
  intro _
  exact ih
Proof state after:
no goals
Theorem: List.map_eq_self_iff
Proof state before:
α : Type
f : α → α
⊢ map f [] = [] ↔ ∀ x ∈ [], f x = x
Tactic:
simp
Proof state after:
no goals
Theorem: List.map_eq_self_iff
Proof state before:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
⊢ map f (hd :: tl) = hd :: tl ↔ ∀ x ∈ hd :: tl, f x = x
Tactic:
simp
Proof state after:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
⊢ f hd = hd → (map f tl = tl ↔ ∀ a ∈ tl, f a = a)
Theorem: List.map_eq_self_iff
Proof state before:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
⊢ f hd = hd → (map f tl = tl ↔ ∀ a ∈ tl, f a = a)
Tactic:
intro _
Proof state after:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
a✝ : f hd = hd
⊢ map f tl = tl ↔ ∀ a ∈ tl, f a = a
Theorem: List.map_eq_self_iff
Proof state before:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
a✝ : f hd = hd
⊢ map f tl = tl ↔ ∀ a ∈ tl, f a = a
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.map_mem_id
Proof state before:
α : Type
f : α → α
xs : List α
h1 : ∀ x ∈ xs, f x = x
⊢ map f xs = xs
Tactic:
induction xs
Proof state after:
case nil
α : Type
f : α → α
h1 : ∀ x ∈ [], f x = x
⊢ map f [] = []

case cons
α : Type
f : α → α
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x = x) → map f tail✝ = tail✝
h1 : ∀ x ∈ head✝ :: tail✝, f x = x
⊢ map f (head✝ :: tail✝) = head✝ :: tail✝
Theorem: List.map_mem_id
Proof state before:
α : Type
f : α → α
h1 : ∀ x ∈ [], f x = x
⊢ map f [] = []
Tactic:
case nil =>
  simp
Proof state after:
no goals
Theorem: List.map_mem_id
Proof state before:
α : Type
f : α → α
h1 : ∀ x ∈ [], f x = x
⊢ map f [] = []
Tactic:
simp
Proof state after:
no goals