Theorem: Execution.Executable.Next.for_tag_strictly_monotonic
Proof state before:
net : Network
next : Next net
exec : Executable net
h :
  (match h :
      nextTime
        { state := exec.state, tag := exec.tag,
          queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec), reactors := exec.reactors,
          physicalOffset := exec.physicalOffset, toPropagate := exec.toPropagate } with
    | none => none
    | some time =>
      some
        { tag := Tag.advance exec.tag time,
          events :=
            (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time.val
                (_ :
                  ∀
                    (x :
                      Time.From
                        { state := exec.state, tag := exec.tag,
                              queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                              reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                              toPropagate := exec.toPropagate }.tag.time),
                    Queue.nextTime
                          { state := exec.state, tag := exec.tag,
                              queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                              reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                              toPropagate := exec.toPropagate }.queue =
                        some x →
                      time ≤ x)).fst,
          queue :=
            (_ :
                time.val =
                  (Tag.advance
                      { state := exec.state, tag := exec.tag,
                          queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                          reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                          toPropagate := exec.toPropagate }.tag
                      time).time) ▸
              Queue.merge
                (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time.val
                    (_ :
                      ∀
                        (x :
                          Time.From
                            { state := exec.state, tag := exec.tag,
                                  queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                  reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                  toPropagate := exec.toPropagate }.tag.time),
                        Queue.nextTime
                              { state := exec.state, tag := exec.tag,
                                  queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                  reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                  toPropagate := exec.toPropagate }.queue =
                            some x →
                          time ≤ x)).snd
                (Execution.Executable.nextTimerEvents
                  { state := exec.state, tag := exec.tag,
                    queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                    reactors := exec.reactors, physicalOffset := exec.physicalOffset, toPropagate := exec.toPropagate }
                  (Array.filterMap (fun x => Event.timer? x)
                    (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time.val
                        (_ :
                          ∀
                            (x :
                              Time.From
                                { state := exec.state, tag := exec.tag,
                                      queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                      reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                      toPropagate := exec.toPropagate }.tag.time),
                            Queue.nextTime
                                  { state := exec.state, tag := exec.tag,
                                      queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                      reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                      toPropagate := exec.toPropagate }.queue =
                                some x →
                              time ≤ x)).fst
                    0
                    (Array.size
                      (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time.val
                          (_ :
                            ∀
                              (x :
                                Time.From
                                  { state := exec.state, tag := exec.tag,
                                        queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                        reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                        toPropagate := exec.toPropagate }.tag.time),
                              Queue.nextTime
                                    { state := exec.state, tag := exec.tag,
                                        queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                        reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                        toPropagate := exec.toPropagate }.queue =
                                  some x →
                                time ≤ x)).fst))
                  time.val) }) =
    some next
⊢ exec.tag < next.tag
Tactic:
split at h
Proof state after:
case h_1
net : Network
next : Next net
exec : Executable net
heq✝ :
  nextTime
      { state := exec.state, tag := exec.tag,
        queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec), reactors := exec.reactors,
        physicalOffset := exec.physicalOffset, toPropagate := exec.toPropagate } =
    none
h : none = some next
⊢ exec.tag < next.tag

case h_2
net : Network
next : Next net
exec : Executable net
time✝ :
  Time.From
    (time
      { state := exec.state, tag := exec.tag,
        queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec), reactors := exec.reactors,
        physicalOffset := exec.physicalOffset, toPropagate := exec.toPropagate })
heq✝ :
  nextTime
      { state := exec.state, tag := exec.tag,
        queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec), reactors := exec.reactors,
        physicalOffset := exec.physicalOffset, toPropagate := exec.toPropagate } =
    some time✝
h :
  some
      { tag := Tag.advance exec.tag time✝,
        events :=
          (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time✝.val
              (_ :
                ∀
                  (x :
                    Time.From
                      { state := exec.state, tag := exec.tag,
                            queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                            reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                            toPropagate := exec.toPropagate }.tag.time),
                  Queue.nextTime
                        { state := exec.state, tag := exec.tag,
                            queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                            reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                            toPropagate := exec.toPropagate }.queue =
                      some x →
                    time✝ ≤ x)).fst,
        queue :=
          (_ :
              time✝.val =
                (Tag.advance
                    { state := exec.state, tag := exec.tag,
                        queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                        reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                        toPropagate := exec.toPropagate }.tag
                    time✝).time) ▸
            Queue.merge
              (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time✝.val
                  (_ :
                    ∀
                      (x :
                        Time.From
                          { state := exec.state, tag := exec.tag,
                                queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                toPropagate := exec.toPropagate }.tag.time),
                      Queue.nextTime
                            { state := exec.state, tag := exec.tag,
                                queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                toPropagate := exec.toPropagate }.queue =
                          some x →
                        time✝ ≤ x)).snd
              (Execution.Executable.nextTimerEvents
                { state := exec.state, tag := exec.tag,
                  queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                  reactors := exec.reactors, physicalOffset := exec.physicalOffset, toPropagate := exec.toPropagate }
                (Array.filterMap (fun x => Event.timer? x)
                  (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time✝.val
                      (_ :
                        ∀
                          (x :
                            Time.From
                              { state := exec.state, tag := exec.tag,
                                    queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                    reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                    toPropagate := exec.toPropagate }.tag.time),
                          Queue.nextTime
                                { state := exec.state, tag := exec.tag,
                                    queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                    reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                    toPropagate := exec.toPropagate }.queue =
                              some x →
                            time✝ ≤ x)).fst
                  0
                  (Array.size
                    (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time✝.val
                        (_ :
                          ∀
                            (x :
                              Time.From
                                { state := exec.state, tag := exec.tag,
                                      queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                      reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                      toPropagate := exec.toPropagate }.tag.time),
                            Queue.nextTime
                                  { state := exec.state, tag := exec.tag,
                                      queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                      reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                      toPropagate := exec.toPropagate }.queue =
                                some x →
                              time✝ ≤ x)).fst))
                time✝.val) } =
    some next
⊢ exec.tag < next.tag