internlm/Lean-Github huggingface dataset:
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
a1 : isFreeIn v H
⊢ Function.updateListITE (Function.updateITE V h1_x d) zs ds v = Function.updateListITE V zs ds v
Tactic:
apply Function.updateListITE_updateIte
Proof state after:
case h1.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
⊢ ¬v = h1_x
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h1.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
⊢ ¬v = h1_x
Tactic:
intro contra
Proof state after:
case h1.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
contra : v = h1_x
⊢ False
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h1.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
contra : v = h1_x
⊢ False
Tactic:
subst contra
Proof state after:
case h1.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_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
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
h1_1 : ¬isFreeIn v H
⊢ False
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h1.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_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
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
h1_1 : ¬isFreeIn v H
⊢ False
Tactic:
contradiction
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)
X : DefName
xs : 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 (def_ X xs) ↔ Holds D J V E (def_ X xs)
Tactic:
cases E
Proof state after:
case nil
D : Type
I J : Interpretation D
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)
X : DefName
xs : 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) [] H ↔ J.pred_var_ P ds)
⊢ Holds D I V [] (def_ X xs) ↔ Holds D J V [] (def_ X xs)

case cons
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
head✝ : Definition
tail✝ : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (head✝ :: tail✝) H ↔ J.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (def_ X xs) ↔ Holds D J V (head✝ :: tail✝) (def_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
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)
X : DefName
xs : 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) [] H ↔ J.pred_var_ P ds)
⊢ Holds D I V [] (def_ X xs) ↔ Holds D J V [] (def_ X xs)
Tactic:
case nil =>
  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
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)
X : DefName
xs : 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) [] H ↔ J.pred_var_ P ds)
⊢ Holds D I V [] (def_ X xs) ↔ Holds D J V [] (def_ X xs)
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
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
⊢ Holds D I V (hd :: tl) (def_ X xs) ↔ Holds D J V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D J (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D J V tl (def_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D J (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D J V tl (def_ X xs)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D J (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

case neg
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D J V tl (def_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D J (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ I.pred_const_ = J.pred_const_

case h2
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length hd.q → (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
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.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
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length hd.q → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet]
Proof state after:
case h2
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), (P, ds.length) ∈ hd.q.predVarSet → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h2
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), (P, ds.length) ∈ hd.q.predVarSet → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp only [hd.h2]
Proof state after:
case h2
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), (P, ds.length) ∈ ∅ → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h2
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), (P, ds.length) ∈ ∅ → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D J V tl (def_ X xs)
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ I.pred_const_ = J.pred_const_

case h2
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ X xs) → (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
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.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
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ X xs) → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn]
Proof state after:
case h2
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem
Proof state before:
case h2
D : Type
I J : Interpretation D
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)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_is_valid
Proof state before:
F F' : Formula
P : PredName
zs : List VarName
H : Formula
h1 : IsSub P zs H F F'
h2 : F.IsValid
⊢ F'.IsValid
Tactic:
simp only [IsValid] at h2
Proof state after:
F F' : Formula
P : PredName
zs : List VarName
H : Formula
h1 : IsSub P zs H F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ F'.IsValid