Theorem: Independent.no_shared_state_deps (ReactorModel/Execution/Theorems/Dependency.lean)

State before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k
Tactic:
have hd₁ := rcn₁.target_mem_deps hs
State after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : Change.Normal.target { cpt := Component.Valued.stv, id := j, value := v } ∈ rcn₁.deps Kind.out
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k

State before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : Change.Normal.target { cpt := Component.Valued.stv, id := j, value := v } ∈ rcn₁.deps Kind.out
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k
Tactic:
simp [Change.Normal.target] at hd₁
State after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k

State before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k
Tactic:
by_contra hd₂
State after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
⊢ False

State before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
⊢ False
Tactic:
have ⟨_, _, hc₁, hr₁⟩ := obj?_some_split h₁
State after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ False

State before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ False
Tactic:
have ⟨_, _, hc₂, hr₂⟩ := obj?_some_split h₂
State after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
⊢ False

State before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
⊢ False
Tactic:
have hc := Proper.wellformed rtr |>.shared_state_local hc₁ hc₂ hr₁ hr₂ hd₁ hd₂
State after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc : w✝³ = w✝¹
⊢ False

State before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc : w✝³ = w✝¹
⊢ False
Tactic:
injection hc₂ ▸ hc ▸ hc₁ with hc
State after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
⊢ False

State before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
⊢ False
Tactic:
cases Dependency.hazard hc₁ hr₁ (hc ▸ hr₂) hi.not_eq hd₁ hd₂ (.inl rfl)
State after:
case inl
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
h✝ : i₁ <[rtr] i₂
⊢ False

case inr
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
h✝ : i₂ <[rtr] i₁
⊢ False

State before:
case inl
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
h✝ : i₁ <[rtr] i₂
⊢ False

case inr
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
h✝ : i₂ <[rtr] i₁
⊢ False
Tactic:
all_goals simp [hi.left, hi.right] at *
State after:
no goals

State before:
case inr
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
h✝ : i₂ <[rtr] i₁
⊢ False
Tactic:
simp [hi.left, hi.right] at *
State after:
no goals