internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
⊢ Function.updateITE V h1_x (V h1_y) h1_x = Function.updateITE V h1_x (V h1_y) h1_y
Tactic:
unfold Function.updateITE
Proof state after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
⊢ (if h1_x = h1_x then V h1_y else V h1_x) = if h1_y = h1_x then V h1_y else V h1_y
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
⊢ (if h1_x = h1_x then V h1_y else V h1_x) = if h1_y = h1_x then V h1_y else V h1_y
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E ((eq_ h1_x h1_y).imp_ ((eq_ h1_x h1_z).imp_ (eq_ h1_y h1_z)))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), V h1_x = V h1_y → V h1_x = V h1_z → V h1_y = V h1_z
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), V h1_x = V h1_y → V h1_x = V h1_z → V h1_y = V h1_z
Tactic:
intro V a1 a2
Proof state after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_y = V h1_z
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_y = V h1_z
Tactic:
trans V h1_x
Proof state after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_y = V h1_x

D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_x = V h1_z
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_y = V h1_x
Tactic:
simp only [a1]
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_x = V h1_z
Tactic:
exact a2
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_n : ℕ
h1_name : PredName
h1_xs h1_ys : Fin h1_n → VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (eqSubPred h1_name h1_n h1_xs h1_ys)
Tactic:
sorry
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ h1_phi)
Tactic:
obtain ⟨σ', a1⟩ := h1_σ.2
Proof state after:
case intro
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
⊢ ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ h1_phi)
Theorem: MM0.holds_is_proof
Proof state before:
case intro
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
⊢ ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ h1_phi)
Tactic:
have s1 : IsMetaVarOrAllDefInEnv E h1_phi := is_proof_imp_is_meta_var_or_all_def_in_env E h1_Γ h1_Δ h1_phi h1_4
Proof state after:
case intro
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
⊢ ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ h1_phi)
Theorem: MM0.holds_is_proof
Proof state before:
case intro
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
⊢ ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ h1_phi)
Tactic:
intro V
Proof state after:
case intro
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
⊢ Holds D I V M E (sub h1_σ h1_τ h1_phi)
Theorem: MM0.holds_is_proof
Proof state before:
case intro
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
⊢ Holds D I V M E (sub h1_σ h1_τ h1_phi)
Tactic:
simp only [← holds_sub D I V M E h1_σ σ' h1_τ h1_phi s1 a1]
Proof state after:
case intro
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
⊢ Holds D I (V ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E h1_phi
Theorem: MM0.holds_is_proof
Proof state before:
case intro.nf
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
⊢ ∀ (v : VarName) (X : MetaVarName),
    (v, X) ∈ h1_Γ → IsNotFree D I (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E (meta_var_ X) v
Tactic:
intro v X a2
Proof state after:
case intro.nf
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
v : VarName
X : MetaVarName
a2 : (v, X) ∈ h1_Γ
⊢ IsNotFree D I (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E (meta_var_ X) v
Theorem: MM0.holds_is_proof
Proof state before:
case intro.nf
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
v : VarName
X : MetaVarName
a2 : (v, X) ∈ h1_Γ
⊢ IsNotFree D I (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E (meta_var_ X) v
Tactic:
exact lem_1 D I M E h1_Γ h1_Γ' h1_σ σ' h1_τ a1 nf h1_2 v X a2
Proof state after:
no goals