internlm/Lean-Github huggingface dataset:
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✝
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✝
Tactic:
case _ v _ =>
  have e := @LawfulUpdatable.equiv _ cpt hd v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  exact hi ho' hv ht
Proof state after:
no goals
Theorem: Reactor.set.go_updated
Proof state before:
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
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
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✝
Tactic:
have e := @LawfulUpdatable.equiv _ cpt hd v _ rtr
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✝
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd 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✝
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
⊢ go (update rtr cpt hd v) cpt vs tail✝[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
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
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt hd v[Component.val cpt][i] = some w✝
⊢ 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✝
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt hd v[Component.val cpt][i] = some w✝
⊢ go (update rtr cpt hd v) cpt vs tail✝[Component.val cpt][i] = some v✝
Tactic:
exact hi ho' hv ht
Proof state after:
no goals
Theorem: Reactor.set_updated'
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
⊢ set rtr cpt vs[Component.val cpt] = fun i => do
    let x ← rtr[Component.val cpt][i]
    some (Option.getD (vs i) x)
Tactic:
ext1 i
Proof state after:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
⊢ set rtr cpt vs[Component.val cpt][i] = do
    let x ← rtr[Component.val cpt][i]
    some (Option.getD (vs i) x)
Theorem: Reactor.set_updated'
Proof state before:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
⊢ set rtr cpt vs[Component.val cpt][i] = do
    let x ← rtr[Component.val cpt][i]
    some (Option.getD (vs i) x)
Tactic:
cases ho : rtr[cpt][i] <;> simp [bind, ho, Option.getD] <;> try split
Proof state after:
case h.none
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
ho : rtr[Component.val cpt][i] = none
⊢ set rtr cpt vs[Component.val cpt][i] = none

case h.some.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
x✝ : Value
heq✝ : vs i = some x✝
⊢ set rtr cpt vs[Component.val cpt][i] = some x✝

case h.some.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
heq✝ : vs i = none
⊢ set rtr cpt vs[Component.val cpt][i] = some val✝
Theorem: Reactor.set_updated'
Proof state before:
case h.some
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
⊢ set rtr cpt vs[Component.val cpt][i] =
    some
      (match vs i with
      | some x => x
      | none => val✝)
Tactic:
split
Proof state after:
case h.some.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
x✝ : Value
heq✝ : vs i = some x✝
⊢ set rtr cpt vs[Component.val cpt][i] = some x✝

case h.some.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
heq✝ : vs i = none
⊢ set rtr cpt vs[Component.val cpt][i] = some val✝
Theorem: Reactor.set_updated'
Proof state before:
case h.none
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
ho : rtr[Component.val cpt][i] = none
⊢ set rtr cpt vs[Component.val cpt][i] = none
Tactic:
exact Equivalent.obj?_none_iff set_equiv |>.mp ho
Proof state after:
no goals
Theorem: Reactor.set_updated'
Proof state before:
case h.some.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
x✝ : Value
heq✝ : vs i = some x✝
⊢ set rtr cpt vs[Component.val cpt][i] = some x✝
Tactic:
exact set.go_updated ho ‹_› $ mem_ids_iff.mpr ⟨_, ho⟩
Proof state after:
no goals
Theorem: Reactor.set_updated'
Proof state before:
case h.some.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
heq✝ : vs i = none
⊢ set rtr cpt vs[Component.val cpt][i] = some val✝
Tactic:
exact set.go_preserves ho $ .inr $ .inr ‹_›
Proof state after:
no goals
Theorem: Reactor.set_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
⊢ set rtr cpt vs[Component.val cpt] = vs
Tactic:
simp [set_updated', bind, Option.bind]
Proof state after:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
⊢ (fun i =>
      match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
      | none, x => none
      | some a, b => b a) =
    vs
Theorem: Reactor.set_updated
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
⊢ (fun i =>
      match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
      | none, x => none
      | some a, b => b a) =
    vs
Tactic:
ext1 i
Proof state after:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
⊢ (match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
    | none, x => none
    | some a, b => b a) =
    vs i
Theorem: Reactor.set_updated
Proof state before:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
⊢ (match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
    | none, x => none
    | some a, b => b a) =
    vs i
Tactic:
split
Proof state after:
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
heq✝ : rtr[Component.val cpt][i] = none
⊢ none = vs i

case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
heq✝ : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Theorem: Reactor.set_updated
Proof state before:
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
heq✝ : rtr[Component.val cpt][i] = none
⊢ none = vs i

case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
heq✝ : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
all_goals
  case' _ hn =>
    simp [Partial.ids, Set.ext_iff] at h
    specialize h i
    simp [hn] at h
Proof state after:
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
hn : rtr[Component.val cpt][i] = none
h : ∀ (x : Value), ¬vs i = some x
⊢ none = vs i

case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Theorem: Reactor.set_updated
Proof state before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
heq✝ : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
case' _ hn =>
  simp [Partial.ids, Set.ext_iff] at h
  specialize h i
  simp [hn] at h
Proof state after:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Theorem: Reactor.set_updated
Proof state before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
simp [Partial.ids, Set.ext_iff] at h
Proof state after:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∀ (x : ID), (∃ b, vs x = some b) ↔ ∃ b, rtr[Component.val cpt][x] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Theorem: Reactor.set_updated
Proof state before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∀ (x : ID), (∃ b, vs x = some b) ↔ ∃ b, rtr[Component.val cpt][x] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
specialize h i
Proof state after:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : (∃ b, vs i = some b) ↔ ∃ b, rtr[Component.val cpt][i] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Theorem: Reactor.set_updated
Proof state before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : (∃ b, vs i = some b) ↔ ∃ b, rtr[Component.val cpt][i] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
simp [hn] at h
Proof state after:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Theorem: Reactor.set_updated
Proof state before:
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
hn : rtr[Component.val cpt][i] = none
h : ∀ (x : Value), ¬vs i = some x
⊢ none = vs i
Tactic:
exact Option.eq_none_iff_forall_not_mem.mpr h |>.symm
Proof state after:
no goals
Theorem: Reactor.set_updated
Proof state before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
obtain ⟨_, h⟩ := h
Proof state after:
case h.h_2.intro
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
w✝ : Value
h : vs i = some w✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Theorem: Reactor.set_updated
Proof state before:
case h.h_2.intro
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
w✝ : Value
h : vs i = some w✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Reactor.set_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
⊢ set rtr cpt vs[Component.val c] = rtr[Component.val c]
Tactic:
ext1 i
Proof state after:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
⊢ set rtr cpt vs[Component.val c][i] = rtr[Component.val c][i]
Theorem: Reactor.set_preserves
Proof state before:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
⊢ set rtr cpt vs[Component.val c][i] = rtr[Component.val c][i]
Tactic:
cases ho : rtr[c][i]
Proof state after:
case h.none
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
ho : rtr[Component.val c][i] = none
⊢ set rtr cpt vs[Component.val c][i] = none

case h.some
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
val✝ : Component.type α (Component.val c)
ho : rtr[Component.val c][i] = some val✝
⊢ set rtr cpt vs[Component.val c][i] = some val✝
Theorem: Reactor.set_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
val✝ : Component.type α (Component.val c)
ho : rtr[Component.val c][i] = some val✝
⊢ set rtr cpt vs[Component.val c][i] = some val✝
Tactic:
case some => exact set.go_preserves ho (.inl h)
Proof state after:
no goals
Theorem: Reactor.set_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
ho : rtr[Component.val c][i] = none
⊢ set rtr cpt vs[Component.val c][i] = none
Tactic:
case none => exact Equivalent.obj?_none_iff set_equiv |>.mp ho
Proof state after:
no goals
Theorem: Reactor.set_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
val✝ : Component.type α (Component.val c)
ho : rtr[Component.val c][i] = some val✝
⊢ set rtr cpt vs[Component.val c][i] = some val✝
Tactic:
exact set.go_preserves ho (.inl h)
Proof state after:
no goals
Theorem: Reactor.set_preserves
Proof state before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
ho : rtr[Component.val c][i] = none
⊢ set rtr cpt vs[Component.val c][i] = none
Tactic:
exact Equivalent.obj?_none_iff set_equiv |>.mp ho
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.tag_le
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : Steps s₁ s₂
⊢ s₁.tag ≤ s₂.tag
Tactic:
induction e
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
⊢ s✝.tag ≤ s✝.tag

case step
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
a_ih✝ : s₂✝.tag ≤ s₃✝.tag
⊢ s₁✝.tag ≤ s₃✝.tag
Theorem: Execution.Grouped.Steps.tag_le
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
⊢ s✝.tag ≤ s✝.tag
Tactic:
case refl => rfl
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.tag_le
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
hi : s₂✝.tag ≤ s₃✝.tag
⊢ s₁✝.tag ≤ s₃✝.tag
Tactic:
case step e _ hi => exact le_trans e.tag_le hi
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.tag_le
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
⊢ s✝.tag ≤ s✝.tag
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.tag_le
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
hi : s₂✝.tag ≤ s₃✝.tag
⊢ s₁✝.tag ≤ s₃✝.tag
Tactic:
exact le_trans e.tag_le hi
Proof state after:
no goals