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_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih :
  ∀ (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
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_phi
Tactic:
exact h1_ih M nf hyp (Function.updateITE V h1_x d)
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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 ((forall_ h1_x (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_x h1_phi).imp_ (forall_ h1_x h1_psi)))
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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),
    (∀ (d : D),
        Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi) →
      (∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi) →
        ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_psi
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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),
    (∀ (d : D),
        Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi) →
      (∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi) →
        ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_psi
Tactic:
intro V a1 a2 d
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_psi
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_psi
Tactic:
apply a1 d
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_phi
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_phi
Tactic:
exact a2 d
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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 (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
have s1 : IsNotFree D I M E h1_phi h1_x
Proof state after:
case s1
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
⊢ IsNotFree D I M E h1_phi 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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Theorem: MM0.holds_is_proof
Proof state before:
case s1
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
⊢ IsNotFree D I M E h1_phi 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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
apply not_free_imp_is_not_free D I M E h1_phi h1_Γ h1_x h1_2
Proof state after:
case s1
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
⊢ ∀ (X : MetaVarName), (h1_x, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) 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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Theorem: MM0.holds_is_proof
Proof state before:
case s1
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
⊢ ∀ (X : MetaVarName), (h1_x, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) 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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
exact nf 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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi → ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi → ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
Tactic:
intro V a1 a
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I (Function.updateITE V h1_x a) M E h1_phi
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : IsNotFree D I M E h1_phi h1_x
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I (Function.updateITE V h1_x a) M E h1_phi
Tactic:
unfold IsNotFree at s1
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : ∀ (V : Valuation D) (d : D), Holds D I V M E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) M E h1_phi
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I (Function.updateITE V h1_x a) M E h1_phi
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : ∀ (V : Valuation D) (d : D), Holds D I V M E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) M E h1_phi
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I (Function.updateITE V h1_x a) M E h1_phi
Tactic:
simp only [← s1 V a]
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : ∀ (V : Valuation D) (d : D), Holds D I V M E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) M E h1_phi
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I V M E h1_phi
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_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x 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
s1 : ∀ (V : Valuation D) (d : D), Holds D I V M E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) M E h1_phi
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I V M E h1_phi
Tactic:
exact 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 : 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), Holds D I V M E (exists_ h1_x (eq_ h1_x h1_y))
Tactic:
unfold exists_
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), Holds D I V M E (forall_ h1_x (eq_ h1_x h1_y).not_).not_
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), Holds D I V M E (forall_ h1_x (eq_ h1_x h1_y).not_).not_
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 : 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), ¬∀ (d : D), ¬Function.updateITE V h1_x d h1_x = Function.updateITE V h1_x d 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), ¬∀ (d : D), ¬Function.updateITE V h1_x d h1_x = Function.updateITE V h1_x d h1_y
Tactic:
simp
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), ∃ x, Function.updateITE V h1_x x h1_x = Function.updateITE V h1_x x 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), ∃ x, Function.updateITE V h1_x x h1_x = Function.updateITE V h1_x x h1_y
Tactic:
intro V
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
⊢ ∃ x, Function.updateITE V h1_x x h1_x = Function.updateITE V h1_x x 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
⊢ ∃ x, Function.updateITE V h1_x x h1_x = Function.updateITE V h1_x x h1_y
Tactic:
apply Exists.intro (V h1_y)
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
⊢ Function.updateITE V h1_x (V h1_y) h1_x = Function.updateITE V h1_x (V h1_y) h1_y