internlm/Lean-Github huggingface dataset:
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.out)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.out)
ho₁ : rtr₁[Component.val Component.Valued.out][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.out][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
case out => injection (rf₁.outputs  ▸ ho₁) ▸ rf₂.outputs  ▸ ho₂
Proof state after:
no goals
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.stv)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.stv)
ho₁ : rtr₁[Component.val Component.Valued.stv][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.stv][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
injection (rf₁.eq_state ▸ ho₁) ▸ rf₂.eq_state ▸ ho₂
Proof state after:
no goals
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.act)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.act)
ho₁ : rtr₁[Component.val Component.Valued.act][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.act][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
injection (rf₁.acts     ▸ ho₁) ▸ rf₂.acts     ▸ ho₂
Proof state after:
no goals
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.inp)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.inp)
ho₁ : rtr₁[Component.val Component.Valued.inp][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.inp][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
injection (rf₁.inputs   ▸ ho₁) ▸ rf₂.inputs   ▸ ho₂
Proof state after:
no goals
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.out)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.out)
ho₁ : rtr₁[Component.val Component.Valued.out][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.out][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
injection (rf₁.outputs  ▸ ho₁) ▸ rf₂.outputs  ▸ ho₂
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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)
]
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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)]
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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
]
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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
]
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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
Proof state after:
no goals
Theorem: Reactor.refresh_correct
Proof 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 _ _]
Proof state after:
no goals
Theorem: Change.Targets.norm_not
Proof state before:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
⊢ cpt ≠ c ∨ i ≠ j
Tactic:
by_contra hc
Proof state after:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
hc : ¬(cpt ≠ c ∨ i ≠ j)
⊢ False
Theorem: Change.Targets.norm_not
Proof state before:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
hc : ¬(cpt ≠ c ∨ i ≠ j)
⊢ False
Tactic:
simp [not_or] at hc
Proof state after:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
hc : cpt = c ∧ i = j
⊢ False
Theorem: Change.Targets.norm_not
Proof state before:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
hc : cpt = c ∧ i = j
⊢ False
Tactic:
exact hc.left ▸ hc.right ▸ h $ .intro
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s
ht : s₁.tag = s₂.tag
hp : s₁.progress = s₂.progress
tl₁ : State α
steps₁ : Steps s tl₁
tail₁ : Tail tl₁ s₁
tl₂ : State α
steps₂ : Steps s tl₂
tail₂ : Tail tl₂ s₂
⊢ s₁ = s₂
Tactic:
replace ht : tl₁.tag = tl₂.tag := tail₁.preserves_tag ▸ ht ▸ tail₂.preserves_tag.symm
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s
hp : s₁.progress = s₂.progress
tl₁ : State α
steps₁ : Steps s tl₁
tail₁ : Tail tl₁ s₁
tl₂ : State α
steps₂ : Steps s tl₂
tail₂ : Tail tl₂ s₂
ht : tl₁.tag = tl₂.tag
⊢ s₁ = s₂
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s
hp : s₁.progress = s₂.progress
tl₁ : State α
steps₁ : Steps s tl₁
tail₁ : Tail tl₁ s₁
tl₂ : State α
steps₂ : Steps s tl₂
tail₂ : Tail tl₂ s₂
ht : tl₁.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
induction steps₁ <;> cases steps₂
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
tail₁ : Tail tl₂ s₁
ht : tl₂.tag = tl₂.tag
⊢ s₁ = s₂

case refl.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Step s✝ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
a✝ : Step tl₂ s₂✝
n : State.Nontrivial tl₂
⊢ s₁ = s₂

case step.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝¹ s₃✝ : State α
a✝³ : Step s₁✝ s₂✝¹
a✝² : Steps s₂✝¹ s₃✝
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
tail₁ : Tail tl₂ s₁
ht : tl₂.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
case refl.refl => exact tail₁.deterministic hp tail₂
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝¹ s₃✝ : State α
e₁ : Step s₁✝ s₂✝¹
a✝ : Steps s₂✝¹ s₃✝
hi : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
s₂✝ : State α
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ tl₂
⊢ s₁ = s₂
Tactic:
case step.step e₁ _ hi _ e₂ e₂' => 
  cases e₁.deterministic e₂
  exact hi (e₁.preserves_nontrivial n) tail₁ e₂' ht
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
case refl.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Step s✝ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
a✝ : Step tl₂ s₂✝
n : State.Nontrivial tl₂
⊢ s₁ = s₂
Tactic:
all_goals cases ‹Step _ _›
Proof state after:
case refl.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s✝ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case refl.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s✝ ↓ₜ s₂✝
⊢ s₁ = s₂

case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ₜ s₂✝
⊢ s₁ = s₂
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
e' : Steps s₂✝ tl₂
e : s✝ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
case refl.step.time e' e   => exact absurd ht $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
e' : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
case step.refl.time e' _ e => exact absurd ht.symm $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
case refl.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s✝ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
all_goals cases ‹Steps _ _›
Proof state after:
case refl.step.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
a✝ : s✝ ↓ᵢ| tl₂
⊢ s₁ = s₂

case refl.step.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ : State α
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₂✝ s₁ → Steps s₂✝ tl₂ → s₂✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₂✝ s₁
ht : s₂✝.tag = tl₂.tag
⊢ s₁ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₁ = s₂
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
e : s✝ ↓ᵢ| tl₂
⊢ s₁ = s₂
Tactic:
case refl.step.inst.refl e =>
  cases tail₂.closed_to_none e.closed
  cases tail₁
  case none   => exact absurd hp $ ne_of_ssubset e.progress_ssubset
  case some f => exact f.deterministic e.exec hp
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ : State α
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₂✝ s₁ → Steps s₂✝ tl₂ → s₂✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₂✝ s₁
ht : s₂✝.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
case step.refl.inst.refl e _  =>
  cases tail₁.closed_to_none e.closed
  cases tail₂
  case none   => exact absurd hp.symm $ ne_of_ssubset e.progress_ssubset
  case some f => exact e.exec.deterministic f hp
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
case refl.step.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₁ = s₂
Tactic:
all_goals cases ‹Step _ _›
Proof state after:
case refl.step.inst.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case refl.step.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂

case step.refl.inst.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ tl₂
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
case refl.step.inst.step.time e _ f' f => exact absurd ht $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
case step.refl.inst.step.time e _ f' f => exact absurd ht.symm $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ tl₂
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
case refl.step.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
case step.refl.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
tail₁ : Tail tl₂ s₁
ht : tl₂.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
exact tail₁.deterministic hp tail₂
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝¹ s₃✝ : State α
e₁ : Step s₁✝ s₂✝¹
a✝ : Steps s₂✝¹ s₃✝
hi : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
s₂✝ : State α
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ tl₂
⊢ s₁ = s₂
Tactic:
cases e₁.deterministic e₂
Proof state after:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝ s₃✝ : State α
e₁ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
hi : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ tl₂
⊢ s₁ = s₂
Theorem: Execution.Grouped.deterministic
Proof state before:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝ s₃✝ : State α
e₁ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
hi : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ tl₂
⊢ s₁ = s₂
Tactic:
exact hi (e₁.preserves_nontrivial n) tail₁ e₂' ht
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
a✝ : Step tl₂ s₂✝
n : State.Nontrivial tl₂
⊢ s₁ = s₂
Tactic:
cases ‹Step _ _›
Proof state after:
case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ₜ s₂✝
⊢ s₁ = s₂