internlm/Lean-Github huggingface dataset:
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:
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:
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 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:
cases ‹Steps _ _›
Proof state after:
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:
cases tail₂.closed_to_none e.closed
Proof state after:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
⊢ s₁ = s₂
Theorem: Execution.Grouped.deterministic
Proof state before:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
⊢ s₁ = s₂
Tactic:
cases tail₁
Proof state after:
case refl.none
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ : State α
tail₂ : Tail s₂ s₂
n : State.Nontrivial s₁
ht : s₁.tag = s₂.tag
e : s₁ ↓ᵢ| s₂
⊢ s₁ = s₂

case refl.some
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : 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₁ : State α
tail₂ : Tail s₂ s₂
n : State.Nontrivial s₁
ht : s₁.tag = s₂.tag
e : s₁ ↓ᵢ| s₂
⊢ s₁ = s₂
Tactic:
case none   => exact absurd hp $ ne_of_ssubset e.progress_ssubset
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₁ s✝ : State α
n : State.Nontrivial s✝
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
f : s✝ ↓ᵢ+ s₁
⊢ s₁ = s₂
Tactic:
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₁ : State α
tail₂ : Tail s₂ s₂
n : State.Nontrivial s₁
ht : s₁.tag = s₂.tag
e : s₁ ↓ᵢ| s₂
⊢ s₁ = s₂
Tactic:
exact absurd hp $ ne_of_ssubset e.progress_ssubset
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₁ s✝ : State α
n : State.Nontrivial s✝
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
f : s✝ ↓ᵢ+ s₁
⊢ s₁ = s₂
Tactic:
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:
cases tail₁.closed_to_none e.closed
Proof state after:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
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₂
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₂
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:
cases tail₂
Proof state after:
case refl.none
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ : State α
tail₁ : Tail s₁ s₁
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ s₂ → s₁.tag = s₂.tag → s₁ = s₂
ht : s₁.tag = s₂.tag
⊢ s₁ = s₂

case refl.some
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : 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
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₁ : State α
tail₁ : Tail s₁ s₁
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ s₂ → s₁.tag = s₂.tag → s₁ = s₂
ht : s₁.tag = s₂.tag
⊢ s₁ = s₂
Tactic:
case none   => exact absurd hp.symm $ ne_of_ssubset e.progress_ssubset
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 α
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
f : tl₂ ↓ᵢ+ s₂
⊢ s₁ = s₂
Tactic:
case some f => exact e.exec.deterministic f 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₁ : State α
tail₁ : Tail s₁ s₁
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ s₂ → s₁.tag = s₂.tag → s₁ = s₂
ht : s₁.tag = s₂.tag
⊢ s₁ = s₂
Tactic:
exact absurd hp.symm $ ne_of_ssubset e.progress_ssubset
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 α
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
f : tl₂ ↓ᵢ+ s₂
⊢ s₁ = s₂
Tactic:
exact e.exec.deterministic f hp
Proof state after:
no goals
Theorem: Execution.Grouped.deterministic
Proof state before:
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:
cases ‹Step _ _›
Proof state after:
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:
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:
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:
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:
exact e.nonrepeatable f |>.elim
Proof state after:
no goals
Theorem: Execution.to_grouped
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
n : State.Nontrivial s₁
e : s₁ ⇓ s₂
⊢ Nonempty (Grouped s₁ s₂)
Tactic:
induction e <;> try cases ‹_ ↓ _›
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
⊢ Nonempty (Grouped s✝ s✝)

case trans.skip
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)

case trans.exec
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)

case trans.time
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
t✝ : s₁✝ ↓ₜ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Theorem: Execution.to_grouped
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
⊢ Nonempty (Grouped s✝ s✝)
Tactic:
case refl => exact ⟨.refl, .none⟩
Proof state after:
no goals
Theorem: Execution.to_grouped
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e : s₁✝ ↓ₜ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Tactic:
case trans.time hi e => 
  exact match hi $ e.preserves_nontrivial n with
  | ⟨.refl, tl⟩              => ⟨.step e .refl, tl⟩ 
  | ⟨.step (.inst f) f', tl⟩ => ⟨.step (.time e) $ .step f f', tl⟩
  | ⟨.step (.time f) _, _⟩   => e.nonrepeatable f n |>.elim
Proof state after:
no goals
Theorem: Execution.to_grouped
Proof state before:
case trans.skip
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)

case trans.exec
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Tactic:
all_goals
  case _ hi e =>
    let ⟨steps, tail⟩ := hi $ e.preserves_nontrivial n
    exact match steps, tail with
    | .refl,                   .none    => ⟨.refl, .some $ .single e⟩ 
    | .refl,                   .some e' => ⟨.refl, .some $ .trans e e'⟩
    | .step (.inst ⟨f, h⟩) f', tl       => ⟨.step (.inst ⟨.trans e f, h⟩) f', tl⟩
    | .step (.time f) f',      tl       => ⟨.step (.inst ⟨.single e, f.closed⟩) $ .step f f', tl⟩
Proof state after:
no goals
Theorem: Execution.to_grouped
Proof state before:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ s₂✝
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Tactic:
cases ‹_ ↓ _›
Proof state after:
case trans.skip
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)

