internlm/Lean-Github huggingface dataset:
Theorem: oneSidedLocalRuleTruth
Proof state before:
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
w_1 : W
left : relate M α w w_1
right : ¬evaluate M w_1 φ
⊢ evaluate M w (discon (unfoldDiamond α φ))

case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
a : evaluate M w (discon (unfoldDiamond α φ))
⊢ ∃ x, relate M α w x ∧ ¬evaluate M x φ
Tactic:
done
Proof state after:
no goals
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (Con [⌈α⌉φ]) ↔ evaluate M w (discon (unfoldBox α φ))
Tactic:
rw [conEval]
Proof state after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldBox α φ))
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldBox α φ))
Tactic:
simp only [List.mem_singleton, forall_eq]
Proof state after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (⌈α⌉φ) ↔ evaluate M w (discon (unfoldBox α φ))
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (⌈α⌉φ) ↔ evaluate M w (discon (unfoldBox α φ))
Tactic:
rw [localBoxTruth α φ W M w]
Proof state after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset α ℓ φ)) (allTP α))) ↔ evaluate M w (discon (unfoldBox α φ))
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset α ℓ φ)) (allTP α))) ↔ evaluate M w (discon (unfoldBox α φ))
Tactic:
simp only [disEval, List.mem_map, exists_exists_and_eq_and, unfoldBox, disconEval]
Proof state after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) ↔ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) ↔ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
Tactic:
constructor
Proof state after:
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) → ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f

case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f) → ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))
Theorem: oneSidedLocalRuleTruth
Proof state before:
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) → ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
Tactic:
rintro ⟨l,hyp⟩
Proof state after:
case mp.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
Theorem: oneSidedLocalRuleTruth
Proof state before:
case mp.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
Tactic:
use l
Proof state after:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
Theorem: oneSidedLocalRuleTruth
Proof state before:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
Tactic:
rw [conEval] at hyp
Proof state after:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
Theorem: oneSidedLocalRuleTruth
Proof state before:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
Tactic:
tauto
Proof state after:
no goals
Theorem: oneSidedLocalRuleTruth
Proof state before:
case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f) → ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))
Tactic:
rintro ⟨l,hyp⟩
Proof state after:
case mpr.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))
Theorem: oneSidedLocalRuleTruth
Proof state before:
case mpr.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))
Tactic:
use l
Proof state after:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
Theorem: oneSidedLocalRuleTruth
Proof state before:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
Tactic:
rw [conEval]
Proof state after:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (Con [~⌈α⌉φ]) ↔ evaluate M w (discon (unfoldDiamond α φ))
Tactic:
rw [conEval]
Proof state after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [~⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldDiamond α φ))
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [~⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldDiamond α φ))
Tactic:
simp only [List.mem_singleton, forall_eq, discon, unfoldDiamond]
Proof state after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (~⌈α⌉φ) ↔ evaluate M w (discon (List.map (fun Fδ => Yset Fδ φ) (H α)))
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (~⌈α⌉φ) ↔ evaluate M w (discon (List.map (fun Fδ => Yset Fδ φ) (H α)))
Tactic:
rw [localDiamondTruth α φ W M w, disEval, disconEval]
Proof state after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ φ)) (H α), evaluate M w f) ↔
    ∃ Y ∈ List.map (fun Fδ => Yset Fδ φ) (H α), ∀ f ∈ Y, evaluate M w f
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ φ)) (H α), evaluate M w f) ↔
    ∃ Y ∈ List.map (fun Fδ => Yset Fδ φ) (H α), ∀ f ∈ Y, evaluate M w f
Tactic:
apply mapCon_mapForall
Proof state after:
no goals
Theorem: loadRuleTruth
Proof state before:
χ : LoadFormula
B : List (List Formula × Option NegLoadFormula)
lr : LoadRule (~'χ) B
⊢ (~unload χ)≡dis
      (List.map
        (fun x =>
          match x with
          | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
        B)
Tactic:
intro W M w
Proof state after:
χ : LoadFormula
B : List (List Formula × Option NegLoadFormula)
lr : LoadRule (~'χ) B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          B))
Theorem: loadRuleTruth
Proof state before:
χ : LoadFormula
B : List (List Formula × Option NegLoadFormula)
lr : LoadRule (~'χ) B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          B))
Tactic:
cases lr
Proof state after:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
χ✝ : LoadFormula
⊢ evaluate M w (~unload (⌊α✝⌋χ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad α✝ χ✝)))

case dia'
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (~unload (⌊α✝⌋φ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad' α✝ φ✝)))
Theorem: loadRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α✝ : Program
χ✝ : LoadFormula
⊢ evaluate M w (~unload (⌊α✝⌋χ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad α✝ χ✝)))
Tactic:
case dia =>
  sorry
Proof state after:
no goals
Theorem: loadRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (~unload (⌊α✝⌋φ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad' α✝ φ✝)))
Tactic:
case dia' =>
  sorry
Proof state after:
no goals
Theorem: loadRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α✝ : Program
χ✝ : LoadFormula
⊢ evaluate M w (~unload (⌊α✝⌋χ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad α✝ χ✝)))
Tactic:
sorry
Proof state after:
no goals
Theorem: loadRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (~unload (⌊α✝⌋φ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad' α✝ φ✝)))
Tactic:
sorry
Proof state after:
no goals
Theorem: Option.some_subseteq
Proof state before:
α : Type u_1
x : α
O : Option α
⊢ some x ⊆ O ↔ some x = O
Tactic:
cases O
Proof state after:
case none
α : Type u_1
x : α
⊢ some x ⊆ none ↔ some x = none

case some
α : Type u_1
x val✝ : α
⊢ some x ⊆ some val✝ ↔ some x = some val✝
Theorem: Option.some_subseteq
Proof state before:
case none
α : Type u_1
x : α
⊢ some x ⊆ none ↔ some x = none

case some
α : Type u_1
x val✝ : α
⊢ some x ⊆ some val✝ ↔ some x = some val✝
Tactic:
all_goals simp
Proof state after:
no goals
Theorem: Option.some_subseteq
Proof state before:
case some
α : Type u_1
x val✝ : α
⊢ some x ⊆ some val✝ ↔ some x = some val✝
Tactic:
simp
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
lrA : LocalRuleApp (L, R, O) C
M : KripkeModel W
w : W
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
rcases lrA with ⟨Lcond, Rcond, Ocond, rule, preconditionProof⟩
Proof state after:
case mk
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress✝ : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress✝
preconditionProof : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
hC✝ : C = applyLocalRule rule (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
case mk
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress✝ : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress✝
preconditionProof : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
hC✝ : C = applyLocalRule rule (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
cases rule
Proof state after:
case mk.oneSidedL
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
hC✝ : C = applyLocalRule (LocalRule.oneSidedL orule✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.oneSidedR
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
preconditionProof : ∅.Sublist L ∧ Rcond.Sublist R ∧ none ⊆ O
hC✝ : C = applyLocalRule (LocalRule.oneSidedR orule✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.LRnegL
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ϕ✝ : Formula
preconditionProof : [ϕ✝].Sublist L ∧ [~ϕ✝].Sublist R ∧ none ⊆ O
hC✝ : C = applyLocalRule (LocalRule.LRnegL ϕ✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.LRnegR
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ϕ✝ : Formula
preconditionProof : [~ϕ✝].Sublist L ∧ [ϕ✝].Sublist R ∧ none ⊆ O
hC✝ : C = applyLocalRule (LocalRule.LRnegR ϕ✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.loadedL
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
preconditionProof : ∅.Sublist L ∧ ∅.Sublist R ∧ some (Sum.inl (~'χ✝)) ⊆ O
hC✝ : C = applyLocalRule (LocalRule.loadedL χ✝ lrule✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.loadedR
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
preconditionProof : ∅.Sublist L ∧ ∅.Sublist R ∧ some (Sum.inr (~'χ✝)) ⊆ O
hC✝ : C = applyLocalRule (LocalRule.loadedR χ✝ lrule✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [φ].Sublist L ∧ [~φ].Sublist R ∧ none ⊆ O
hC : C = applyLocalRule (LocalRule.LRnegL φ) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
case LRnegL φ hC =>
  subst hC
  simp [applyLocalRule] at *
  intro hyp
  have := hyp φ
  have := hyp (~φ)
  aesop
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [~φ].Sublist L ∧ [φ].Sublist R ∧ none ⊆ O
hC : C = applyLocalRule (LocalRule.LRnegR φ) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
case LRnegR φ hC =>
  subst hC
  simp [applyLocalRule] at *
  intro hyp
  have := hyp φ
  have := hyp (~φ)
  aesop
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
hC : C = applyLocalRule (LocalRule.oneSidedL orule) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
have osTruth := oneSidedLocalRuleTruth orule W M w
Proof state after:
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
hC : C = applyLocalRule (LocalRule.oneSidedL orule) (L, R, O)
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
hC : C = applyLocalRule (LocalRule.oneSidedL orule) (L, R, O)
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
subst hC
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.oneSidedL orule) (L, R, O), (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.oneSidedL orule) (L, R, O), (M, w)⊨Ci
Tactic:
simp [applyLocalRule] at *
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
⊢ (M, w)⊨(L, R, O) ↔ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
⊢ (M, w)⊨(L, R, O) ↔ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
constructor
Proof state after:
case mp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
⊢ (M, w)⊨(L, R, O) → ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)

case mpr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
⊢ (∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)) → (M, w)⊨(L, R, O)
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
⊢ (M, w)⊨(L, R, O) → ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
intro w_LRO
Proof state after:
case mp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
have : evaluate M w (discon ress) := by
  rw [← osTruth, conEval]
  intro f f_in; apply w_LRO
  simp only [List.mem_union_iff, List.mem_append]
  exact Or.inl $ Or.inl $ List.Sublist.subset preconditionProof f_in
Proof state after:
case mp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
this : evaluate M w (discon ress)
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
this : evaluate M w (discon ress)
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
rw [disconEval] at this
Proof state after:
case mp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
this : ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
this : ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
rcases this with ⟨Y, Y_in, claim⟩
Proof state after:
case mp.intro.intro
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Theorem: localRuleTruth
Proof state before:
case mp.intro.intro
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
use Y
Proof state after:
case h
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ Y ∈ ress ∧ (M, w)⊨(L.diff Lcond ++ Y, R, O)