Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux (FOL/NV/Sub/Var/All/Rec/Admits.lean)

State before:
case s1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
⊢ ∀ x ∈ xs, V x = (V' ∘ σ') x
Tactic:
intro x a1
State after:
case s1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
⊢ V x = (V' ∘ σ') x

State before:
case s1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
⊢ V x = (V' ∘ σ') x
Tactic:
simp
State after:
case s1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
⊢ V x = V' (σ' x)

State before:
case s1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
⊢ V x = V' (σ' x)
Tactic:
apply h2
State after:
case s1.a
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
⊢ x ∈ binders ∨ σ' x ∉ binders

State before:
case s1.a
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
⊢ x ∈ binders ∨ σ' x ∉ binders
Tactic:
by_cases c3 : x ∈ binders
State after:
case pos
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∈ binders
⊢ x ∈ binders ∨ σ' x ∉ binders

case neg
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∉ binders
⊢ x ∈ binders ∨ σ' x ∉ binders

State before:
case pos
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∈ binders
⊢ x ∈ binders ∨ σ' x ∉ binders
Tactic:
left
State after:
case pos.h
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∈ binders
⊢ x ∈ binders

State before:
case pos.h
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∈ binders
⊢ x ∈ binders
Tactic:
exact c3
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∉ binders
⊢ x ∈ binders ∨ σ' x ∉ binders
Tactic:
right
State after:
case neg.h
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∉ binders
⊢ σ' x ∉ binders

State before:
case neg.h
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∉ binders
⊢ σ' x ∉ binders
Tactic:
simp only [h3 x c3]
State after:
case neg.h
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∉ binders
⊢ σ x ∉ binders

State before:
case neg.h
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
x : VarName
a1 : x ∈ xs
c3 : x ∉ binders
⊢ σ x ∉ binders
Tactic:
exact h1 x a1 c3
State after:
no goals

State before:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
s1 : List.map V xs = List.map (V' ∘ σ') xs
v : VarName
a1 : isFreeIn v hd.q
⊢ v ∈ hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
State after:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
s1 : List.map V xs = List.map (V' ∘ σ') xs
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args

State before:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
s1 : List.map V xs = List.map (V' ∘ σ') xs
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args
Tactic:
simp only [← List.mem_toFinset]
State after:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
s1 : List.map V xs = List.map (V' ∘ σ') xs
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset

State before:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
s1 : List.map V xs = List.map (V' ∘ σ') xs
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset
Tactic:
apply Finset.mem_of_subset hd.h1 a1
State after:
no goals

State before:
case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
s1 : List.map V xs = List.map (V' ∘ σ') xs
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = (List.map (V' ∘ σ') xs).length
Tactic:
simp
State after:
case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
s1 : List.map V xs = List.map (V' ∘ σ') xs
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = xs.length

State before:
case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
s1 : List.map V xs = List.map (V' ∘ σ') xs
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = xs.length
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(X = hd.name ∧ (List.map σ' xs).length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ X (List.map σ' xs))
Tactic:
simp only [List.length_map] at c2
State after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ X (List.map σ' xs))

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ X (List.map σ' xs))
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : X = hd.name ∧ (List.map σ' xs).length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs))) tl hd.q
Tactic:
simp at c2
State after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs))) tl hd.q

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs))) tl hd.q
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl F ↔ Holds D I V' tl (fastReplaceFree σ' F))
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(X = hd.name ∧ (List.map σ' xs).length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X (List.map σ' xs))
Tactic:
specialize ih V V' σ σ' binders (def_ X xs)
State after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(X = hd.name ∧ (List.map σ' xs).length = hd.args.length)
ih :
  admitsAux σ binders (def_ X xs) →
    (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
      (∀ v ∈ binders, v = σ' v) →
        (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (fastReplaceFree σ' (def_ X xs)))
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X (List.map σ' xs))

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(X = hd.name ∧ (List.map σ' xs).length = hd.args.length)
ih :
  admitsAux σ binders (def_ X xs) →
    (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
      (∀ v ∈ binders, v = σ' v) →
        (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (fastReplaceFree σ' (def_ X xs)))
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X (List.map σ' xs))
Tactic:
simp only [fastReplaceFree] at ih
State after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(X = hd.name ∧ (List.map σ' xs).length = hd.args.length)
ih :
  admitsAux σ binders (def_ X xs) →
    (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
      (∀ v ∈ binders, v = σ' v) →
        (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X (List.map σ' xs)))
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X (List.map σ' xs))

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h1 : ∀ v ∈ xs, v ∉ binders → σ v ∉ binders
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(X = hd.name ∧ (List.map σ' xs).length = hd.args.length)
ih :
  admitsAux σ binders (def_ X xs) →
    (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
      (∀ v ∈ binders, v = σ' v) →
        (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X (List.map σ' xs)))
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X (List.map σ' xs))
Tactic:
apply ih h1 h2 h2' h3
State after:
no goals