internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h2
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders phi F' → (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
y : VarName
phi' : Formula
d : D
h1_binders : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
h1_1 : AlphaEqvVarAssignment D h1_binders h1_V h1_V'
a_ih✝ :
  isAlphaEqvAux ((x, y) :: h1_binders) phi phi' →
    (Holds D I (Function.updateITE h1_V x d) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE h1_V' y d) (head✝ :: tail✝) phi')
h2 : isAlphaEqvAux ((x, y) :: (h1_x, h1_y) :: h1_binders) phi phi'
⊢ isAlphaEqvAux ((x, y) :: (h1_x, h1_y) :: h1_binders) phi phi'
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : a✝³ = a✝¹ ∧ isAlphaEqvVarList binders a✝² a✝
⊢ Holds D I V [] (def_ a✝³ a✝²) ↔ Holds D I V' [] (def_ a✝¹ a✝)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
⊢ Holds D I V (hd :: tl) (def_ X xs) ↔ Holds D I V' (hd :: tl) (def_ Y ys)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
⊢ (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 Y = hd.name ∧ ys.length = hd.args.length then
      Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
    else Holds D I V' tl (def_ Y ys)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Tactic:
case _ c1 c2 =>
  cases h2
  case intro h2_left h2_right =>
    simp only [isAlphaEqvVarList_length binders xs ys h2_right] at c1
    subst h2_left
    contradiction
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : Y = hd.name ∧ ys.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Tactic:
case _ c1 c2 =>
  cases h2
  case intro h2_left h2_right =>
    simp only [← isAlphaEqvVarList_length binders xs ys h2_right] at c2
    subst h2_left
    contradiction
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ Y ys)
Tactic:
case _ c1 c2 =>
  exact ih V V' (def_ X xs) (def_ Y ys) binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.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' ys)) tl hd.q
Tactic:
cases h2
Proof state after:
case intro
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
left✝ : X = Y
right✝ : isAlphaEqvVarList binders xs ys
⊢ 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' ys)) tl hd.q
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ 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' ys)) tl hd.q
Tactic:
apply Holds_coincide_Var
Proof state after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' ys) v
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' ys) 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 F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
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' ys) v
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
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' ys) v
Tactic:
simp only [aux_2 D binders xs ys V V' h1 h2_right]
Proof state after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V' ys) v = Function.updateListITE V' hd.args (List.map V' ys) v
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V' ys) v = Function.updateListITE V' hd.args (List.map V' ys) v
Tactic:
apply Function.updateListITE_mem_eq_len
Proof state after:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ v ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = (List.map V' ys).length
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ v ∈ hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args
Tactic:
simp only [← List.mem_toFinset]
Proof state after:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1.h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset
Tactic:
apply Finset.mem_of_subset hd.h1 a1
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = (List.map V' ys).length
Tactic:
simp
Proof state after:
case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = ys.length
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = ys.length
Tactic:
simp only [eq_comm]
Proof state after:
case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ ys.length = hd.args.length
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1.h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ ys.length = hd.args.length
Tactic:
cases c2
Proof state after:
case h1.h2.intro
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
left✝ : Y = hd.name
right✝ : ys.length = hd.args.length
⊢ ys.length = hd.args.length
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
c2_left : Y = hd.name
c2_right : ys.length = hd.args.length
⊢ ys.length = hd.args.length
Tactic:
case intro c2_left c2_right =>
  exact c2_right
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
c2_left : Y = hd.name
c2_right : ys.length = hd.args.length
⊢ ys.length = hd.args.length
Tactic:
exact c2_right
Proof state after:
no goals