internlm/Lean-Github huggingface dataset:
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ ∀ (V : Valuation D) (d : D),
    (if X = E_hd.name ∧ xs.length = E_hd.args.length then
        Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
      else Holds D I V M E_tl (def_ X xs)) ↔
      if X = E_hd.name ∧ xs.length = E_hd.args.length then
        Holds D I (Function.updateListITE (Function.updateITE V v d) E_hd.args (List.map (Function.updateITE V v d) xs))
          M E_tl E_hd.F
      else Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
Tactic:
intro V a
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
        E_tl E_hd.F
    else Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
        E_tl E_hd.F
    else Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
      E_tl E_hd.F

case neg
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)
Tactic:
case _ c1 =>
  exact E_ih h2 V a
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
      E_tl E_hd.F
Tactic:
apply holds_coincide_var D I (Function.updateListITE V E_hd.args (List.map V xs)) (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M E_tl E_hd.F E_hd.args E_hd.nf
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ v_1 ∈ E_hd.args,
    Function.updateListITE V E_hd.args (List.map V xs) v_1 =
      Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v_1
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ v_1 ∈ E_hd.args,
    Function.updateListITE V E_hd.args (List.map V xs) v_1 =
      Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v_1
Tactic:
intro v' a1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ Function.updateListITE V E_hd.args (List.map V xs) v' =
    Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v'
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ Function.updateListITE V E_hd.args (List.map V xs) v' =
    Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v'
Tactic:
apply Function.updateListITE_map_updateIte V (Function.updateITE V v a)
Proof state after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ ∀ y ∈ xs, ¬y = v

case h2
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ E_hd.args.length = xs.length

case h3
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ v' ∈ E_hd.args
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ ∀ y ∈ xs, ¬y = v
Tactic:
intro y a2 contra
Proof state after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
y : VarName
a2 : y ∈ xs
contra : y = v
⊢ False
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
y : VarName
a2 : y ∈ xs
contra : y = v
⊢ False
Tactic:
subst contra
Proof state after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
y : VarName
a2 : y ∈ xs
h1 : y ∉ xs
h2 : ∀ (X : MetaVarName), (y, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V y d)
E_ih :
  (∀ (X : MetaVarName), (y, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V y d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V y d) M E_tl (def_ X xs)
⊢ False
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
y : VarName
a2 : y ∈ xs
h1 : y ∉ xs
h2 : ∀ (X : MetaVarName), (y, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V y d)
E_ih :
  (∀ (X : MetaVarName), (y, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V y d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V y d) M E_tl (def_ X xs)
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case h2
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ E_hd.args.length = xs.length
Tactic:
cases c1
Proof state after:
case h2.intro
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
v' : VarName
a1 : v' ∈ E_hd.args
left✝ : X = E_hd.name
right✝ : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
v' : VarName
a1 : v' ∈ E_hd.args
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Tactic:
case intro c1_left c1_right =>
simp only [c1_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
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
v' : VarName
a1 : v' ∈ E_hd.args
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Tactic:
simp only [c1_right]
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
case h3
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ v' ∈ E_hd.args
Tactic:
exact a1
Proof state after:
no goals
Theorem: MM0.not_free_imp_is_not_free
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)
Tactic:
exact E_ih h2 V a
Proof state after:
no goals
Theorem: MM0.lem_1
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
⊢ ∀ (v : VarName) (X : MetaVarName),
    (v, X) ∈ Γ → IsNotFree D I (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) v
Tactic:
intro v X a1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ IsNotFree D I (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) v
Theorem: MM0.lem_1
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ IsNotFree D I (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) v
Tactic:
unfold IsNotFree
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) ↔
      Holds D I (Function.updateITE V v d) (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X)
Theorem: MM0.lem_1
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X) ↔
      Holds D I (Function.updateITE V v d) (fun X V' => Holds D I (V' ∘ σ') M E (τ X)) E (meta_var_ X)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
⊢ ∀ (V : Valuation D) (d : D), Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE V v d ∘ σ') M E (τ X)