internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
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 : D
v : VarName
c1 : ¬v = x
a1 : σ' v ∉ binders'
⊢ ¬(if v = x then x else σ' v) = x →
    (if v = x then d else V v) = if (if v = x then x else σ' v) = x then d else V' (if v = x then x else σ' v)
Tactic:
simp only [if_neg c1]
Proof state after:
case neg
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 : D
v : VarName
c1 : ¬v = x
a1 : σ' v ∉ binders'
⊢ ¬σ' v = x → V v = if σ' v = x then d else V' (σ' v)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
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 : D
v : VarName
c1 : ¬v = x
a1 : σ' v ∉ binders'
⊢ ¬σ' v = x → V v = if σ' v = x then d else V' (σ' v)
Tactic:
intro a2
Proof state after:
case neg
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 : D
v : VarName
c1 : ¬v = x
a1 : σ' v ∉ binders'
a2 : ¬σ' v = x
⊢ V v = if σ' v = x then d else V' (σ' v)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
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 : D
v : VarName
c1 : ¬v = x
a1 : σ' v ∉ binders'
a2 : ¬σ' v = x
⊢ V v = if σ' v = x then d else V' (σ' v)
Tactic:
simp only [if_neg a2]
Proof state after:
case neg
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 : D
v : VarName
c1 : ¬v = x
a1 : σ' v ∉ binders'
a2 : ¬σ' v = x
⊢ V v = V' (σ' v)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
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 : D
v : VarName
c1 : ¬v = x
a1 : σ' v ∉ binders'
a2 : ¬σ' v = x
⊢ V v = V' (σ' v)
Tactic:
apply h3 v a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h.h4
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 : D
⊢ ∀ (v : VarName), v ∈ binders' ∨ v = x → v = Function.updateITE σ' x x v
Tactic:
intro v a1
Proof state after:
case h.h4
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
⊢ v = Function.updateITE σ' x x v
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h.h4
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
⊢ v = Function.updateITE σ' x x v
Tactic:
simp only [Function.updateITE]
Proof state after:
case h.h4
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
⊢ v = if v = x then x else σ' v
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h.h4
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
⊢ v = if v = x then x else σ' v
Tactic:
split_ifs
Proof state after:
case pos
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
h✝ : v = x
⊢ v = x

case neg
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
h✝ : ¬v = x
⊢ v = σ' v
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
c1 : v = x
⊢ v = x
Tactic:
case _ c1 =>
  exact c1
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'
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
c1 : ¬v = x
⊢ v = σ' v
Tactic:
case _ c1 =>
  cases a1
  case _ c2 =>
    exact h4 v c2
  case _ c2 =>
    contradiction
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'
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
c1 : v = x
⊢ v = x
Tactic:
exact c1
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'
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 : D
v : VarName
a1 : v ∈ binders' ∨ v = x
c1 : ¬v = x
⊢ v = σ' v
Tactic:
cases a1
Proof state after:
case inl
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 : D
v : VarName
c1 : ¬v = x
h✝ : v ∈ binders'
⊢ v = σ' v

case inr
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 : D
v : VarName
c1 : ¬v = x
h✝ : v = x
⊢ v = σ' v
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 : D
v : VarName
c1 : ¬v = x
c2 : v ∈ binders'
⊢ v = σ' v
Tactic:
case _ c2 =>
  exact h4 v c2
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'
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 : D
v : VarName
c1 : ¬v = x
c2 : v = x
⊢ v = σ' v
Tactic:
case _ c2 =>
  contradiction
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'
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 : D
v : VarName
c1 : ¬v = x
c2 : v ∈ binders'
⊢ v = σ' v
Tactic:
exact h4 v c2
Proof state after:
no goals