Theorem: Execution.State.indep_output_disjoint_targets (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ Disjoint (Reaction.Output.targets (output s i₁)) (Reaction.Output.targets (output s i₂))
Tactic:
cases h₁ : s.rtr[.rcn][i₁] <;> cases h₂ : s.rtr[.rcn][i₂] <;> simp [output, h₁, h₂]
State after:
case none.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Reaction.Output.targets [] = ∅

case none.some
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
val✝ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some val✝
⊢ Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (val✝.body (input s i₂)))

case some.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Disjoint (Reaction.Output.targets (val✝.body (input s i₁))) (Reaction.Output.targets [])

case some.some
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝¹ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝¹
val✝ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some val✝
⊢ Disjoint (Reaction.Output.targets (val✝¹.body (input s i₁))) (Reaction.Output.targets (val✝.body (input s i₂)))

State before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ Disjoint (Reaction.Output.targets (rcn₁.body (input s i₁))) (Reaction.Output.targets (rcn₂.body (input s i₂)))
Tactic:
case some.some rcn₁ rcn₂ =>
  simp [Set.disjoint_iff_forall_ne]
  intro _ _ ⟨_, hc₁, ht₁⟩ _ _ ⟨_, hc₂, ht₂⟩ hc hj
  cases hc; cases hj; cases ht₁; cases ht₂
  replace hc₁ := rcn₁.target_mem_deps hc₁
  replace hc₂ := rcn₂.target_mem_deps hc₂
  cases Dependency.shared_out_dep h₁ h₂ hi.not_eq hc₁ hc₂ <;> simp [hi.left, hi.right] at *
State after:
no goals

State before:
case none.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Reaction.Output.targets [] = ∅

case none.some
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
val✝ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some val✝
⊢ Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (val✝.body (input s i₂)))

case some.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Disjoint (Reaction.Output.targets (val✝.body (input s i₁))) (Reaction.Output.targets [])
Tactic:
all_goals simp [Reaction.Output.targets]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ Disjoint (Reaction.Output.targets (rcn₁.body (input s i₁))) (Reaction.Output.targets (rcn₂.body (input s i₂)))
Tactic:
simp [Set.disjoint_iff_forall_ne]
State after:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets (rcn₁.body (input s i₁)) →
      ∀ (a_2 : Component.Valued) (b_1 : ID),
        (a_2, b_1) ∈ Reaction.Output.targets (rcn₂.body (input s i₂)) → a = a_2 → ¬b = b_1

State before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets (rcn₁.body (input s i₁)) →
      ∀ (a_2 : Component.Valued) (b_1 : ID),
        (a_2, b_1) ∈ Reaction.Output.targets (rcn₂.body (input s i₂)) → a = a_2 → ¬b = b_1
Tactic:
intro _ _ ⟨_, hc₁, ht₁⟩ _ _ ⟨_, hc₂, ht₂⟩ hc hj
State after:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝¹ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝¹, b✝¹).1 (a✝¹, b✝¹).2
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
hc : a✝¹ = a✝
hj : b✝¹ = b✝
⊢ False

State before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝¹ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝¹, b✝¹).1 (a✝¹, b✝¹).2
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
hc : a✝¹ = a✝
hj : b✝¹ = b✝
⊢ False
Tactic:
cases hc
State after:
case refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝¹).1 (a✝, b✝¹).2
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
hj : b✝¹ = b✝
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False

State before:
case refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝¹).1 (a✝, b✝¹).2
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
hj : b✝¹ = b✝
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False
Tactic:
cases hj
State after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝).1 (a✝, b✝).2
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False

State before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝).1 (a✝, b✝).2
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False
Tactic:
cases ht₁
State after:
case refl.refl.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
v✝ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₁.body (input s i₁)
⊢ False

State before:
case refl.refl.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
v✝ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₁.body (input s i₁)
⊢ False
Tactic:
cases ht₂
State after:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.body (input s i₁)
v✝ : Component.Valued.changeType (a✝, b✝).1
hc₂ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.body (input s i₂)
⊢ False

State before:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.body (input s i₁)
v✝ : Component.Valued.changeType (a✝, b✝).1
hc₂ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.body (input s i₂)
⊢ False
Tactic:
replace hc₁ := rcn₁.target_mem_deps hc₁
State after:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ v✝ : Component.Valued.changeType (a✝, b✝).1
hc₂ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.body (input s i₂)
hc₁ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.deps Kind.out
⊢ False

State before:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ v✝ : Component.Valued.changeType (a✝, b✝).1
hc₂ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.body (input s i₂)
hc₁ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.deps Kind.out
⊢ False
Tactic:
replace hc₂ := rcn₂.target_mem_deps hc₂
State after:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ v✝ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.deps Kind.out
hc₂ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.deps Kind.out
⊢ False

State before:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ v✝ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.deps Kind.out
hc₂ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.deps Kind.out
⊢ False
Tactic:
cases Dependency.shared_out_dep h₁ h₂ hi.not_eq hc₁ hc₂ <;> simp [hi.left, hi.right] at *
State after:
no goals

State before:
case some.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Disjoint (Reaction.Output.targets (val✝.body (input s i₁))) (Reaction.Output.targets [])
Tactic:
simp [Reaction.Output.targets]
State after:
no goals