internlm/Lean-Github huggingface dataset:
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : Steps s s₁
e₂ : Steps s s₂
n : State.Nontrivial s
ht : s₁.tag = s₂.tag
hp : s₁.progress = s₂.progress
⊢ s₁ = s₂
Tactic:
induction e₁ <;> cases e₂
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s₂
ht : s₂.tag = s₂.tag
hp : s₂.progress = s₂.progress
⊢ s₂ = s₂

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

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

case step.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ s₃✝ : State α
a✝³ : Step s₁✝ s₂✝¹
a✝² : Steps s₂✝¹ s₃✝
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
n : State.Nontrivial s₁✝
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s₃✝ = s₂
Theorem: Execution.Grouped.Steps.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
⊢ s₂ = s₂
Tactic:
case refl.refl => rfl
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ s₃✝ : State α
e₁ : Step s₁✝ s₂✝¹
a✝ : Steps s₂✝¹ s₃✝
hi : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
n : State.Nontrivial s₁✝
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
s₂✝ : State α
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ s₂
⊢ s₃✝ = s₂
Tactic:
case step.step e₁ _ hi _ e₂ e₂' => 
  exact hi (e₁.deterministic e₂ ▸ e₂') (e₁.preserves_nontrivial n) ht hp
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
case refl.step
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Step s✝ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s✝ = s₂

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

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

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

case step.refl.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
e' : Steps s₂✝ s₂
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.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
e' : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ₜ 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.Steps.deterministic
Proof state before:
case refl.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Steps s₂✝ s₂
a✝ : s✝ ↓ᵢ| s₂✝
⊢ s✝ = s₂

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

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

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

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

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| 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₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₂
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s✝ = s₂

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

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

case step.refl.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₂
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.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| 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.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₂
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.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| 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.Steps.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
⊢ s₂ = s₂
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ s₃✝ : State α
e₁ : Step s₁✝ s₂✝¹
a✝ : Steps s₂✝¹ s₃✝
hi : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
n : State.Nontrivial s₁✝
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
s₂✝ : State α
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ s₂
⊢ s₃✝ = s₂
Tactic:
exact hi (e₁.deterministic e₂ ▸ e₂') (e₁.preserves_nontrivial n) ht hp
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
a✝ : Step s₂ s₂✝
n : State.Nontrivial s₂
⊢ s₃✝ = s₂
Tactic:
cases ‹Step _ _›
Proof state after:
case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂

case step.refl.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
e' : Steps s₂✝ s₂
e : s✝ ↓ₜ s₂✝
⊢ s✝ = s₂
Tactic:
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.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
e' : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Tactic:
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.Steps.deterministic
Proof state before:
case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂
Tactic:
cases ‹Steps _ _›
Proof state after:
case step.refl.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ : State α
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₂✝.tag = s₂.tag → s₂✝.progress = s₂.progress → s₂✝ = s₂
ht : s₂✝.tag = s₂.tag
hp : s₂✝.progress = s₂.progress
⊢ s₂✝ = s₂

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

case step.refl.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₂
f : s₂✝¹ ↓ₜ s₂✝
⊢ s✝ = s₂
Tactic:
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.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Tactic:
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.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₂
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s✝ = s₂
Tactic:
exact e.nonrepeatable f |>.elim
Proof state after:
no goals
Theorem: Execution.Grouped.Steps.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂
Tactic:
exact e.nonrepeatable f |>.elim
Proof state after:
no goals
Theorem: Execution.State.input_congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i : ID
hr : autoParam (s₁.rtr = s₂.rtr) _auto✝
ht : autoParam (s₁.tag = s₂.tag) _auto✝
⊢ input s₁ i = input s₂ i
Tactic:
simp [input, input.restriction, hr, ht]
Proof state after:
no goals
Theorem: Execution.State.output_congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i : ID
hr : autoParam (s₁.rtr = s₂.rtr) _auto✝
ht : autoParam (s₁.tag = s₂.tag) _auto✝
⊢ output s₁ i = output s₂ i
Tactic:
simp [output, input_congr hr ht, hr]
Proof state after:
no goals
Theorem: Execution.State.record_comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
rcn₁ rcn₂ : ID
⊢ record (record s rcn₁) rcn₂ = record (record s rcn₂) rcn₁
Tactic:
simp [record]
Proof state after:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
rcn₁ rcn₂ : ID
⊢ Set.insert rcn₂ (Set.insert rcn₁ s.progress) = Set.insert rcn₁ (Set.insert rcn₂ s.progress)
Theorem: Execution.State.record_comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
rcn₁ rcn₂ : ID
⊢ Set.insert rcn₂ (Set.insert rcn₁ s.progress) = Set.insert rcn₁ (Set.insert rcn₂ s.progress)
Tactic:
apply Set.insert_comm
Proof state after:
no goals
Theorem: Execution.State.schedule_events_congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ s₁ s₂ : State α
i : ID
t : Time
v : Value
h : s₁.events = s₂.events
⊢ (schedule s₁ i t v).events = (schedule s₂ i t v).events
Tactic:
simp [schedule, h]
Proof state after:
no goals
Theorem: Execution.State.schedule_ne_comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
i₁ i₂ : ID
t₁ t₂ : Time
v₁ v₂ : Value
h : i₁ ≠ i₂
⊢ schedule (schedule s i₁ t₁ v₁) i₂ t₂ v₂ = schedule (schedule s i₂ t₂ v₂) i₁ t₁ v₁
Tactic:
simp [schedule]
Proof state after:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
i₁ i₂ : ID
t₁ t₂ : Time
v₁ v₂ : Value
h : i₁ ≠ i₂
⊢ (Partial.update (Partial.update s.events i₁ fun x => schedule.go x t₁ v₁) i₂ fun x => schedule.go x t₂ v₂) =
    Partial.update (Partial.update s.events i₂ fun x => schedule.go x t₂ v₂) i₁ fun x => schedule.go x t₁ v₁
Theorem: Execution.State.schedule_ne_comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
i₁ i₂ : ID
t₁ t₂ : Time
v₁ v₂ : Value
h : i₁ ≠ i₂
⊢ (Partial.update (Partial.update s.events i₁ fun x => schedule.go x t₁ v₁) i₂ fun x => schedule.go x t₂ v₂) =
    Partial.update (Partial.update s.events i₂ fun x => schedule.go x t₂ v₂) i₁ fun x => schedule.go x t₁ v₁
Tactic:
apply Partial.update_ne_comm _ h
Proof state after:
no goals
Theorem: Execution.State.Allows.congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
constructor <;> intro ⟨hm, hd, hu⟩
Proof state after:
case mp
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₁.rtr[Component.rcn]
hd : dependencies s₁.rtr i ⊆ s₁.progress
hu : i ∉ s₁.progress
⊢ Allows s₂ i

case mpr
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ Allows s₁ i
Theorem: Execution.State.Allows.congr
Proof state before:
case mp
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₁.rtr[Component.rcn]
hd : dependencies s₁.rtr i ⊆ s₁.progress
hu : i ∉ s₁.progress
⊢ Allows s₂ i

case mpr
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ Allows s₁ i
Tactic:
all_goals
  exact {
    mem := by first | exact Equivalent.mem_iff hr |>.mp hm | exact Equivalent.mem_iff hr |>.mpr hm
    deps := equiv_eq_dependencies hr ▸ hp ▸ hd
    unprocessed := hp ▸ hu
  }
Proof state after:
no goals
Theorem: Execution.State.Allows.congr
Proof state before:
case mpr
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ Allows s₁ i
Tactic:
exact {
  mem := by first | exact Equivalent.mem_iff hr |>.mp hm | exact Equivalent.mem_iff hr |>.mpr hm
  deps := equiv_eq_dependencies hr ▸ hp ▸ hd
  unprocessed := hp ▸ hu
}
Proof state after:
no goals
Theorem: Execution.State.Allows.congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ i ∈ s₁.rtr[Component.rcn]
Tactic:
first | exact Equivalent.mem_iff hr |>.mp hm | exact Equivalent.mem_iff hr |>.mpr hm
Proof state after:
no goals
Theorem: Execution.State.Allows.congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₁.rtr[Component.rcn]
hd : dependencies s₁.rtr i ⊆ s₁.progress
hu : i ∉ s₁.progress
⊢ i ∈ s₂.rtr[Component.rcn]
Tactic:
exact Equivalent.mem_iff hr |>.mp hm
Proof state after:
no goals
Theorem: Execution.State.Allows.congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ i ∈ s₁.rtr[Component.rcn]
Tactic:
exact Equivalent.mem_iff hr |>.mpr hm
Proof state after:
no goals
Theorem: Execution.State.Allows.iff_record_indep
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ Allows s i₂ ↔ Allows (record s i₁) i₂
Tactic:
simp [record, Allows.def]
Proof state after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ i₂ ∈ s.rtr[Component.rcn] →
    (dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
      dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress)