internlm/Lean-Github huggingface dataset:
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inl
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_L : f ∈ L
⊢ evaluate M w f
Tactic:
apply w_LYRO
Proof state after:
case mpr.intro.intro.inl.inl.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_L : f ∈ L
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inl.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_L : f ∈ L
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
⊢ evaluate M w f
Tactic:
rcases em (f ∈ Rcond) with f_in_cond | f_notin_cond
Proof state after:
case mpr.intro.intro.inl.inr.inl
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ evaluate M w f

case mpr.intro.intro.inl.inr.inr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ evaluate M w f
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inr.inl
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this✝ osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
this : ∀ f ∈ Rcond, evaluate M w f
⊢ evaluate M w f
Tactic:
exact this f f_in_cond
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∀ f ∈ Rcond, evaluate M w f
Tactic:
rw [← conEval, osTruth, disconEval]
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
Tactic:
use Y
Proof state after:
case h
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ Y ∈ ress ∧ ∀ f ∈ Y, evaluate M w f
Theorem: localRuleTruth
Proof state before:
case h
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ Y ∈ ress ∧ ∀ f ∈ Y, evaluate M w f
Tactic:
constructor
Proof state after:
case h.left
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ Y ∈ ress

case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∀ f ∈ Y, evaluate M w f
Theorem: localRuleTruth
Proof state before:
case h.left
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ Y ∈ ress
Tactic:
exact Y_in
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∀ f ∈ Y, evaluate M w f
Tactic:
intro f f_in
Proof state after:
case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f✝ : Formula
f_in_R : f✝ ∈ R
f_in_cond : f✝ ∈ Rcond
f : Formula
f_in : f ∈ Y
⊢ evaluate M w f
Theorem: localRuleTruth
Proof state before:
case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f✝ : Formula
f_in_R : f✝ ∈ R
f_in_cond : f✝ ∈ Rcond
f : Formula
f_in : f ∈ Y
⊢ evaluate M w f
Tactic:
apply w_LYRO
Proof state after:
case h.right.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f✝ : Formula
f_in_R : f✝ ∈ R
f_in_cond : f✝ ∈ Rcond
f : Formula
f_in : f ∈ Y
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case h.right.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f✝ : Formula
f_in_R : f✝ ∈ R
f_in_cond : f✝ ∈ Rcond
f : Formula
f_in : f ∈ Y
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inr.inr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ evaluate M w f
Tactic:
apply w_LYRO
Proof state after:
case mpr.intro.intro.inl.inr.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inr.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
Proof state after:
case mpr.intro.intro.inl.inr.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ (f ∈ L ∨ f ∈ R.diff Rcond ∨ f ∈ Y) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inr.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ (f ∈ L ∨ f ∈ R.diff Rcond ∨ f ∈ Y) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inl $ Or.inr $ Or.inl $ List.mem_diff_of_mem f_in_R f_notin_cond
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
apply w_LYRO
Proof state after:
case mpr.intro.intro.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
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.LRnegL φ) (L, R, O)
⊢ (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
φ : Formula
preconditionProof : [φ].Sublist L ∧ [~φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegL φ) (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
φ : Formula
preconditionProof : [φ].Sublist L ∧ [~φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegL φ) (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
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
⊢ ¬(M, w)⊨(L, R, O)
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
⊢ ¬(M, w)⊨(L, R, O)
Tactic:
intro hyp
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False
Tactic:
have := hyp φ
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False
Tactic:
have := hyp (~φ)
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False
Tactic:
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:
subst hC
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [~φ].Sublist L ∧ [φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegR φ) (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
φ : Formula
preconditionProof : [~φ].Sublist L ∧ [φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegR φ) (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
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
⊢ ¬(M, w)⊨(L, R, O)
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
⊢ ¬(M, w)⊨(L, R, O)
Tactic:
intro hyp
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False
Tactic:
have := hyp φ
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False
Tactic:
have := hyp (~φ)
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False
Tactic:
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
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
Tactic:
have := loadRuleTruth lrule W M w
Proof state after:
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)
this :
  evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          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
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)
this :
  evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress))
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
rw [disEval] at this
Proof state after:
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)
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci