Theorem: Execution.Executable.nextTime_le_queue_nextTime (Runtime/Execution/Next.lean)

State before:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
⊢ nextTime exec = some t → Queue.nextTime exec.queue = some q → t ≤ q
Tactic:
intro ht hq
State after:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht : nextTime exec = some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q

State before:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht : nextTime exec = some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q
Tactic:
simp [nextTime] at ht
State after:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht :
  (match exec.state with
    | State.shuttingDown => none
    | State.shutdownPending =>
      some
        { val := time exec,
          property :=
            (_ :
              Nat.Linear.ExprCnstr.denote [(time exec).ns]
                { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) }
    | State.executing => Queue.nextTime exec.queue) =
    some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q

State before:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht :
  (match exec.state with
    | State.shuttingDown => none
    | State.shutdownPending =>
      some
        { val := time exec,
          property :=
            (_ :
              Nat.Linear.ExprCnstr.denote [(time exec).ns]
                { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) }
    | State.executing => Queue.nextTime exec.queue) =
    some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q
Tactic:
split at ht <;> simp_all
State after:
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } =
    t
⊢ t ≤ q

State before:
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } =
    t
⊢ t ≤ q
Tactic:
simp [←ht]
State after:
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } =
    t
⊢ { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } ≤
    q

State before:
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } =
    t
⊢ { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } ≤
    q
Tactic:
exact q.property
State after:
no goals