internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ Holds D I V E F ↔ Holds D I V' E F'
Tactic:
induction E generalizing F F' binders V V'
Proof state after:
case nil
D : Type
I : Interpretation D
V V' : VarAssignment D
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ 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 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')
V V' : VarAssignment D
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I V' (head✝ :: tail✝) F'
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:
case nil.def_.def_ =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : PredName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ Y ys)
Tactic:
case
  pred_const_.pred_const_ X xs Y ys
| pred_var_.pred_var_ X xs Y ys =>
  cases h2
  case intro h2_left h2_right =>
    simp only [Holds]
    subst h2_left
    congr! 1
    exact aux_2 D binders xs ys V V' h1 h2_right
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : True
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) false_
Tactic:
case true_.true_ | false_.false_ =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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')
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)
h1 : AlphaEqvVarAssignment D binders V V'
phi' : Formula
h2 : isAlphaEqvAux binders phi phi'
⊢ Holds D I V (head✝ :: tail✝) phi.not_ ↔ Holds D I V' (head✝ :: tail✝) phi'.not_
Tactic:
case not_.not_ phi phi_ih phi' =>
  simp only [Holds]
  congr! 1
  exact phi_ih V V' phi' binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case cons.def_.def_
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')
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 : isAlphaEqvAux binders (def_ a✝³ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)
Tactic:
simp only [isAlphaEqvAux] at h2
Proof state after:
case cons.def_.def_
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')
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 (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : PredName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ Y ys)
Tactic:
cases h2
Proof state after:
case intro
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : PredName
ys : List VarName
left✝ : X = Y
right✝ : isAlphaEqvVarList binders xs ys
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ Y ys)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : PredName
ys : List VarName
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ Y ys)
Tactic:
case intro h2_left h2_right =>
  simp only [Holds]
  subst h2_left
  congr! 1
  exact aux_2 D binders xs ys V V' h1 h2_right
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : PredName
ys : List VarName
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ Y ys)
Tactic:
simp only [Holds]
Proof state after:
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : PredName
ys : List VarName
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ Y (List.map V' ys)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : PredName
ys : List VarName
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ Y (List.map V' ys)
Tactic:
subst h2_left
Proof state after:
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2_right : isAlphaEqvVarList binders xs ys
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V' ys)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2_right : isAlphaEqvVarList binders xs ys
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V' ys)
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 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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2_right : isAlphaEqvVarList binders xs ys
⊢ List.map V xs = List.map V' ys
Theorem: FOL.NV.isAlphaEqv_Holds_aux
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 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 : PredName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2_right : isAlphaEqvVarList binders xs ys
⊢ List.map V xs = List.map V' ys
Tactic:
exact aux_2 D binders xs ys V V' h1 h2_right
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
h2 : isAlphaEqvVar binders x y ∧ isAlphaEqvVar binders x' y'
⊢ Holds D I V (head✝ :: tail✝) (eq_ x x') ↔ Holds D I V' (head✝ :: tail✝) (eq_ y y')
Tactic:
cases h2
Proof state after:
case intro
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
left✝ : isAlphaEqvVar binders x y
right✝ : isAlphaEqvVar binders x' y'
⊢ Holds D I V (head✝ :: tail✝) (eq_ x x') ↔ Holds D I V' (head✝ :: tail✝) (eq_ y y')
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
h2_left : isAlphaEqvVar binders x y
h2_right : isAlphaEqvVar binders x' y'
⊢ Holds D I V (head✝ :: tail✝) (eq_ x x') ↔ Holds D I V' (head✝ :: tail✝) (eq_ y y')
Tactic:
simp only [Holds]
Proof state after:
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
h2_left : isAlphaEqvVar binders x y
h2_right : isAlphaEqvVar binders x' y'
⊢ V x = V x' ↔ V' y = V' y'
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
h2_left : isAlphaEqvVar binders x y
h2_right : isAlphaEqvVar binders x' y'
⊢ V x = V x' ↔ V' y = V' y'
Tactic:
congr! 1
Proof state after:
case a.h.e'_2
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
h2_left : isAlphaEqvVar binders x y
h2_right : isAlphaEqvVar binders x' y'
⊢ V x = V' y

case a.h.e'_3
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
h2_left : isAlphaEqvVar binders x y
h2_right : isAlphaEqvVar binders x' y'
⊢ V x' = V' y'
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case a.h.e'_2
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
h2_left : isAlphaEqvVar binders x y
h2_right : isAlphaEqvVar binders x' y'
⊢ V x = V' y
Tactic:
exact aux_1 D binders x y V V' h1 h2_left
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case a.h.e'_3
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 x' : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y y' : VarName
h2_left : isAlphaEqvVar binders x y
h2_right : isAlphaEqvVar binders x' y'
⊢ V x' = V' y'
Tactic:
exact aux_1 D binders x' y' V V' h1 h2_right
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : True
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) false_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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')
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)
h1 : AlphaEqvVarAssignment D binders V V'
phi' : Formula
h2 : isAlphaEqvAux binders phi phi'
⊢ Holds D I V (head✝ :: tail✝) phi.not_ ↔ Holds D I V' (head✝ :: tail✝) phi'.not_
Tactic:
simp only [Holds]
Proof state after:
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')
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)
h1 : AlphaEqvVarAssignment D binders V V'
phi' : Formula
h2 : isAlphaEqvAux binders phi phi'
⊢ ¬Holds D I V (head✝ :: tail✝) phi ↔ ¬Holds D I V' (head✝ :: tail✝) phi'
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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')
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)
h1 : AlphaEqvVarAssignment D binders V V'
phi' : Formula
h2 : isAlphaEqvAux binders phi phi'
⊢ ¬Holds D I V (head✝ :: tail✝) phi ↔ ¬Holds D I V' (head✝ :: tail✝) phi'
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
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')
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)
h1 : AlphaEqvVarAssignment D binders V V'
phi' : Formula
h2 : isAlphaEqvAux binders phi phi'
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi'
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case a.h.e'_1.a
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')
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)
h1 : AlphaEqvVarAssignment D binders V V'
phi' : Formula
h2 : isAlphaEqvAux binders phi phi'
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi'
Tactic:
exact phi_ih V V' phi' binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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')
phi psi : 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')
psi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders psi F' → (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
phi' psi' : Formula
h2 : isAlphaEqvAux binders phi phi' ∧ isAlphaEqvAux binders psi psi'
⊢ Holds D I V (head✝ :: tail✝) (phi.iff_ psi) ↔ Holds D I V' (head✝ :: tail✝) (phi'.iff_ psi')
Tactic:
cases h2
Proof state after:
case intro
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')
phi psi : 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')
psi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders psi F' → (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
phi' psi' : Formula
left✝ : isAlphaEqvAux binders phi phi'
right✝ : isAlphaEqvAux binders psi psi'
⊢ Holds D I V (head✝ :: tail✝) (phi.iff_ psi) ↔ Holds D I V' (head✝ :: tail✝) (phi'.iff_ psi')