internlm/Lean-Github huggingface dataset:
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case left
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
Tactic:
exact phi_ih h1_left
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case right
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
Tactic:
exact psi_ih h1_right
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (forall_ x phi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
E : Env
σ : Instantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (forall_ x phi))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (forall_ x phi))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ meta_var_ phi))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ meta_var_ phi))
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (def_ X xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (def_ X xs))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (def_ X xs))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ (List.map (↑σ) xs).length = d.args.length
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ (List.map (↑σ) xs).length = d.args.length
Tactic:
simp
Proof state after:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
Tactic:
exact h1
Proof state after:
no goals
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
E : Env
h1 : E.WellFormed
⊢ E.Nodup
Tactic:
induction E
Proof state after:
case nil
h1 : Env.WellFormed []
⊢ Env.Nodup []

case cons
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Env.WellFormed tail✝ → Env.Nodup tail✝
h1 : Env.WellFormed (head✝ :: tail✝)
⊢ Env.Nodup (head✝ :: tail✝)
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
h1 : Env.WellFormed []
⊢ Env.Nodup []
Tactic:
case nil =>
  unfold Env.Nodup
  simp
Proof state after:
no goals
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
h1 : Env.WellFormed []
⊢ Env.Nodup []
Tactic:
unfold Env.Nodup
Proof state after:
h1 : Env.WellFormed []
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) []
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
h1 : Env.WellFormed []
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) []
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → Env.Nodup tl
h1 : Env.WellFormed (hd :: tl)
⊢ Env.Nodup (hd :: tl)
Tactic:
unfold Env.Nodup at ih
Proof state after:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
h1 : Env.WellFormed (hd :: tl)
⊢ Env.Nodup (hd :: tl)
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
h1 : Env.WellFormed (hd :: tl)
⊢ Env.Nodup (hd :: tl)
Tactic:
unfold Env.WellFormed at h1
Proof state after:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Env.Nodup (hd :: tl)
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Env.Nodup (hd :: tl)
Tactic:
cases h1
Proof state after:
case intro
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
left✝ : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
right✝ : IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Env.Nodup (hd :: tl)
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ Env.Nodup (hd :: tl)
Tactic:
cases h1_right
Proof state after:
case intro
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ Env.Nodup (hd :: tl)
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ Env.Nodup (hd :: tl)
Tactic:
unfold Env.Nodup
Proof state after:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (hd :: tl)
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (hd :: tl)
Tactic:
simp
Proof state after:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ (∀ a' ∈ tl, hd.name = a'.name → ¬hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ (∀ a' ∈ tl, hd.name = a'.name → ¬hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl
Tactic:
constructor
Proof state after:
case left
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ ∀ a' ∈ tl, hd.name = a'.name → ¬hd.args.length = a'.args.length

case right
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
case left
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ ∀ a' ∈ tl, hd.name = a'.name → ¬hd.args.length = a'.args.length
Tactic:
exact h1_left
Proof state after:
no goals
Theorem: MM0.well_formed_env_has_no_dup
Proof state before:
case right
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl
Tactic:
exact ih h1_right_right
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ E
h2 : IsMetaVarOrAllDefInEnv E F
⊢ IsMetaVarOrAllDefInEnv E' F
Tactic:
induction E generalizing F
Proof state after:
case nil
E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ []
h2 : IsMetaVarOrAllDefInEnv [] F
⊢ IsMetaVarOrAllDefInEnv E' F

case cons
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
F : Formula
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) F
⊢ IsMetaVarOrAllDefInEnv E' F
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
h1 : ∃ E1, E' = E1 ++ []
X : DefName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
case nil.def_ X xs =>
  unfold IsMetaVarOrAllDefInEnv at h2
  simp at h2
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
X : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ X)
⊢ IsMetaVarOrAllDefInEnv E' (meta_var_ X)
Tactic:
case meta_var_ X =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
X : PredName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (pred_ X xs)
Tactic:
case pred_ X xs =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
x y : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E' (eq_ x y)
Tactic:
case eq_ x y =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ IsMetaVarOrAllDefInEnv E' true_
Tactic:
case true_ =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi.not_
⊢ IsMetaVarOrAllDefInEnv E' phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h2
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (forall_ x phi)
⊢ IsMetaVarOrAllDefInEnv E' (forall_ x phi)
Tactic:
case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h2
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
X : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ X)
⊢ IsMetaVarOrAllDefInEnv E' (meta_var_ X)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
X : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ X)
⊢ True
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
X : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ X)
⊢ True
Tactic:
simp only
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
X : PredName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (pred_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
X : PredName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ X xs)
⊢ True
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
X : PredName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ X xs)
⊢ True
Tactic:
simp only
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
x y : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E' (eq_ x y)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
x y : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ x y)
⊢ True
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
x y : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ x y)
⊢ True
Tactic:
simp only
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ IsMetaVarOrAllDefInEnv E' true_
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ True
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ True
Tactic:
simp only
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi.not_
⊢ IsMetaVarOrAllDefInEnv E' phi.not_
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi.not_
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi.not_
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi
Tactic:
exact phi_ih h2
Proof state after:
no goals