internlm/Lean-Github huggingface dataset:
Theorem: bigDis_sat
Proof state before:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigDis l) → ∃ φ ∈ l, Evaluate (M, w) φ
Tactic:
intro satDis
Proof state after:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis l)
⊢ ∃ φ ∈ l, Evaluate (M, w) φ
Theorem: bigDis_sat
Proof state before:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis l)
⊢ ∃ φ ∈ l, Evaluate (M, w) φ
Tactic:
induction l
Proof state after:
case mp.nil
W : Type
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis [])
⊢ ∃ φ ∈ [], Evaluate (M, w) φ

case mp.cons
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : Evaluate (M, w) (bigDis tail✝) → ∃ φ ∈ tail✝, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head✝ :: tail✝))
⊢ ∃ φ ∈ head✝ :: tail✝, Evaluate (M, w) φ
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis [])
⊢ ∃ φ ∈ [], Evaluate (M, w) φ
Tactic:
case nil => tauto
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis [])
⊢ ∃ φ ∈ [], Evaluate (M, w) φ
Tactic:
tauto
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
⊢ ∃ φ ∈ head :: tail, Evaluate (M, w) φ
Tactic:
cases em (Evaluate (M, w) head)
Proof state after:
case inl
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : Evaluate (M, w) head
⊢ ∃ φ ∈ head :: tail, Evaluate (M, w) φ

case inr
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : ¬Evaluate (M, w) head
⊢ ∃ φ ∈ head :: tail, Evaluate (M, w) φ
Theorem: bigDis_sat
Proof state before:
case inl
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : Evaluate (M, w) head
⊢ ∃ φ ∈ head :: tail, Evaluate (M, w) φ
Tactic:
use head
Proof state after:
case h
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : Evaluate (M, w) head
⊢ head ∈ head :: tail ∧ Evaluate (M, w) head
Theorem: bigDis_sat
Proof state before:
case h
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : Evaluate (M, w) head
⊢ head ∈ head :: tail ∧ Evaluate (M, w) head
Tactic:
aesop
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
case inr
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : ¬Evaluate (M, w) head
⊢ ∃ φ ∈ head :: tail, Evaluate (M, w) φ
Tactic:
have : ((Evaluate (M, w) head) ∨ Evaluate (M, w) (bigDis tail)) :=
  by unfold bigDis; aesop
Proof state after:
case inr
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : ¬Evaluate (M, w) head
this : Evaluate (M, w) head ∨ Evaluate (M, w) (bigDis tail)
⊢ ∃ φ ∈ head :: tail, Evaluate (M, w) φ
Theorem: bigDis_sat
Proof state before:
case inr
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : ¬Evaluate (M, w) head
this : Evaluate (M, w) head ∨ Evaluate (M, w) (bigDis tail)
⊢ ∃ φ ∈ head :: tail, Evaluate (M, w) φ
Tactic:
aesop
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : ¬Evaluate (M, w) head
⊢ Evaluate (M, w) head ∨ Evaluate (M, w) (bigDis tail)
Tactic:
unfold bigDis
Proof state after:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : ¬Evaluate (M, w) head
⊢ Evaluate (M, w) head ∨
    Evaluate (M, w)
      (match tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest)
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : ¬Evaluate (M, w) head
⊢ Evaluate (M, w) head ∨
    Evaluate (M, w)
      (match tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest)
Tactic:
aesop
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ (∃ φ ∈ l, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis l)
Tactic:
intro satOne
Proof state after:
case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
satOne : ∃ φ ∈ l, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis l)
Theorem: bigDis_sat
Proof state before:
case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
satOne : ∃ φ ∈ l, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis l)
Tactic:
induction l
Proof state after:
case mpr.nil
W : Type
M : KripkeModel W
w : W
satOne : ∃ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis [])

