internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_2.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
Tactic:
intro P ds a1
Proof state after:
case a.h.e'_2.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_2.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
apply h2
Proof state after:
case a.h.e'_2.a.h2.a
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_2.a.h2.a
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi
Tactic:
right
Proof state after:
case a.h.e'_2.a.h2.a.h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ predVarOccursIn P ds.length psi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_2.a.h2.a.h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ predVarOccursIn P ds.length psi
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I' (Function.updateITE V x d) (head✝ :: tail✝) phi
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I' (Function.updateITE V x a) (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I' (Function.updateITE V x a) (head✝ :: tail✝) phi
Tactic:
intro d
Proof state after:
case h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi ↔ Holds D I' (Function.updateITE V x d) (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi ↔ Holds D I' (Function.updateITE V x d) (head✝ :: tail✝) phi
Tactic:
exact phi_ih (Function.updateITE V x d) h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I' (Function.updateITE V x d) (head✝ :: tail✝) phi
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I' (Function.updateITE V x a) (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I' (Function.updateITE V x d) (head✝ :: tail✝) phi
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I' (Function.updateITE V x a) (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.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 I' (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I' V tl (def_ X xs)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.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 I' (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

case neg
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I' V tl (def_ X xs)
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.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 I' (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
case pos c1 =>
  apply ih
  intro P ds a1
  simp only [predVarOccursIn_iff_mem_predVarSet P ds.length] at a1
  simp only [hd.h2] at a1
  simp at a1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I' V tl (def_ X xs)
Tactic:
case neg c1 =>
  apply ih
  intro P ds a1
  simp only [predVarOccursIn] at a1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.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 I' (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
apply ih
Proof state after:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.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 ↔ I'.pred_var_ P ds)
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.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 ↔ I'.pred_var_ P ds)
Tactic:
intro P ds a1
Proof state after:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length hd.q
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length hd.q
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet P ds.length] at a1
Proof state after:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : (P, ds.length) ∈ hd.q.predVarSet
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds