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

State before:
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
by_cases hm₁ : rcn₁.Mutates <;> by_cases hm₂ : rcn₂.Mutates
State after:
case pos
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

State before:
case pos
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
rotate_left
State after:
case neg
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

State before:
case neg
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact .inl $ .mutNorm hc h₁ h₂ hm₁ (by simp_all [Reaction.Mutates])
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ Reaction.Normal rcn₂
Tactic:
simp_all [Reaction.Mutates]
State after:
no goals

State before:
case pos
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact .inr $ .mutNorm hc h₂ h₁ hm₂ (by simp_all [Reaction.Mutates])
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ Reaction.Normal rcn₁
Tactic:
simp_all [Reaction.Mutates]
State after:
no goals

State before:
case pos
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
cases Proper.wellformed rtr |>.ordered_prio hc h₁ h₂ hn hp
State after:
case pos.inl
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₁.prio < rcn₂.prio
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos.inr
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₂.prio < rcn₁.prio
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

State before:
case pos.inl
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₁.prio < rcn₂.prio
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact .inr $ .prio hc h₂ h₁ (by simp_all) ‹_›
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₁.prio < rcn₂.prio
⊢ Reaction.Mutates rcn₂ ↔ Reaction.Mutates rcn₁
Tactic:
simp_all
State after:
no goals

State before:
case pos.inr
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₂.prio < rcn₁.prio
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact .inl $ .prio hc h₁ h₂ (by simp_all) ‹_›
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr : α
c : 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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₂.prio < rcn₁.prio
⊢ Reaction.Mutates rcn₁ ↔ Reaction.Mutates rcn₂
Tactic:
simp_all
State after:
no goals