Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof state before:
case action.action
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
id✝ : ActionId net✝
a✝ : reaction.val.actionSources.vars
h :
  (match Trigger.action a✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.action id✝ ≡ Trigger.action a✝
⊢ Activates exec (Reaction.Trigger.action id✝)

case timer.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
id✝ : TimerId net✝
t✝ : reaction.val.timers
h :
  (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.timer id✝ ≡ Trigger.timer t✝
⊢ Activates exec (Reaction.Trigger.timer id✝)

case startup.startup
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  (match Trigger.startup with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.startup ≡ Trigger.startup
⊢ Activates exec Reaction.Trigger.startup

case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
⊢ Activates exec Reaction.Trigger.shutdown
Tactic:
all_goals
  simp at h
  constructor
  cases equiv
  all_goals
    simp_all [actionIsPresent, portIsPresent, reactionInputs]
    try assumption
Proof state after:
no goals