internlm/Lean-Github huggingface dataset:
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 ∘ Function.updateITE id v t) E phi
Tactic:
simp only [Function.updateITE_comp_left]
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 (Function.updateITE (V ∘ id) v (V t)) E 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 (Function.updateITE (V ∘ id) v (V t)) E phi
Tactic:
simp
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 (Function.updateITE V v (V t)) E 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 (Function.updateITE V v (V t)) E phi
Tactic:
exact a2 (V t)
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi.imp_ (forall_ v phi))
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
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_ (forall_ v phi))
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
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_ (forall_ v phi))
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V 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
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi → ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
Tactic:
intro a2 d
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V 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
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
have s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
Proof state after:
case s1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi

Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I (Function.updateITE V v d) E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case s1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi

Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
{
  apply Holds_coincide_Var
  intro v' a1
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    subst c1
    contradiction
  case _ c1 =>
    rfl
}
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ 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
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
simp only [s1]
Proof state after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I V E phi
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I V E phi
Tactic:
exact a2
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case s1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
Tactic:
apply Holds_coincide_Var
Proof state after:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ ∀ (v_1 : VarName), isFreeIn v_1 phi → Function.updateITE V v d v_1 = V v_1
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ ∀ (v_1 : VarName), isFreeIn v_1 phi → Function.updateITE V v d v_1 = V v_1
Tactic:
intro v' a1
Proof state after:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
⊢ Function.updateITE V v d v' = V v'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
⊢ Function.updateITE V v d v' = V v'
Tactic:
simp only [Function.updateITE]
Proof state after:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
⊢ (if v' = v then d else V v') = V v'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
⊢ (if v' = v then d else V v') = V v'
Tactic:
split_ifs
Proof state after:
case pos
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
h✝ : v' = v
⊢ d = V v'

case neg
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
h✝ : ¬v' = v
⊢ V v' = V v'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
c1 : v' = v
⊢ d = V v'
Tactic:
case _ c1 =>
  subst c1
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
c1 : ¬v' = v
⊢ V v' = V v'
Tactic:
case _ c1 =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
c1 : v' = v
⊢ d = V v'
Tactic:
subst c1
Proof state after:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
ih : ¬isFreeIn v' phi
⊢ d = V v'
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
ih : ¬isFreeIn v' phi
⊢ d = V v'
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
c1 : ¬v' = v
⊢ V v' = V v'
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
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 ∈ [], Holds D I V E H) → Holds D I V E (forall_ v phi)
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
v : VarName
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
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (forall_ v phi)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
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
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (forall_ v phi)
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F : Formula
v : VarName
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
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ ∀ (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
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
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
Tactic:
intro d
Proof state after:
Δ : List Formula
F : Formula
v : VarName
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
a✝ : ∀ H ∈ [], Holds D I V E H
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
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
a✝ : ∀ H ∈ [], Holds D I V E H
d : D
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
apply ih_2
Proof state after:
case a
Δ : List Formula
F : Formula
v : VarName
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
a✝ : ∀ H ∈ [], Holds D I V E H
d : D
⊢ ∀ H ∈ [], Holds D I (Function.updateITE V v d) E H
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a
Δ : List Formula
F : Formula
v : VarName
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
a✝ : ∀ H ∈ [], Holds D I V E H
d : D
⊢ ∀ H ∈ [], Holds D I (Function.updateITE V v d) E H
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (eq_ v v)
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
v : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (eq_ v v)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
v : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (eq_ v v)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E (((eq_ x_0 y_0).and_ (eq_ x_1 y_1)).imp_ ((eq_ x_0 x_1).iff_ (eq_ y_0 y_1)))
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (((eq_ x_0 y_0).and_ (eq_ x_1 y_1)).imp_ ((eq_ x_0 x_1).iff_ (eq_ y_0 y_1)))
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (((eq_ x_0 y_0).and_ (eq_ x_1 y_1)).imp_ ((eq_ x_0 x_1).iff_ (eq_ y_0 y_1)))
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ V x_0 = V y_0 ∧ V x_1 = V y_1 → (V x_0 = V x_1 ↔ V y_0 = V y_1)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ V x_0 = V y_0 ∧ V x_1 = V y_1 → (V x_0 = V x_1 ↔ V y_0 = V y_1)
Tactic:
intro a2
Proof state after:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : V x_0 = V y_0 ∧ V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : V x_0 = V y_0 ∧ V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
Tactic:
cases a2
Proof state after:
case intro
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
left✝ : V x_0 = V y_0
right✝ : V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2_left : V x_0 = V y_0
a2_right : V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
Tactic:
case _ a2_left a2_right =>
  simp only [a2_left]
  simp only [a2_right]
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2_left : V x_0 = V y_0
a2_right : V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
Tactic:
simp only [a2_left]
Proof state after:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2_left : V x_0 = V y_0
a2_right : V x_1 = V y_1
⊢ V y_0 = V x_1 ↔ V y_0 = V y_1
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2_left : V x_0 = V y_0
a2_right : V x_1 = V y_1
⊢ V y_0 = V x_1 ↔ V y_0 = V y_1
Tactic:
simp only [a2_right]
Proof state after:
no goals
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((List.foldr and_ true_ (List.zipWith eq_ xs ys)).imp_ ((pred_var_ X xs).iff_ (pred_var_ X ys)))
Tactic:
intro D I V E _
Proof state after:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((List.foldr and_ true_ (List.zipWith eq_ xs ys)).imp_ ((pred_var_ X xs).iff_ (pred_var_ X ys)))
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((List.foldr and_ true_ (List.zipWith eq_ xs ys)).imp_ ((pred_var_ X xs).iff_ (pred_var_ X ys)))
Tactic:
simp only [Holds]
Proof state after:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys)) →
    (I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V ys))
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys)) →
    (I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V ys))
Tactic:
intro a1
Proof state after:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys))
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V ys)
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys))
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V ys)
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys))
⊢ List.map V xs = List.map V ys
Theorem: FOL.NV.Program.Backend.soundness
Proof state before:
case a.h.e'_4
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys))
⊢ List.map V xs = List.map V ys
Tactic:
induction xs generalizing ys
Proof state after:
case a.h.e'_4.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
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

case a.h.e'_4.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
tail_ih✝ :
  ∀ (ys : List VarName),
    tail✝.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ tail✝ ys)) → List.map V tail✝ = List.map V ys
ys : List VarName
ih_1 : (head✝ :: tail✝).length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (head✝ :: tail✝) ys))
⊢ List.map V (head✝ :: tail✝) = List.map V ys