internlm/Lean-Github huggingface dataset:
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝¹ : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝ : oh Q X
⊢ plus (P⋀Q) X ∧ minus (P⋀Q) X ∧ oh (P⋀Q) X
Tactic:
rcases i X with ⟨X_saturated, _, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated : Saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ plus (P⋀Q) X ∧ minus (P⋀Q) X ∧ oh (P⋀Q) X
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated : Saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ plus (P⋀Q) X ∧ minus (P⋀Q) X ∧ oh (P⋀Q) X
Tactic:
unfold Saturated at X_saturated
Proof state after:
case intro.intro.intro.intro.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ plus (P⋀Q) X ∧ minus (P⋀Q) X ∧ oh (P⋀Q) X
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ plus (P⋀Q) X ∧ minus (P⋀Q) X ∧ oh (P⋀Q) X
Tactic:
rcases X_saturated P Q with ⟨_, andSplit, notAndSplit⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
andSplit : P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
⊢ plus (P⋀Q) X ∧ minus (P⋀Q) X ∧ oh (P⋀Q) X
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
andSplit : P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
⊢ plus (P⋀Q) X
Tactic:
intro PandQ_in_X
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
andSplit : P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
⊢ Evaluate (M, X) (P⋀Q)
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
andSplit : P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
⊢ Evaluate (M, X) (P⋀Q)
Tactic:
specialize andSplit PandQ_in_X
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
andSplit : P ∈ ↑X ∧ Q ∈ ↑X
⊢ Evaluate (M, X) (P⋀Q)
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
andSplit : P ∈ ↑X ∧ Q ∈ ↑X
⊢ Evaluate (M, X) (P⋀Q)
Tactic:
cases' andSplit with P_in_X Q_in_X
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
P_in_X : P ∈ ↑X
Q_in_X : Q ∈ ↑X
⊢ Evaluate (M, X) (P⋀Q)
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
P_in_X : P ∈ ↑X
Q_in_X : Q ∈ ↑X
⊢ Evaluate (M, X) (P⋀Q)
Tactic:
unfold Evaluate
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
P_in_X : P ∈ ↑X
Q_in_X : Q ∈ ↑X
⊢ Evaluate (M, X) P ∧ Evaluate (M, X) Q
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left.intro.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
P_in_X : P ∈ ↑X
Q_in_X : Q ∈ ↑X
⊢ Evaluate (M, X) P
Tactic:
exact plus_IH_P P_in_X
Proof state after:
no goals
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left.intro.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
PandQ_in_X : P⋀Q ∈ ↑X
P_in_X : P ∈ ↑X
Q_in_X : Q ∈ ↑X
⊢ Evaluate (M, X) Q
Tactic:
exact plus_IH_Q Q_in_X
Proof state after:
no goals
Theorem: truthLemma
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
andSplit : P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
⊢ minus (P⋀Q) X
Tactic:
intro notPandQ_in_X
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P Q : Formula
IH_P : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
IH_Q : ∀ (X : ↑Worlds), plus Q X ∧ minus Q X ∧ oh Q X
X : ↑Worlds
plus_IH_P : plus P X
minus_IH_P : minus P X
right✝² : oh P X
plus_IH_Q : plus Q X
minus_IH_Q : minus Q X
right✝¹ : oh Q X
X_saturated :
  let X := ↑X;
  ∀ (P Q : Formula), (~~P ∈ X → P ∈ X) ∧ (P⋀Q ∈ X → P ∈ X ∧ Q ∈ X) ∧ (~(P⋀Q) ∈ X → ~P ∈ X ∨ ~Q ∈ X)
left✝¹ : ⊥ ∉ ↑X
right✝ : ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ~~P ∈ ↑X → P ∈ ↑X
andSplit : P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X
notAndSplit : ~(P⋀Q) ∈ ↑X → ~P ∈ ↑X ∨ ~Q ∈ ↑X
notPandQ_in_X : ~(P⋀Q) ∈ ↑X
⊢ ¬Evaluate (M, X) (P⋀Q)