case trans.exec
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)

case trans.time
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
t✝ : s₁✝ ↓ₜ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Theorem: Execution.to_grouped
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
⊢ Nonempty (Grouped s✝ s✝)
Tactic:
exact ⟨.refl, .none⟩
Proof state after:
no goals
Theorem: Execution.to_grouped
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e : s₁✝ ↓ₜ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Tactic:
exact match hi $ e.preserves_nontrivial n with
| ⟨.refl, tl⟩              => ⟨.step e .refl, tl⟩ 
| ⟨.step (.inst f) f', tl⟩ => ⟨.step (.time e) $ .step f f', tl⟩
| ⟨.step (.time f) _, _⟩   => e.nonrepeatable f n |>.elim
Proof state after:
no goals
Theorem: Execution.to_grouped
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e : s₁✝ ↓ₑ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Tactic:
case _ hi e =>
  let ⟨steps, tail⟩ := hi $ e.preserves_nontrivial n
  exact match steps, tail with
  | .refl,                   .none    => ⟨.refl, .some $ .single e⟩ 
  | .refl,                   .some e' => ⟨.refl, .some $ .trans e e'⟩
  | .step (.inst ⟨f, h⟩) f', tl       => ⟨.step (.inst ⟨.trans e f, h⟩) f', tl⟩
  | .step (.time f) f',      tl       => ⟨.step (.inst ⟨.single e, f.closed⟩) $ .step f f', tl⟩
Proof state after:
no goals
Theorem: Execution.to_grouped
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e : s₁✝ ↓ₑ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Tactic:
let ⟨steps, tail⟩ := hi $ e.preserves_nontrivial n
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e : s₁✝ ↓ₑ s₂✝
tl✝ : State α
steps : Grouped.Steps s₂✝ tl✝
tail : Grouped.Tail tl✝ s₃✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Theorem: Execution.to_grouped
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e : s₁✝ ↓ₑ s₂✝
tl✝ : State α
steps : Grouped.Steps s₂✝ tl✝
tail : Grouped.Tail tl✝ s₃✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
Tactic:
exact match steps, tail with
| .refl,                   .none    => ⟨.refl, .some $ .single e⟩ 
| .refl,                   .some e' => ⟨.refl, .some $ .trans e e'⟩
| .step (.inst ⟨f, h⟩) f', tl       => ⟨.step (.inst ⟨.trans e f, h⟩) f', tl⟩
| .step (.time f) f',      tl       => ⟨.step (.inst ⟨.single e, f.closed⟩) $ .step f f', tl⟩
Proof state after:
no goals
Theorem: Execution.State.Over.exists_unprocessed_of_not_closed
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr rtr₁ : α
s : State.Over rtr
hc : ¬Closed s.toState
⊢ ∃ i ∈ s.rtr[Component.rcn], i ∉ s.progress
Tactic:
have ⟨i, _, _⟩ := Set.exists_of_ssubset $ s.progress_ssubset_of_not_closed hc
Proof state after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr rtr₁ : α
s : State.Over rtr
hc : ¬Closed s.toState
i : ID
left✝ : i ∈ Partial.ids (s.rtr[Component.rcn])
right✝ : i ∉ s.progress
⊢ ∃ i ∈ s.rtr[Component.rcn], i ∉ s.progress
Theorem: Execution.State.Over.exists_unprocessed_of_not_closed
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr rtr₁ : α
s : State.Over rtr
hc : ¬Closed s.toState
i : ID
left✝ : i ∈ Partial.ids (s.rtr[Component.rcn])
right✝ : i ∉ s.progress
⊢ ∃ i ∈ s.rtr[Component.rcn], i ∉ s.progress
Tactic:
exists i
Proof state after:
no goals
Theorem: Execution.State.Over.exists_allowed_of_acyclic_has_unprocessed
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr : α
s : State.Over rtr
_x✝ :
  (i : Component.idType Component.rcn) ×'
    (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝⁴ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y _x✝ →
      ∃ i, Allows s.toState i
i : Component.idType Component.rcn
a✝³ : (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝² :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := a✝³ } →
      ∃ i, Allows s.toState i
a : Dependency.Acyclic rtr
h₁✝¹ : (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝¹ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := h₁✝¹ } } →
      ∃ i, Allows s.toState i
h₁✝ : i ∈ s.rtr[Component.rcn]
h₂✝ : i ∉ s.progress
a✝ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := { fst := h₁✝, snd := h₂✝ } } } →
      ∃ i, Allows s.toState i
h✝ : ¬dependencies s.rtr i \ s.progress = ∅
w✝ : ID
hd : w✝ ∈ dependencies s.rtr i \ s.progress
h₁ : w✝ ∈ dependencies s.rtr i
h₂ : w✝ ∉ s.progress
h : dependencies rtr w✝ ⊆ dependencies rtr i ∧ ¬dependencies rtr w✝ = dependencies rtr i
⊢ dependencies rtr w✝ \ s.progress ⊆ dependencies rtr i \ s.progress
Tactic:
case subset =>
  intro x hx
  simp [Set.mem_diff] at hx ⊢
  exact ⟨h.left hx.left, hx.right⟩
Proof state after:
no goals