internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ¬(X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length)
s2 : Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ (I' D I V'' (E_hd :: E_tl) τ).pred_const_ = (I' D I V'' E_tl τ).pred_const_
Tactic:
simp only [I']
Proof state after:
case h1
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ¬(X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length)
s2 : Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ (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_hd :: E_tl) ((τ X ds.length).get ⋯).2
          else I.pred_var_ X ds
        else I.pred_var_ X ds).pred_const_ =
    (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_tl ((τ X ds.length).get ⋯).2
          else I.pred_var_ X ds
        else I.pred_var_ X ds).pred_const_
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ¬(X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length)
s2 : Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ (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_hd :: E_tl) ((τ X ds.length).get ⋯).2
          else I.pred_var_ X ds
        else I.pred_var_ X ds).pred_const_ =
    (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_tl ((τ X ds.length).get ⋯).2
          else I.pred_var_ X ds
        else I.pred_var_ X ds).pred_const_
Tactic:
simp only [Interpretation.usingPred]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ¬(X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length)
s2 : Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (def_ X xs) →
      ((I' D I V'' (E_hd :: E_tl) τ).pred_var_ P ds ↔ (I' D I V'' E_tl τ).pred_var_ P ds)
Tactic:
intro P ds a1
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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ¬(X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length)
s2 : Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length (def_ X xs)
⊢ (I' D I V'' (E_hd :: E_tl) τ).pred_var_ P ds ↔ (I' D I V'' E_tl τ).pred_var_ P ds
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ¬(X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length)
s2 : Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length (def_ X xs)
⊢ (I' D I V'' (E_hd :: E_tl) τ).pred_var_ P ds ↔ (I' D I V'' E_tl τ).pred_var_ P ds
Tactic:
simp only [predVarOccursIn] at a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ Holds D (I' D I V E τ) V E F ↔ Holds D I V E (sub c τ F)
Tactic:
apply substitution_theorem_aux
Proof state after:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ (x : VarName), isFreeIn x F → V x = V (id x)

case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ x ∈ F.predVarSet.biUnion (predVarFreeVarSet τ), V x = V x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ (x : VarName), isFreeIn x F → V x = V (id x)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem
Proof state before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ x ∈ F.predVarSet.biUnion (predVarFreeVarSet τ), V x = V x
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_is_valid
Proof state before:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : F.IsValid
⊢ (sub c τ F).IsValid
Tactic:
simp only [IsValid] at h1
Proof state after:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (sub c τ F).IsValid
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_is_valid
Proof state before:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (sub c τ F).IsValid
Tactic:
simp only [IsValid]
Proof state after:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (sub c τ F)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_is_valid
Proof state before:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (sub c τ F)
Tactic:
intro D I V E
Proof state after:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (sub c τ F)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_is_valid
Proof state before:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (sub c τ F)
Tactic:
simp only [← substitution_theorem]
Proof state after:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D (I' D I V E τ) V E F
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_is_valid
Proof state before:
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
h1 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D (I' D I V E τ) V E F
Tactic:
apply h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (pred_const_ h1_X h1_ts) ↔ Holds D J V E (pred_const_ h1_X h1_ts)
Tactic:
case pred_const_ h1_X h1_ts =>
  simp only [Holds]
  simp only [h3_const]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
case pred_occurs_in h1_X h1_ts h1_1 h1_2 =>
  obtain s1 := Sub.Var.All.Rec.substitution_theorem D I V E (Function.updateListITE id zs h1_ts) H h1_2
  obtain s2 := Function.updateListITE_comp id V zs h1_ts
  simp only [s2] at s1
  simp at s1
  specialize h2 h1_X (List.map V h1_ts)
  simp only [s1] at h2
  simp only [Holds]
  apply h2
  simp
  exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x h1_y : VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (eq_ h1_x h1_y) ↔ Holds D J V E (eq_ h1_x h1_y)
Tactic:
case eq_ h1_x h1_y =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E false_ ↔ Holds D J V E false_
Tactic:
case true_ | false_ =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_phi'.not_ ↔ Holds D J V E h1_phi.not_
Tactic:
case not_ h1_phi h1_phi' _ h1_ih =>
  simp only [Holds]
  congr! 1
  exact h1_ih V h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (exists_ h1_x h1_phi') ↔ Holds D J V E (exists_ h1_x h1_phi)
Tactic:
case
  forall_ h1_x h1_phi h1_phi' h1_1 _ h1_ih
| exists_ h1_x h1_phi h1_phi' h1_1 _ h1_ih =>
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply h1_ih
  intro Q ds a1
  specialize h2 Q ds a1
  have s1 :
    Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔
      Holds D I (Function.updateListITE V zs ds) E H :=
    by
    apply Holds_coincide_Var
    intro v a1
    apply Function.updateListITE_updateIte
    intro contra
    subst contra
    contradiction
  simp only [h2] at s1
  exact s1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (pred_const_ h1_X h1_ts) ↔ Holds D J V E (pred_const_ h1_X h1_ts)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ I.pred_const_ h1_X (List.map V h1_ts) ↔ J.pred_const_ h1_X (List.map V h1_ts)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ I.pred_const_ h1_X (List.map V h1_ts) ↔ J.pred_const_ h1_X (List.map V h1_ts)
Tactic:
simp only [h3_const]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : ¬(h1_X = P ∧ h1_ts.length = zs.length)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (pred_var_ h1_X h1_ts) ↔ Holds D J V E (pred_var_ h1_X h1_ts)
Tactic:
simp at h1_1
Proof state after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ Holds D I V E (pred_var_ h1_X h1_ts) ↔ Holds D J V E (pred_var_ h1_X h1_ts)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ Holds D I V E (pred_var_ h1_X h1_ts) ↔ Holds D J V E (pred_var_ h1_X h1_ts)
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ I.pred_const_ = J.pred_const_

case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (pred_var_ h1_X h1_ts) → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ I.pred_const_ = J.pred_const_
Tactic:
exact h3_const
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (pred_var_ h1_X h1_ts) → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
intro X ds a1
Proof state after:
case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
X : PredName
ds : List D
a1 : predVarOccursIn X ds.length (pred_var_ h1_X h1_ts)
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds