Theorem: Queue.merge_mem₂ (Runtime/Utilities/Queue.lean)

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
⊢ event ∈ queue₂ → event ∈ merge queue₁ queue₂
Tactic:
intro h
State after:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈ merge queue₁ queue₂

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈ merge queue₁ queue₂
Tactic:
simp [merge]
State after:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈
    if isEmpty queue₁ = true then queue₂
    else
      if isEmpty queue₂ = true then queue₁
      else
        {
          events :=
            merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
              merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                (Array.split queue₂.events fun x => decide (time x = bound)).snd,
          sorted :=
            (_ :
              Sorted
                (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
          bounded :=
            (_ :
              ∀ {event : ε},
                (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                          (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                        merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                          (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                    some event →
                  bound ≤ time event) }

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈
    if isEmpty queue₁ = true then queue₂
    else
      if isEmpty queue₂ = true then queue₁
      else
        {
          events :=
            merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
              merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                (Array.split queue₂.events fun x => decide (time x = bound)).snd,
          sorted :=
            (_ :
              Sorted
                (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
          bounded :=
            (_ :
              ∀ {event : ε},
                (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                          (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                        merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                          (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                    some event →
                  bound ≤ time event) }
Tactic:
split <;> try split
State after:
case inl
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : isEmpty queue₁ = true
⊢ event ∈ queue₂

case inr.inl
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : isEmpty queue₂ = true
⊢ event ∈ queue₁

case inr.inr
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : isEmpty queue₁ = true
⊢ event ∈ queue₂
Tactic:
case inl => exact h
State after:
no goals

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : isEmpty queue₂ = true
⊢ event ∈ queue₁
Tactic:
case inr.inl he =>
  rw [isEmpty, Array.isEmpty_iff_data_eq_nil] at he
  simp [Membership.mem, he] at h
  contradiction
State after:
no goals

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
case inr.inr =>
  by_cases time event = bound
  case inl ht =>
    sorry
  case inr ht =>
    sorry
State after:
no goals

State before:
case inr
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
⊢ event ∈
    if isEmpty queue₂ = true then queue₁
    else
      {
        events :=
          merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
              (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
            merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
              (Array.split queue₂.events fun x => decide (time x = bound)).snd,
        sorted :=
          (_ :
            Sorted
              (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                    (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                  merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                    (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
        bounded :=
          (_ :
            ∀ {event : ε},
              (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                        (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                      merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                        (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                  some event →
                bound ≤ time event) }
Tactic:
split
State after:
case inr.inl
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : isEmpty queue₂ = true
⊢ event ∈ queue₁

case inr.inr
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : isEmpty queue₁ = true
⊢ event ∈ queue₂
Tactic:
exact h
State after:
no goals

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : isEmpty queue₂ = true
⊢ event ∈ queue₁
Tactic:
rw [isEmpty, Array.isEmpty_iff_data_eq_nil] at he
State after:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
⊢ event ∈ queue₁

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
⊢ event ∈ queue₁
Tactic:
simp [Membership.mem, he] at h
State after:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
h : List.Mem event []
⊢ event ∈ queue₁

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
h : List.Mem event []
⊢ event ∈ queue₁
Tactic:
contradiction
State after:
no goals

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
by_cases time event = bound
State after:
case inl
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝² : ¬isEmpty queue₁ = true
h✝¹ : ¬isEmpty queue₂ = true
h✝ : time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }

case inr
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝² : ¬isEmpty queue₁ = true
h✝¹ : ¬isEmpty queue₂ = true
h✝ : ¬time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
ht : time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
case inl ht =>
  sorry
State after:
no goals

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
ht : ¬time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
case inr ht =>
  sorry
State after:
no goals

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
ht : time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
sorry
State after:
no goals

State before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
ht : ¬time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
sorry
State after:
no goals