Theorem: LN.HoldsCoincideVar (FOL/LN/Paper.lean)

State before:
D : Type
I : Interpretation D
V V' : VarAssignment D
F : Formula
h1 : ∀ (v : Var), occursFreeIn v F → V v = V' v
⊢ Holds D I V F ↔ Holds D I V' F
Tactic:
induction F generalizing V V'
State after:
case pred_
D : Type
I : Interpretation D
a✝¹ : String
a✝ : List Var
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (pred_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (pred_ a✝¹ a✝) ↔ Holds D I V' (pred_ a✝¹ a✝)

case not_
D : Type
I : Interpretation D
a✝ : Formula
a_ih✝ : ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v a✝ → V v = V' v) → (Holds D I V a✝ ↔ Holds D I V' a✝)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v a✝.not_ → V v = V' v
⊢ Holds D I V a✝.not_ ↔ Holds D I V' a✝.not_

case imp_
D : Type
I : Interpretation D
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v a✝¹ → V v = V' v) → (Holds D I V a✝¹ ↔ Holds D I V' a✝¹)
a_ih✝ : ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v a✝ → V v = V' v) → (Holds D I V a✝ ↔ Holds D I V' a✝)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (a✝¹.imp_ a✝) → V v = V' v
⊢ Holds D I V (a✝¹.imp_ a✝) ↔ Holds D I V' (a✝¹.imp_ a✝)

case forall_
D : Type
I : Interpretation D
a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v a✝ → V v = V' v) → (Holds D I V a✝ ↔ Holds D I V' a✝)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (forall_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (forall_ a✝¹ a✝) ↔ Holds D I V' (forall_ a✝¹ a✝)

State before:
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (pred_ X vs) → V v = V' v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I V' (pred_ X vs)
Tactic:
case pred_ X vs =>
  simp only [occursFreeIn] at h1
  simp only [Holds]
  congr! 1
  simp only [List.map_eq_map_iff]
  exact h1
State after:
no goals

State before:
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi.not_ → V v = V' v
⊢ Holds D I V phi.not_ ↔ Holds D I V' phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [occursFreeIn] at h1
  simp only [Holds]
  congr! 1
  exact phi_ih V V' h1
State after:
no goals

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (forall_ x phi) → V v = V' v
⊢ Holds D I V (forall_ x phi) ↔ Holds D I V' (forall_ x phi)
Tactic:
case forall_ x phi phi_ih =>
  simp only [occursFreeIn] at h1
  simp only [Holds]
  apply forall_congr'
  intro d
  apply phi_ih
  intro v a1
  cases v
  case free_ x =>
    simp only [shift]
    apply h1
    exact a1
  case bound_ i =>
    cases i
    case zero =>
      simp only [shift]
    case succ i =>
      simp only [shift]
      apply h1
      simp only [lift]
      exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (pred_ X vs) → V v = V' v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I V' (pred_ X vs)
Tactic:
simp only [occursFreeIn] at h1
State after:
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I V' (pred_ X vs)

State before:
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I V' (pred_ X vs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ I.pred_ X (List.map V vs) ↔ I.pred_ X (List.map V' vs)

