internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_sub
Proof state before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
simp only [← s1]
Proof state after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE V (↑σ x) a ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Theorem: MM0.holds_sub
Proof state before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE V (↑σ x) a ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
exact phi_ih (Function.updateITE V (σ.val x) a) h1
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (def_ X xs) ↔ Holds D I V M E (sub σ τ (def_ X xs))
Tactic:
induction E
Proof state after:
case nil
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))

case cons
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  IsMetaVarOrAllDefInEnv tail✝ (def_ X xs) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M tail✝ (τ X')) tail✝ (def_ X xs) ↔
      Holds D I V M tail✝ (sub σ τ (def_ X xs)))
h1 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (head✝ :: tail✝) (τ X')) (head✝ :: tail✝) (def_ X xs) ↔
    Holds D I V M (head✝ :: tail✝) (sub σ τ (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
h1 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))
Tactic:
case nil =>
  unfold IsMetaVarOrAllDefInEnv at h1
  simp at h1
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
h1 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X 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
h1 : ∃ d ∈ [], X = d.name ∧ xs.length = d.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (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
h1 : ∃ d ∈ [], X = d.name ∧ xs.length = d.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))
Tactic:
simp at h1
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 :
  IsMetaVarOrAllDefInEnv 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) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (def_ X xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv 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
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)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (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
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)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (def_ X xs))
Tactic:
have s1 : E_hd.F.metaVarSet = ∅ :=
  no_meta_var_imp_meta_var_set_is_empty E_hd.F E_hd.args E_hd.nf
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
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 = ∅
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (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
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 = ∅
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (def_ X xs))
Tactic:
unfold sub
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
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 = ∅
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: 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
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 = ∅
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (def_ X (List.map (↑σ) xs))
Tactic:
simp only [Holds]
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
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 = ∅
⊢ (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))
        (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F
    else Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ (List.map (↑σ) xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map (↑σ) xs))) M E_tl E_hd.F
    else 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
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 = ∅
⊢ (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))
        (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F
    else Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ (List.map (↑σ) xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map (↑σ) xs))) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
simp
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
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 = ∅
⊢ (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))
        (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F
    else Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs)) ↔
    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 (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
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 = ∅
⊢ (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))
        (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F
    else Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs)) ↔
    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 (List.map (↑σ) xs))
Tactic:
split_ifs
Proof state after:
case pos
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 = ∅
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ 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

case neg
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 = ∅
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))
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:
case _ c1 =>
  unfold IsMetaVarOrAllDefInEnv at h1
  simp at h1
  cases h1
  case inl c2 =>
    contradiction
  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
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 (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:
cases c1
Proof state after:
case intro
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 = ∅
left✝ : X = E_hd.name
right✝ : xs.length = E_hd.args.length
⊢ 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
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
⊢ 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:
have s2 : Holds D I (Function.updateListITE (V ∘ σ.val) E_hd.args (List.map (V ∘ σ.val) xs)) M E_tl E_hd.F ↔ Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ.val) xs)) M E_tl E_hd.F
Proof state after:
case s2
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
⊢ 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

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
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:
simp only [← s2]
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
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