internlm/Lean-Github huggingface dataset:
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : NotFree Γ v (pred_ X xs)
⊢ IsNotFree D I M E (pred_ X xs) v
Tactic:
case pred_ X xs =>
  unfold NotFree at h1
  unfold IsNotFree
  simp only [Holds]
  intro V d
  congr! 1
  apply List.map_congr
  intro x a1
  have s1 : ¬ x = v
  intro contra
  subst contra
  contradiction
  unfold Function.updateITE
  simp only [if_neg s1]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : NotFree Γ v (eq_ x y)
⊢ IsNotFree D I M E (eq_ x y) v
Tactic:
case eq_ x y =>
  unfold NotFree at h1
  unfold IsNotFree
  simp only [Holds]
  intro V d
  cases h1
  case intro h1_left h1_right =>
    simp only [Function.updateITE]
    simp only [if_neg h1_left]
    simp only [if_neg h1_right]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ IsNotFree D I M E true_ v
Tactic:
case true_ =>
  unfold IsNotFree
  intro V d
  simp only [Holds]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v phi.not_
⊢ IsNotFree D I M E phi.not_ v
Tactic:
case not_ phi phi_ih =>
  unfold NotFree at h1
  unfold IsNotFree at phi_ih
  unfold IsNotFree
  intro V d
  simp only [Holds]
  congr! 1
  exact phi_ih h1 V d
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : MetaVarName
h1 : NotFree Γ v (meta_var_ X)
⊢ IsNotFree D I M E (meta_var_ X) v
Tactic:
unfold NotFree at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : MetaVarName
h1 : (v, X) ∈ Γ
⊢ IsNotFree D I M E (meta_var_ X) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : MetaVarName
h1 : (v, X) ∈ Γ
⊢ IsNotFree D I M E (meta_var_ X) v
Tactic:
exact h2 X h1
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : NotFree Γ v (pred_ X xs)
⊢ IsNotFree D I M E (pred_ X xs) v
Tactic:
unfold NotFree at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ IsNotFree D I M E (pred_ X xs) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ IsNotFree D I M E (pred_ X xs) v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (pred_ X xs) ↔ Holds D I (Function.updateITE V v d) M E (pred_ X xs)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (pred_ X xs) ↔ Holds D I (Function.updateITE V v d) M E (pred_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ ∀ (V : Valuation D) (d : D), I X (List.map V xs) ↔ I X (List.map (Function.updateITE V v d) xs)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ ∀ (V : Valuation D) (d : D), I X (List.map V xs) ↔ I X (List.map (Function.updateITE V v d) xs)
Tactic:
intro V d
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ I X (List.map V xs) ↔ I X (List.map (Function.updateITE V v d) xs)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ I X (List.map V xs) ↔ I X (List.map (Function.updateITE V v d) xs)
Tactic:
congr! 1
Proof state after:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ List.map V xs = List.map (Function.updateITE V v d) xs
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ List.map V xs = List.map (Function.updateITE V v d) xs
Tactic:
apply List.map_congr
Proof state after:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ ∀ x ∈ xs, V x = Function.updateITE V v d x
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ ∀ x ∈ xs, V x = Function.updateITE V v d x
Tactic:
intro x a1
Proof state after:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
⊢ V x = Function.updateITE V v d x
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
⊢ V x = Function.updateITE V v d x
Tactic:
have s1 : ¬ x = v
Proof state after:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
⊢ ¬x = v

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
⊢ ¬x = v

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Tactic:
intro contra
Proof state after:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
contra : x = v
⊢ False

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
contra : x = v
⊢ False

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Tactic:
subst contra
Proof state after:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
X : PredName
xs : List VarName
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
h1 : x ∉ xs
⊢ False

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
X : PredName
xs : List VarName
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
h1 : x ∉ xs
⊢ False

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Tactic:
contradiction
Proof state after:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Tactic:
unfold Function.updateITE
Proof state after:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = if x = v then d else V x
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = if x = v then d else V x
Tactic:
simp only [if_neg s1]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : NotFree Γ v (eq_ x y)
⊢ IsNotFree D I M E (eq_ x y) v
Tactic:
unfold NotFree at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ IsNotFree D I M E (eq_ x y) v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ IsNotFree D I M E (eq_ x y) v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (eq_ x y) ↔ Holds D I (Function.updateITE V v d) M E (eq_ x y)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (eq_ x y) ↔ Holds D I (Function.updateITE V v d) M E (eq_ x y)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Tactic:
intro V d
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
V : Valuation D
d : D
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
V : Valuation D
d : D
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Tactic:
cases h1
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
left✝ : ¬x = v
right✝ : ¬y = v
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Tactic:
case intro h1_left h1_right =>
  simp only [Function.updateITE]
  simp only [if_neg h1_left]
  simp only [if_neg h1_right]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Tactic:
simp only [Function.updateITE]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ (if x = v then d else V x) = if y = v then d else V y
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ (if x = v then d else V x) = if y = v then d else V y
Tactic:
simp only [if_neg h1_left]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ V x = if y = v then d else V y
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ V x = if y = v then d else V y
Tactic:
simp only [if_neg h1_right]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ IsNotFree D I M E true_ v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E true_ ↔ Holds D I (Function.updateITE V v d) M E true_
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E true_ ↔ Holds D I (Function.updateITE V v d) M E true_
Tactic:
intro V d
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
V : Valuation D
d : D
⊢ Holds D I V M E true_ ↔ Holds D I (Function.updateITE V v d) M E true_
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
V : Valuation D
d : D
⊢ Holds D I V M E true_ ↔ Holds D I (Function.updateITE V v d) M E true_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v phi.not_
⊢ IsNotFree D I M E phi.not_ v
Tactic:
unfold NotFree at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v phi
⊢ IsNotFree D I M E phi.not_ v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v phi
⊢ IsNotFree D I M E phi.not_ v
Tactic:
unfold IsNotFree at phi_ih
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
⊢ IsNotFree D I M E phi.not_ v
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
⊢ IsNotFree D I M E phi.not_ v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E phi.not_ ↔ Holds D I (Function.updateITE V v d) M E phi.not_