internlm/Lean-Github huggingface dataset:
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:
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 : 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)
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi') ↔ ∃ d, Holds D J (Function.updateITE V h1_x d) E h1_phi
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)
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi') ↔ ∃ d, Holds D J (Function.updateITE V h1_x d) E h1_phi
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
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)
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x a) E h1_phi
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h
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)
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x a) E h1_phi
Tactic:
intro d
Proof state after:
case h
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)
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x d) E h1_phi
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h
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)
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply h1_ih
Proof state after:
case h.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 : 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)
d : D
⊢ ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length →
      (Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h.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 : 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)
d : D
⊢ ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length →
      (Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds)
Tactic:
intro Q ds a1
Proof state after:
case h.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 : 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)
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h.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 : 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)
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Tactic:
specialize h2 Q ds a1
Proof state after:
case h.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 : 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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h.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 : 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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Tactic:
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
Proof state after:
case h.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 : 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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
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
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h.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 : 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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
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
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Tactic:
simp only [h2] at s1
Proof state after:
case h.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 : 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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
s1 : Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h.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 : 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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
s1 : Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Tactic:
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 : 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)
⊢ (∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi') ↔
    ∀ (d : D), Holds D J (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply forall_congr'
Proof state after:
case h
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)
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x a) E h1_phi
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)
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi') ↔ ∃ d, Holds D J (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply exists_congr
Proof state after:
case h
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)
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x a) E h1_phi
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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ 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
Tactic:
apply Holds_coincide_Var
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 : 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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ ∀ (v : VarName),
    isFreeIn v H → Function.updateListITE (Function.updateITE V h1_x d) zs ds v = Function.updateListITE V zs ds v
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 : 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
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ ∀ (v : VarName),
    isFreeIn v H → Function.updateListITE (Function.updateITE V h1_x d) zs ds v = Function.updateListITE V zs ds v
Tactic:
intro v a1
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 : 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
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
⊢ Function.updateListITE (Function.updateITE V h1_x d) zs ds v = Function.updateListITE V zs ds v