internlm/Lean-Github huggingface dataset:
Theorem: Reactor.set.go_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬(i = hd ∨ i ∈ tl)
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
push_neg at h
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
h : i ≠ hd ∧ i ∉ tl
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Theorem: Reactor.set.go_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
h : i ≠ hd ∧ i ∉ tl
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
simp [hi ho' $ .inr $ .inl h.right]
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
h : i ≠ hd ∧ i ∉ tl
⊢ w✝ = o
Theorem: Reactor.set.go_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
h : i ≠ hd ∧ i ∉ tl
⊢ w✝ = o
Tactic:
injection ho' ▸ ho ▸ obj?_preserved_id h.left
Proof state after:
no goals
Theorem: Reactor.set.go_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
have hh : i ≠ hd := by by_contra; simp_all
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
hh : i ≠ hd
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Theorem: Reactor.set.go_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
hh : i ≠ hd
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
have ho' := ho ▸ (@LawfulUpdatable.lawful _ _ rtr cpt hd v).obj?_preserved (c := c) (.inr hh)
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
hh : i ≠ hd
ho' : update rtr cpt hd v[Component.val c][i] = some o
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Theorem: Reactor.set.go_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
hh : i ≠ hd
ho' : update rtr cpt hd v[Component.val c][i] = some o
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
exact hi ho' (.inr $ .inr h)
Proof state after:
no goals
Theorem: Reactor.set.go_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
⊢ i ≠ hd
Tactic:
by_contra
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
a✝ : i = hd
⊢ False
Theorem: Reactor.set.go_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
a✝ : i = hd
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
i : ID
v : Value
ids : List ID
cpt : Component.Valued
o : Component.type α (Component.val cpt)
vs : ID ⇀ Value
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i ∈ ids
⊢ go rtr cpt vs ids[Component.val cpt][i] = some v
Tactic:
induction ids generalizing rtr o v i <;> simp at h
Proof state after:
case cons
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
tail_ih✝ :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i = head✝ ∨ i ∈ tail✝
⊢ go rtr cpt vs (head✝ :: tail✝)[Component.val cpt][i] = some v
Theorem: Reactor.set.go_updated
Proof state before:
case cons
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
tail_ih✝ :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i = head✝ ∨ i ∈ tail✝
⊢ go rtr cpt vs (head✝ :: tail✝)[Component.val cpt][i] = some v
Tactic:
cases h
Proof state after:
case cons.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
tail_ih✝ :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h✝ : i = head✝
⊢ go rtr cpt vs (head✝ :: tail✝)[Component.val cpt][i] = some v

case cons.inr
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
tail_ih✝ :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h✝ : i ∈ tail✝
⊢ go rtr cpt vs (head✝ :: tail✝)[Component.val cpt][i] = some v
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i = head✝
⊢ go rtr cpt vs (head✝ :: tl)[Component.val cpt][i] = some v
Tactic:
case cons.inl tl hi h =>
  subst h
  simp [go, hv]
  have e := @LawfulUpdatable.equiv _ cpt i v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  by_cases ht : i ∈ tl
  case pos => exact hi ho' hv ht
  case neg => simp [set.go_preserves ho' (.inr $ .inl ht), ho' ▸ obj?_updated, ho]
Proof state after:
no goals
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i = head✝
⊢ go rtr cpt vs (head✝ :: tl)[Component.val cpt][i] = some v
Tactic:
subst h
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
⊢ go rtr cpt vs (i :: tl)[Component.val cpt][i] = some v
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
⊢ go rtr cpt vs (i :: tl)[Component.val cpt][i] = some v
Tactic:
simp [go, hv]
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
have e := @LawfulUpdatable.equiv _ cpt i v _ rtr
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
by_cases ht : i ∈ tl
Proof state after:
case pos
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∈ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v

case neg
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∉ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∈ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
case pos => exact hi ho' hv ht
Proof state after:
no goals
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∉ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
case neg => simp [set.go_preserves ho' (.inr $ .inl ht), ho' ▸ obj?_updated, ho]
Proof state after:
no goals
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∈ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
exact hi ho' hv ht
Proof state after:
no goals
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∉ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
simp [set.go_preserves ho' (.inr $ .inl ht), ho' ▸ obj?_updated, ho]
Proof state after:
no goals
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
⊢ go rtr cpt vs (hd :: tail✝)[Component.val cpt][i] = some v
Tactic:
simp [go]
Proof state after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
⊢ (match vs hd with
      | none => go rtr cpt vs tail✝
      | some v => go (update rtr cpt hd v) cpt vs tail✝)[Component.val cpt][i] =
    some v
Theorem: Reactor.set.go_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
⊢ (match vs hd with
      | none => go rtr cpt vs tail✝
      | some v => go (update rtr cpt hd v) cpt vs tail✝)[Component.val cpt][i] =
    some v
Tactic:
split
Proof state after:
case h_1
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
x✝ : Option Value
heq✝ : vs hd = none
⊢ go rtr cpt vs tail✝[Component.val cpt][i] = some v

case h_2
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
x✝ : Option Value
v✝ : Value
heq✝ : vs hd = some v✝
⊢ go (update rtr cpt hd v✝) cpt vs tail✝[Component.val cpt][i] = some v