Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : rcns e₁ ~ rcns e₂
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
induction e₁
State after:
case single
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
e₂ : s₁✝ ↓ᵢ+ s₂
hp : rcns (single a✝) ~ rcns e₂
⊢ s₂✝.rtr = s₂.rtr ∧ s₂✝.events = s₂.events

case trans
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : ∀ (e₂ : s₂✝ ↓ᵢ+ s₂), rcns a✝ ~ rcns e₂ → s₃✝.rtr = s₂.rtr ∧ s₃✝.events = s₂.events
e₂ : s₁✝ ↓ᵢ+ s₂
hp : rcns (trans a✝¹ a✝) ~ rcns e₂
⊢ s₃✝.rtr = s₂.rtr ∧ s₃✝.events = s₂.events

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e₂ : s₁✝ ↓ᵢ+ s₂
hp : rcns (single e) ~ rcns e₂
⊢ s₂✝.rtr = s₂.rtr ∧ s₂✝.events = s₂.events
Tactic:
case single e =>
  cases e₂ <;> simp [rcns] at hp ⊢
  case single e' => simp [e.deterministic e' hp]
  case trans e'  => exact absurd rfl (hp.right ▸ e'.rcns_ne_nil)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
case trans s sₘ₁ s₁ e₁ e₁' hi =>
  have hm := hp.mem_iff.mp $ List.mem_cons_self _ _
  have hm' := e₁'.head_minimal e₁ |>.perm hp
  have ⟨e₂, he₂⟩ := e₂.prepend_minimal hm hm'
  cases e₂ <;> simp [rcns] at he₂
  case trans sₘ₂ e₂ e₂' =>
    have ⟨h, h'⟩ := he₂
    cases e₁.deterministic e₂ h.symm
    apply hi e₂'
    rw [h']
    exact List.perm_cons _ |>.mp (hp.trans $ List.perm_cons_erase hm)
  case single =>
    exfalso
    simp [rcns] at hp
    have ⟨hd, tl, h⟩ := e₂.rcns_cons
    have ⟨_, _, h'⟩ := e₁'.rcns_cons
    simp [h, h'] at hp he₂
    have h := he₂.right.symm ▸ List.erase_cons e₁.rcn hd tl
    split at h <;> try assumption
    simp [←h] at hp
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e₂ : s₁✝ ↓ᵢ+ s₂
hp : rcns (single e) ~ rcns e₂
⊢ s₂✝.rtr = s₂.rtr ∧ s₂✝.events = s₂.events
Tactic:
cases e₂ <;> simp [rcns] at hp ⊢
State after:
case single
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₁✝ ↓ᵢ s₂
hp : rcn e = rcn a✝
⊢ s₂✝.rtr = s₂.rtr ∧ s₂✝.events = s₂.events

case trans
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ : State α
e : s₁✝ ↓ᵢ s₂✝¹
s₂✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hp : rcn e = rcn a✝¹ ∧ [] = rcns a✝
⊢ s₂✝¹.rtr = s₂.rtr ∧ s₂✝¹.events = s₂.events

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₁✝ ↓ᵢ s₂
hp : rcn e = rcn e'
⊢ s₂✝.rtr = s₂.rtr ∧ s₂✝.events = s₂.events
Tactic:
case single e' => simp [e.deterministic e' hp]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ : State α
e : s₁✝ ↓ᵢ s₂✝¹
s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hp : rcn e = rcn a✝ ∧ [] = rcns e'
⊢ s₂✝¹.rtr = s₂.rtr ∧ s₂✝¹.events = s₂.events
Tactic:
case trans e'  => exact absurd rfl (hp.right ▸ e'.rcns_ne_nil)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₁✝ ↓ᵢ s₂
hp : rcn e = rcn e'
⊢ s₂✝.rtr = s₂.rtr ∧ s₂✝.events = s₂.events
Tactic:
simp [e.deterministic e' hp]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ : State α
e : s₁✝ ↓ᵢ s₂✝¹
s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hp : rcn e = rcn a✝ ∧ [] = rcns e'
⊢ s₂✝¹.rtr = s₂.rtr ∧ s₂✝¹.events = s₂.events
Tactic:
exact absurd rfl (hp.right ▸ e'.rcns_ne_nil)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
have hm := hp.mem_iff.mp $ List.mem_cons_self _ _
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
have hm' := e₁'.head_minimal e₁ |>.perm hp
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
have ⟨e₂, he₂⟩ := e₂.prepend_minimal hm hm'
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
e₂ : s ↓ᵢ+ s₂
he₂ : rcns e₂ = rcn e₁ :: List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
e₂ : s ↓ᵢ+ s₂
he₂ : rcns e₂ = rcn e₁ :: List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
cases e₂ <;> simp [rcns] at he₂
State after:
case single
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events

case trans
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
s₂✝ : State α
a✝¹ : s ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
he₂ : rcn a✝¹ = rcn e₁ ∧ rcns a✝ = List.erase (rcns e₂) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
sₘ₂ : State α
e₂ : s ↓ᵢ sₘ₂
e₂' : sₘ₂ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
case trans sₘ₂ e₂ e₂' =>
  have ⟨h, h'⟩ := he₂
  cases e₁.deterministic e₂ h.symm
  apply hi e₂'
  rw [h']
  exact List.perm_cons _ |>.mp (hp.trans $ List.perm_cons_erase hm)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
case single =>
  exfalso
  simp [rcns] at hp
  have ⟨hd, tl, h⟩ := e₂.rcns_cons
  have ⟨_, _, h'⟩ := e₁'.rcns_cons
  simp [h, h'] at hp he₂
  have h := he₂.right.symm ▸ List.erase_cons e₁.rcn hd tl
  split at h <;> try assumption
  simp [←h] at hp
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
sₘ₂ : State α
e₂ : s ↓ᵢ sₘ₂
e₂' : sₘ₂ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
have ⟨h, h'⟩ := he₂
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
sₘ₂ : State α
e₂ : s ↓ᵢ sₘ₂
e₂' : sₘ₂ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
h : rcn e₂ = rcn e₁
h' : rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
sₘ₂ : State α
e₂ : s ↓ᵢ sₘ₂
e₂' : sₘ₂ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
h : rcn e₂ = rcn e₁
h' : rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
cases e₁.deterministic e₂ h.symm
State after:
case refl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
e₂ : s ↓ᵢ sₘ₁
e₂' : sₘ₁ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
h : rcn e₂ = rcn e₁
h' : rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events

State before:
case refl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
e₂ : s ↓ᵢ sₘ₁
e₂' : sₘ₁ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
h : rcn e₂ = rcn e₁
h' : rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
apply hi e₂'
State after:
case refl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
e₂ : s ↓ᵢ sₘ₁
e₂' : sₘ₁ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
h : rcn e₂ = rcn e₁
h' : rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ rcns e₁' ~ rcns e₂'

State before:
case refl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
e₂ : s ↓ᵢ sₘ₁
e₂' : sₘ₁ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
h : rcn e₂ = rcn e₁
h' : rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ rcns e₁' ~ rcns e₂'
Tactic:
rw [h']
State after:
case refl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
e₂ : s ↓ᵢ sₘ₁
e₂' : sₘ₁ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
h : rcn e₂ = rcn e₁
h' : rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ rcns e₁' ~ List.erase (rcns e₂✝) (rcn e₁)

State before:
case refl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂✝ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
e₂ : s ↓ᵢ sₘ₁
e₂' : sₘ₁ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
h : rcn e₂ = rcn e₁
h' : rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ rcns e₁' ~ List.erase (rcns e₂✝) (rcn e₁)
Tactic:
exact List.perm_cons _ |>.mp (hp.trans $ List.perm_cons_erase hm)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
Tactic:
exfalso
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
⊢ False
Tactic:
simp [rcns] at hp
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
⊢ False
Tactic:
have ⟨hd, tl, h⟩ := e₂.rcns_cons
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
⊢ False
Tactic:
have ⟨_, _, h'⟩ := e₁'.rcns_cons
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
⊢ False
Tactic:
simp [h, h'] at hp he₂
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
⊢ False
Tactic:
have h := he₂.right.symm ▸ List.erase_cons e₁.rcn hd tl
State after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h : [] = if (hd == rcn e₁) = true then tl else hd :: List.erase tl (rcn e₁)
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h : [] = if (hd == rcn e₁) = true then tl else hd :: List.erase tl (rcn e₁)
⊢ False
Tactic:
split at h <;> try assumption
State after:
case inl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝¹ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h✝ : (hd == rcn e₁) = true
h : [] = tl
⊢ False

State before:
case inl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝¹ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h✝ : (hd == rcn e₁) = true
h : [] = tl
⊢ False
Tactic:
simp [←h] at hp
State after:
no goals

State before:
case inr
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝¹ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h✝ : ¬(hd == rcn e₁) = true
h : False
⊢ False
Tactic:
assumption
State after:
no goals