internlm/Lean-Github huggingface dataset:
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hm : i ∈ rcns e'
hr : rcn e :: rcns e' ≮[s₁.rtr] i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcns e') i
Tactic:
induction e' generalizing s₁ <;> simp [rcns] at *
Proof state after:
case single
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn a✝] ≮[s₁.rtr] i
hm : i = rcn a✝
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn a✝] i

case trans
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂✝),
    i ∈ rcns a✝ → (rcn e :: rcns a✝ ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns a✝) i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn a✝¹ :: rcns a✝) i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn e'] i
Tactic:
case single e' =>
  have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' $ hm ▸ hr.cons_head
  exists trans f (single f')
  simp [hm, rcns, ←hf₁, ←hf₂]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i = rcn e' ∨ i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
case trans s₁ s₂ s₄ e' e'' hi =>
  cases hm
  case inl hm =>
    simp [hm] at hr
    have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' hr.cons_head
    exists trans f $ trans f' e''
    simp [hm, rcns, ←hf₁, ←hf₂]
  case inr hm =>
    have ⟨f, hf⟩ :=  hi e' hm $ hr.cons_tail.equiv e.equiv
    cases f <;> simp [rcns] at hf
    case trans f f'' =>
      have ⟨h₁, h₂⟩ := hf
      have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
      exists trans f $ trans f' f''
      have h₃ := e''.rcns.erase_cons_tail <| by
        simp only [beq_iff_eq]; exact head_not_mem_tail e' e'' hm
      simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn e'] i
Tactic:
have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' $ hm ▸ hr.cons_head
Proof state after:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn e'] i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn e'] i
Tactic:
exists trans f (single f')
Proof state after:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (single f')) = i :: rcn e :: List.erase [rcn e'] i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (single f')) = i :: rcn e :: List.erase [rcn e'] i
Tactic:
simp [hm, rcns, ←hf₁, ←hf₂]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i = rcn e' ∨ i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
cases hm
Proof state after:
case inl
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
h✝ : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

case inr
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
h✝ : i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
case inl hm =>
  simp [hm] at hr
  have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' hr.cons_head
  exists trans f $ trans f' e''
  simp [hm, rcns, ←hf₁, ←hf₂]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
case inr hm =>
  have ⟨f, hf⟩ :=  hi e' hm $ hr.cons_tail.equiv e.equiv
  cases f <;> simp [rcns] at hf
  case trans f f'' =>
    have ⟨h₁, h₂⟩ := hf
    have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
    exists trans f $ trans f' f''
    have h₃ := e''.rcns.erase_cons_tail <| by
      simp only [beq_iff_eq]; exact head_not_mem_tail e' e'' hm
    simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
simp [hm] at hr
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' hr.cons_head
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
exists trans f $ trans f' e''
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (trans f' e'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (trans f' e'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
simp [hm, rcns, ←hf₁, ←hf₂]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
have ⟨f, hf⟩ :=  hi e' hm $ hr.cons_tail.equiv e.equiv
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
f : s₁✝ ↓ᵢ+ s₄
hf : rcns f = i :: rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
f : s₁✝ ↓ᵢ+ s₄
hf : rcns f = i :: rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
cases f <;> simp [rcns] at hf
Proof state after:
case trans
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₄
hf : rcn a✝¹ = i ∧ rcns a✝ = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
case trans f f'' =>
  have ⟨h₁, h₂⟩ := hf
  have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
  exists trans f $ trans f' f''
  have h₃ := e''.rcns.erase_cons_tail <| by
    simp only [beq_iff_eq]; exact head_not_mem_tail e' e'' hm
  simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
have ⟨h₁, h₂⟩ := hf
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
exists trans f $ trans f' f''
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (trans f' f'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (trans f' f'')) = i :: rcn e :: 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'' hm
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
h₃ : List.erase (rcn e' :: rcns e'') i = rcn e' :: List.erase (rcns e'') i
⊢ rcns (trans f (trans f' f'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
h₃ : List.erase (rcn e' :: rcns e'') i = rcn e' :: List.erase (rcns e'') i
⊢ rcns (trans f (trans f' f'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ¬(?m.81182 == ?m.81181) = true
Tactic:
simp only [beq_iff_eq]
Proof state after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ¬?m.81182 = ?m.81181
Theorem: Execution.Instantaneous.Step.TC.cons_prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ¬?m.81182 = ?m.81181
Tactic:
exact head_not_mem_tail e' e'' hm
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.prepend_minimal
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ+ s₂
hm : i ∈ rcns e
hr : rcns e ≮[s₁.rtr] i
⊢ ∃ e', rcns e' = i :: List.erase (rcns e) i
Tactic:
cases e <;> (simp [rcns] at *; try cases ‹_ ∨ _›)
Proof state after:
case single
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
a✝ : s₁ ↓ᵢ s₂
hr : [rcn a✝] ≮[s₁.rtr] i
hm : i = rcn a✝
⊢ ∃ e', rcns e' = i :: List.erase [rcn a✝] i

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:
case single e =>
  exists single e
  simp [hm, rcns]
Proof state after:
no goals