Theorem: Dependency.equiv (ReactorModel/Execution/Theorems/Dependency.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
d : j₁ <[rtr₂] j₂
⊢ j₁ <[rtr₁] j₂
Tactic:
induction d with
| prio h₁ h₂ h₃ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  exact prio h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
| depOverlap h₁ h₂ =>
  exact depOverlap (e.obj?_rcn_eq.symm ▸ h₁) (e.obj?_rcn_eq.symm ▸ h₂) ‹_› ‹_› ‹_›
| mutNorm h₁ h₂ h₃ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  exact mutNorm h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
| mutNest h₁ h₂ h₃ _ h₄ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  have ⟨_, h₂'⟩ := get?_some_iff e (cpt := .rtr) |>.mpr ⟨_, h₂⟩
  have h₄' := mem_get?_iff (get?_rtr_some_equiv e h₂' h₂) (cpt := .rcn) |>.mpr h₄
  exact mutNest h₁' h₂' (get?_rcn_eq e ▸ h₃) ‹_› h₄'
| trans _ _ d₁ d₂ =>
  exact trans d₁ d₂
State after:
no goals

State before:
case prio
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
i₁✝ : ID
rcn₁✝ : Component.type (Component.type α Component.rtr) Component.rcn
i₂✝ : ID
rcn₂✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{i₁✝} = some rcn₁✝
h₃ : con✝{Component.rcn}{i₂✝} = some rcn₂✝
a✝¹ : Reaction.Mutates rcn₁✝ ↔ Reaction.Mutates rcn₂✝
a✝ : rcn₁✝.prio > rcn₂✝.prio
⊢ i₁✝ <[rtr₁] i₂✝
Tactic:
have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
State after:
case prio
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
i₁✝ : ID
rcn₁✝ : Component.type (Component.type α Component.rtr) Component.rcn
i₂✝ : ID
rcn₂✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{i₁✝} = some rcn₁✝
h₃ : con✝{Component.rcn}{i₂✝} = some rcn₂✝
a✝¹ : Reaction.Mutates rcn₁✝ ↔ Reaction.Mutates rcn₂✝
a✝ : rcn₁✝.prio > rcn₂✝.prio
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ i₁✝ <[rtr₁] i₂✝

State before:
case prio
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
i₁✝ : ID
rcn₁✝ : Component.type (Component.type α Component.rtr) Component.rcn
i₂✝ : ID
rcn₂✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{i₁✝} = some rcn₁✝
h₃ : con✝{Component.rcn}{i₂✝} = some rcn₂✝
a✝¹ : Reaction.Mutates rcn₁✝ ↔ Reaction.Mutates rcn₂✝
a✝ : rcn₁✝.prio > rcn₂✝.prio
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ i₁✝ <[rtr₁] i₂✝
Tactic:
exact prio h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
State after:
no goals

State before:
case depOverlap
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i₁✝ : Component.idType Component.rcn
rcn₁✝ : Component.type α Component.rcn
i₂✝ : Component.idType Component.rcn
rcn₂✝ : Component.type α Component.rcn
d✝ : Reaction.Dependency
h₁ : rtr₂[Component.rcn][i₁✝] = some rcn₁✝
h₂ : rtr₂[Component.rcn][i₂✝] = some rcn₂✝
a✝² : d✝ ∈ rcn₁✝.deps Kind.out
a✝¹ : d✝ ∈ rcn₂✝.deps Kind.in
a✝ : d✝.cpt ≠ Component.Valued.stv
⊢ i₁✝ <[rtr₁] i₂✝
Tactic:
exact depOverlap (e.obj?_rcn_eq.symm ▸ h₁) (e.obj?_rcn_eq.symm ▸ h₂) ‹_› ‹_› ‹_›
State after:
no goals

State before:
case mutNorm
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iₙ✝ : ID
n✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{iₘ✝} = some m✝
h₃ : con✝{Component.rcn}{iₙ✝} = some n✝
a✝¹ : Reaction.Mutates m✝
a✝ : Reaction.Normal n✝
⊢ iₘ✝ <[rtr₁] iₙ✝
Tactic:
have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
State after:
case mutNorm
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iₙ✝ : ID
n✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{iₘ✝} = some m✝
h₃ : con✝{Component.rcn}{iₙ✝} = some n✝
a✝¹ : Reaction.Mutates m✝
a✝ : Reaction.Normal n✝
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ iₘ✝ <[rtr₁] iₙ✝

State before:
case mutNorm
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iₙ✝ : ID
n✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{iₘ✝} = some m✝
h₃ : con✝{Component.rcn}{iₙ✝} = some n✝
a✝¹ : Reaction.Mutates m✝
a✝ : Reaction.Normal n✝
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ iₘ✝ <[rtr₁] iₙ✝
Tactic:
exact mutNorm h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
State after:
no goals

State before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
⊢ iₘ✝ <[rtr₁] iᵣ✝
Tactic:
have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
State after:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ rtr₁✝
⊢ iₘ✝ <[rtr₁] iᵣ✝

State before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ rtr₁✝
⊢ iₘ✝ <[rtr₁] iᵣ✝
Tactic:
have ⟨_, h₂'⟩ := get?_some_iff e (cpt := .rtr) |>.mpr ⟨_, h₂⟩
State after:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
⊢ iₘ✝ <[rtr₁] iᵣ✝

State before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
⊢ iₘ✝ <[rtr₁] iᵣ✝
Tactic:
have h₄' := mem_get?_iff (get?_rtr_some_equiv e h₂' h₂) (cpt := .rcn) |>.mpr h₄
State after:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
h₄' : iᵣ✝ ∈ w✝{Component.rcn}
⊢ iₘ✝ <[rtr₁] iᵣ✝

State before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
h₄' : iᵣ✝ ∈ w✝{Component.rcn}
⊢ iₘ✝ <[rtr₁] iᵣ✝
Tactic:
exact mutNest h₁' h₂' (get?_rcn_eq e ▸ h₃) ‹_› h₄'
State after:
no goals

State before:
case trans
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i₁✝ i₂✝ i₃✝ : ID
a✝¹ : i₁✝ <[rtr₂] i₂✝
a✝ : i₂✝ <[rtr₂] i₃✝
d₁ : i₁✝ <[rtr₁] i₂✝
d₂ : i₂✝ <[rtr₁] i₃✝
⊢ i₁✝ <[rtr₁] i₃✝
Tactic:
exact trans d₁ d₂
State after:
no goals