internlm/Lean-Github huggingface dataset:
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
case trans.inl e e' h =>
  exists trans e e'
  simp [rcns, h]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
case trans.inr e e' h =>
  have h' := e'.rcns.erase_cons_tail <| by simp only [beq_iff_eq]; exact head_not_mem_tail e e' h
  exact h' ▸ cons_prepend_minimal e e' h hr
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hm : i ∈ rcns (trans a✝¹ a✝)
hr : rcns (trans a✝¹ a✝) ≮[s₁.rtr] i
⊢ ∃ e', rcns e' = i :: List.erase (rcns (trans a✝¹ a✝)) i
Tactic:
simp [rcns] at *
Proof state after:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i
Tactic:
try cases ‹_ ∨ _›
Proof state after:
case trans.inl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i = rcn a✝¹
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

case trans.inr
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i
Tactic:
cases ‹_ ∨ _›
Proof state after:
case trans.inl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i = rcn a✝¹
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

case trans.inr
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ ∃ e', rcns e' = i :: List.erase [rcn e] i
Tactic:
exists single e
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ rcns (single e) = i :: List.erase [rcn e] i
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ rcns (single e) = i :: List.erase [rcn e] i
Tactic:
simp [hm, rcns]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
exists trans e e'
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ rcns (trans e e') = i :: List.erase (rcn e :: rcns e') i
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ rcns (trans e e') = i :: List.erase (rcn e :: rcns e') i
Tactic:
simp [rcns, h]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
have h' := e'.rcns.erase_cons_tail <| by simp only [beq_iff_eq]; exact head_not_mem_tail e e' h
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
h' : List.erase (rcn e :: rcns e') i = rcn e :: List.erase (rcns e') i
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
h' : List.erase (rcn e :: rcns e') i = rcn e :: List.erase (rcns e') i
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
exact h' ▸ cons_prepend_minimal e e' h hr
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ¬(?m.91125 == ?m.91124) = true
Tactic:
simp only [beq_iff_eq]
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ¬?m.91125 = ?m.91124
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ¬?m.91125 = ?m.91124
Tactic:
exact head_not_mem_tail e e' h
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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₁
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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 ⊢
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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 _ _
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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'
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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₂
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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₂
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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₂'
Proof 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₂'
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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']
Proof 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₁)
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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
Proof 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
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof 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
Proof 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