internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_coincide_env
Proof state before:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = a.args.length
Tactic:
simp only [← h2_1_right_right]
Proof state after:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = xs.length
Theorem: MM0.holds_coincide_env
Proof state before:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = xs.length
Tactic:
simp only [c1_right]
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1 : ¬(X = E1_hd.name ∧ xs.length = E1_hd.args.length)
⊢ Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
exact E1_ih h3_right
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 : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Tactic:
case meta_var_ X =>
  cases h2
  case intro h2_left h2_right =>
    unfold sub
    simp only [Holds]
    simp only [Function.comp.assoc]
    simp only [h2_left]
    simp only [Function.comp_id]
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 : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ X xs) ↔
    Holds D I V M E (sub σ τ (pred_ X xs))
Tactic:
case pred_ X xs =>
  unfold sub
  simp only [Holds]
  simp
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 y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ x y) ↔ Holds D I V M E (sub σ τ (eq_ x y))
Tactic:
case eq_ x y =>
  unfold sub
  simp only [Holds]
  simp
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
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E (sub σ τ true_)
Tactic:
case true_ =>
  unfold sub
  simp only [Holds]
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
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.not_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi.not_)
Tactic:
case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  simp only [Holds]
  congr! 1
  exact phi_ih V 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 : 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 (forall_ x phi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  cases h2
  case intro h2_left h2_right =>
    unfold sub
    simp only [Holds]
    apply forall_congr'
    intro a
    have s1 : Function.updateITE V (σ.val x) a ∘ σ.val = Function.updateITE (V ∘ σ.val) x a
    apply Function.updateITE_comp_right_injective
    apply Instantiation.is_injective
    simp only [← s1]
    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 : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Tactic:
cases h2
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Tactic:
case intro h2_left h2_right =>
  unfold sub
  simp only [Holds]
  simp only [Function.comp.assoc]
  simp only [h2_left]
  simp only [Function.comp_id]
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
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Tactic:
unfold sub
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔ Holds D I V M E (τ X)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔ Holds D I V M E (τ X)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I ((V ∘ ↑σ) ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I ((V ∘ ↑σ) ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)
Tactic:
simp only [Function.comp.assoc]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)
Tactic:
simp only [h2_left]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ id) M E (τ X) ↔ Holds D I V M E (τ X)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ id) M E (τ X) ↔ Holds D I V M E (τ X)
Tactic:
simp only [Function.comp_id]
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 : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ X xs) ↔
    Holds D I V M E (sub σ τ (pred_ X xs))
Tactic:
unfold sub
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ X xs) ↔
    Holds D I V M E (pred_ X (List.map (↑σ) xs))
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 : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ X xs) ↔
    Holds D I V M E (pred_ X (List.map (↑σ) xs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ I X (List.map (V ∘ ↑σ) xs) ↔ I X (List.map V (List.map (↑σ) xs))
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 : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ I X (List.map (V ∘ ↑σ) xs) ↔ I X (List.map V (List.map (↑σ) xs))
Tactic:
simp
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 y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ x y) ↔ Holds D I V M E (sub σ τ (eq_ x y))
Tactic:
unfold sub
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ x y) ↔ Holds D I V M E (eq_ (↑σ x) (↑σ y))
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 y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ x y) ↔ Holds D I V M E (eq_ (↑σ x) (↑σ y))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ (V ∘ ↑σ) x = (V ∘ ↑σ) y ↔ V (↑σ x) = V (↑σ y)
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 y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ (V ∘ ↑σ) x = (V ∘ ↑σ) y ↔ V (↑σ x) = V (↑σ y)
Tactic:
simp
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
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E (sub σ τ true_)
Tactic:
unfold sub
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E true_
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E true_
Tactic:
simp only [Holds]
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
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.not_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi.not_)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
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
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi.not_)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
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
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi.not_)
Tactic:
unfold sub
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
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
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi).not_
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
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
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi).not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
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
⊢ ¬Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ ¬Holds D I V M E (sub σ τ phi)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
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
⊢ ¬Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ ¬Holds D I V M E (sub σ τ phi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
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
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi)
Theorem: MM0.holds_sub
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
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
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi)
Tactic:
exact phi_ih V 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
phi psi : 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))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : 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))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))