internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi → V v = V' v
⊢ ¬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 : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_Var
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 : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi
Tactic:
exact phi_ih V V' h1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V (head✝ :: tail✝) psi) ↔
    (Holds D I V' (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) psi)
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 : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi

case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi
Theorem: FOL.NV.Holds_coincide_Var
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 : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi
Tactic:
apply phi_ih V V'
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 : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v phi → V v = V' v
Theorem: FOL.NV.Holds_coincide_Var
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 : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v phi → V v = V' v
Tactic:
intro v a1
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 : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ V v = V' v
Theorem: FOL.NV.Holds_coincide_Var
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 : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ V v = V' v
Tactic:
apply h1
Proof state after:
case a.h.e'_1.a.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_1.a.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Tactic:
left
Proof state after:
case a.h.e'_1.a.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_1.a.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi
Tactic:
apply psi_ih V V'
Proof state after:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v psi → V v = V' v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v psi → V v = V' v
Tactic:
intro v a1
Proof state after:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ V v = V' v
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ V v = V' v
Tactic:
apply h1
Proof state after:
case a.h.e'_2.a.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_2.a.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Tactic:
right
Proof state after:
case a.h.e'_2.a.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v psi
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case a.h.e'_2.a.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v psi
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
simp at h1
Proof state after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) (head✝ :: tail✝) phi
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi ↔ Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Theorem: FOL.NV.Holds_coincide_Var
Proof state before:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi ↔ Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
apply phi_ih
Proof state after:
case h.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
⊢ ∀ (v : VarName), isFreeIn v phi → Function.updateITE V x d v = Function.updateITE V' x d v