internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi psi chi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.imp_ (psi.imp_ chi)).imp_ ((phi.imp_ psi).imp_ (phi.imp_ chi)))
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F phi psi chi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (Holds D I V E phi → Holds D I V E psi → Holds D I V E chi) →
    (Holds D I V E phi → Holds D I V E psi) → Holds D I V E phi → Holds D I V E chi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi psi chi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (Holds D I V E phi → Holds D I V E psi → Holds D I V E chi) →
    (Holds D I V E phi → Holds D I V E psi) → Holds D I V E phi → Holds D I V E chi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.not_.imp_ psi.not_).imp_ (psi.imp_ phi))
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.not_.imp_ psi.not_).imp_ (psi.imp_ phi))
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.not_.imp_ psi.not_).imp_ (psi.imp_ phi))
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (¬Holds D I V E phi → ¬Holds D I V E psi) → Holds D I V E psi → Holds D I V E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (¬Holds D I V E phi → ¬Holds D I V E psi) → Holds D I V E psi → Holds D I V E phi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E (phi.imp_ psi)
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E psi
Tactic:
intro D I V E a1
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E (phi.imp_ psi)
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E psi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E (phi.imp_ psi)
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E psi
Tactic:
simp only [Holds] at ih_major
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ Holds D I V E psi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ Holds D I V E psi
Tactic:
apply ih_major
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ ∀ H ∈ Δ', Holds D I V E H

case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ Holds D I V E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ ∀ H ∈ Δ', Holds D I V E H
Tactic:
intro H' a2
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
H' : Formula
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
H' : Formula
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
exact a1 H' a2
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ Holds D I V E phi
Tactic:
apply ih_minor
Proof state after:
case a.a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ ∀ H ∈ Δ', Holds D I V E H
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a.a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ ∀ H ∈ Δ', Holds D I V E H
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E (H.imp_ phi)
Tactic:
intro D I V E a1
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E (H.imp_ phi)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E (H.imp_ phi)
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E H → Holds D I V E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E H → Holds D I V E phi
Tactic:
intro a2
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E phi
Tactic:
apply ih_2
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
Tactic:
simp
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
Tactic:
constructor
Proof state after:
case a.left
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E H

case a.right
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ ∀ a ∈ Δ', Holds D I V E a
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a.left
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E H
Tactic:
exact a2
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a.right
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ ∀ a ∈ Δ', Holds D I V E a
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((forall_ v (phi.imp_ psi)).imp_ ((forall_ v phi).imp_ (forall_ v psi)))
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((forall_ v (phi.imp_ psi)).imp_ ((forall_ v phi).imp_ (forall_ v psi)))
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((forall_ v (phi.imp_ psi)).imp_ ((forall_ v phi).imp_ (forall_ v psi)))
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi) →
    (∀ (d : D), Holds D I (Function.updateITE V v d) E phi) → ∀ (d : D), Holds D I (Function.updateITE V v d) E psi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi) →
    (∀ (d : D), Holds D I (Function.updateITE V v d) E phi) → ∀ (d : D), Holds D I (Function.updateITE V v d) E psi
Tactic:
intro a2 a3 d
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi
a3 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E psi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi
a3 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E psi
Tactic:
apply a2 d
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi
a3 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi
a3 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
exact a3 d
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Tactic:
obtain s1 := FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem D I V E (Function.updateITE id v t) freshChar phi
Proof state after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
⊢ Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
⊢ Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V v d) E phi) →
    Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V v d) E phi) →
    Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi)
Tactic:
intro a2
Proof state after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi)
Tactic:
simp only [s1]
Proof state after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I (V ∘ Function.updateITE id v t) E phi