Theorem: Execution.to_grouped (ReactorModel/Execution/Theorems/Grouped/Basic.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
n : State.Nontrivial s₁
e : s₁ ⇓ s₂
⊢ Nonempty (Grouped s₁ s₂)
Tactic:
induction e <;> try cases ‹_ ↓ _›
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₃✝)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
⊢ Nonempty (Grouped s✝ s✝)
Tactic:
case refl => exact ⟨.refl, .none⟩
State after:
no goals

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
State after:
no goals

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⟩
State after:
no goals

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 ‹_ ↓ _›
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₃✝)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
⊢ Nonempty (Grouped s✝ s✝)
Tactic:
exact ⟨.refl, .none⟩
State after:
no goals

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
State after:
no goals

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⟩
State after:
no goals

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
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₃✝)

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⟩
State after:
no goals