Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated (Runtime/Execution/Triggers.lean)

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
⊢ Reaction.Trigger.port p ≡ Trigger.port p' →
    (Activates exec (Reaction.Trigger.port p) ↔
      Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true)
Tactic:
intro he
State after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
⊢ Activates exec (Reaction.Trigger.port p) ↔
    Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
⊢ Activates exec (Reaction.Trigger.port p) ↔
    Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
Tactic:
constructor <;> intro h
State after:
case mp
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true

case mpr
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
⊢ Activates exec (Reaction.Trigger.port p)

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
Tactic:
case mp reactor =>
  simp only [triggers.activated, reactionInputs]
  cases hp : reaction.subPS.coe p'
  case inl loc =>
    simp
    cases he
    case input hi =>
      simp [hi] at hp
      cases h
      case port h =>
        simp [portIsPresent, hp] at h
        exact h
    case output ho =>
      rw [ho] at hp
      contradiction
  case inr sub =>
    have ⟨c, output⟩ := sub
    simp at output ⊢
    cases he
    case input hi =>
      rw [hi] at hp
      contradiction
    case output c' output' ho =>
      simp [ho] at hp
      injection hp with hc ho
      subst hc
      subst ho
      cases h
      case port h =>
        simp [portIsPresent] at h
        have ⟨v, hv⟩ := h
        exists cast sorry v
        simp [hv]
        sorry
State after:
no goals

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
⊢ Activates exec (Reaction.Trigger.port p)
Tactic:
case mpr =>
  sorry
State after:
no goals

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
Tactic:
simp only [triggers.activated, reactionInputs]
State after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Interface.Subscheme.coe p') =
    true

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Interface.Subscheme.coe p') =
    true
Tactic:
cases hp : reaction.subPS.coe p'
State after:
case inl
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
val✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl val✝
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inl val✝) =
    true

case inr
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
val✝ : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr val✝
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr val✝) =
    true

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inl loc) =
    true
Tactic:
case inl loc =>
  simp
  cases he
  case input hi =>
    simp [hi] at hp
    cases h
    case port h =>
      simp [portIsPresent, hp] at h
      exact h
  case output ho =>
    rw [ho] at hp
    contradiction
State after:
no goals

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr sub
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr sub) =
    true
Tactic:
case inr sub =>
  have ⟨c, output⟩ := sub
  simp at output ⊢
  cases he
  case input hi =>
    rw [hi] at hp
    contradiction
  case output c' output' ho =>
    simp [ho] at hp
    injection hp with hc ho
    subst hc
    subst ho
    cases h
    case port h =>
      simp [portIsPresent] at h
      have ⟨v, hv⟩ := h
      exists cast sorry v
      simp [hv]
      sorry
State after:
no goals

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inl loc) =
    true
Tactic:
simp
State after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
cases he
State after:
case input
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
a✝ : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v

case output
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
a✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
case input hi =>
  simp [hi] at hp
  cases h
  case port h =>
    simp [portIsPresent, hp] at h
    exact h
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
case output ho =>
  rw [ho] at hp
  contradiction
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
simp [hi] at hp
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
cases h
State after:
case port
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
a✝ : portIsPresent exec { reactor := reactor, port := input✝ } = true
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
h : portIsPresent exec { reactor := reactor, port := input✝ } = true
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
case port h =>
  simp [portIsPresent, hp] at h
  exact h
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
h : portIsPresent exec { reactor := reactor, port := input✝ } = true
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
simp [portIsPresent, hp] at h
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
h : ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
h : ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
exact h
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
rw [ho] at hp
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
hp : Sum.inr { fst := c✝, snd := output✝ } = Sum.inl loc
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
hp : Sum.inr { fst := c✝, snd := output✝ } = Sum.inl loc
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
contradiction
State after:
no goals

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr sub
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr sub) =
    true
Tactic:
have ⟨c, output⟩ := sub
State after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr { fst := c, snd := output }) =
    true

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr { fst := c, snd := output }) =
    true
Tactic:
simp at output ⊢
State after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
cases he
State after:
case input
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
a✝ : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v

case output
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
a✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
case input hi =>
  rw [hi] at hp
  contradiction
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
case output c' output' ho =>
  simp [ho] at hp
  injection hp with hc ho
  subst hc
  subst ho
  cases h
  case port h =>
    simp [portIsPresent] at h
    have ⟨v, hv⟩ := h
    exists cast sorry v
    simp [hv]
    sorry
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
rw [hi] at hp
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Sum.inl input✝ = Sum.inr { fst := c, snd := output }
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Sum.inl input✝ = Sum.inr { fst := c, snd := output }
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
contradiction
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
simp [ho] at hp
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
hp : { fst := c', snd := output' } = { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
hp : { fst := c', snd := output' } = { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
injection hp with hc ho
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
hc : c' = c
ho : HEq output' output
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
hc : c' = c
ho : HEq output' output
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
subst hc
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
output : (Class.interface (Child.class c') Reactor.InterfaceKind.outputs).vars
ho : HEq output' output
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output)) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
output : (Class.interface (Child.class c') Reactor.InterfaceKind.outputs).vars
ho : HEq output' output
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
subst ho
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
cases h
State after:
case port
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
a✝ : portIsPresent exec { reactor := Path.extend reactor c', port := cast _ output' } = true
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : portIsPresent exec { reactor := Path.extend reactor c', port := cast _ output' } = true
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
case port h =>
  simp [portIsPresent] at h
  have ⟨v, hv⟩ := h
  exists cast sorry v
  simp [hv]
  sorry
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : portIsPresent exec { reactor := Path.extend reactor c', port := cast _ output' } = true
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
simp [portIsPresent] at h
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
have ⟨v, hv⟩ := h
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
exists cast sorry v
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some (cast _ v)

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some (cast _ v)
Tactic:
simp [hv]
State after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ cast _ (some v) = some (cast _ v)

State before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ cast _ (some v) = some (cast _ v)
Tactic:
sorry
State after:
no goals

State before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
⊢ Activates exec (Reaction.Trigger.port p)
Tactic:
sorry
State after:
no goals