internlm/Lean-Github huggingface dataset:
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V
      (if 0 < 0 then bound_ 0
      else
        if x : 0 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[0 - 0]
        else bound_ (0 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V (free_ hd)
Tactic:
simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ (i + 1))
Tactic:
simp only [shift]
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shiftList D V (List.map (V ∘ free_) tl) (bound_ i)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shiftList D V (List.map (V ∘ free_) tl) (bound_ i)
Tactic:
simp only [← ih]
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    (V ∘ Var.openList 0 (List.map free_ tl)) (bound_ i)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    (V ∘ Var.openList 0 (List.map free_ tl)) (bound_ i)
Tactic:
simp
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    V (Var.openList 0 (List.map free_ tl) (bound_ i))
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    V (Var.openList 0 (List.map free_ tl) (bound_ i))
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V
      (if i + 1 < 0 then bound_ (i + 1)
      else
        if x : i + 1 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[i + 1 - 0]
        else bound_ (i + 1 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V
      (if i < 0 then bound_ i
      else
        if x : i - 0 < (List.map free_ tl).length then (List.map free_ tl)[i - 0]
        else bound_ (i - 0 - (List.map free_ tl).length + 0))
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V
      (if i + 1 < 0 then bound_ (i + 1)
      else
        if x : i + 1 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[i + 1 - 0]
        else bound_ (i + 1 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V
      (if i < 0 then bound_ i
      else
        if x : i - 0 < (List.map free_ tl).length then (List.map free_ tl)[i - 0]
        else bound_ (i - 0 - (List.map free_ tl).length + 0))
Tactic:
simp
Proof state after:
no goals
Theorem: LN.lc_at_iff_lc
Proof state before:
F : Formula
⊢ Formula.lc_at 0 F ↔ F.lc
Tactic:
constructor
Proof state after:
case mp
F : Formula
⊢ Formula.lc_at 0 F → F.lc

case mpr
F : Formula
⊢ F.lc → Formula.lc_at 0 F
Theorem: LN.lc_at_iff_lc
Proof state before:
case mp
F : Formula
⊢ Formula.lc_at 0 F → F.lc
Tactic:
intro a1
Proof state after:
case mp
F : Formula
a1 : Formula.lc_at 0 F
⊢ F.lc
Theorem: LN.lc_at_iff_lc
Proof state before:
case mp
F : Formula
a1 : Formula.lc_at 0 F
⊢ F.lc
Tactic:
sorry
Proof state after:
no goals
Theorem: LN.lc_at_iff_lc
Proof state before:
case mpr
F : Formula
⊢ F.lc → Formula.lc_at 0 F
Tactic:
intro a1
Proof state after:
case mpr
F : Formula
a1 : F.lc
⊢ Formula.lc_at 0 F
Theorem: LN.lc_at_iff_lc
Proof state before:
case mpr
F : Formula
a1 : F.lc
⊢ Formula.lc_at 0 F
Tactic:
sorry
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof 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'
Proof 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✝)
Theorem: LN.HoldsCoincideVar
Proof 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
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof 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
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof 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
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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)
Theorem: LN.HoldsCoincideVar
Proof 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]
Proof 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)
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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]
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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_
Theorem: LN.HoldsCoincideVar
Proof 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]
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof 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]
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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)
Theorem: LN.HoldsCoincideVar
Proof 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]
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof state after:
no goals
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof 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)
Theorem: LN.HoldsCoincideVar
Proof 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]
Proof 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
Theorem: LN.HoldsCoincideVar
Proof 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
Proof state after:
no goals