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

State before:
D : Type
I : Interpretation D
V : VarAssignment D
j : ℕ
zs : List String
F : Formula
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) F ↔ Holds D I V (Formula.openList j (List.map free_ zs) F)
Tactic:
induction F generalizing V j
State after:
case pred_
D : Type
I : Interpretation D
zs : List String
a✝¹ : String
a✝ : List Var
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (pred_ a✝¹ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (pred_ a✝¹ a✝))

case not_
D : Type
I : Interpretation D
zs : List String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝.not_ ↔
    Holds D I V (Formula.openList j (List.map free_ zs) a✝.not_)

case imp_
D : Type
I : Interpretation D
zs : List String
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝¹ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (a✝¹.imp_ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (a✝¹.imp_ a✝))

case forall_
D : Type
I : Interpretation D
zs : List String
a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (forall_ a✝¹ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (forall_ a✝¹ a✝))

State before:
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (pred_ X vs) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (pred_ X vs))
Tactic:
case pred_ X vs =>
  simp only [Holds]
  congr! 1
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi.not_ ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [Holds]
  congr! 1
  apply phi_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (forall_ a✝ phi) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (forall_ a✝ phi))
Tactic:
case forall_ _ phi phi_ih =>
  simp only [Holds]
  apply forall_congr'
  intro d
  simp only [← phi_ih]
  congr!
  apply ShiftVarOpenList
State after:
no goals

State before:
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (pred_ X vs) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (pred_ X vs))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ I.pred_ X (List.map (V ∘ Var.openList j (List.map free_ zs)) vs) ↔
    I.pred_ X (List.map V (List.map (Var.openList j (List.map free_ zs)) vs))

State before:
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ I.pred_ X (List.map (V ∘ Var.openList j (List.map free_ zs)) vs) ↔
    I.pred_ X (List.map V (List.map (Var.openList j (List.map free_ zs)) vs))
Tactic:
congr! 1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ List.map (V ∘ Var.openList j (List.map free_ zs)) vs = List.map V (List.map (Var.openList j (List.map free_ zs)) vs)

State before:
case a.h.e'_4
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ List.map (V ∘ Var.openList j (List.map free_ zs)) vs = List.map V (List.map (Var.openList j (List.map free_ zs)) vs)
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi.not_ ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi.not_)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ ¬Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ ¬Holds D I V (Formula.openList j (List.map free_ zs) phi)

State before:
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ ¬Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ ¬Holds D I V (Formula.openList j (List.map free_ zs) phi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
zs : List String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
Tactic:
apply phi_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (phi.imp_ psi) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (phi.imp_ psi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi → Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi) → Holds D I V (Formula.openList j (List.map free_ zs) psi)

State before:
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi → Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi) → Holds D I V (Formula.openList j (List.map free_ zs) psi)
Tactic:
congr! 1
State after:
case a.h.a
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)

case a.h'.a
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
a✝ : Holds D I V (Formula.openList j (List.map free_ zs) phi)
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)

State before:
case a.h.a
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
Tactic:
apply phi_ih
State after:
no goals

State before:
case a.h'.a
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
a✝ : Holds D I V (Formula.openList j (List.map free_ zs) phi)
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
Tactic:
apply psi_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (forall_ a✝ phi) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (forall_ a✝ phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ (∀ (d : D), Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi) ↔
    ∀ (d : D), Holds D I (shift D V d) (Formula.openList (j + 1) (List.map free_ zs) phi)

State before:
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ (∀ (d : D), Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi) ↔
    ∀ (d : D), Holds D I (shift D V d) (Formula.openList (j + 1) (List.map free_ zs) phi)
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ ∀ (a : D),
    Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) a) phi ↔
      Holds D I (shift D V a) (Formula.openList (j + 1) (List.map free_ zs) phi)

State before:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ ∀ (a : D),
    Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) a) phi ↔
      Holds D I (shift D V a) (Formula.openList (j + 1) (List.map free_ zs) phi)
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi ↔
    Holds D I (shift D V d) (Formula.openList (j + 1) (List.map free_ zs) phi)

State before:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi ↔
    Holds D I (shift D V d) (Formula.openList (j + 1) (List.map free_ zs) phi)
Tactic:
simp only [← phi_ih]
State after:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi ↔
    Holds D I (shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)) phi

State before:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi ↔
    Holds D I (shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)) phi
Tactic:
congr!
State after:
case h.a.h.e'_3
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d = shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)

State before:
case h.a.h.e'_3
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d = shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)
Tactic:
apply ShiftVarOpenList
State after:
no goals