internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E false_ ↔ Holds D I V' E false_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi phi' : Formula
a✝ : IsSubAux σ' binders' phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E phi.not_ ↔ Holds D I V' E phi'.not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi phi' : Formula
a✝ : IsSubAux σ' binders' phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ ¬Holds D I V E phi ↔ ¬Holds D I V' E phi'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi phi' : Formula
a✝ : IsSubAux σ' binders' phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ ¬Holds D I V E phi ↔ ¬Holds D I V' E phi'
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi phi' : Formula
a✝ : IsSubAux σ' binders' phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E phi ↔ Holds D I V' E phi'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi phi' : Formula
a✝ : IsSubAux σ' binders' phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E phi ↔ Holds D I V' E phi'
Tactic:
exact ih_2 V V' h2 h3 h4
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi psi phi' psi' : Formula
a✝¹ : IsSubAux σ' binders' phi phi'
a✝ : IsSubAux σ' binders' psi psi'
phi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
psi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E psi ↔ Holds D I V' E psi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E (phi.iff_ psi) ↔ Holds D I V' E (phi'.iff_ psi')
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi psi phi' psi' : Formula
a✝¹ : IsSubAux σ' binders' phi phi'
a✝ : IsSubAux σ' binders' psi psi'
phi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
psi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E psi ↔ Holds D I V' E psi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ (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.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi psi phi' psi' : Formula
a✝¹ : IsSubAux σ' binders' phi phi'
a✝ : IsSubAux σ' binders' psi psi'
phi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
psi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E psi ↔ Holds D I V' E psi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ (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:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi psi phi' psi' : Formula
a✝¹ : IsSubAux σ' binders' phi phi'
a✝ : IsSubAux σ' binders' psi psi'
phi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
psi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E psi ↔ Holds D I V' E psi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E phi ↔ Holds D I V' E phi'

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi psi phi' psi' : Formula
a✝¹ : IsSubAux σ' binders' phi phi'
a✝ : IsSubAux σ' binders' psi psi'
phi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
psi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E psi ↔ Holds D I V' E psi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E psi ↔ Holds D I V' E psi'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi psi phi' psi' : Formula
a✝¹ : IsSubAux σ' binders' phi phi'
a✝ : IsSubAux σ' binders' psi psi'
phi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
psi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E psi ↔ Holds D I V' E psi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E phi ↔ Holds D I V' E phi'
Tactic:
apply phi_ih_2 V V' h2 h3 h4
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi psi phi' psi' : Formula
a✝¹ : IsSubAux σ' binders' phi phi'
a✝ : IsSubAux σ' binders' psi psi'
phi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
psi_ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E psi ↔ Holds D I V' E psi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E psi ↔ Holds D I V' E psi'
Tactic:
apply psi_ih_2 V V' h2 h3 h4
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders' ∪ {x}, V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName), Function.updateITE σ' x x v ∉ binders' ∪ {x} → V v = V' (Function.updateITE σ' x x v)) →
        (∀ v ∈ binders' ∪ {x}, v = Function.updateITE σ' x x v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E (exists_ x phi) ↔ Holds D I V' E (exists_ x phi')
Tactic:
simp at ih_2
Proof state after:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
⊢ Holds D I V E (exists_ x phi) ↔ Holds D I V' E (exists_ x phi')
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
⊢ Holds D I V E (exists_ x phi) ↔ Holds D I V' E (exists_ x phi')
Tactic:
have s1 : ∀ (v : VarName), ¬ v = x → v ∈ binders' → ¬ σ' v = x
Proof state after:
case s1
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
⊢ ∀ (v : VarName), ¬v = x → v ∈ binders' → ¬σ' v = x

D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
s1 : ∀ (v : VarName), ¬v = x → v ∈ binders' → ¬σ' v = x
⊢ Holds D I V E (exists_ x phi) ↔ Holds D I V' E (exists_ x phi')
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case s1
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
v : VarName
a1 : ¬v = x
a2 : v ∈ binders'
contra : σ' v = x
⊢ v = σ' v

D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
s1 : ∀ (v : VarName), ¬v = x → v ∈ binders' → ¬σ' v = x
⊢ Holds D I V E (exists_ x phi) ↔ Holds D I V' E (exists_ x phi')
Tactic:
exact h4 v a2
Proof state after:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
s1 : ∀ (v : VarName), ¬v = x → v ∈ binders' → ¬σ' v = x
⊢ Holds D I V E (exists_ x phi) ↔ Holds D I V' E (exists_ x phi')
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
s1 : ∀ (v : VarName), ¬v = x → v ∈ binders' → ¬σ' v = x
⊢ Holds D I V E (exists_ x phi) ↔ Holds D I V' E (exists_ x phi')
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
s1 : ∀ (v : VarName), ¬v = x → v ∈ binders' → ¬σ' v = x
⊢ (∃ d, Holds D I (Function.updateITE V x d) E phi) ↔ ∃ d, Holds D I (Function.updateITE V' x d) E phi'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
s1 : ∀ (v : VarName), ¬v = x → v ∈ binders' → ¬σ' v = x
⊢ (∃ d, Holds D I (Function.updateITE V x d) E phi) ↔ ∃ d, Holds D I (Function.updateITE V' x d) E phi'
Tactic:
first | apply forall_congr'| apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x : VarName
phi phi' : Formula
a✝ : IsSubAux (Function.updateITE σ' x x) (binders' ∪ {x}) phi phi'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), v ∈ binders' ∨ v = x → V v = V' (Function.updateITE σ' x x v)) →
      (∀ (v : VarName),
          Function.updateITE σ' x x v ∉ binders' →
            ¬Function.updateITE σ' x x v = x → V v = V' (Function.updateITE σ' x x v)) →
        (∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v) →
          (Holds D I V E phi ↔ Holds D I V' E phi')
s1 : ∀ (v : VarName), ¬v = x → v ∈ binders' → ¬σ' v = x
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E phi ↔ Holds D I (Function.updateITE V' x a) E phi'