internlm/Lean-Github huggingface dataset:
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 : (P, ds.length) ∈ hd.q.predVarSet
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
simp only [hd.h2] 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) ∈ ∅
⊢ 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 : (P, ds.length) ∈ ∅
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
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:
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 (def_ X xs) → (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 (def_ X xs) → (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 (def_ X xs)
⊢ 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 (def_ X xs)
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
simp only [predVarOccursIn] at a1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ¬Holds D I V E' phi ↔ ¬Holds D I V E phi
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih V h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) E' phi) ↔ ∃ d, Holds D I (Function.updateITE V x d) E phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih
  exact h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ a✝¹ a✝)
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)
Tactic:
simp only [all_def_in_env] at h2
Proof state after:
case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, a✝¹ = d.name ∧ a✝.length = d.args.length
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ Holds D I V E' (exists_ a✝¹ a✝) ↔ Holds D I V E (exists_ a✝¹ a✝)
Tactic:
simp only [Holds]
Proof state after:
case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ (∃ d, Holds D I (Function.updateITE V a✝¹ d) E' a✝) ↔ ∃ d, Holds D I (Function.updateITE V a✝¹ d) E a✝
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ¬Holds D I V E' phi ↔ ¬Holds D I V E phi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ Holds D I V E' phi ↔ Holds D I V E phi
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ Holds D I V E' phi ↔ Holds D I V E phi
Tactic:
exact phi_ih V h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2 : all_def_in_env E phi ∧ all_def_in_env E psi
⊢ (Holds D I V E' phi ↔ Holds D I V E' psi) ↔ (Holds D I V E phi ↔ Holds D I V E psi)
Tactic:
cases h2
Proof state after:
case intro
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
left✝ : all_def_in_env E phi
right✝ : all_def_in_env E psi
⊢ (Holds D I V E' phi ↔ Holds D I V E' psi) ↔ (Holds D I V E phi ↔ Holds D I V E psi)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ (Holds D I V E' phi ↔ Holds D I V E' psi) ↔ (Holds D I V E phi ↔ Holds D I V E psi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' phi ↔ Holds D I V E phi

case a.h.e'_2.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' psi ↔ Holds D I V E psi
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' phi ↔ Holds D I V E phi
Tactic:
exact phi_ih V h2_left
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' psi ↔ Holds D I V E psi
Tactic:
exact psi_ih V h2_right
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) E' phi) ↔ ∃ d, Holds D I (Function.updateITE V x d) E phi
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
d : D
⊢ Holds D I (Function.updateITE V x d) E' phi ↔ Holds D I (Function.updateITE V x d) E phi
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
d : D
⊢ Holds D I (Function.updateITE V x d) E' phi ↔ Holds D I (Function.updateITE V x d) E phi
Tactic:
apply phi_ih
Proof state after:
case h.h2
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
d : D
⊢ all_def_in_env E phi
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case h.h2
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
d : D
⊢ all_def_in_env E phi
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) E' phi) ↔ ∀ (d : D), Holds D I (Function.updateITE V x d) E phi
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) E' phi) ↔ ∃ d, Holds D I (Function.updateITE V x d) E phi
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
apply Exists.elim h1
Proof state after:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
⊢ ∀ (a : Env), E' = a ++ E → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
⊢ ∀ (a : Env), E' = a ++ E → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))
Tactic:
intro E1 h1_1
Proof state after:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
clear h1
Proof state after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp only [all_def_in_env] at h2
Proof state after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
apply Exists.elim h2
Proof state after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ ∀ (a : Definition),
    a ∈ E ∧ X = a.name ∧ xs.length = a.args.length → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ ∀ (a : Definition),
    a ∈ E ∧ X = a.name ∧ xs.length = a.args.length → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))
Tactic:
intro a h2_1
Proof state after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
clear h2
Proof state after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp only [Env.nodup_] at h3
Proof state after:
D : Type
I : Interpretation D
E E' : Env
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) E'
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E E' : Env
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) E'
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
subst h1_1
Proof state after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1 ++ E)
⊢ Holds D I V (E1 ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1 ++ E)
⊢ Holds D I V (E1 ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
induction E1
Proof state after:
case nil
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V ([] ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

case cons
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (tail✝ ++ E) →
    (Holds D I V (tail✝ ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (head✝ :: tail✝ ++ E)
⊢ Holds D I V (head✝ :: tail✝ ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V ([] ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
case nil =>
  simp
Proof state after:
no goals