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

State before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
have ⟨_, _, hc₁, hr₁⟩ := obj?_some_split h₁
State after:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

State before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
have ⟨_, _, hc₂, hr₂⟩ := obj?_some_split h₂
State after:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
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₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

State before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
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₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
have hc := Proper.wellformed rtr |>.shared_dep_local hc₁ hc₂ hr₁ hr₂ hd₁ hd₂
State after:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
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✝¹
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

State before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
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✝¹
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
injection hc₂ ▸ hc ▸ hc₁ with hc
State after:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
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✝²
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

State before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
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✝²
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact same_con_shared_out_dep hc₁ hr₁ (hc ▸ hr₂) hn hd₁ hd₂
State after:
no goals