Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift (Runtime/Execution/Triggers.lean)

State before:
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t : Reaction.triggerType reaction.val
⊢ Trigger.lift t ≡ t
Tactic:
cases t
State after:
case startup
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.startup ≡ _root_.Trigger.startup

case shutdown
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.shutdown ≡ _root_.Trigger.shutdown

case port
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
⊢ Trigger.lift (_root_.Trigger.port p✝) ≡ _root_.Trigger.port p✝

case action
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
a✝ : reaction.val.actionSources.vars
⊢ Trigger.lift (_root_.Trigger.action a✝) ≡ _root_.Trigger.action a✝

case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.lift (_root_.Trigger.timer t✝) ≡ _root_.Trigger.timer t✝

State before:
case startup
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.startup ≡ _root_.Trigger.startup

case shutdown
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.shutdown ≡ _root_.Trigger.shutdown

case port
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
⊢ Trigger.lift (_root_.Trigger.port p✝) ≡ _root_.Trigger.port p✝

case action
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
a✝ : reaction.val.actionSources.vars
⊢ Trigger.lift (_root_.Trigger.action a✝) ≡ _root_.Trigger.action a✝

case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.lift (_root_.Trigger.timer t✝) ≡ _root_.Trigger.timer t✝
Tactic:
all_goals
  simp [Trigger.lift]
  first
  | constructor
  | split <;> (constructor; assumption)
State after:
no goals

State before:
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.lift (_root_.Trigger.timer t✝) ≡ _root_.Trigger.timer t✝
Tactic:
simp [Trigger.lift]
State after:
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.timer { reactor := reactor, timer := (_ : reaction.val.timers = timers (Path.class reactor)) ▸ t✝ } ≡
    _root_.Trigger.timer t✝

State before:
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.timer { reactor := reactor, timer := (_ : reaction.val.timers = timers (Path.class reactor)) ▸ t✝ } ≡
    _root_.Trigger.timer t✝
Tactic:
first
| constructor
| split <;> (constructor; assumption)
State after:
no goals

State before:
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.timer { reactor := reactor, timer := (_ : reaction.val.timers = timers (Path.class reactor)) ▸ t✝ } ≡
    _root_.Trigger.timer t✝
Tactic:
constructor
State after:
no goals

State before:
case port
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
⊢ (match Interface.Subscheme.coe p✝ with
    | Sum.inl input => port { reactor := reactor, port := input }
    | Sum.inr { fst := c, snd := output } =>
      port
        { reactor := Path.extend reactor c,
          port :=
            cast
              (_ :
                ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c).vars =
                  (interface (Path.class (Path.extend reactor c))
                      (match Reactor.PortKind.output with
                      | Reactor.PortKind.input => Reactor.InterfaceKind.inputs
                      | Reactor.PortKind.output => Reactor.InterfaceKind.outputs)).vars)
              output }) ≡
    _root_.Trigger.port p✝
Tactic:
split <;> (constructor; assumption)
State after:
no goals

State before:
case port.h_2
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
x✝ : (reactionInputScheme (Path.class reactor)).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
heq✝ : Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
⊢ port
      { reactor := Path.extend reactor c✝,
        port :=
          cast
            (_ :
              ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars =
                (interface (Path.class (Path.extend reactor c✝))
                    (match Reactor.PortKind.output with
                    | Reactor.PortKind.input => Reactor.InterfaceKind.inputs
                    | Reactor.PortKind.output => Reactor.InterfaceKind.outputs)).vars)
            output✝ } ≡
    _root_.Trigger.port p✝
Tactic:
constructor
State after:
case port.h_2.a
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
x✝ : (reactionInputScheme (Path.class reactor)).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
heq✝ : Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
⊢ Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }

State before:
case port.h_2.a
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
x✝ : (reactionInputScheme (Path.class reactor)).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
heq✝ : Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
⊢ Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
Tactic:
assumption
State after:
no goals