internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (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_1 ∈ H :: Δ', Holds D I V E H_1
⊢ ∀ H ∈ Δ', Holds D I V E H
Tactic:
intro H' a2
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (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_1 ∈ H :: Δ', Holds D I V E H_1
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
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (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_1 ∈ H :: Δ', Holds D I V E H_1
H' : Formula
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
simp at a1
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (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' : Formula
a2 : H' ∈ Δ'
a1 : Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (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' : Formula
a2 : H' ∈ Δ'
a1 : Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
cases a1
Proof state after:
case a.intro
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (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' : Formula
a2 : H' ∈ Δ'
left✝ : Holds D I V E H
right✝ : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (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' : Formula
a2 : H' ∈ Δ'
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
case _ a1_left a1_right =>
  exact a1_right H' a2
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 Δ' phi✝
ih_2 :
  ∀ (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' : Formula
a2 : H' ∈ Δ'
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
exact a1_right H' a2
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 :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
Tactic:
intro D I V E a1
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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_1 ∈ H :: Δ', Holds D I V E H_1
⊢ 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 :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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_1 ∈ H :: Δ', Holds D I V E H_1
⊢ 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 :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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_1 ∈ H :: Δ', Holds D I V E H_1
⊢ ∀ H_1 ∈ H :: 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 :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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_1 ∈ H :: Δ', Holds D I V E H_1
⊢ ∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1
Tactic:
intro H' a2
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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_1 ∈ H :: Δ', Holds D I V E H_1
H' : Formula
a2 : H' ∈ H :: H :: Δ'
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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_1 ∈ H :: Δ', Holds D I V E H_1
H' : Formula
a2 : H' ∈ H :: H :: Δ'
⊢ Holds D I V E H'
Tactic:
simp at a1
Proof state after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a2 : H' ∈ H :: H :: Δ'
a1 : Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a2 : H' ∈ H :: H :: Δ'
a1 : Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
cases a1
Proof state after:
case a.intro
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a2 : H' ∈ H :: H :: Δ'
left✝ : Holds D I V E H
right✝ : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a2 : H' ∈ H :: H :: Δ'
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
case _ a1_left a1_right =>
  simp at a2
  cases a2
  case _ a2 =>
    simp only [a2]
    exact a1_left
  case _ a2 =>
    exact a1_right H' a2
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 :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a2 : H' ∈ H :: H :: Δ'
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
simp at a2
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H ∨ H' ∈ Δ'
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H ∨ H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
cases a2
Proof state after:
case inl
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
h✝ : H' = H
⊢ Holds D I V E H'

case inr
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
h✝ : H' ∈ Δ'
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H
⊢ Holds D I V E H'
Tactic:
case _ a2 =>
  simp only [a2]
  exact a1_left
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 :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
case _ a2 =>
  exact a1_right H' a2
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 :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H
⊢ Holds D I V E H'
Tactic:
simp only [a2]
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H
⊢ Holds D I V E H
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H
⊢ Holds D I V E H
Tactic:
exact a1_left
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 :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: 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' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
exact a1_right H' a2
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
Tactic:
intro D I V E a1
Proof state after:
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, 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
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, 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
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
⊢ ∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
⊢ ∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H
Tactic:
intro H' a2
Proof state after:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
⊢ Holds D I V E H'
Tactic:
simp at a1
Proof state after:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ Holds D I V E H'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ Holds D I V E H'
Tactic:
apply a1
Proof state after:
case a.a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ H' ∈ Δ_1 ∨ H' = H_2 ∨ H' = H_1 ∨ H' ∈ Δ_2
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a.a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ H' ∈ Δ_1 ∨ H' = H_2 ∨ H' = H_1 ∨ H' ∈ Δ_2
Tactic:
simp at a2
Proof state after:
case a.a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
a2 : H' ∈ Δ_1 ∨ H' = H_1 ∨ H' = H_2 ∨ H' ∈ Δ_2
⊢ H' ∈ Δ_1 ∨ H' = H_2 ∨ H' = H_1 ∨ H' ∈ Δ_2
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a.a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
a2 : H' ∈ Δ_1 ∨ H' = H_1 ∨ H' = H_2 ∨ H' ∈ Δ_2
⊢ H' ∈ Δ_1 ∨ H' = H_2 ∨ H' = H_1 ∨ H' ∈ Δ_2
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [phi], Holds D I V E H) → Holds D I V E phi
Tactic:
intro D I V E a1
Proof state after:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ [phi], Holds D I V E H
⊢ Holds D I V E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ [phi], Holds D I V E H
⊢ Holds D I V E phi
Tactic:
simp at a1
Proof state after:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : Holds D I V E phi
⊢ Holds D I V E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : Holds D I V E phi
⊢ Holds D I V E phi
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E true_
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E true_
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E true_
Tactic:
simp only [Holds]
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.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.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.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 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 phi
Tactic:
tauto
Proof state after:
no goals
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),
    (∀ 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:
intro D I V E _
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.imp_ (psi.imp_ chi)).imp_ ((phi.imp_ psi).imp_ (phi.imp_ chi)))