internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys : List VarName
ih_1 : [].length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] ys))
⊢ List.map V [] = List.map V ys
Tactic:
case _ =>
  cases ys
  case _ =>
    simp only [Holds]
  case cons ys_hd ys_tl =>
    simp at ih_1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys : List VarName
ih_1 : [].length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] ys))
⊢ List.map V [] = List.map V ys
Tactic:
cases ys
Proof state after:
case nil
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ih_1 : [].length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] []))
⊢ List.map V [] = List.map V []

case cons
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
head✝ : VarName
tail✝ : List VarName
ih_1 : [].length = (head✝ :: tail✝).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] (head✝ :: tail✝)))
⊢ List.map V [] = List.map V (head✝ :: tail✝)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ih_1 : [].length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] []))
⊢ List.map V [] = List.map V []
Tactic:
case _ =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys_hd : VarName
ys_tl : List VarName
ih_1 : [].length = (ys_hd :: ys_tl).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] (ys_hd :: ys_tl)))
⊢ List.map V [] = List.map V (ys_hd :: ys_tl)
Tactic:
case cons ys_hd ys_tl =>
  simp at ih_1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ih_1 : [].length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] []))
⊢ List.map V [] = List.map V []
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys_hd : VarName
ys_tl : List VarName
ih_1 : [].length = (ys_hd :: ys_tl).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] (ys_hd :: ys_tl)))
⊢ List.map V [] = List.map V (ys_hd :: ys_tl)
Tactic:
simp at ih_1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys : List VarName
ih_1 : (xs_hd :: xs_tl).length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) ys))
⊢ List.map V (xs_hd :: xs_tl) = List.map V ys
Tactic:
cases ys
Proof state after:
case nil
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ih_1 : (xs_hd :: xs_tl).length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) []))
⊢ List.map V (xs_hd :: xs_tl) = List.map V []

case cons
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
head✝ : VarName
tail✝ : List VarName
ih_1 : (xs_hd :: xs_tl).length = (head✝ :: tail✝).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) (head✝ :: tail✝)))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (head✝ :: tail✝)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ih_1 : (xs_hd :: xs_tl).length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) []))
⊢ List.map V (xs_hd :: xs_tl) = List.map V []
Tactic:
case nil =>
  simp at ih_1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ih_1 : (xs_hd :: xs_tl).length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) []))
⊢ List.map V (xs_hd :: xs_tl) = List.map V []
Tactic:
simp at ih_1
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) (ys_hd :: ys_tl)))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
simp at ih_1
Proof state after:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) (ys_hd :: ys_tl)))
ih_1 : xs_tl.length = ys_tl.length
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) (ys_hd :: ys_tl)))
ih_1 : xs_tl.length = ys_tl.length
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
simp at a1
Proof state after:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
a1 : Holds D I V E ((eq_ xs_hd ys_hd).and_ (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl)))
ih_1 : xs_tl.length = ys_tl.length
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
a1 : Holds D I V E ((eq_ xs_hd ys_hd).and_ (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl)))
ih_1 : xs_tl.length = ys_tl.length
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
simp only [Holds] at a1
Proof state after:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1 : V xs_hd = V ys_hd ∧ Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1 : V xs_hd = V ys_hd ∧ Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
cases a1
Proof state after:
case intro
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
left✝ : V xs_hd = V ys_hd
right✝ : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
simp
Proof state after:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ V xs_hd = V ys_hd ∧ List.map V xs_tl = List.map V ys_tl
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ V xs_hd = V ys_hd ∧ List.map V xs_tl = List.map V ys_tl
Tactic:
constructor
Proof state after:
case left
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ V xs_hd = V ys_hd

case right
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V xs_tl = List.map V ys_tl
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case left
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ V xs_hd = V ys_hd
Tactic:
exact a1_left
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case right
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V xs_tl = List.map V ys_tl
Tactic:
apply xs_ih ys_tl ih_1 a1_right
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 (false_.iff_ true_.not_)
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 (false_.iff_ true_.not_)
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 (false_.iff_ true_.not_)
Tactic:
simp only [Holds]
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
⊢ False ↔ ¬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
⊢ False ↔ ¬True
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.and_ psi).iff_ (phi.imp_ psi.not_).not_)
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.and_ psi).iff_ (phi.imp_ psi.not_).not_)
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.and_ psi).iff_ (phi.imp_ psi.not_).not_)
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 → ¬Holds D I V E psi)
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 → ¬Holds D I V E psi)
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.or_ psi).iff_ (phi.not_.imp_ psi))
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.or_ psi).iff_ (phi.not_.imp_ psi))
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.or_ psi).iff_ (phi.not_.imp_ psi))
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 → Holds D I V E psi
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 → Holds D I V E psi
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.iff_ psi).imp_ ((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_).imp_
            (((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_.imp_ (phi.iff_ psi)).not_).not_
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.iff_ psi).imp_ ((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_).imp_
        (((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_.imp_ (phi.iff_ psi)).not_).not_
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.iff_ psi).imp_ ((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_).imp_
        (((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_.imp_ (phi.iff_ psi)).not_).not_
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 → Holds D I V E psi) → ¬(Holds D I V E psi → Holds D I V E phi))) →
      ¬(¬((Holds D I V E phi → Holds D I V E psi) → ¬(Holds D I V E psi → Holds D I V E phi)) →
          (Holds D I V E phi ↔ Holds D I V E psi)))
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 → Holds D I V E psi) → ¬(Holds D I V E psi → Holds D I V E phi))) →
      ¬(¬((Holds D I V E phi → Holds D I V E psi) → ¬(Holds D I V E psi → Holds D I V E phi)) →
          (Holds D I V E phi ↔ Holds D I V E psi)))
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : 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 ((exists_ v phi).iff_ (forall_ v phi.not_).not_)
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
v : 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 ((exists_ v phi).iff_ (forall_ v phi.not_).not_)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : 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 ((exists_ v phi).iff_ (forall_ v phi.not_).not_)
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (∃ 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 : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (∃ d, Holds D I (Function.updateITE V v d) E phi) ↔ ¬∀ (d : D), ¬Holds D I (Function.updateITE V v d) E phi
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × 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 ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ) Δ', Holds D I V E H) →
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
intro D I V E a1
Proof state after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × 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 ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ) Δ', Holds D I V E H
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)