internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
⊢ hd.args.length = (List.map (V ∘ fun x => if v = x then t else x) xs).length
Tactic:
simp at c1
Proof state after:
case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = (List.map (V ∘ fun x => if v = x then t else x) xs).length
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = (List.map (V ∘ fun x => if v = x then t else x) xs).length
Tactic:
simp
Proof state after:
case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = xs.length
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
c1 : 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.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ Holds D I (fun c => if c = v then V' t else V c) tl (def_ X xs) ↔
    Holds D I V tl (def_ X (List.map (fun x => if v = x then t else x) xs))
Tactic:
apply ih V binders
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ fastAdmitsAux v t binders (def_ X xs)

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ ∀ v ∉ binders, V' v = V v
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ fastAdmitsAux v t binders (def_ X xs)
Tactic:
simp only [fastAdmitsAux]
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ v ∈ xs → t ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ v ∈ xs → t ∉ binders
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ ∀ v ∉ binders, V' v = V v
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmits v t F
⊢ Holds D I (Function.updateITE V v (V t)) E F ↔ Holds D I V E (fastReplaceFree v t F)
Tactic:
simp only [fastAdmits] at h1
Proof state after:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmitsAux v t ∅ F
⊢ Holds D I (Function.updateITE V v (V t)) E F ↔ Holds D I V E (fastReplaceFree v t F)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmitsAux v t ∅ F
⊢ Holds D I (Function.updateITE V v (V t)) E F ↔ Holds D I V E (fastReplaceFree v t F)
Tactic:
apply substitution_theorem_aux D I V V E v t ∅ F h1
Proof state after:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmitsAux v t ∅ F
⊢ ∀ v ∉ ∅, V v = V v
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmitsAux v t ∅ F
⊢ ∀ v ∉ ∅, V v = V v
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_is_valid
Proof state before:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : F.IsValid
⊢ (fastReplaceFree v t F).IsValid
Tactic:
simp only [IsValid] at h2
Proof state after:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (fastReplaceFree v t F).IsValid
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_is_valid
Proof state before:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (fastReplaceFree v t F).IsValid
Tactic:
simp only [IsValid]
Proof state after:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (fastReplaceFree v t F)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_is_valid
Proof state before:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (fastReplaceFree v t F)
Tactic:
intro D I V E
Proof state after:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (fastReplaceFree v t F)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_is_valid
Proof state before:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (fastReplaceFree v t F)
Tactic:
simp only [← substitution_theorem D I V E v t F h1]
Proof state after:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (Function.updateITE V v (V t)) E F
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_is_valid
Proof state before:
v t : VarName
F : Formula
h1 : fastAdmits v t F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (Function.updateITE V v (V t)) E F
Tactic:
apply h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
h1 : ∀ (v : VarName), isFreeIn v F → V v = V' v
⊢ Holds D I V E F ↔ Holds D I V' E F
Tactic:
induction E generalizing F V V'
Proof state after:
case nil
D : Type
I : Interpretation D
V V' : VarAssignment D
F : Formula
h1 : ∀ (v : VarName), isFreeIn v F → V v = V' v
⊢ Holds D I V [] F ↔ Holds D I V' [] F

case cons
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
V V' : VarAssignment D
F : Formula
h1 : ∀ (v : VarName), isFreeIn v F → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I V' (head✝ :: tail✝) F
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ (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)) ↔
    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)
Tactic:
case cons.def_ hd tl ih X xs =>
  split_ifs
  case pos c1 =>
    apply ih
    intro v a1
    simp only [isFreeIn_iff_mem_freeVarSet v hd.q] at a1
    have s1 : v ∈ List.toFinset hd.args
    apply Finset.mem_of_subset hd.h1 a1
    simp only [List.mem_toFinset] at s1
    apply Function.updateListITE_fun_coincide_mem_eq_len V V' hd.args xs v h1 s1
    tauto
  case neg c1 =>
    apply ih
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V' xs)
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  congr! 1
  simp only [List.map_eq_map_iff]
  exact h1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), v = x ∨ v = y → V v = V' v
⊢ V x = V y ↔ V' x = V' y
Tactic:
case eq_ x y =>
  simp at h1
  cases h1
  case intro h1_left h1_right =>
    congr! 1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi → V v = V' v
⊢ ¬Holds D I V (head✝ :: tail✝) phi ↔ ¬Holds D I V' (head✝ :: tail✝) phi
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih V V' h1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp at h1
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih
  intro v a1
  simp only [Function.updateITE]
  split_ifs <;> tauto
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)
Tactic:
simp only [isFreeIn] at h1
Proof state after:
case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ a✝, V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ a✝, V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)
Tactic:
simp only [Holds]
Proof state after:
case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ a✝, V v = V' v
⊢ (if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I (Function.updateListITE V head✝.args (List.map V a✝)) tail✝ head✝.q
    else Holds D I V tail✝ (def_ a✝¹ a✝)) ↔
    if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I (Function.updateListITE V' head✝.args (List.map V' a✝)) tail✝ head✝.q
    else Holds D I V' tail✝ (def_ a✝¹ a✝)
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V' xs)
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ List.map V xs = List.map V' xs
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ List.map V xs = List.map V' xs
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ ∀ x ∈ xs, V x = V' x
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ ∀ x ∈ xs, V x = V' x
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), v = x ∨ v = y → V v = V' v
⊢ V x = V y ↔ V' x = V' y
Tactic:
simp at h1
Proof state after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1 : V x = V' x ∧ V y = V' y
⊢ V x = V y ↔ V' x = V' y
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1 : V x = V' x ∧ V y = V' y
⊢ V x = V y ↔ V' x = V' y
Tactic:
cases h1
Proof state after:
case intro
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
left✝ : V x = V' x
right✝ : V y = V' y
⊢ V x = V y ↔ V' x = V' y
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1_left : V x = V' x
h1_right : V y = V' y
⊢ V x = V y ↔ V' x = V' y
Tactic:
case intro h1_left h1_right =>
  congr! 1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1_left : V x = V' x
h1_right : V y = V' y
⊢ V x = V y ↔ V' x = V' y
Tactic:
congr! 1
Proof state after:
no goals