internlm/Lean-Github huggingface dataset:
Theorem: Execution.Step.Apply.RTC.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e₁ : s₁✝ -[hd✝]→ s₂✝¹
a✝ : s₂✝¹ -[tl✝]→ s₃✝
hi : ∀ {s₂ : State α}, s₂✝¹ -[tl✝]→ s₂ → s₃✝ = s₂
s₂ s₂✝ : State α
e₂ : s₁✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂
⊢ s₃✝ = s₂
Tactic:
case trans.trans e₁ _ hi _ e₂ e₂' => exact hi $ (e₁.deterministic e₂) ▸ e₂'
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
s✝ : State α
⊢ s✝ = s✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e₁ : s₁✝ -[hd✝]→ s₂✝¹
a✝ : s₂✝¹ -[tl✝]→ s₃✝
hi : ∀ {s₂ : State α}, s₂✝¹ -[tl✝]→ s₂ → s₃✝ = s₂
s₂ s₂✝ : State α
e₂ : s₁✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂
⊢ s₃✝ = s₂
Tactic:
exact hi $ (e₁.deterministic e₂) ▸ e₂'
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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₁ₒ
Proof 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₁ₒ
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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₁
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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₁
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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
Proof 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₁ₒ
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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
Proof 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₁ₒ
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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₁ₒ
Proof 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₁ₒ
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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
Proof 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
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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
Proof 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
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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
Proof 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
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.ne_targets_comm_apply
Proof 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
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
ht : Disjoint (Reaction.Output.targets out₁) (Reaction.Output.targets out₂)
e₁ : s -[out₁]→ s₁
e₁₂ : s₁ -[out₂]→ s₁₂
e₂ : s -[out₂]→ s₂
e₂₁ : s₂ -[out₁]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
induction e₁ generalizing s₂ <;> cases e₁₂ <;> cases e₂ <;> cases e₂₁
Proof state after:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ : State α
c : Change
out out₁ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets [])
⊢ s₁₂ = s₁₂

case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
a✝³ : s✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
a✝¹ : s✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.trans.trans.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝¹ : Change
s₁✝ s₂✝³ : State α
tl✝¹ : Reaction.Output
s₃✝ : State α
a✝⁷ : s₁✝ -[hd✝¹]→ s₂✝³
a✝⁶ : s₂✝³ -[tl✝¹]→ s₃✝
s₂ : State α
hd✝ : Change
s₂✝² : State α
tl✝ : Reaction.Output
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝¹) (Reaction.Output.targets (hd✝ :: tl✝)) →
      s₃✝ -[hd✝ :: tl✝]→ s₁₂ → s₂✝³ -[hd✝ :: tl✝]→ s₂ → s₂ -[tl✝¹]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd✝¹ :: tl✝¹)) (Reaction.Output.targets (hd✝ :: tl✝))
a✝⁵ : s₃✝ -[hd✝]→ s₂✝²
a✝⁴ : s₂✝² -[tl✝]→ s₁₂
s₂✝¹ : State α
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₂
s₂✝ : State α
a✝¹ : s₂ -[hd✝¹]→ s₂✝
a✝ : s₂✝ -[tl✝¹]→ s₂₁
⊢ s₁₂ = s₂₁
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₁₂ : State α
c : Change
out out₁ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets [])
⊢ s₁₂ = s₁₂
Tactic:
case refl.refl.refl.refl => rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
case trans.trans.trans.trans hd₁ s z₁ tl₁ _ e₁ e₁' hd₂ _ tl₂ hi e₂ e₂' _ f₂ f₂' _ f₁ f₁' =>
  have h₁ : ∀ {t}, hd₁.target = some t → ¬t ∈ Reaction.Output.targets (hd₂ :: tl₂) := by
    intro _ h hm₂
    have hm₁ := Reaction.Output.target_mem_targets (out := hd₁ :: tl₁) (by simp) h
    exact absurd rfl $ Set.disjoint_iff_forall_ne.mp ht hm₁ hm₂
  have h₂ : Disjoint tl₁.targets $ Reaction.Output.targets (hd₂ :: tl₂) := by
    simp [Set.disjoint_iff_forall_ne]
    intro _ _ hm₁ _ _ hm₂ h₁ h₂
    subst h₁ h₂
    exact Set.disjoint_left.mp ht (Reaction.Output.mem_targets_cons hm₁) hm₂
  have ⟨_, g₁⟩ := Apply.RTC.construct z₁ (hd₂ :: tl₂)
  cases ne_targets_comm_apply h₁ (trans f₂ f₂') f₁ e₁ g₁
  exact hi h₂ (.trans e₂ e₂') g₁ f₁'
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
a✝³ : s✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
a✝¹ : s✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
case' refl.trans.trans.refl e₁ e₁' _ e₂ e₂' => skip
Proof state after:
case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
case' trans.refl.refl.trans e₁ e₁' _ _ e₂ e₂' => skip
Proof state after:
case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
e₁ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
e₁' : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
e₂ : s₁✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
e₁ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
e₁' : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
e₂ : s₁✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
all_goals cases e₁.deterministic e₂; exact e₁'.deterministic e₂'
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₁₂ : State α
c : Change
out out₁ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets [])
⊢ s₁₂ = s₁₂
Tactic:
rfl
Proof state after:
no goals