internlm/Lean-Github huggingface dataset:
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 χ) ↔
    ∃
      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
Tactic:
subst hC
Proof state after:
W : Type
L R : List Formula
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
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 ∈ applyLocalRule (LocalRule.loadedL χ lrule) (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
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
preconditionProof : ∅.Sublist L ∧ ∅.Sublist R ∧ some (Sum.inl (~'χ)) ⊆ 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 ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, O), (M, w)⊨Ci
Tactic:
simp at preconditionProof
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
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
preconditionProof : some (Sum.inl (~'χ)) = O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (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
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
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
preconditionProof : some (Sum.inl (~'χ)) = O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, O), (M, w)⊨Ci
Tactic:
subst preconditionProof
Proof state after:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
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, some (Sum.inl (~'χ))) ↔
    ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, some (Sum.inl (~'χ))), (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
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, some (Sum.inl (~'χ))) ↔
    ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, some (Sum.inl (~'χ))), (M, w)⊨Ci
Tactic:
simp [modelCanSemImplyForm,modelCanSemImplyLLO] at *
Proof state after:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) ↔
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) ↔
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci
Tactic:
constructor
Proof state after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) →
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci

case mpr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci) →
    ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) →
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci
Tactic:
intro hyp
Proof state after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
have hyp' := hyp (~unload χ)
Proof state after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ((~unload χ) ∈ L ∨ (~unload χ) ∈ R) ∨ (~unload χ) = (~unload χ) → evaluate M w (~unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ((~unload χ) ∈ L ∨ (~unload χ) ∈ R) ∨ (~unload χ) = (~unload χ) → evaluate M w (~unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
simp at hyp'
Proof state after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ¬evaluate M w (unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ¬evaluate M w (unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
rw [this] at hyp'
Proof state after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
rcases hyp' with ⟨f, ⟨X , O, in_ress, def_f⟩, w_f⟩
Proof state after:
case mp.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_f : Con (X ++ (Option.map negUnload O).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
case mp.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_f : Con (X ++ (Option.map negUnload O).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
cases O
Proof state after:
case mp.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

case mp.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val✝)).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
case mp.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
use (L ++ X, R, some (Sum.inl (~'χ)))
Proof state after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl (~'χ)))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
Theorem: localRuleTruth
Proof state before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl (~'χ)))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
Tactic:
constructor
Proof state after:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inl b with
        | none => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
        (L ++ X, R, some (Sum.inl (~'χ)))

case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
Theorem: localRuleTruth
Proof state before:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inl b with
        | none => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
        (L ++ X, R, some (Sum.inl (~'χ)))
Tactic:
use X, none
Proof state after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (X, none) ∈ ress ∧
    (match Option.map Sum.inl none with
      | none => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
      (L ++ X, R, some (Sum.inl (~'χ)))