internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h.h1
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 : D
⊢ ∀ (v : VarName), isFreeIn v phi → Function.updateITE V x d v = Function.updateITE V' x d v
Tactic:
intro v a1
Proof state after:
case h.h1
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 : D
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE V x d v = Function.updateITE V' x d v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h.h1
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 : D
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE V x d v = Function.updateITE V' x d v
Tactic:
simp only [Function.updateITE]
Proof state after:
case h.h1
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 : D
v : VarName
a1 : isFreeIn v phi
⊢ (if v = x then d else V v) = if v = x then d else V' v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h.h1
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 : D
v : VarName
a1 : isFreeIn v phi
⊢ (if v = x then d else V v) = if v = x then d else V' v
Tactic:
split_ifs <;> 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 : 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 : D), Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
apply forall_congr'
Proof state after:
case h
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
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) (head✝ :: tail✝) phi
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:
apply exists_congr
Proof state after:
case h
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
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) (head✝ :: tail✝) phi
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:
split_ifs
Proof state after:
case pos
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
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V' hd.args (List.map V' xs)) tl hd.q

case neg
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
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X xs)
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
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V' hd.args (List.map V' xs)) tl hd.q
Tactic:
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
Proof state after:
no goals
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X xs)
Tactic:
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
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
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V' hd.args (List.map V' xs)) tl hd.q
Tactic:
apply ih
Proof state after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
intro v a1
Proof state after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet v hd.q] at a1
Proof state after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
have s1 : v ∈ List.toFinset hd.args
Proof state after:
case s1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset

case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args.toFinset
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case s1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset

case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args.toFinset
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
apply Finset.mem_of_subset hd.h1 a1
Proof state after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args.toFinset
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args.toFinset
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
simp only [List.mem_toFinset] at s1
Proof state after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
apply Function.updateListITE_fun_coincide_mem_eq_len V V' hd.args xs v h1 s1
Proof state after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args
⊢ hd.args.length = xs.length
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args
⊢ hd.args.length = xs.length
Tactic:
tauto
Proof state after:
no goals
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X xs)
Tactic:
apply ih
Proof state after:
case h1
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (v : VarName), isFreeIn v (def_ X xs) → V v = V' v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h1
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (v : VarName), isFreeIn v (def_ X xs) → V v = V' v
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
V : VarAssignment D
E : Env
F : Formula
h1 : I.pred_const_ = I'.pred_const_
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V E F ↔ Holds D I' V E F
Tactic:
induction E generalizing F V
Proof state after:
case nil
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
V : VarAssignment D
F : Formula
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V [] F ↔ Holds D I' V [] F

case cons
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
V : VarAssignment D
F : Formula
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I' V (head✝ :: tail✝) F
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (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 P ds a1
    simp only [predVarOccursIn_iff_mem_predVarSet P ds.length] at a1
    simp only [hd.h2] at a1
    simp at a1
  case neg c1 =>
    apply ih
    intro P ds a1
    simp only [predVarOccursIn] at a1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_const_ X (List.map V xs) ↔ I'.pred_const_ X (List.map V xs)
Tactic:
case pred_const_ X xs =>
  simp only [h1]
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = X ∧ ds.length = xs.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
case pred_var_ X xs =>
  simp at h2
  specialize h2 X (List.map V xs)
  simp at h2
  exact h2
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_PredVar
Proof state before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ¬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 h2
Proof state after:
no goals