internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
apply holds_coincide_meta_var_no_meta_var
Proof state after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ E_hd.F.metaVarSet = ∅
Theorem: MM0.holds_sub
Proof state before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ E_hd.F.metaVarSet = ∅
Tactic:
exact s1
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
case s2.h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : 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.holds_sub
Proof state before:
case s2.h2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = (List.map (V ∘ ↑σ) xs).length
Tactic:
simp
Proof state after:
case s2.h2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = xs.length
Theorem: MM0.holds_sub
Proof state before:
case s2.h2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = xs.length
Tactic:
simp only [c1_right]
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h1 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h1 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
simp at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h1 : X = E_hd.name ∧ xs.length = E_hd.args.length ∨ ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h1 : X = E_hd.name ∧ xs.length = E_hd.args.length ∨ ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
cases h1
Proof state after:
case inl
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

case inr
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h✝ : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
case inl c2 =>
  contradiction
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
case inr c2 =>
  unfold sub at E_ih
  simp only [← E_ih c2]
  apply holds_coincide_meta_var
  unfold Formula.metaVarSet
  simp
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
contradiction
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
unfold sub at E_ih
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
simp only [← E_ih c2]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs)
Tactic:
apply holds_coincide_meta_var
Proof state after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ ∀ (V' : Valuation D),
    ∀ X_1 ∈ (def_ X xs).metaVarSet, Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X_1) ↔ Holds D I (V' ∘ σ') M E_tl (τ X_1)
Theorem: MM0.holds_sub
Proof state before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ ∀ (V' : Valuation D),
    ∀ X_1 ∈ (def_ X xs).metaVarSet, Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X_1) ↔ Holds D I (V' ∘ σ') M E_tl (τ X_1)
Tactic:
unfold Formula.metaVarSet
Proof state after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X) ↔ Holds D I (V' ∘ σ') M E_tl (τ X)
Theorem: MM0.holds_sub
Proof state before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X) ↔ Holds D I (V' ∘ σ') M E_tl (τ X)
Tactic:
simp
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
F : Formula
Γ : List (VarName × MetaVarName)
v : VarName
h1 : NotFree Γ v F
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
⊢ IsNotFree D I M E F v
Tactic:
induction F
Proof state after:
case meta_var_
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
a✝ : MetaVarName
h1 : NotFree Γ v (meta_var_ a✝)
⊢ IsNotFree D I M E (meta_var_ a✝) v

case pred_
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
a✝¹ : PredName
a✝ : List VarName
h1 : NotFree Γ v (pred_ a✝¹ a✝)
⊢ IsNotFree D I M E (pred_ a✝¹ a✝) v

case eq_
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
a✝¹ a✝ : VarName
h1 : NotFree Γ v (eq_ a✝¹ a✝)
⊢ IsNotFree D I M E (eq_ a✝¹ a✝) v

case true_
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

case not_
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
a✝ : Formula
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v a✝.not_
⊢ IsNotFree D I M E a✝.not_ v

case imp_
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
a✝¹ a✝ : Formula
a_ih✝¹ : NotFree Γ v a✝¹ → IsNotFree D I M E a✝¹ v
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v (a✝¹.imp_ a✝)
⊢ IsNotFree D I M E (a✝¹.imp_ a✝) v

case forall_
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
a✝¹ : VarName
a✝ : Formula
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v (forall_ a✝¹ a✝)
⊢ IsNotFree D I M E (forall_ a✝¹ a✝) v

case def_
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
a✝¹ : DefName
a✝ : List VarName
h1 : NotFree Γ v (def_ a✝¹ a✝)
⊢ IsNotFree D I M E (def_ a✝¹ a✝) 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 : NotFree Γ v (meta_var_ X)
⊢ IsNotFree D I M E (meta_var_ X) v
Tactic:
case meta_var_ X =>
  unfold NotFree at h1
  exact h2 X h1
Proof state after:
no goals