internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I V M E' true_ ↔ Holds D I V M E true_
Tactic:
case true_ =>
  simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ Holds D I V M E' phi.not_ ↔ Holds D I V M E phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  simp only [Holds]
  congr! 1
  exact phi_ih V h2
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ Holds D I V M E' (forall_ x phi) ↔ Holds D I V M E (forall_ x phi)
Tactic:
case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  simp only [Holds]
  apply forall_congr'
  intro a
  exact phi_ih (Function.updateITE V x a) h2
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : MetaVarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I V M E' (meta_var_ X) ↔ Holds D I V M E (meta_var_ X)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : PredName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I V M E' (pred_ X xs) ↔ Holds D I V M E (pred_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x y : VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I V M E' (eq_ x y) ↔ Holds D I V M E (eq_ x y)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I V M E' true_ ↔ Holds D I V M E true_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ Holds D I V M E' phi.not_ ↔ Holds D I V M E phi.not_
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' phi.not_ ↔ Holds D I V M E phi.not_
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' phi.not_ ↔ Holds D I V M E phi.not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ ¬Holds D I V M E' phi ↔ ¬Holds D I V M E phi
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ ¬Holds D I V M E' phi ↔ ¬Holds D I V M E phi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' phi ↔ Holds D I V M E phi
Theorem: MM0.holds_coincide_env
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' phi ↔ Holds D I V M E phi
Tactic:
exact phi_ih V h2
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
Tactic:
cases h2
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
left✝ : IsMetaVarOrAllDefInEnv E phi
right✝ : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' phi → Holds D I V M E' psi ↔ Holds D I V M E phi → Holds D I V M E psi
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' phi → Holds D I V M E' psi ↔ Holds D I V M E phi → Holds D I V M E psi
Tactic:
congr! 1
Proof state after:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' phi ↔ Holds D I V M E phi

case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
a✝ : Holds D I V M E phi
⊢ Holds D I V M E' psi ↔ Holds D I V M E psi
Theorem: MM0.holds_coincide_env
Proof state before:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' phi ↔ Holds D I V M E phi
Tactic:
exact phi_ih V h2_left
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
a✝ : Holds D I V M E phi
⊢ Holds D I V M E' psi ↔ Holds D I V M E psi
Tactic:
exact psi_ih V h2_right
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ Holds D I V M E' (forall_ x phi) ↔ Holds D I V M E (forall_ x phi)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' (forall_ x phi) ↔ Holds D I V M E (forall_ x phi)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' (forall_ x phi) ↔ Holds D I V M E (forall_ x phi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M E' phi) ↔ ∀ (d : D), Holds D I (Function.updateITE V x d) M E phi
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M E' phi) ↔ ∀ (d : D), Holds D I (Function.updateITE V x d) M E phi
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) M E' phi ↔ Holds D I (Function.updateITE V x a) M E phi
Theorem: MM0.holds_coincide_env
Proof state before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) M E' phi ↔ Holds D I (Function.updateITE V x a) M E phi
Tactic:
intro a
Proof state after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
a : D
⊢ Holds D I (Function.updateITE V x a) M E' phi ↔ Holds D I (Function.updateITE V x a) M E phi
Theorem: MM0.holds_coincide_env
Proof state before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
a : D
⊢ Holds D I (Function.updateITE V x a) M E' phi ↔ Holds D I (Function.updateITE V x a) M E phi
Tactic:
exact phi_ih (Function.updateITE V x a) h2
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
apply Exists.elim h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ ∀ (a : Env), E' = a ++ E → (Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs))
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ ∀ (a : Env), E' = a ++ E → (Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs))
Tactic:
intro E1 h1_1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
clear h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
apply Exists.elim h2
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∀ (a : Definition),
    a ∈ E ∧ X = a.name ∧ xs.length = a.args.length → (Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs))
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∀ (a : Definition),
    a ∈ E ∧ X = a.name ∧ xs.length = a.args.length → (Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs))
Tactic:
intro a h2_1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
clear h2
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation 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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation 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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
unfold Env.Nodup at h3
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation 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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation 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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
cases h2_1
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
left✝ : a ∈ E
right✝ : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1_left : a ∈ E
h2_1_right : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
cases h2_1_right
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1_left : a ∈ E
left✝ : X = a.name
right✝ : xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
subst h1_1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1 ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)