Theorem: Reactor.refresh_correct (ReactorModel/Execution/Theorems/Reactor.lean)

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ refresh rtr acts[Component.stv] = rtr[Component.stv]
Tactic:
rw [
  refresh, set_preserves (by simp : .stv ≠ .act), set_preserves (by simp : .stv ≠ .out), 
  set_preserves (by simp : .stv ≠ .inp)
]
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ Component.Valued.stv ≠ Component.Valued.act
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ Component.Valued.stv ≠ Component.Valued.out
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ Component.Valued.stv ≠ Component.Valued.inp
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ refresh rtr acts[Component.act] = acts
Tactic:
rw [refresh, set_updated $ h ▸ (Equivalent.ids_eq $ Equivalent.trans set_equiv set_equiv)]
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ refresh rtr acts[Component.inp] = Partial.map (fun x => Value.absent) (rtr[Component.inp])
Tactic:
rw [
  refresh, set_preserves (by simp : .inp ≠ .act), set_preserves (by simp : .inp ≠ .out), 
  set_updated $ Partial.const_ids _ _, Partial.const_eq_map_const
]
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ Component.Valued.inp ≠ Component.Valued.act
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ Component.Valued.inp ≠ Component.Valued.out
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ refresh rtr acts[Component.out] = Partial.map (fun x => Value.absent) (rtr[Component.out])
Tactic:
rw [
  refresh, set_preserves (by simp : .out ≠ .act),
  set_updated $ by rw [Equivalent.ids_eq set_equiv, Partial.const_ids _ _],
  Partial.const_eq_map_const
]
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ Component.Valued.out ≠ Component.Valued.act
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ Partial.ids (Partial.const (Partial.ids (rtr[Component.out])) Value.absent) =
    Partial.ids
      (set rtr Component.Valued.inp
          (Partial.const (Partial.ids (rtr[Component.inp])) Value.absent)[Component.val Component.Valued.out])
Tactic:
rw [Equivalent.ids_eq set_equiv, Partial.const_ids _ _]
State after:
no goals