internlm/Lean-Github huggingface dataset:
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 ne =>
  simp [Set.ext_iff]
  refine ⟨_, h₂, ?_⟩
  rw [iff_true_right $ s.rtr_eq ▸ h₁]
  exact a _
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
x : Component.idType Component.rcn
hx : x ∈ dependencies rtr w✝ ∧ x ∉ s.progress
⊢ x ∈ dependencies rtr i ∧ x ∉ s.progress
Tactic:
exact ⟨h.left hx.left, hx.right⟩
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
⊢ w✝ ∉ dependencies rtr w✝
Tactic:
exact a _
Proof state after:
no goals
Theorem: Execution.State.Over.forcing_not_closed
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s : State.Over rtr✝
rtr : α
rcn : ID
h : rcn ∈ rtr[Component.rcn]
⊢ ¬Closed (forcing rtr rcn).toState
Tactic:
simp [State.Closed, forcing]
Proof state after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s : State.Over rtr✝
rtr : α
rcn : ID
h : rcn ∈ rtr[Component.rcn]
⊢ rcn ∈ Partial.ids (rtr[Component.rcn])
Theorem: Execution.State.Over.forcing_not_closed
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s : State.Over rtr✝
rtr : α
rcn : ID
h : rcn ∈ rtr[Component.rcn]
⊢ rcn ∈ Partial.ids (rtr[Component.rcn])
Tactic:
exact h
Proof state after:
no goals
Theorem: Execution.State.Over.forcing_skip_step_rcn_eq
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₛ s
⊢ Step.Skip.rcn e = rcn
Tactic:
have h := e.allows_rcn.unprocessed
Proof state after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₛ s
h : Step.Skip.rcn e ∉ (forcing rtr rcn).progress
⊢ Step.Skip.rcn e = rcn
Theorem: Execution.State.Over.forcing_skip_step_rcn_eq
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₛ s
h : Step.Skip.rcn e ∉ (forcing rtr rcn).progress
⊢ Step.Skip.rcn e = rcn
Tactic:
simp [forcing] at h
Proof state after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₛ s
h : Step.Skip.rcn e ∈ Partial.ids (rtr[Component.rcn]) → Step.Skip.rcn e = rcn
⊢ Step.Skip.rcn e = rcn
Theorem: Execution.State.Over.forcing_skip_step_rcn_eq
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₛ s
h : Step.Skip.rcn e ∈ Partial.ids (rtr[Component.rcn]) → Step.Skip.rcn e = rcn
⊢ Step.Skip.rcn e = rcn
Tactic:
exact h e.allows_rcn.mem
Proof state after:
no goals
Theorem: Execution.State.Over.forcing_exec_step_rcn_eq
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
⊢ Step.Exec.rcn e = rcn
Tactic:
have h := e.allows_rcn.unprocessed
Proof state after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
h : Step.Exec.rcn e ∉ (forcing rtr rcn).progress
⊢ Step.Exec.rcn e = rcn
Theorem: Execution.State.Over.forcing_exec_step_rcn_eq
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
h : Step.Exec.rcn e ∉ (forcing rtr rcn).progress
⊢ Step.Exec.rcn e = rcn
Tactic:
simp [forcing] at h
Proof state after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
h : Step.Exec.rcn e ∈ Partial.ids (rtr[Component.rcn]) → Step.Exec.rcn e = rcn
⊢ Step.Exec.rcn e = rcn
Theorem: Execution.State.Over.forcing_exec_step_rcn_eq
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
h : Step.Exec.rcn e ∈ Partial.ids (rtr[Component.rcn]) → Step.Exec.rcn e = rcn
⊢ Step.Exec.rcn e = rcn
Tactic:
exact h e.allows_rcn.mem
Proof state after:
no goals
Theorem: Execution.Step.Time.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
⊢ s₁ = s₂
Tactic:
have hn := e₁.next_tag.deterministic e₂.next_tag
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
hn : s₁.tag = s₂.tag
⊢ s₁ = s₂
Theorem: Execution.Step.Time.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
hn : s₁.tag = s₂.tag
⊢ s₁ = s₂
Tactic:
have hr := hn ▸ e₁.refreshed |>.deterministic e₂.refreshed
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
hn : s₁.tag = s₂.tag
hr : s₁.rtr = s₂.rtr
⊢ s₁ = s₂
Theorem: Execution.Step.Time.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
hn : s₁.tag = s₂.tag
hr : s₁.rtr = s₂.rtr
⊢ s₁ = s₂
Tactic:
ext1 <;> simp [hn, hr, e₁.progress_empty, e₂.progress_empty, e₁.events_eq, e₂.events_eq]
Proof state after:
no goals
Theorem: Execution.Step.Skip.preserves_rtr
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.rtr = s₂.rtr
Tactic:
simp [e.dst_eq, State.record_preserves_rtr]
Proof state after:
no goals
Theorem: Execution.Step.Skip.preserves_tag
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.tag = s₂.tag
Tactic:
simp [e.dst_eq, State.record_preserves_tag]
Proof state after:
no goals
Theorem: Execution.Step.Skip.preserves_events
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.events = s₂.events
Tactic:
simp [e.dst_eq, State.record_preserves_events]
Proof state after:
no goals
Theorem: Execution.Step.Skip.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.rtr ≈ s₂.rtr
Tactic:
simp [e.dst_eq, State.record_preserves_rtr]
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.rtr ≈ s₁.rtr
Theorem: Execution.Step.Skip.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.rtr ≈ s₁.rtr
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Execution.Step.Skip.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₂.progress = Set.insert (rcn e) s₁.progress
Tactic:
simp [e.dst_eq, State.record_progress_eq]
Proof state after:
no goals
Theorem: Execution.Step.Skip.indep_allows_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₛ s₂
hi : i ≮[s₁.rtr]≯ rcn e
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
simp [e.dst_eq, Allows.iff_record_indep hi.symm]
Proof state after:
no goals
Theorem: Execution.Step.Skip.triggers_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₛ s₂
⊢ Triggers s₁ i ↔ Triggers s₂ i
Tactic:
simp [e.dst_eq, Triggers.iff_record (s := s₁) (i₁ := e.rcn)]
Proof state after:
no goals
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂ = s₂₁
Tactic:
ext1
Proof state after:
case rtr
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.rtr = s₂₁.rtr

