Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply (ReactorModel/Execution/Theorems/Step/Apply.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets out
eₒ : s -[out]→ sₒ
eₒ₁ : sₒ -[c]→ sₒ₁
e₁ : s -[c]→ s₁
e₁ₒ : s₁ -[out]→ s₁ₒ
⊢ sₒ₁ = s₁ₒ
Tactic:
induction eₒ generalizing s₁ <;> cases e₁ₒ
State after:
case refl.refl
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ s✝ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets []
eₒ₁ : s✝ -[c]→ sₒ₁
e₁ : s✝ -[c]→ s₁ₒ
⊢ sₒ₁ = s₁ₒ

case trans.trans
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₃✝
a_ih✝ :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl✝) →
      s₃✝ -[c]→ sₒ₁ → s₂✝¹ -[c]→ s₁ → s₁ -[tl✝]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd✝ :: tl✝)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
a✝¹ : s₁ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₁ₒ
⊢ sₒ₁ = s₁ₒ

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ s✝ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets []
eₒ₁ : s✝ -[c]→ sₒ₁
e₁ : s✝ -[c]→ s₁ₒ
⊢ sₒ₁ = s₁ₒ
Tactic:
case refl.refl => exact eₒ₁.deterministic e₁
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ s✝ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets []
eₒ₁ : s✝ -[c]→ sₒ₁
e₁ : s✝ -[c]→ s₁ₒ
⊢ sₒ₁ = s₁ₒ
Tactic:
exact eₒ₁.deterministic e₁
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
⊢ sₒ₁ = s₁ₒ
Tactic:
have h : hd.target ≠ c.target ∨ hd.target = none := by
  by_contra hc
  push_neg at hc
  have ⟨_, h⟩ := Option.ne_none_iff_exists.mp hc.right
  exact ht (hc.left ▸ h.symm) $ Reaction.Output.target_mem_targets (by simp) h.symm
State after:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
h : Change.target hd ≠ Change.target c ∨ Change.target hd = none
⊢ sₒ₁ = s₁ₒ

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
h : Change.target hd ≠ Change.target c ∨ Change.target hd = none
⊢ sₒ₁ = s₁ₒ
Tactic:
have ⟨_, e'⟩ := Apply.construct s' c
State after:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
h : Change.target hd ≠ Change.target c ∨ Change.target hd = none
fst✝ : State α
e' : s' -[c]→ fst✝
⊢ sₒ₁ = s₁ₒ

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
h : Change.target hd ≠ Change.target c ∨ Change.target hd = none
fst✝ : State α
e' : s' -[c]→ fst✝
⊢ sₒ₁ = s₁ₒ
Tactic:
cases Apply.ne_target_comm h eₒ e' e₁ e₁ₒ
State after:
case refl
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
h : Change.target hd ≠ Change.target c ∨ Change.target hd = none
e' : s' -[c]→ s₂✝
⊢ sₒ₁ = s₁ₒ

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
⊢ Change.target hd ≠ Change.target c ∨ Change.target hd = none
Tactic:
by_contra hc
State after:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
hc : ¬(Change.target hd ≠ Change.target c ∨ Change.target hd = none)
⊢ False

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
hc : ¬(Change.target hd ≠ Change.target c ∨ Change.target hd = none)
⊢ False
Tactic:
push_neg at hc
State after:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
hc : Change.target hd = Change.target c ∧ Change.target hd ≠ none
⊢ False

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
hc : Change.target hd = Change.target c ∧ Change.target hd ≠ none
⊢ False
Tactic:
have ⟨_, h⟩ := Option.ne_none_iff_exists.mp hc.right
State after:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
hc : Change.target hd = Change.target c ∧ Change.target hd ≠ none
w✝ : Component.Valued × ID
h : some w✝ = Change.target hd
⊢ False

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
hc : Change.target hd = Change.target c ∧ Change.target hd ≠ none
w✝ : Component.Valued × ID
h : some w✝ = Change.target hd
⊢ False
Tactic:
exact ht (hc.left ▸ h.symm) $ Reaction.Output.target_mem_targets (by simp) h.symm
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
sₒ sₒ₁ s₁ₒ : State α
hd : Change
s₁✝ s' : State α
tl : Reaction.Output
s₃✝ : State α
eₒ : s₁✝ -[hd]→ s'
a✝ : s' -[tl]→ s₃✝
hi :
  ∀ {s₁ : State α},
    (∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets tl) →
      s₃✝ -[c]→ sₒ₁ → s' -[c]→ s₁ → s₁ -[tl]→ s₁ₒ → sₒ₁ = s₁ₒ
s₁ : State α
ht : ∀ {t : Component.Valued × ID}, Change.target c = some t → t ∉ Reaction.Output.targets (hd :: tl)
eₒ₁ : s₃✝ -[c]→ sₒ₁
e₁ : s₁✝ -[c]→ s₁
s₂✝ : State α
e₁ₒ : s₁ -[hd]→ s₂✝
e₁ₒ' : s₂✝ -[tl]→ s₁ₒ
hc : Change.target hd = Change.target c ∧ Change.target hd ≠ none
w✝ : Component.Valued × ID
h : some w✝ = Change.target hd
⊢ hd ∈ hd :: tl
Tactic:
simp
State after:
no goals