internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_coincide_meta_var
Proof state before:
case neg
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I V M' E_tl (def_ X xs)
Tactic:
apply E_ih
Proof state after:
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
Theorem: MM0.holds_coincide_meta_var
Proof state before:
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
Tactic:
unfold Formula.metaVarSet
Proof state after:
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'
Theorem: MM0.holds_coincide_meta_var
Proof state before:
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.holds_coincide_meta_var_no_meta_var
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
E : Env
F : Formula
h1 : F.metaVarSet = ∅
⊢ Holds D I V M E F ↔ Holds D I V M' E F
Tactic:
apply holds_coincide_meta_var
Proof state after:
case h1
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
E : Env
F : Formula
h1 : F.metaVarSet = ∅
⊢ ∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V'
Theorem: MM0.holds_coincide_meta_var_no_meta_var
Proof state before:
case h1
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
E : Env
F : Formula
h1 : F.metaVarSet = ∅
⊢ ∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V'
Tactic:
simp only [h1]
Proof state after:
case h1
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
E : Env
F : Formula
h1 : F.metaVarSet = ∅
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'
Theorem: MM0.holds_coincide_meta_var_no_meta_var
Proof state before:
case h1
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
E : Env
F : Formula
h1 : F.metaVarSet = ∅
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
name : DefName
args : List VarName
h1 : Holds D I V M E (def_ name args)
⊢ ∃ d ∈ E, name = d.name ∧ args.length = d.args.length
Tactic:
induction E
Proof state after:
case nil
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
h1 : Holds D I V M [] (def_ name args)
⊢ ∃ d ∈ [], name = d.name ∧ args.length = d.args.length

case cons
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I V M tail✝ (def_ name args) → ∃ d ∈ tail✝, name = d.name ∧ args.length = d.args.length
h1 : Holds D I V M (head✝ :: tail✝) (def_ name args)
⊢ ∃ d ∈ head✝ :: tail✝, name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
h1 : Holds D I V M [] (def_ name args)
⊢ ∃ d ∈ [], name = d.name ∧ args.length = d.args.length
Tactic:
case nil =>
  simp only [Holds] at h1
Proof state after:
no goals
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
h1 : Holds D I V M [] (def_ name args)
⊢ ∃ d ∈ [], name = d.name ∧ args.length = d.args.length
Tactic:
simp only [Holds] at h1
Proof state after:
no goals
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h1 : Holds D I V M (E_hd :: E_tl) (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
simp only [Holds] at h1
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h1 :
  if name = E_hd.name ∧ args.length = E_hd.args.length then
    Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
  else Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h1 :
  if name = E_hd.name ∧ args.length = E_hd.args.length then
    Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
  else Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
split_ifs at h1
Proof state after:
case pos
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h✝ : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length

case neg
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h✝ : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
case _ c1 =>
  apply Exists.intro E_hd
  simp
  exact c1
Proof state after:
no goals
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
apply Exists.intro E_hd
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ E_hd ∈ E_hd :: E_tl ∧ name = E_hd.name ∧ args.length = E_hd.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ E_hd ∈ E_hd :: E_tl ∧ name = E_hd.name ∧ args.length = E_hd.args.length
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ name = E_hd.name ∧ args.length = E_hd.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ name = E_hd.name ∧ args.length = E_hd.args.length
Tactic:
exact c1
Proof state after:
no goals
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
specialize E_ih h1
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
apply Exists.elim E_ih
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
⊢ ∀ (a : Definition),
    a ∈ E_tl ∧ name = a.name ∧ args.length = a.args.length →
      ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
⊢ ∀ (a : Definition),
    a ∈ E_tl ∧ name = a.name ∧ args.length = a.args.length →
      ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
intro d E_ih_1
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1 : d ∈ E_tl ∧ name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1 : d ∈ E_tl ∧ name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
cases E_ih_1
Proof state after:
case intro
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
left✝ : d ∈ E_tl
right✝ : name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
apply Exists.intro d
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_hd :: E_tl ∧ name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_hd :: E_tl ∧ name = d.name ∧ args.length = d.args.length
Tactic:
constructor
Proof state after:
case left
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_hd :: E_tl

case right
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ name = d.name ∧ args.length = d.args.length
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
case left
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_hd :: E_tl
Tactic:
simp
Proof state after:
case left
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d = E_hd ∨ d ∈ E_tl
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
case left
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d = E_hd ∨ d ∈ E_tl
Tactic:
right
Proof state after:
case left.h
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_tl
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
case left.h
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_tl
Tactic:
exact E_ih_1_left
Proof state after:
no goals
Theorem: MM0.def_holds_imp_def_in_env
Proof state before:
case right
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ name = d.name ∧ args.length = d.args.length
Tactic:
exact E_ih_1_right
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ E
h2 : IsMetaVarOrAllDefInEnv E F
h3 : E'.Nodup
⊢ Holds D I V M E' F ↔ Holds D I V M E F
Tactic:
induction F generalizing V
Proof state after:
case meta_var_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝ : MetaVarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (meta_var_ a✝)
⊢ Holds D I V M E' (meta_var_ a✝) ↔ Holds D I V M E (meta_var_ a✝)

case pred_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ : PredName
a✝ : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)
⊢ Holds D I V M E' (pred_ a✝¹ a✝) ↔ Holds D I V M E (pred_ a✝¹ a✝)

case eq_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ a✝ : VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)
⊢ Holds D I V M E' (eq_ a✝¹ a✝) ↔ Holds D I V M E (eq_ a✝¹ a✝)

case true_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I V M E' true_ ↔ Holds D I V M E true_

case not_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝ : Formula
a_ih✝ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝ → (Holds D I V M E' a✝ ↔ Holds D I V M E a✝)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E a✝.not_
⊢ Holds D I V M E' a✝.not_ ↔ Holds D I V M E a✝.not_

case imp_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝¹ → (Holds D I V M E' a✝¹ ↔ Holds D I V M E a✝¹)
a_ih✝ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝ → (Holds D I V M E' a✝ ↔ Holds D I V M E a✝)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)
⊢ Holds D I V M E' (a✝¹.imp_ a✝) ↔ Holds D I V M E (a✝¹.imp_ a✝)

case forall_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝ → (Holds D I V M E' a✝ ↔ Holds D I V M E a✝)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)
⊢ Holds D I V M E' (forall_ a✝¹ a✝) ↔ Holds D I V M E (forall_ a✝¹ a✝)

case def_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ : DefName
a✝ : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)
⊢ Holds D I V M E' (def_ a✝¹ a✝) ↔ Holds D I V M E (def_ a✝¹ a✝)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : MetaVarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I V M E' (meta_var_ X) ↔ Holds D I V M E (meta_var_ X)
Tactic:
case meta_var_ X =>
  simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : PredName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I V M E' (pred_ X xs) ↔ Holds D I V M E (pred_ X xs)
Tactic:
case pred_ X xs =>
  simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x y : VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I V M E' (eq_ x y) ↔ Holds D I V M E (eq_ x y)
Tactic:
case eq_ x y =>
  simp only [Holds]
Proof state after:
no goals