Theorem: bigDis_sat (Bml/bigConDis.lean)

State before:
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigDis l) ↔ ∃ φ ∈ l, Evaluate (M, w) φ
Tactic:
constructor
State after:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigDis l) → ∃ φ ∈ l, Evaluate (M, w) φ

case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ (∃ φ ∈ l, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis l)

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
State after:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis l)
⊢ ∃ φ ∈ l, Evaluate (M, w) φ

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
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) φ

State before:
W : Type
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis [])
⊢ ∃ φ ∈ [], Evaluate (M, w) φ
Tactic:
case nil => tauto
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis [])
⊢ ∃ φ ∈ [], Evaluate (M, w) φ
Tactic:
tauto
State after:
no goals

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)
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) φ

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
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

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
State after:
no goals

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
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) φ

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
State after:
no goals

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
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)

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
State after:
no goals

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
State after:
case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
satOne : ∃ φ ∈ l, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis l)

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
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✝))

State before:
W : Type
M : KripkeModel W
w : W
satOne : ∃ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis [])
Tactic:
case nil => tauto
State after:
no goals

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
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
satOne : ∃ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis [])
Tactic:
tauto
State after:
no goals

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
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))

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
State after:
no goals

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
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)

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
State after:
no goals