internlm/Lean-Github huggingface dataset:
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:
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₂
Proof state after:
α : 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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ s₁₂ = s₂₁
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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ s₁₂ = s₂₁
Tactic:
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₂
Proof state after:
α : 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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
⊢ s₁₂ = s₂₁
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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
⊢ s₁₂ = s₂₁
Tactic:
have ⟨_, g₁⟩ := Apply.RTC.construct z₁ (hd₂ :: tl₂)
Proof state after:
α : 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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
fst✝ : State α
g₁ : z₁ -[hd₂ :: tl₂]→ fst✝
⊢ s₁₂ = s₂₁
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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
fst✝ : State α
g₁ : z₁ -[hd₂ :: tl₂]→ fst✝
⊢ s₁₂ = s₂₁
Tactic:
cases ne_targets_comm_apply h₁ (trans f₂ f₂') f₁ e₁ g₁
Proof state after:
case refl
α : 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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
g₁ : z₁ -[hd₂ :: tl₂]→ s₂✝
⊢ s₁₂ = s₂₁
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
case refl
α : 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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
g₁ : z₁ -[hd₂ :: tl₂]→ s₂✝
⊢ s₁₂ = s₂₁
Tactic:
exact hi h₂ (.trans e₂ e₂') g₁ f₁'
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₂₁
⊢ ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
Tactic:
intro _ h hm₂
Proof state after:
α : 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₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False
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₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False
Tactic:
have hm₁ := Reaction.Output.target_mem_targets (out := hd₁ :: tl₁) (by simp) h
Proof state after:
α : 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₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
hm₁ : t✝ ∈ Reaction.Output.targets (hd₁ :: tl₁)
⊢ False
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₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
hm₁ : t✝ ∈ Reaction.Output.targets (hd₁ :: tl₁)
⊢ False
Tactic:
exact absurd rfl $ Set.disjoint_iff_forall_ne.mp ht hm₁ hm₂
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₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ 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₂₁ : 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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
Tactic:
simp [Set.disjoint_iff_forall_ne]
Proof state after:
α : 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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets tl₁ →
      ∀ (a_2 : Component.Valued) (b_1 : ID), (a_2, b_1) ∈ Reaction.Output.targets (hd₂ :: tl₂) → a = a_2 → ¬b = b_1
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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets tl₁ →
      ∀ (a_2 : Component.Valued) (b_1 : ID), (a_2, b_1) ∈ Reaction.Output.targets (hd₂ :: tl₂) → a = a_2 → ¬b = b_1
Tactic:
intro _ _ hm₁ _ _ hm₂ h₁ h₂
Proof state after:
α : 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₂₁
h₁✝ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
a✝¹ : Component.Valued
b✝¹ : ID
hm₁ : (a✝¹, b✝¹) ∈ Reaction.Output.targets tl₁
a✝ : Component.Valued
b✝ : ID
hm₂ : (a✝, b✝) ∈ Reaction.Output.targets (hd₂ :: tl₂)
h₁ : a✝¹ = a✝
h₂ : b✝¹ = b✝
⊢ False
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₂₁
h₁✝ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
a✝¹ : Component.Valued
b✝¹ : ID
hm₁ : (a✝¹, b✝¹) ∈ Reaction.Output.targets tl₁
a✝ : Component.Valued
b✝ : ID
hm₂ : (a✝, b✝) ∈ Reaction.Output.targets (hd₂ :: tl₂)
h₁ : a✝¹ = a✝
h₂ : b✝¹ = b✝
⊢ False
Tactic:
subst h₁ h₂
Proof state after:
α : 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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
a✝ : Component.Valued
b✝ : ID
hm₁ : (a✝, b✝) ∈ Reaction.Output.targets tl₁
hm₂ : (a✝, b✝) ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False
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₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
a✝ : Component.Valued
b✝ : ID
hm₁ : (a✝, b✝) ∈ Reaction.Output.targets tl₁
hm₂ : (a✝, b✝) ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False
Tactic:
exact Set.disjoint_left.mp ht (Reaction.Output.mem_targets_cons hm₁) hm₂
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✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
cases e₁.deterministic e₂
Proof state after:
case refl.trans.trans.refl.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₁₂
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Theorem: Execution.Step.Apply.RTC.disjoint_targets_comm
Proof state before:
case refl.trans.trans.refl.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₁₂
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
exact e₁'.deterministic e₂'
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.progress_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ᵢ s₂
⊢ s₁.progress ⊂ s₂.progress
Tactic:
simp [e.progress_eq, Set.ssubset_iff_insert]
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ᵢ s₂
⊢ ∃ a ∉ s₁.progress, insert a s₁.progress ⊆ Set.insert (rcn e) s₁.progress
Theorem: Execution.Instantaneous.Step.progress_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ᵢ s₂
⊢ ∃ a ∉ s₁.progress, insert a s₁.progress ⊆ Set.insert (rcn e) s₁.progress
Tactic:
exists e.rcn, e.allows_rcn.unprocessed
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.seq_wellordered
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
⊢ rcn e₂ ≮[s₁.rtr] rcn e₁
Tactic:
by_contra d
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
d : rcn e₂ <[s₁.rtr] rcn e₁
⊢ False