internlm/Lean-Github huggingface dataset:
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:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  first | apply forall_congr' | apply exists_congr
  intro d
  exact phi_ih (Function.updateITE V x d) h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case cons.def_
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)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (def_ a✝¹ a✝)
Tactic:
simp only [predVarOccursIn] at h2
Proof state after:
case cons.def_
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)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (def_ a✝¹ a✝)
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case cons.def_
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)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (def_ a✝¹ a✝)
Tactic:
simp only [Holds]
Proof state after:
case cons.def_
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)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I (Function.updateListITE V head✝.args (List.map V a✝)) tail✝ head✝.q
    else Holds D I V tail✝ (def_ a✝¹ a✝)) ↔
    if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I' (Function.updateListITE V head✝.args (List.map V a✝)) tail✝ head✝.q
    else Holds D I' V tail✝ (def_ a✝¹ a✝)
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 : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_const_ X (List.map V xs) ↔ I'.pred_const_ X (List.map V xs)
Tactic:
simp only [h1]
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 : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = X ∧ ds.length = xs.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
simp at h2
Proof state after:
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 : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = X → ds.length = xs.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
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 : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = X → ds.length = xs.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
specialize h2 X (List.map V xs)
Proof state after:
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 : PredName
xs : List VarName
V : VarAssignment D
h2 : X = X → (List.map V xs).length = xs.length → (I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs))
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
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 : PredName
xs : List VarName
V : VarAssignment D
h2 : X = X → (List.map V xs).length = xs.length → (I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs))
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
simp at h2
Proof state after:
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 : PredName
xs : List VarName
V : VarAssignment D
h2 : I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
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 : PredName
xs : List VarName
V : VarAssignment D
h2 : I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
exact 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)
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)
⊢ ¬Holds D I V (head✝ :: tail✝) phi ↔ ¬Holds D I' V (head✝ :: tail✝) phi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.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 : 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)
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_1.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 : 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)
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi
Tactic:
exact phi_ih V h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_1.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)
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi
Tactic:
apply phi_ih
Proof state after:
case a.h.e'_1.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 phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_1.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 phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
Tactic:
intro P ds a1
Proof state after:
case a.h.e'_1.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 phi
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_1.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 phi
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
apply h2
Proof state after:
case a.h.e'_1.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 phi
⊢ predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_1.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 phi
⊢ predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi
Tactic:
left
Proof state after:
case a.h.e'_1.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 phi
⊢ predVarOccursIn P ds.length phi
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_1.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 phi
⊢ predVarOccursIn P ds.length phi
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
case a.h.e'_2.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)
⊢ Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi
Tactic:
apply psi_ih
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), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)