Theorem: Execution.Step.Exec.indep_triggers_iff (ReactorModel/Execution/Theorems/Step/Exec.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
⊢ Triggers s₁ i ↔ Triggers s₂ i
Tactic:
constructor <;> intro ⟨ho, ht⟩
State after:
case mp
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₂ i

case mpr
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₁ i

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₂ i
Tactic:
case mp =>
  have ho' := Equivalent.obj?_rcn_eq e.equiv ▸ ho
  have ht' := e.indep_input_eq hi.symm ‹_› ‹_› ▸ ht
  exact ⟨ho', ht'⟩
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₁ i
Tactic:
case mpr =>
  have ho' := Equivalent.obj?_rcn_eq e.equiv |>.symm ▸ ho
  have ht' := e.indep_input_eq hi.symm ‹_› ‹_› |>.symm ▸ ht
  exact ⟨ho', ht'⟩
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₂ i
Tactic:
have ho' := Equivalent.obj?_rcn_eq e.equiv ▸ ho
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
⊢ Triggers s₂ i

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
⊢ Triggers s₂ i
Tactic:
have ht' := e.indep_input_eq hi.symm ‹_› ‹_› ▸ ht
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₂ i

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₂ i
Tactic:
exact ⟨ho', ht'⟩
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₁ i
Tactic:
have ho' := Equivalent.obj?_rcn_eq e.equiv |>.symm ▸ ho
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
ho' : s₁.rtr[Component.rcn][i] = some rcn✝
⊢ Triggers s₁ i

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
ho' : s₁.rtr[Component.rcn][i] = some rcn✝
⊢ Triggers s₁ i
Tactic:
have ht' := e.indep_input_eq hi.symm ‹_› ‹_› |>.symm ▸ ht
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
ho' : s₁.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₁ i

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
ho' : s₁.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₁ i
Tactic:
exact ⟨ho', ht'⟩
State after:
no goals