State before:
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ I.pred_ X (List.map V vs) ↔ I.pred_ X (List.map V' vs)
Tactic:
congr! 1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ List.map V vs = List.map V' vs

State before:
case a.h.e'_4
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ List.map V vs = List.map V' vs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case a.h.e'_4
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ ∀ x ∈ vs, V x = V' x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ ∀ x ∈ vs, V x = V' x
Tactic:
exact h1
State after:
no goals

State before:
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi.not_ → V v = V' v
⊢ Holds D I V phi.not_ ↔ Holds D I V' phi.not_
Tactic:
simp only [occursFreeIn] at h1
State after:
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi → V v = V' v
⊢ Holds D I V phi.not_ ↔ Holds D I V' phi.not_

State before:
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi → V v = V' v
⊢ Holds D I V phi.not_ ↔ Holds D I V' phi.not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi → V v = V' v
⊢ ¬Holds D I V phi ↔ ¬Holds D I V' phi

State before:
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi → V v = V' v
⊢ ¬Holds D I V phi ↔ ¬Holds D I V' phi
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi → V v = V' v
⊢ Holds D I V phi ↔ Holds D I V' phi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v phi → V v = V' v
⊢ Holds D I V phi ↔ Holds D I V' phi
Tactic:
exact phi_ih V V' h1
State after:
no goals

State before:
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I V' (phi.imp_ psi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
⊢ Holds D I V phi → Holds D I V psi ↔ Holds D I V' phi → Holds D I V' psi

State before:
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
⊢ Holds D I V phi → Holds D I V psi ↔ Holds D I V' phi → Holds D I V' psi
Tactic:
congr! 1
State after:
case a.h.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
⊢ Holds D I V phi ↔ Holds D I V' phi

case a.h'.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
⊢ Holds D I V psi ↔ Holds D I V' psi

State before:
case a.h.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
⊢ Holds D I V phi ↔ Holds D I V' phi
Tactic:
apply phi_ih
State after:
case a.h.a.h1
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
⊢ ∀ (v : Var), occursFreeIn v phi → V v = V' v

State before:
case a.h.a.h1
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
⊢ ∀ (v : Var), occursFreeIn v phi → V v = V' v
Tactic:
intro v a1
State after:
case a.h.a.h1
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
v : Var
a1 : occursFreeIn v phi
⊢ V v = V' v

State before:
case a.h.a.h1
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
v : Var
a1 : occursFreeIn v phi
⊢ V v = V' v
Tactic:
apply h1
State after:
case a.h.a.h1.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
v : Var
a1 : occursFreeIn v phi
⊢ occursFreeIn v (phi.imp_ psi)

State before:
case a.h.a.h1.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
v : Var
a1 : occursFreeIn v phi
⊢ occursFreeIn v (phi.imp_ psi)
Tactic:
simp only [occursFreeIn]
State after:
case a.h.a.h1.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
v : Var
a1 : occursFreeIn v phi
⊢ occursFreeIn v phi ∨ occursFreeIn v psi

State before:
case a.h.a.h1.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
v : Var
a1 : occursFreeIn v phi
⊢ occursFreeIn v phi ∨ occursFreeIn v psi
Tactic:
tauto
State after:
no goals

State before:
case a.h'.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
⊢ Holds D I V psi ↔ Holds D I V' psi
Tactic:
apply psi_ih
State after:
case a.h'.a.h1
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
⊢ ∀ (v : Var), occursFreeIn v psi → V v = V' v

State before:
case a.h'.a.h1
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
⊢ ∀ (v : Var), occursFreeIn v psi → V v = V' v
Tactic:
intro v a1
State after:
case a.h'.a.h1
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
v : Var
a1 : occursFreeIn v psi
⊢ V v = V' v

State before:
case a.h'.a.h1
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
v : Var
a1 : occursFreeIn v psi
⊢ V v = V' v
Tactic:
apply h1
State after:
case a.h'.a.h1.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
v : Var
a1 : occursFreeIn v psi
⊢ occursFreeIn v (phi.imp_ psi)

State before:
case a.h'.a.h1.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
v : Var
a1 : occursFreeIn v psi
⊢ occursFreeIn v (phi.imp_ psi)
Tactic:
simp only [occursFreeIn]
State after:
case a.h'.a.h1.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
v : Var
a1 : occursFreeIn v psi
⊢ occursFreeIn v phi ∨ occursFreeIn v psi

State before:
case a.h'.a.h1.a
D : Type
I : Interpretation D
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
a✝ : Holds D I V' phi
v : Var
a1 : occursFreeIn v psi
⊢ occursFreeIn v phi ∨ occursFreeIn v psi
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (forall_ x phi) → V v = V' v
⊢ Holds D I V (forall_ x phi) ↔ Holds D I V' (forall_ x phi)
Tactic:
simp only [occursFreeIn] at h1
State after:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ Holds D I V (forall_ x phi) ↔ Holds D I V' (forall_ x phi)

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ Holds D I V (forall_ x phi) ↔ Holds D I V' (forall_ x phi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ (∀ (d : D), Holds D I (shift D V d) phi) ↔ ∀ (d : D), Holds D I (shift D V' d) phi

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ (∀ (d : D), Holds D I (shift D V d) phi) ↔ ∀ (d : D), Holds D I (shift D V' d) phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ ∀ (a : D), Holds D I (shift D V a) phi ↔ Holds D I (shift D V' a) phi

