internlm/Lean-Github huggingface dataset:
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
cases LawfulUpdate.unique u₁ u₂
Proof state after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
cases LawfulUpdate.unique u₁ u₂
Proof state after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
cases LawfulUpdate.unique u₁ u₂
Proof state after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case mut.stv.stv.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝
Tactic:
try exact LawfulUpdate.unique ‹_› ‹_›
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case stv.stv.stv.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝
Tactic:
try case _ u₁ _ _ _ u₂ _ u₃ _ u₄ => exact LawfulUpdate.ne_comm u₁ u₂ u₃ u₄ $ by simp [ht]
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case mut.stv.stv.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝
Tactic:
exact LawfulUpdate.unique ‹_› ‹_›
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
u₂ :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
u₃ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
u₄ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝
Tactic:
case _ u₁ _ _ _ u₂ _ u₃ _ u₄ => exact LawfulUpdate.ne_comm u₁ u₂ u₃ u₄ $ by simp [ht]
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
u₂ :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
u₃ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
u₄ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝
Tactic:
exact LawfulUpdate.ne_comm u₁ u₂ u₃ u₄ $ by simp [ht]
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
u₂ :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
u₃ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
u₄ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ Component.Valued.stv ≠ Component.Valued.stv ∨ i✝¹ ≠ i✝
Tactic:
simp [ht]
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_tag
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
e : s₁ -[out]→ s₂
⊢ s₁.tag = s₂.tag
Tactic:
induction e
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.tag = s✝.tag

case trans
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
a_ih✝ : s₂✝.tag = s₃✝.tag
⊢ s₁✝.tag = s₃✝.tag
Theorem: Execution.Step.Apply.RTC.preserves_tag
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.tag = s✝.tag
Tactic:
case refl => rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_tag
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : s₂✝.tag = s₃✝.tag
⊢ s₁✝.tag = s₃✝.tag
Tactic:
case trans e _ hi => exact e.preserves_tag ▸ hi
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_tag
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.tag = s✝.tag
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_tag
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : s₂✝.tag = s₃✝.tag
⊢ s₁✝.tag = s₃✝.tag
Tactic:
exact e.preserves_tag ▸ hi
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
e : s₁ -[out]→ s₂
⊢ s₁.progress = s₂.progress
Tactic:
induction e
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.progress = s✝.progress

case trans
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
a_ih✝ : s₂✝.progress = s₃✝.progress
⊢ s₁✝.progress = s₃✝.progress
Theorem: Execution.Step.Apply.RTC.preserves_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.progress = s✝.progress
Tactic:
case refl => rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : s₂✝.progress = s₃✝.progress
⊢ s₁✝.progress = s₃✝.progress
Tactic:
case trans e _ hi => exact e.preserves_progress ▸ hi
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.progress = s✝.progress
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : s₂✝.progress = s₃✝.progress
⊢ s₁✝.progress = s₃✝.progress
Tactic:
exact e.preserves_progress ▸ hi
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
e : s₁ -[out]→ s₂
⊢ s₁.rtr ≈ s₂.rtr
Tactic:
induction e
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.rtr ≈ s✝.rtr

case trans
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
a_ih✝ : s₂✝.rtr ≈ s₃✝.rtr
⊢ s₁✝.rtr ≈ s₃✝.rtr
Theorem: Execution.Step.Apply.RTC.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.rtr ≈ s✝.rtr
Tactic:
case refl => exact .refl _
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : s₂✝.rtr ≈ s₃✝.rtr
⊢ s₁✝.rtr ≈ s₃✝.rtr
Tactic:
case trans e _ hi => exact Equivalent.trans e.equiv hi
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ s✝ : State α
⊢ s✝.rtr ≈ s✝.rtr
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : s₂✝.rtr ≈ s₃✝.rtr
⊢ s₁✝.rtr ≈ s₃✝.rtr
Tactic:
exact Equivalent.trans e.equiv hi
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_unchanged
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ -[out]→ s₂
h : List.Forall (fun x => ¬Change.Targets x cpt i) out
⊢ s₁.rtr[Component.val cpt][i] = s₂.rtr[Component.val cpt][i]
Tactic:
induction e
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
s✝ : State α
h : List.Forall (fun x => ¬Change.Targets x cpt i) []
⊢ s✝.rtr[Component.val cpt][i] = s✝.rtr[Component.val cpt][i]

case trans
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
a_ih✝ :
  List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
