internlm/Lean-Github huggingface dataset:
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
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
Tactic:
simp only [predVarOccursIn] at 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 : X = h1_X ∧ ds.length = h1_ts.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
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
X : PredName
ds : List D
a1 : X = h1_X ∧ ds.length = h1_ts.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
Tactic:
cases a1
Proof state after:
case h2.intro
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
left✝ : X = h1_X
right✝ : ds.length = h1_ts.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
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
X : PredName
ds : List D
a1_left : X = h1_X
a1_right : ds.length = h1_ts.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
Tactic:
subst a1_left
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_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)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
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_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)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
Tactic:
apply h3_var
Proof state after:
case a
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_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)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ ¬(X = P ∧ ds.length = zs.length)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a
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_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)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ ¬(X = P ∧ ds.length = zs.length)
Tactic:
simp
Proof state after:
case a
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_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)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ X = P → ¬ds.length = zs.length
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a
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_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)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ X = P → ¬ds.length = zs.length
Tactic:
intro a2
Proof state after:
case a
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_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)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
a2 : X = P
⊢ ¬ds.length = zs.length
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a
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_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)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
a2 : X = P
⊢ ¬ds.length = zs.length
Tactic:
subst a2
Proof state after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : X = X → ¬h1_ts.length = zs.length
⊢ ¬ds.length = zs.length
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : X = X → ¬h1_ts.length = zs.length
⊢ ¬ds.length = zs.length
Tactic:
simp at h1_1
Proof state after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
⊢ ¬ds.length = zs.length
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
⊢ ¬ds.length = zs.length
Tactic:
intro contra
Proof state after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ False
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ False
Tactic:
apply h1_1
Proof state after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = zs.length
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = zs.length
Tactic:
trans List.length ds
Proof state after:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = ds.length

D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ ds.length = zs.length
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = ds.length
Tactic:
simp only [eq_comm]
Proof state after:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ ds.length = h1_ts.length
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ ds.length = h1_ts.length
Tactic:
exact a1_right
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
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ ds.length = zs.length
Tactic:
exact contra
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:
obtain s1 := Sub.Var.All.Rec.substitution_theorem D I V E (Function.updateListITE id zs h1_ts) H h1_2
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
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)
s1 :
  Holds D I (V ∘ Function.updateListITE id zs h1_ts) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ 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)
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)
s1 :
  Holds D I (V ∘ Function.updateListITE id zs h1_ts) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ 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:
obtain s2 := Function.updateListITE_comp id V zs h1_ts
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
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)
s1 :
  Holds D I (V ∘ Function.updateListITE id zs h1_ts) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
⊢ 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)
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)
s1 :
  Holds D I (V ∘ Function.updateListITE id zs h1_ts) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
⊢ 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:
simp only [s2] at s1
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
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)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE (V ∘ id) zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ 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)