internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) V' E_tl (def_ X xs) ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
Tactic:
case _ c1 c2 =>
  simp only [List.length_map] at c2
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Tactic:
simp only [← s2]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Tactic:
clear s2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ Holds D (I' D I V'' (E_hd :: E_tl) τ) (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V' E_hd.args (List.map (V ∘ σ) xs)) E_tl E_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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ (I' D I V'' (E_hd :: E_tl) τ).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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length E_hd.q → ((I' D I V'' (E_hd :: E_tl) τ).pred_var_ P ds ↔ I.pred_var_ P ds)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s2.h1.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
x : VarName
a1 : isFreeIn x E_hd.q
⊢ ∀ y ∈ xs, (V ∘ σ) y = (V ∘ σ) y
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s2.h1.h2
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
x : VarName
a1 : isFreeIn x E_hd.q
⊢ E_hd.args.length = xs.length
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s2.h1.h3
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
x : VarName
a1 : isFreeIn x E_hd.q
⊢ x ∈ E_hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case s2.h1.h3
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
x : VarName
a1 : x ∈ E_hd.q.freeVarSet
⊢ x ∈ E_hd.args
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s2.h1.h3
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
x : VarName
a1 : x ∈ E_hd.q.freeVarSet
⊢ x ∈ E_hd.args
Tactic:
simp only [← List.mem_toFinset]
Proof state after:
case s2.h1.h3
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
x : VarName
a1 : x ∈ E_hd.q.freeVarSet
⊢ x ∈ E_hd.args.toFinset
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s2.h1.h3
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
x : VarName
a1 : x ∈ E_hd.q.freeVarSet
⊢ x ∈ E_hd.args.toFinset
Tactic:
apply Finset.mem_of_subset E_hd.h1 a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ (I' D I V'' (E_hd :: E_tl) τ).pred_const_ = I.pred_const_
Tactic:
simp only [I']
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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ (Interpretation.usingPred D I 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) (E_hd :: E_tl) ((τ X ds.length).get ⋯).2
          else I.pred_var_ X ds
        else I.pred_var_ X ds).pred_const_ =
    I.pred_const_
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ (Interpretation.usingPred D I 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) (E_hd :: E_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 only [Interpretation.usingPred]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length E_hd.q → ((I' D I V'' (E_hd :: E_tl) τ).pred_var_ P ds ↔ I.pred_var_ P ds)
Tactic:
intro P ds a1
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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)) →
      (∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E_tl τ) V' E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs)))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
c2 : X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length E_hd.q
⊢ (I' D I V'' (E_hd :: E_tl) τ).pred_var_ P ds ↔ I.pred_var_ P ds