Theorem: Execution.Executable.Triggers.iff_triggers_eq_true (Runtime/Execution/Triggers.lean)

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction ↔ Execution.Executable.triggers exec reaction = true
Tactic:
unfold triggers
State after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction ↔
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction ↔
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true
Tactic:
constructor
State after:
case mp
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction →
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true

case mpr
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true →
    Triggers exec reaction

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction →
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true
Tactic:
case mp =>
  intro ⟨equiv, mem, active⟩
  rw [Array.any_iff_mem_where]
  refine ⟨_, mem, ?_⟩
  exact Activates.iff_equiv_trigger_activated equiv |>.mp active
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true →
    Triggers exec reaction
Tactic:
case mpr =>
  intro h
  have ⟨t', mem, active⟩ := Array.any_iff_mem_where.mp h
  have ⟨_, equiv⟩ : ∃ t, t ≡ t' := ⟨_, Reaction.Trigger.Equiv.lift t'⟩
  refine .witness equiv mem ?_
  exact Activates.iff_equiv_trigger_activated equiv |>.mpr active
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction →
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true
Tactic:
intro ⟨equiv, mem, active⟩
State after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
Tactic:
rw [Array.any_iff_mem_where]
State after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ ∃ a, a ∈ reaction.val.triggers.data ∧ Execution.Executable.triggers.activated exec reaction a = true

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ ∃ a, a ∈ reaction.val.triggers.data ∧ Execution.Executable.triggers.activated exec reaction a = true
Tactic:
refine ⟨_, mem, ?_⟩
State after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Execution.Executable.triggers.activated exec reaction t'✝ = true

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Execution.Executable.triggers.activated exec reaction t'✝ = true
Tactic:
exact Activates.iff_equiv_trigger_activated equiv |>.mp active
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true →
    Triggers exec reaction
Tactic:
intro h
State after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
⊢ Triggers exec reaction

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
⊢ Triggers exec reaction
Tactic:
have ⟨t', mem, active⟩ := Array.any_iff_mem_where.mp h
State after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
⊢ Triggers exec reaction

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
⊢ Triggers exec reaction
Tactic:
have ⟨_, equiv⟩ : ∃ t, t ≡ t' := ⟨_, Reaction.Trigger.Equiv.lift t'⟩
State after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
w✝ : Reaction.Trigger net✝
equiv : w✝ ≡ t'
⊢ Triggers exec reaction

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
w✝ : Reaction.Trigger net✝
equiv : w✝ ≡ t'
⊢ Triggers exec reaction
Tactic:
refine .witness equiv mem ?_
State after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
w✝ : Reaction.Trigger net✝
equiv : w✝ ≡ t'
⊢ Activates exec w✝

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
w✝ : Reaction.Trigger net✝
equiv : w✝ ≡ t'
⊢ Activates exec w✝
Tactic:
exact Activates.iff_equiv_trigger_activated equiv |>.mpr active
State after:
no goals