Theorem: Execution.Step.Apply.RTC.preserves_unchanged
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
s✝ : State α
h : List.Forall (fun x => ¬Change.Targets x cpt i) []
⊢ s✝.rtr[Component.val cpt][i] = s✝.rtr[Component.val cpt][i]
Tactic:
case refl => rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_unchanged
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
Tactic:
case trans e _ hi =>
  have ⟨hh, ht⟩ := List.forall_cons _ _ _ |>.mp h
  exact e.preserves_unchanged hh ▸ hi ht
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_unchanged
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
s✝ : State α
h : List.Forall (fun x => ¬Change.Targets x cpt i) []
⊢ s✝.rtr[Component.val cpt][i] = s✝.rtr[Component.val cpt][i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.preserves_unchanged
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
Tactic:
have ⟨hh, ht⟩ := List.forall_cons _ _ _ |>.mp h
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
hh : ¬Change.Targets hd✝ cpt i
ht : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
Theorem: Execution.Step.Apply.RTC.preserves_unchanged
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
hh : ¬Change.Targets hd✝ cpt i
ht : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
Tactic:
exact e.preserves_unchanged hh ▸ hi ht
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.allows_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
e : s₁ -[out]→ s₂
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
induction e
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
s✝ : State α
⊢ Allows s✝ i ↔ Allows s✝ i

case trans
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
a_ih✝ : Allows s₂✝ i ↔ Allows s₃✝ i
⊢ Allows s₁✝ i ↔ Allows s₃✝ i
Theorem: Execution.Step.Apply.RTC.allows_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
s✝ : State α
⊢ Allows s✝ i ↔ Allows s✝ i
Tactic:
case refl => rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.allows_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : Allows s₂✝ i ↔ Allows s₃✝ i
⊢ Allows s₁✝ i ↔ Allows s₃✝ i
Tactic:
case trans e _ hi => exact e.allows_iff.trans hi
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.allows_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
s✝ : State α
⊢ Allows s✝ i ↔ Allows s✝ i
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.allows_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : Allows s₂✝ i ↔ Allows s₃✝ i
⊢ Allows s₁✝ i ↔ Allows s₃✝ i
Tactic:
exact e.allows_iff.trans hi
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
rcn : ID
e₁ : s -[out]→ s₁
e₂ : (record s rcn) -[out]→ s₂
⊢ record s₁ rcn = s₂
Tactic:
induction e₁ <;> cases e₂
Proof state after:
case refl.refl
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
rcn : ID
s✝ : State α
⊢ record s✝ rcn = record s✝ rcn

case trans.trans
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
rcn : ID
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₃✝
a_ih✝ : (record s₂✝¹ rcn) -[tl✝]→ s₂ → record s₃✝ rcn = s₂
s₂✝ : State α
a✝¹ : (record s₁✝ rcn) -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂
⊢ record s₃✝ rcn = s₂
Theorem: Execution.Step.Apply.RTC.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
rcn : ID
s✝ : State α
⊢ record s✝ rcn = record s✝ rcn
Tactic:
case refl.refl => rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
rcn : ID
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e₁ : s₁✝ -[hd✝]→ s₂✝¹
a✝ : s₂✝¹ -[tl✝]→ s₃✝
hi : (record s₂✝¹ rcn) -[tl✝]→ s₂ → record s₃✝ rcn = s₂
s₂✝ : State α
e₂ : (record s₁✝ rcn) -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂
⊢ record s₃✝ rcn = s₂
Tactic:
case trans.trans e₁ _ hi _ e₂ e₂' => exact hi $ (e₁.comm_record e₂).symm ▸ e₂'
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
rcn : ID
s✝ : State α
⊢ record s✝ rcn = record s✝ rcn
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
rcn : ID
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e₁ : s₁✝ -[hd✝]→ s₂✝¹
a✝ : s₂✝¹ -[tl✝]→ s₃✝
hi : (record s₂✝¹ rcn) -[tl✝]→ s₂ → record s₃✝ rcn = s₂
s₂✝ : State α
e₂ : (record s₁✝ rcn) -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂
⊢ record s₃✝ rcn = s₂
Tactic:
exact hi $ (e₁.comm_record e₂).symm ▸ e₂'
Proof state after:
no goals
Theorem: Execution.Step.Apply.RTC.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
e₁ : s -[out]→ s₁
e₂ : s -[out]→ s₂
⊢ s₁ = s₂
Tactic:
induction e₁ generalizing s₂ <;> cases e₂
Proof state after:
case refl.refl
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
s✝ : State α
⊢ s✝ = s✝

case trans.trans
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₂✝¹ -[tl✝]→ s₂ → s₃✝ = s₂
s₂ s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂
⊢ s₃✝ = s₂
Theorem: Execution.Step.Apply.RTC.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
s✝ : State α
⊢ s✝ = s✝
Tactic:
case refl.refl => rfl
Proof state after:
no goals