case tag
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.tag = s₂₁.tag

case progress
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.progress = s₂₁.progress

case events
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.events = s₂₁.events
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.rtr = s₂₁.rtr
Tactic:
case rtr => 
  exact e₁₂.preserves_rtr ▸ e₁.preserves_rtr ▸ e₂₁.preserves_rtr ▸ e₂.preserves_rtr
Proof state after:
no goals
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.tag = s₂₁.tag
Tactic:
case tag => 
  exact e₁₂.preserves_tag ▸ e₁.preserves_tag ▸ e₂₁.preserves_tag ▸ e₂.preserves_tag
Proof state after:
no goals
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.events = s₂₁.events
Tactic:
case events => 
  exact e₁₂.preserves_events ▸ e₁.preserves_events ▸ e₂₁.preserves_events ▸ e₂.preserves_events
Proof state after:
no goals
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.progress = s₂₁.progress
Tactic:
case progress  =>
  have h₁ := e₁.progress_eq ▸ e₁₂.progress_eq
  have h₂ := e₂.progress_eq ▸ e₂₁.progress_eq
  rw [hr₁, hr₂] at *
  simp [h₁, h₂]
  apply Set.insert_comm
Proof state after:
no goals
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.rtr = s₂₁.rtr
Tactic:
exact e₁₂.preserves_rtr ▸ e₁.preserves_rtr ▸ e₂₁.preserves_rtr ▸ e₂.preserves_rtr
Proof state after:
no goals
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.tag = s₂₁.tag
Tactic:
exact e₁₂.preserves_tag ▸ e₁.preserves_tag ▸ e₂₁.preserves_tag ▸ e₂.preserves_tag
Proof state after:
no goals
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.events = s₂₁.events
Tactic:
exact e₁₂.preserves_events ▸ e₁.preserves_events ▸ e₂₁.preserves_events ▸ e₂.preserves_events
Proof state after:
no goals
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.progress = s₂₁.progress
Tactic:
have h₁ := e₁.progress_eq ▸ e₁₂.progress_eq
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Tactic:
have h₂ := e₂.progress_eq ▸ e₂₁.progress_eq
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Tactic:
rw [hr₁, hr₂] at *
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Tactic:
simp [h₁, h₂]
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress) = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
Theorem: Execution.Step.Skip.comm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress) = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
Tactic:
apply Set.insert_comm
Proof state after:
no goals
Theorem: Execution.Step.Skip.unprocessed_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ unprocessed s₂ = unprocessed s₁ \ {rcn e}
Tactic:
ext i
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
⊢ i ∈ unprocessed s₂ ↔ i ∈ unprocessed s₁ \ {rcn e}
Theorem: Execution.Step.Skip.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
⊢ i ∈ unprocessed s₂ ↔ i ∈ unprocessed s₁ \ {rcn e}
Tactic:
simp [State.unprocessed, Equivalent.obj?_rcn_eq e.equiv, and_assoc, e.progress_eq]
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
⊢ i ∈ s₂.rtr[Component.rcn] → (i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e)