case mpr.cons
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : (∃ φ ∈ tail✝, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail✝)
satOne : ∃ φ ∈ head✝ :: tail✝, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis (head✝ :: tail✝))
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
satOne : ∃ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis [])
Tactic:
case nil => tauto
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis (head :: tail))
Tactic:
case cons head tail ih =>
  have : Evaluate (M, w) (bigDis (head :: tail)) ↔
    ((Evaluate (M, w) head) ∨ Evaluate (M, w) (bigDis tail)) :=
    by unfold bigDis; aesop
  aesop
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
satOne : ∃ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis [])
Tactic:
tauto
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis (head :: tail))
Tactic:
have : Evaluate (M, w) (bigDis (head :: tail)) ↔
  ((Evaluate (M, w) head) ∨ Evaluate (M, w) (bigDis tail)) :=
  by unfold bigDis; aesop
Proof state after:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
this : Evaluate (M, w) (bigDis (head :: tail)) ↔ Evaluate (M, w) head ∨ Evaluate (M, w) (bigDis tail)
⊢ Evaluate (M, w) (bigDis (head :: tail))
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
this : Evaluate (M, w) (bigDis (head :: tail)) ↔ Evaluate (M, w) head ∨ Evaluate (M, w) (bigDis tail)
⊢ Evaluate (M, w) (bigDis (head :: tail))
Tactic:
aesop
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis (head :: tail)) ↔ Evaluate (M, w) head ∨ Evaluate (M, w) (bigDis tail)
Tactic:
unfold bigDis
Proof state after:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w)
      (match head :: tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest) ↔
    Evaluate (M, w) head ∨
      Evaluate (M, w)
        (match tail with
        | [] => ⊥
        | [f] => f
        | f :: rest => f⋁bigDis rest)
Theorem: bigDis_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w)
      (match head :: tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest) ↔
    Evaluate (M, w) head ∨
      Evaluate (M, w)
        (match tail with
        | [] => ⊥
        | [f] => f
        | f :: rest => f⋁bigDis rest)
Tactic:
aesop
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigCon l) ↔ ∀ φ ∈ l, Evaluate (M, w) φ
Tactic:
constructor
Proof state after:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigCon l) → ∀ φ ∈ l, Evaluate (M, w) φ

case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ (∀ φ ∈ l, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon l)
Theorem: bigCon_sat
Proof state before:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigCon l) → ∀ φ ∈ l, Evaluate (M, w) φ
Tactic:
intro satCon
Proof state after:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
satCon : Evaluate (M, w) (bigCon l)
⊢ ∀ φ ∈ l, Evaluate (M, w) φ
Theorem: bigCon_sat
Proof state before:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
satCon : Evaluate (M, w) (bigCon l)
⊢ ∀ φ ∈ l, Evaluate (M, w) φ
Tactic:
induction l
Proof state after:
case mp.nil
W : Type
M : KripkeModel W
w : W
satCon : Evaluate (M, w) (bigCon [])
⊢ ∀ φ ∈ [], Evaluate (M, w) φ

case mp.cons
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : Evaluate (M, w) (bigCon tail✝) → ∀ φ ∈ tail✝, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head✝ :: tail✝))
⊢ ∀ φ ∈ head✝ :: tail✝, Evaluate (M, w) φ
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
satCon : Evaluate (M, w) (bigCon [])
⊢ ∀ φ ∈ [], Evaluate (M, w) φ
Tactic:
case nil => tauto
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
⊢ ∀ φ ∈ head :: tail, Evaluate (M, w) φ
Tactic:
case cons head tail ih =>
  have : ((Evaluate (M, w) head) ∧ Evaluate (M, w) (bigCon tail)) :=
    by unfold bigCon; aesop
  aesop
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
satCon : Evaluate (M, w) (bigCon [])
⊢ ∀ φ ∈ [], Evaluate (M, w) φ
Tactic:
tauto
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
⊢ ∀ φ ∈ head :: tail, Evaluate (M, w) φ
Tactic:
have : ((Evaluate (M, w) head) ∧ Evaluate (M, w) (bigCon tail)) :=
  by unfold bigCon; aesop
Proof state after:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
this : Evaluate (M, w) head ∧ Evaluate (M, w) (bigCon tail)
⊢ ∀ φ ∈ head :: tail, Evaluate (M, w) φ
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
this : Evaluate (M, w) head ∧ Evaluate (M, w) (bigCon tail)
⊢ ∀ φ ∈ head :: tail, Evaluate (M, w) φ
Tactic:
aesop
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
⊢ Evaluate (M, w) head ∧ Evaluate (M, w) (bigCon tail)
Tactic:
unfold bigCon
Proof state after:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
⊢ Evaluate (M, w) head ∧
    Evaluate (M, w)
      (match tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest)
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
⊢ Evaluate (M, w) head ∧
    Evaluate (M, w)
      (match tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest)
