internlm/Lean-Github huggingface dataset:
Theorem: loadClaimHelper
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)
Tactic:
have : (⌈List.get δ (i.cast help1)⌉⌈⌈List.drop (i + 1) δ⌉⌉φ) = (⌈⌈List.drop (i.castSucc) δ⌉⌉φ) := by
  simp only [List.append_eq, Fin.coe_castSucc]
  rw [← Formula.boxes]
  have := @List.drop_eq_get_cons _ i δ (by rw [← length_def]; have := Fin.is_lt i; convert this; simp)
  rw [this]
  cases i
  simp_all only [instBot, insTop, List.zip_cons_cons, Subtype.forall, List.append_eq,
    Fin.castSucc_mk, boxes, Fin.cast_mk]
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)
Theorem: loadClaimHelper
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)
Tactic:
rw [this]
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
⊢ (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)
Theorem: loadClaimHelper
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
⊢ (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i.castSucc)
Tactic:
exact IH
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ
Tactic:
simp only [List.append_eq, Fin.coe_castSucc]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈δ.get (Fin.cast help1 i)⌉⌈⌈List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Tactic:
rw [← Formula.boxes]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Tactic:
have := @List.drop_eq_get_cons _ i δ (by rw [← length_def]; have := Fin.is_lt i; convert this; simp)
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : List.drop (↑i) δ = δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : List.drop (↑i) δ = δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈List.drop (↑i) δ⌉⌉φ
Tactic:
rw [this]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : List.drop (↑i) δ = δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ⌉⌉φ
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : List.drop (↑i) δ = δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 i) :: List.drop (↑i + 1) δ⌉⌉φ) = ⌈⌈δ.get ⟨↑i, ⋯⟩ :: List.drop (↑i + 1) δ⌉⌉φ
Tactic:
cases i
Proof state after:
case mk
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
val✝ : ℕ
isLt✝ : val✝ < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val✝, isLt✝⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val✝, isLt✝⟩.castSucc)
this : List.drop (↑⟨val✝, isLt✝⟩) δ = δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 ⟨val✝, isLt✝⟩) :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ) =
    ⌈⌈δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ
Theorem: loadClaimHelper
Proof state before:
case mk
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
help1 : (l.append [Y]).length = δ.length
val✝ : ℕ
isLt✝ : val✝ < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val✝, isLt✝⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val✝, isLt✝⟩.castSucc)
this : List.drop (↑⟨val✝, isLt✝⟩) δ = δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 ⟨val✝, isLt✝⟩) :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ) =
    ⌈⌈δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ
Tactic:
simp_all only [instBot, insTop, List.zip_cons_cons, Subtype.forall, List.append_eq,
  Fin.castSucc_mk, boxes, Fin.cast_mk]
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ ↑i < δ.length
Tactic:
rw [← length_def]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ ↑i < l.length + 1
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ ↑i < l.length + 1
Tactic:
have := Fin.is_lt i
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : ↑i < (l.append [Y]).length
⊢ ↑i < l.length + 1
Theorem: loadClaimHelper
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : ↑i < (l.append [Y]).length
⊢ ↑i < l.length + 1
Tactic:
convert this
Proof state after:
case h.e'_4
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : ↑i < (l.append [Y]).length
⊢ l.length + 1 = (l.append [Y]).length
Theorem: loadClaimHelper
Proof state before:
case h.e'_4
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
this : ↑i < (l.append [Y]).length
⊢ l.length + 1 = (l.append [Y]).length
Tactic:
simp
Proof state after:
no goals
Theorem: loadClaimHelper
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: l ++ [Y]).get i.castSucc) ((l ++ [Y]).get i)
Tactic:
simp [relate]
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Theorem: loadClaimHelper
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: (l ++ [Y])))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Tactic:
rw [List.chain'_iff_get] at lchain
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Theorem: loadClaimHelper
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Tactic:
specialize lchain i ?_
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
⊢ ↑i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1

case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
lchain :
  pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i, ⋯⟩)
    ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i + 1, ⋯⟩)
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Theorem: loadClaimHelper
Proof state before:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
lchain :
  pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i, ⋯⟩)
    ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i + 1, ⋯⟩)
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)
Tactic:
simp only [pairRel, instBot, insTop, List.cons_append, List.zip_cons_cons, List.length_cons, List.append_eq, List.get_cons_succ, List.get_zip] at lchain
Proof state after:
case a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
⊢ relate (↑MG) (δ.get (Fin.cast help1 i)) ((X :: (l ++ [Y])).get i.castSucc) ((l ++ [Y]).get i)