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 : 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)
Tactic:
simp 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 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)
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)
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 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)
Tactic:
specialize h2 h1_X (List.map V 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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔ J.pred_var_ P (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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔ J.pred_var_ P (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 [s1] at h2
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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (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 [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
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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ J.pred_var_ P (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
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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ J.pred_var_ P (List.map V h1_ts)
Tactic:
apply h2
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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ h1_X = P ∧ (List.map V h1_ts).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
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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ h1_X = P ∧ (List.map V h1_ts).length = zs.length
Tactic:
simp
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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ h1_X = P ∧ h1_ts.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
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
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 zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ h1_X = P ∧ h1_ts.length = zs.length
Tactic:
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:
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:
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:
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_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' ↔ ¬Holds D J V 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_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' ↔ ¬Holds D J V E h1_phi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.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_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' ↔ Holds D J V E h1_phi
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_1.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_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' ↔ Holds D J V E h1_phi
Tactic:
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_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (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)
h1_ih_2 :
  ∀ (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_psi' ↔ Holds D J V E h1_psi)
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'.iff_ h1_psi') ↔ Holds D J V E (h1_phi.iff_ h1_psi)
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_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (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)
h1_ih_2 :
  ∀ (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_psi' ↔ Holds D J V E h1_psi)
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' ↔ Holds D I V E h1_psi') ↔ (Holds D J V E h1_phi ↔ Holds D J V E h1_psi)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_1.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_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (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)
h1_ih_2 :
  ∀ (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_psi' ↔ Holds D J V E h1_psi)
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' ↔ Holds D J V E h1_phi
Tactic:
exact h1_ih_1 V h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_2.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_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (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)
h1_ih_2 :
  ∀ (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_psi' ↔ Holds D J V E h1_psi)
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_psi' ↔ Holds D J V E h1_psi
Tactic:
exact h1_ih_2 V h2
Proof state after:
no goals