internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V' v = if v = x then d else V v
Tactic:
simp only [if_neg a1_right]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V' v = V v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V' v = V v
Tactic:
exact h2 v a1_left
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (def_ X xs) ↔
    Holds D I V E (replace c τ (def_ X xs))
Tactic:
cases E
Proof state after:
case nil
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) [] H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace c τ (def_ X xs))

case cons
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
head✝ : Definition
tail✝ : List Definition
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (head✝ :: tail✝) H
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V (head✝ :: tail✝) (def_ X xs) ↔
    Holds D I V (head✝ :: tail✝) (replace c τ (def_ X xs))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) [] H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace c τ (def_ X xs))
Tactic:
case nil =>
  simp only [replace]
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) [] H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace c τ (def_ X xs))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) [] ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (def_ X xs)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) [] ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (replace c τ (def_ X xs))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (def_ X xs)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length hd.q →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length hd.q →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet]
Proof state after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp only [hd.h2]
Proof state after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ ∅ →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ ∅ →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V tl (def_ X xs) ↔
    Holds D I V tl (def_ X xs)
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (def_ X xs) →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_
Tactic:
simp
Proof state after:
no goals