internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : MetaVarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ X)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : MetaVarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : False
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ X)
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : MetaVarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : False
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ X)
Tactic:
contradiction
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ X xs)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ X xs)
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ I X (List.map V xs) ↔ I X (List.map V' xs)
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ I X (List.map V xs) ↔ I X (List.map V' xs)
Tactic:
congr! 1
Proof state after:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ List.map V xs = List.map V' xs
Theorem: MM0.holds_coincide_var
Proof state before:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ List.map V xs = List.map V' xs
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ ∀ x ∈ xs, V x = V' x
Theorem: MM0.holds_coincide_var
Proof state before:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ ∀ x ∈ xs, V x = V' x
Tactic:
tauto
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ x y)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : x ∈ vs ∧ y ∈ vs
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : x ∈ vs ∧ y ∈ vs
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)
Tactic:
cases h1
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
left✝ : x ∈ vs
right✝ : y ∈ vs
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V x = V y ↔ V' x = V' y
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V x = V y ↔ V' x = V' y
Tactic:
congr! 1
Proof state after:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V x = V' x

case a.h.e'_3
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V y = V' y
Theorem: MM0.holds_coincide_var
Proof state before:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V x = V' x
Tactic:
exact h2 x h1_left
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
case a.h.e'_3
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V y = V' y
Tactic:
exact h2 y h1_right
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) true_ ↔ Holds D I V' M (head✝ :: tail✝) true_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V' M (head✝ :: tail✝) phi.not_
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V' M (head✝ :: tail✝) phi.not_
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V' M (head✝ :: tail✝) phi.not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ ¬Holds D I V M (head✝ :: tail✝) phi ↔ ¬Holds D I V' M (head✝ :: tail✝) phi
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ ¬Holds D I V M (head✝ :: tail✝) phi ↔ ¬Holds D I V' M (head✝ :: tail✝) phi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi
Theorem: MM0.holds_coincide_var
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi
Tactic:
exact phi_ih V V' vs h1 h2
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V' M (head✝ :: tail✝) (phi.imp_ psi)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V' M (head✝ :: tail✝) (phi.imp_ psi)
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V' M (head✝ :: tail✝) (phi.imp_ psi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi → Holds D I V M (head✝ :: tail✝) psi ↔
    Holds D I V' M (head✝ :: tail✝) phi → Holds D I V' M (head✝ :: tail✝) psi
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi → Holds D I V M (head✝ :: tail✝) psi ↔
    Holds D I V' M (head✝ :: tail✝) phi → Holds D I V' M (head✝ :: tail✝) psi
Tactic:
cases h1
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
left✝ : NoMetaVarAndAllFreeInList vs phi
right✝ : NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi → Holds D I V M (head✝ :: tail✝) psi ↔
    Holds D I V' M (head✝ :: tail✝) phi → Holds D I V' M (head✝ :: tail✝) psi