Tactic:
aesop
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ (∀ φ ∈ l, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon l)
Tactic:
intro satAll
Proof state after:
case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
satAll : ∀ φ ∈ l, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon l)
Theorem: bigCon_sat
Proof state before:
case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
satAll : ∀ φ ∈ l, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon l)
Tactic:
induction l
Proof state after:
case mpr.nil
W : Type
M : KripkeModel W
w : W
satAll : ∀ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon [])

case mpr.cons
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : (∀ φ ∈ tail✝, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail✝)
satAll : ∀ φ ∈ head✝ :: tail✝, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon (head✝ :: tail✝))
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
satAll : ∀ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon [])
Tactic:
case nil => tauto
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∀ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail)
satAll : ∀ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon (head :: tail))
Tactic:
case cons head tail ih =>
  have : Evaluate (M, w) (bigCon (head :: tail)) ↔
    ((Evaluate (M, w) head) ∧ Evaluate (M, w) (bigCon tail)) :=
    by unfold bigCon; aesop
  aesop
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
satAll : ∀ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon [])
Tactic:
tauto
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∀ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail)
satAll : ∀ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon (head :: tail))
Tactic:
have : Evaluate (M, w) (bigCon (head :: tail)) ↔
  ((Evaluate (M, w) head) ∧ Evaluate (M, w) (bigCon tail)) :=
  by unfold bigCon; aesop
Proof state after:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∀ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail)
satAll : ∀ φ ∈ head :: tail, Evaluate (M, w) φ
this : Evaluate (M, w) (bigCon (head :: tail)) ↔ Evaluate (M, w) head ∧ Evaluate (M, w) (bigCon tail)
⊢ Evaluate (M, w) (bigCon (head :: tail))
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∀ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail)
satAll : ∀ φ ∈ head :: tail, Evaluate (M, w) φ
this : Evaluate (M, w) (bigCon (head :: tail)) ↔ Evaluate (M, w) head ∧ Evaluate (M, w) (bigCon tail)
⊢ Evaluate (M, w) (bigCon (head :: tail))
Tactic:
aesop
Proof state after:
no goals
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∀ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail)
satAll : ∀ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon (head :: tail)) ↔ Evaluate (M, w) head ∧ Evaluate (M, w) (bigCon tail)
Tactic:
unfold bigCon
Proof state after:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∀ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail)
satAll : ∀ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w)
      (match head :: tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest) ↔
    Evaluate (M, w) head ∧
      Evaluate (M, w)
        (match tail with
        | [] => ⊤
        | [f] => f
        | f :: rest => f⋀bigCon rest)
Theorem: bigCon_sat
Proof state before:
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∀ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail)
satAll : ∀ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w)
      (match head :: tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest) ↔
    Evaluate (M, w) head ∧
      Evaluate (M, w)
        (match tail with
        | [] => ⊤
        | [f] => f
        | f :: rest => f⋀bigCon rest)
Tactic:
aesop
Proof state after:
no goals
Theorem: bigDis_union_sat_down
Proof state before:
X : Finset Formula
l : List Formula
⊢ Satisfiable (X ∪ {bigDis l}) → ∃ φ ∈ l, Satisfiable (X ∪ {φ})
Tactic:
simp at *
Proof state after:
X : Finset Formula
l : List Formula
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x),
    ∀ x_3 ∈ l,
      Evaluate (x_1, x_2) x_3 →
        (∀ a ∈ X, Evaluate (x_1, x_2) a) → ∃ φ ∈ l, ∃ W M w, Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Theorem: bigDis_union_sat_down
Proof state before:
X : Finset Formula
l : List Formula
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x),
    ∀ x_3 ∈ l,
      Evaluate (x_1, x_2) x_3 →
        (∀ a ∈ X, Evaluate (x_1, x_2) a) → ∃ φ ∈ l, ∃ W M w, Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
