internlm/Lean-Github huggingface dataset:
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
c2 : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i < j
Tactic:
case _ c2 =>
  exfalso
  apply c2
  exact Nat.sub_lt_left_of_lt_add c1 a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
c2 : i' - j < zs.length
a3_right : False
⊢ i < j
Tactic:
contradiction
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
c2 : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i < j
Tactic:
exfalso
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
c2 : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ False
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
c2 : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ False
Tactic:
apply c2
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
c2 : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i' - j < zs.length
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
c2 : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i' - j < zs.length
Tactic:
exact Nat.sub_lt_left_of_lt_add c1 a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi.not_) ↔ Formula.lc_at (j + zs.length) phi.not_
Tactic:
simp only [Formula.openList]
Proof state after:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi).not_ ↔ Formula.lc_at (j + zs.length) phi.not_
Theorem: LN.lc_at_instantiate
Proof state before:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi).not_ ↔ Formula.lc_at (j + zs.length) phi.not_
Tactic:
simp only [Formula.lc_at]
Proof state after:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
Theorem: LN.lc_at_instantiate
Proof state before:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (phi.imp_ psi)) ↔ Formula.lc_at (j + zs.length) (phi.imp_ psi)
Tactic:
simp only [Formula.openList]
Proof state after:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j ((Formula.openList j (List.map free_ zs) phi).imp_ (Formula.openList j (List.map free_ zs) psi)) ↔
    Formula.lc_at (j + zs.length) (phi.imp_ psi)
Theorem: LN.lc_at_instantiate
Proof state before:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j ((Formula.openList j (List.map free_ zs) phi).imp_ (Formula.openList j (List.map free_ zs) psi)) ↔
    Formula.lc_at (j + zs.length) (phi.imp_ psi)
Tactic:
simp only [Formula.lc_at]
Proof state after:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ∧
      Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔
    Formula.lc_at (j + zs.length) phi ∧ Formula.lc_at (j + zs.length) psi
Theorem: LN.lc_at_instantiate
Proof state before:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ∧
      Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔
    Formula.lc_at (j + zs.length) phi ∧ Formula.lc_at (j + zs.length) psi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi

case a.h.e'_2.a
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
Theorem: LN.lc_at_instantiate
Proof state before:
case a.h.e'_1.a
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
case a.h.e'_2.a
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
Tactic:
apply psi_ih
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (forall_ a✝ phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)
Tactic:
simp only [Formula.openList]
Proof state after:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (forall_ a✝ (Formula.openList (j + 1) (List.map free_ zs) phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)
Theorem: LN.lc_at_instantiate
Proof state before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (forall_ a✝ (Formula.openList (j + 1) (List.map free_ zs) phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)
Tactic:
simp only [Formula.lc_at]
Proof state after:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at (j + 1) (Formula.openList (j + 1) (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length + 1) phi
Theorem: LN.lc_at_instantiate
Proof state before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at (j + 1) (Formula.openList (j + 1) (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length + 1) phi
Tactic:
simp only [phi_ih]
Proof state after:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Theorem: LN.lc_at_instantiate
Proof state before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Tactic:
have s1 : j + 1 + List.length zs = j + List.length zs + 1
Proof state after:
case s1
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ j + 1 + zs.length = j + zs.length + 1

a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
s1 : j + 1 + zs.length = j + zs.length + 1
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Theorem: LN.lc_at_instantiate
Proof state before:
case s1
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ j + 1 + zs.length = j + zs.length + 1

a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
s1 : j + 1 + zs.length = j + zs.length + 1
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Tactic:
linarith
Proof state after:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
s1 : j + 1 + zs.length = j + zs.length + 1
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Theorem: LN.lc_at_instantiate
Proof state before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
s1 : j + 1 + zs.length = j + zs.length + 1
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Tactic:
simp only [s1]
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_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
Tactic:
case struct_1_ Δ' H _ _ ih_2 =>
  intro D I V E a1
  apply ih_2
  intro H' a2
  simp at a1
  cases a1
  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 (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:
case struct_2_ Δ' H _ _ ih_2 =>
  intro D I V E a1
  apply ih_2
  intro H' a2
  simp at a1
  cases a1
  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
Δ_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:
case struct_3_ Δ_1 Δ_2 H_1 H_2 _ _ ih_2 =>
  intro D I V E a1
  apply ih_2
  intro H' a2
  simp at a1
  apply a1
  simp at a2
  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:
case assume_ phi =>
  intro D I V E a1
  simp at a1
  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:
case prop_0_ =>
  intro D I V E _
  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:
case prop_1_ phi psi =>
  intro D I V E _
  simp only [Holds]
  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:
case prop_2_ phi psi chi =>
  intro D I V E _
  simp only [Holds]
  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:
case prop_3_ phi psi =>
  intro D I V E _
  simp only [Holds]
  tauto
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:
case pred_1_ v phi psi =>
  intro D I V E _
  simp only [Holds]
  intro a2 a3 d
  apply a2 d
  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:
case pred_2_ v t phi =>
  intro D I V E _
  obtain s1 := FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem D I V E (Function.updateITE id v t) freshChar phi
  simp only [Holds]
  intro a2
  simp only [s1]
  simp only [Function.updateITE_comp_left]
  simp
  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:
case pred_3_ v phi ih =>
  intro D I V E _
  simp only [Holds]
  intro a2 d
  have s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
  {
    apply Holds_coincide_Var
    intro v' a1
    simp only [Function.updateITE]
    split_ifs
    case _ c1 =>
      subst c1
      contradiction
    case _ c1 =>
      rfl
  }
  simp only [s1]
  exact a2
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:
case gen_ v phi _ ih_2 =>
  intro D I V E _
  simp only [Holds]
  intro d
  apply ih_2
  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:
case eq_1_ v =>
  intro D I V E _
  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:
case eq_2_eq_ x_0 x_1 y_0 y_1 =>
  intro D I V E _
  simp only [Holds]
  intro a2
  cases a2
  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
⊢ ∀ (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:
case def_false_ =>
  intro D I V E _
  simp only [Holds]
  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:
case def_and_ phi psi =>
  intro D I V E _
  simp only [Holds]
  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:
case def_or_ phi psi =>
  intro D I V E _
  simp only [Holds]
  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:
case def_iff_ phi psi =>
  intro D I V E _
  simp only [Holds]
  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:
case def_exists_ v phi =>
  intro D I V E _
  simp only [Holds]
  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:
case sub_ Δ' phi τ _ ih_2 =>
  intro D I V E a1
  simp at a1
  obtain s1 := Sub.Pred.All.Rec.Option.Fresh.substitution_theorem D I V E freshChar τ
  simp only [← s1] at a1
  simp only [← s1]
  apply ih_2
  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 Δ' 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_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 Δ' 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
⊢ 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 Δ' 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
⊢ 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 Δ' 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