internlm/Lean-Github huggingface dataset:
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case right
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ X = d.name ∧ xs.length = d.args.length
Tactic:
exact h2_1_right
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
apply E_ih
Proof state after:
case h1
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ ∃ E1, E' = E1 ++ E_tl

case h2
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ IsMetaVarOrAllDefInEnv E_tl (def_ X xs)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case h1
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ ∃ E1, E' = E1 ++ E_tl
Tactic:
apply Exists.intro (E1 ++ [E_hd])
Proof state after:
case h1
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ E' = E1 ++ [E_hd] ++ E_tl
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case h1
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ E' = E1 ++ [E_hd] ++ E_tl
Tactic:
simp
Proof state after:
case h1
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ E' = E1 ++ E_hd :: E_tl
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case h1
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ E' = E1 ++ E_hd :: E_tl
Tactic:
exact h1_1
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case h2
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ IsMetaVarOrAllDefInEnv E_tl (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
case h2
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ ∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case h2
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ ∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length
Tactic:
apply Exists.intro d
Proof state after:
case h2
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ d ∈ E_tl ∧ X = d.name ∧ xs.length = d.args.length
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case h2
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ d ∈ E_tl ∧ X = d.name ∧ xs.length = d.args.length
Tactic:
constructor
Proof state after:
case h2.left
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ d ∈ E_tl

case h2.right
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ X = d.name ∧ xs.length = d.args.length
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case h2.left
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ d ∈ E_tl
Tactic:
exact c1
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case h2.right
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1_right : X = d.name ∧ xs.length = d.args.length
c1 : d ∈ E_tl
⊢ X = d.name ∧ xs.length = d.args.length
Tactic:
exact h2_1_right
Proof state after:
no goals
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
d : Definition
h1 : E.WellFormed
h2 : d ∈ E
⊢ IsMetaVarOrAllDefInEnv E d.F
Tactic:
induction E
Proof state after:
case nil
d : Definition
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ IsMetaVarOrAllDefInEnv [] d.F

case cons
d head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Env.WellFormed tail✝ → d ∈ tail✝ → IsMetaVarOrAllDefInEnv tail✝ d.F
h1 : Env.WellFormed (head✝ :: tail✝)
h2 : d ∈ head✝ :: tail✝
⊢ IsMetaVarOrAllDefInEnv (head✝ :: tail✝) d.F
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d : Definition
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ IsMetaVarOrAllDefInEnv [] d.F
Tactic:
case nil =>
  simp at h2
Proof state after:
no goals
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d : Definition
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ IsMetaVarOrAllDefInEnv [] d.F
Tactic:
simp at h2
Proof state after:
no goals
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
unfold Env.WellFormed at h1
Proof state after:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d ∈ hd :: tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d ∈ hd :: tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
simp at h2
Proof state after:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
h2 : d = hd ∨ d ∈ tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
h2 : d = hd ∨ d ∈ tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
cases h1
Proof state after:
case intro
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
left✝ : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
right✝ : IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right : IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
cases h1_right
Proof state after:
case intro
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
left✝ : IsMetaVarOrAllDefInEnv tl hd.F
right✝ : Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
Tactic:
apply concat_env_preserves_is_meta_var_or_all_def_in_env tl (hd :: tl)
Proof state after:
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ ∃ E1, hd :: tl = E1 ++ tl

case h2
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv tl d.F
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ ∃ E1, hd :: tl = E1 ++ tl
Tactic:
apply Exists.intro [hd]
Proof state after:
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ hd :: tl = [hd] ++ tl
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ hd :: tl = [hd] ++ tl
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
case h2
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
cases h2
Proof state after:
case h2.inl
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
h✝ : d = hd
⊢ IsMetaVarOrAllDefInEnv tl d.F

case h2.inr
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
h✝ : d ∈ tl
⊢ IsMetaVarOrAllDefInEnv tl d.F
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : d = hd
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
case _ c1 =>
  subst c1
  exact h1_right_left
Proof state after:
no goals
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : d ∈ tl
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
case _ c1 =>
  exact ih h1_right_right c1
Proof state after:
no goals
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : d = hd
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
subst c1
Proof state after:
d : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_right_right : Env.WellFormed tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
⊢ IsMetaVarOrAllDefInEnv tl d.F
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_right_right : Env.WellFormed tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
exact h1_right_left
Proof state after:
no goals
Theorem: MM0.def_in_well_formed_env_is_meta_var_or_all_def_in_env
Proof state before:
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : d ∈ tl
⊢ IsMetaVarOrAllDefInEnv tl d.F
Tactic:
exact ih h1_right_right c1
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
V V' : Valuation D
M : MetaValuation D
E : Env
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M E F ↔ Holds D I V' M E F
Tactic:
induction E generalizing F vs V V'
Proof state after:
case nil
D : Type
I : Interpretation D
M : MetaValuation D
V V' : Valuation D
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M [] F ↔ Holds D I V' M [] F

case cons
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
V V' : Valuation D
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) F ↔ Holds D I V' M (head✝ :: tail✝) F
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I V' M [] (def_ X xs)
Tactic:
case nil.def_ X xs =>
  simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : MetaVarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ X)
Tactic:
case meta_var_ X =>
  unfold NoMetaVarAndAllFreeInList at h1
  contradiction
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ X xs)
Tactic:
case pred_ X xs =>
  unfold NoMetaVarAndAllFreeInList at h1
  simp only [Holds]
  congr! 1
  simp only [List.map_eq_map_iff]
  tauto
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) true_ ↔ Holds D I V' M (head✝ :: tail✝) true_
Tactic:
case true_ =>
  simp only [Holds]
Proof state after:
no goals
Theorem: MM0.holds_coincide_var
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V' M (head✝ :: tail✝) phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  simp only [Holds]
  congr! 1
  exact phi_ih V V' vs h1 h2
Proof state after:
no goals