tauto
Proof state after:
no goals
Theorem: bigCon_union_sat_down
Proof state before:
X : Finset Formula
l : List Formula
⊢ Satisfiable (X ∪ {bigCon l}) → ∀ φ ∈ l, Satisfiable (X ∪ {φ})
Tactic:
simp at *
Proof state after:
X : Finset Formula
l : List Formula
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x),
    (∀ φ ∈ l, Evaluate (x_1, x_2) φ) →
      (∀ a ∈ X, Evaluate (x_1, x_2) a) → ∀ φ ∈ l, ∃ W M w, Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Theorem: bigCon_union_sat_down
Proof state before:
X : Finset Formula
l : List Formula
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x),
    (∀ φ ∈ l, Evaluate (x_1, x_2) φ) →
      (∀ a ∈ X, Evaluate (x_1, x_2) a) → ∀ φ ∈ l, ∃ W M w, Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
tauto
Proof state after:
no goals
Theorem: bigConNeg_union_sat_down
Proof state before:
X : Finset Formula
l : List Formula
⊢ Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)}) → ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
Tactic:
intro hyp
Proof state after:
X : Finset Formula
l : List Formula
hyp : Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)})
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
Theorem: bigConNeg_union_sat_down
Proof state before:
X : Finset Formula
l : List Formula
hyp : Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)})
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
Tactic:
rcases hyp with ⟨W, M, w, sat⟩
Proof state after:
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : ∀ φ ∈ X ∪ {bigCon (List.map (fun x => ~x) l)}, Evaluate (M, w) φ
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
Theorem: bigConNeg_union_sat_down
Proof state before:
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : ∀ φ ∈ X ∪ {bigCon (List.map (fun x => ~x) l)}, Evaluate (M, w) φ
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
Tactic:
simp at *
Proof state after:
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : (∀ a ∈ l, ¬Evaluate (M, w) a) ∧ ∀ a ∈ X, Evaluate (M, w) a
⊢ ∀ φ ∈ l, ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Theorem: bigConNeg_union_sat_down
Proof state before:
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : (∀ a ∈ l, ¬Evaluate (M, w) a) ∧ ∀ a ∈ X, Evaluate (M, w) a
⊢ ∀ φ ∈ l, ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
cases' sat with lNotSat XSat
Proof state after:
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
⊢ ∀ φ ∈ l, ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Theorem: bigConNeg_union_sat_down
Proof state before:
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
⊢ ∀ φ ∈ l, ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
intro φ inl
Proof state after:
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Theorem: bigConNeg_union_sat_down
Proof state before:
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
use W, M, w
Proof state after:
case h
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Theorem: bigConNeg_union_sat_down
Proof state before:
case h
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
apply And.intro (lNotSat φ inl) (XSat)
Proof state after:
no goals
Theorem: eval_neg_BigDis_iff_eval_bigConNeg
Proof state before:
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (~bigDis l) ↔ Evaluate (M, w) (~~bigCon (List.map (fun x => ~x) l))
Tactic:
aesop
Proof state after:
no goals
Theorem: eval_negBigCon_iff_eval_bigDisNeg
Proof state before:
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (~bigCon l) ↔ Evaluate (M, w) (bigDis (List.map (fun x => ~x) l))
Tactic:
aesop
Proof state after:
no goals
Theorem: sat_negBigDis_iff_sat_bigConNeg
Proof state before:
l : List Formula
⊢ Satisfiable (~bigDis l) ↔ Satisfiable (~~bigCon (List.map (fun x => ~x) l))
Tactic:
aesop
Proof state after:
no goals
Theorem: sat_negBigCon_iff_sat_bigDisNeg
Proof state before:
l : List Formula
⊢ Satisfiable (~bigCon l) ↔ Satisfiable (bigDis (List.map (fun x => ~x) l))
Tactic:
aesop
Proof state after:
no goals
Theorem: mytaut1
Proof state before:
p : Char
⊢ Tautology ((·p)↣·p)
Tactic:
unfold Tautology Evaluate
Proof state after:
p : Char
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    match (M, w), (·p)↣·p with
    | (fst, snd), Formula.bottom => False
    | (M, w), ·p => M.val w p
    | (M, w), ~φ => ¬Evaluate (M, w) φ
    | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
    | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