State before:
case h
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
⊢ ∀ (a : D), Holds D I (shift D V a) phi ↔ Holds D I (shift D V' a) phi
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ Holds D I (shift D V d) phi ↔ Holds D I (shift D V' d) phi

State before:
case h
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ Holds D I (shift D V d) phi ↔ Holds D I (shift D V' d) phi
Tactic:
apply phi_ih
State after:
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ ∀ (v : Var), occursFreeIn v phi → shift D V d v = shift D V' d v

State before:
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ ∀ (v : Var), occursFreeIn v phi → shift D V d v = shift D V' d v
Tactic:
intro v a1
State after:
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
v : Var
a1 : occursFreeIn v phi
⊢ shift D V d v = shift D V' d v

State before:
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
v : Var
a1 : occursFreeIn v phi
⊢ shift D V d v = shift D V' d v
Tactic:
cases v
State after:
case h.h1.free_
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a✝ : String
a1 : occursFreeIn (free_ a✝) phi
⊢ shift D V d (free_ a✝) = shift D V' d (free_ a✝)

case h.h1.bound_
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a✝ : ℕ
a1 : occursFreeIn (bound_ a✝) phi
⊢ shift D V d (bound_ a✝) = shift D V' d (bound_ a✝)

State before:
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ shift D V d (free_ x) = shift D V' d (free_ x)
Tactic:
case free_ x =>
  simp only [shift]
  apply h1
  exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ i) phi
⊢ shift D V d (bound_ i) = shift D V' d (bound_ i)
Tactic:
case bound_ i =>
  cases i
  case zero =>
    simp only [shift]
  case succ i =>
    simp only [shift]
    apply h1
    simp only [lift]
    exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ shift D V d (free_ x) = shift D V' d (free_ x)
Tactic:
simp only [shift]
State after:
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ V (free_ x) = V' (free_ x)

State before:
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ V (free_ x) = V' (free_ x)
Tactic:
apply h1
State after:
case a
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ occursFreeIn (lift (free_ x)) phi

State before:
case a
D : Type
I : Interpretation D
x✝ : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
x : String
a1 : occursFreeIn (free_ x) phi
⊢ occursFreeIn (lift (free_ x)) phi
Tactic:
exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ i) phi
⊢ shift D V d (bound_ i) = shift D V' d (bound_ i)
Tactic:
cases i
State after:
case zero
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a1 : occursFreeIn (bound_ 0) phi
⊢ shift D V d (bound_ 0) = shift D V' d (bound_ 0)

case succ
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
n✝ : ℕ
a1 : occursFreeIn (bound_ (n✝ + 1)) phi
⊢ shift D V d (bound_ (n✝ + 1)) = shift D V' d (bound_ (n✝ + 1))

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a1 : occursFreeIn (bound_ 0) phi
⊢ shift D V d (bound_ 0) = shift D V' d (bound_ 0)
Tactic:
case zero =>
  simp only [shift]
State after:
no goals

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ shift D V d (bound_ (i + 1)) = shift D V' d (bound_ (i + 1))
Tactic:
case succ i =>
  simp only [shift]
  apply h1
  simp only [lift]
  exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
a1 : occursFreeIn (bound_ 0) phi
⊢ shift D V d (bound_ 0) = shift D V' d (bound_ 0)
Tactic:
simp only [shift]
State after:
no goals

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ shift D V d (bound_ (i + 1)) = shift D V' d (bound_ (i + 1))
Tactic:
simp only [shift]
State after:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ V (bound_ i) = V' (bound_ i)

State before:
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ V (bound_ i) = V' (bound_ i)
Tactic:
apply h1
State after:
case a
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ occursFreeIn (lift (bound_ i)) phi

State before:
case a
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ occursFreeIn (lift (bound_ i)) phi
Tactic:
simp only [lift]
State after:
case a
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ occursFreeIn (bound_ (i + 1)) phi

State before:
case a
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) phi
⊢ occursFreeIn (bound_ (i + 1)) phi
Tactic:
exact a1
State after:
no goals