internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ Function.updateListITE V hd.args (List.map (V' ∘ σ') xs') v =
    Function.updateListITE V' hd.args (List.map (V' ∘ σ') xs') v
Tactic:
apply Function.updateListITE_mem_eq_len
Proof state after:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Tactic:
obtain s2 := hd.h1 a1
Proof state after:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
a1 : v ∈ hd.q.freeVarSet
s2 : v ∈ hd.args.toFinset
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
a1 : v ∈ hd.q.freeVarSet
s2 : v ∈ hd.args.toFinset
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Tactic:
simp at s2
Proof state after:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
a1 : v ∈ hd.q.freeVarSet
s2 : v ∈ hd.args
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
a1 : v ∈ hd.q.freeVarSet
s2 : v ∈ hd.args
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Tactic:
exact s2
Proof state after:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Tactic:
simp at c2
Proof state after:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
c2 : X' = hd.name ∧ xs'.length = hd.args.length
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
c2 : X' = hd.name ∧ xs'.length = hd.args.length
⊢ hd.args.length = (List.map (V' ∘ σ') xs').length
Tactic:
simp
Proof state after:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
c2 : X' = hd.name ∧ xs'.length = hd.args.length
⊢ hd.args.length = xs'.length
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
s1 : List.map V xs' = List.map (V' ∘ σ') xs'
c2 : X' = hd.name ∧ xs'.length = hd.args.length
⊢ hd.args.length = xs'.length
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
x : VarName
a2 : x ∈ xs'
c3 : x ∈ binders'
⊢ V x = (V' ∘ σ') x
Tactic:
exact h2 x c3
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
x : VarName
a2 : x ∈ xs'
c3 : x ∉ binders'
⊢ V x = (V' ∘ σ') x
Tactic:
apply h3 x
Proof state after:
case neg
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
x : VarName
a2 : x ∈ xs'
c3 : x ∉ binders'
⊢ σ' x ∉ binders'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : X' = hd.name ∧ xs'.length = hd.args.length
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
x : VarName
a2 : x ∈ xs'
c3 : x ∉ binders'
⊢ σ' x ∉ binders'
Tactic:
apply ih_1 x a2 c3
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
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
Proof state after:
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
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'))
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
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
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
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
Proof state after:
no goals