internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
by_cases c2 : v ∈ zs
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
apply Function.updateListITE_mem_eq_len V V' v zs (List.map V xs) c2
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
⊢ zs.length = (List.map V xs).length
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
⊢ zs.length = (List.map V xs).length
Tactic:
cases c1
Proof state after:
case pos.intro
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
left✝ : X = P
right✝ : xs.length = zs.length
⊢ zs.length = (List.map V xs).length
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ zs.length = (List.map V xs).length
Tactic:
case pos.intro c1_left c1_right =>
  simp
  symm
  exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ zs.length = (List.map V xs).length
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ zs.length = xs.length
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ zs.length = xs.length
Tactic:
symm
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ xs.length = zs.length
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ xs.length = zs.length
Tactic:
exact c1_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
by_cases c3 : v ∈ binders
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∈ binders
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∉ binders
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∈ binders
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
specialize h1_right v c3 a1
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∈ binders
h1_right : v ∈ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∈ binders
h1_right : v ∈ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∉ binders
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
apply Function.updateListITE_mem'
Proof state after:
case neg.h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∉ binders
⊢ V v = V' v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case neg.h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∉ binders
⊢ V v = V' v
Tactic:
exact h2 v c3
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
c2 : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
exact s1
Proof state after:
no goals