internlm/Lean-Github huggingface dataset:
Theorem: Execution.Instantaneous.Step.seq_wellordered
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
d : rcn e₂ <[s₁.rtr] rcn e₁
⊢ False
Tactic:
exact e₂.allows_rcn.unprocessed $ e₁.progress_monotonic $ e₁.allows_rcn.deps d
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.seq_rcn_ne
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
⊢ rcn e₁ ≠ rcn e₂
Tactic:
by_contra he
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
he : rcn e₁ = rcn e₂
⊢ False
Theorem: Execution.Instantaneous.Step.seq_rcn_ne
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
he : rcn e₁ = rcn e₂
⊢ False
Tactic:
exact e₂.allows_rcn.unprocessed (he ▸ e₁.rcn_mem_progress)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ᵢ s₁
e₂ : s ↓ᵢ s₂
h : rcn e₁ = rcn e₂
⊢ s₁ = s₂
Tactic:
cases e₁ <;> cases e₂ <;> simp [rcn] at h
Proof state after:
case skip.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
s✝¹ : s ↓ₛ s₁
s✝ : s ↓ₛ s₂
h : Step.Skip.rcn s✝¹ = Step.Skip.rcn s✝
⊢ s₁ = s₂

case skip.exec
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
s✝ : s ↓ₛ s₁
e✝ : s ↓ₑ s₂
h : Step.Skip.rcn s✝ = Step.Exec.rcn e✝
⊢ s₁ = s₂

case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
⊢ s₁ = s₂

case exec.exec
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝¹ : s ↓ₑ s₁
e✝ : s ↓ₑ s₂
h : Step.Exec.rcn e✝¹ = Step.Exec.rcn e✝
⊢ s₁ = s₂
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₛ s₁
e₂ : s ↓ₛ s₂
h : Step.Skip.rcn e₁ = Step.Skip.rcn e₂
⊢ s₁ = s₂
Tactic:
case skip.skip e₁ e₂ => simp [e₁.dst_eq, e₂.dst_eq, h]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₑ s₁
e₂ : s ↓ₑ s₂
h : Step.Exec.rcn e₁ = Step.Exec.rcn e₂
⊢ s₁ = s₂
Tactic:
case exec.exec e₁ e₂ => simp [e₁.dst_eq, e₂.dst_eq, h, e₁.apply.deterministic (h.symm ▸ e₂.apply)]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
case skip.exec
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
s✝ : s ↓ₛ s₁
e✝ : s ↓ₑ s₂
h : Step.Skip.rcn s✝ = Step.Exec.rcn e✝
⊢ s₁ = s₂

case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
⊢ s₁ = s₂
Tactic:
all_goals
  have := ‹_ ↓ₛ _›.not_triggers_rcn
  have := ‹_ ↓ₑ _›.triggers_rcn
  simp_all
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₛ s₁
e₂ : s ↓ₛ s₂
h : Step.Skip.rcn e₁ = Step.Skip.rcn e₂
⊢ s₁ = s₂
Tactic:
simp [e₁.dst_eq, e₂.dst_eq, h]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₑ s₁
e₂ : s ↓ₑ s₂
h : Step.Exec.rcn e₁ = Step.Exec.rcn e₂
⊢ s₁ = s₂
Tactic:
simp [e₁.dst_eq, e₂.dst_eq, h, e₁.apply.deterministic (h.symm ▸ e₂.apply)]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
⊢ s₁ = s₂
Tactic:
have := ‹_ ↓ₛ _›.not_triggers_rcn
Proof state after:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
this : ¬State.Triggers s (Step.Skip.rcn s✝)
⊢ s₁ = s₂
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
this : ¬State.Triggers s (Step.Skip.rcn s✝)
⊢ s₁ = s₂
Tactic:
have := ‹_ ↓ₑ _›.triggers_rcn
Proof state after:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
this✝ : ¬State.Triggers s (Step.Skip.rcn s✝)
this : State.Triggers s (Step.Exec.rcn e✝)
⊢ s₁ = s₂
Theorem: Execution.Instantaneous.Step.deterministic
Proof state before:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
this✝ : ¬State.Triggers s (Step.Skip.rcn s✝)
this : State.Triggers s (Step.Exec.rcn e✝)
⊢ s₁ = s₂
Tactic:
simp_all
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr] rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃
Tactic:
replace h : _ ≮[_]≯ _ := { not_eq := e₁.seq_rcn_ne e₂, left := h, right := e₁.seq_wellordered e₂ }
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr]≯ rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr]≯ rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃
Tactic:
cases e₁ <;> cases e₂
Proof state after:
case skip.skip
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
s✝¹ : s₁ ↓ₛ s₂
s✝ : s₂ ↓ₛ s₃
h : rcn (skip s✝¹) ≮[s₁.rtr]≯ rcn (skip s✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip s✝) ∧ rcn e₂' = rcn (skip s✝¹) ∧ s₃' = s₃

case skip.exec
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
s✝ : s₁ ↓ₛ s₂
e✝ : s₂ ↓ₑ s₃
h : rcn (skip s✝) ≮[s₁.rtr]≯ rcn (exec e✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e✝) ∧ rcn e₂' = rcn (skip s✝) ∧ s₃' = s₃

case exec.skip
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e✝ : s₁ ↓ₑ s₂
s✝ : s₂ ↓ₛ s₃
h : rcn (exec e✝) ≮[s₁.rtr]≯ rcn (skip s✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip s✝) ∧ rcn e₂' = rcn (exec e✝) ∧ s₃' = s₃

case exec.exec
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e✝¹ : s₁ ↓ₑ s₂
e✝ : s₂ ↓ₑ s₃
h : rcn (exec e✝¹) ≮[s₁.rtr]≯ rcn (exec e✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e✝) ∧ rcn e₂' = rcn (exec e✝¹) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
case skip.skip e₁ e₂ =>
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.triggers_iff.not.mpr e₂.not_triggers_rcn
  let s₂' := s₁.record e₂.rcn
  let f₁ : s₁ ↓ₛ s₂' := ⟨ha₁, ht₁⟩
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.triggers_iff.not.mp e₁.not_triggers_rcn
  let s₃' := s₂'.record e₁.rcn
  let f₂ : s₂' ↓ₛ s₃' := ⟨ha₂, ht₂⟩
  refine ⟨_, _, .skip f₁, .skip f₂, rfl, rfl, ?_⟩
  exact Step.Skip.comm e₁ e₂ f₁ f₂ rfl rfl |>.symm
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
case skip.exec e₁ e₂ =>
  have ⟨z₂, a₁⟩ := Step.Apply.RTC.construct s₁ (s₁.output e₂.rcn)
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.triggers_iff.mpr e₂.triggers_rcn
  let s₂' := z₂.record e₂.rcn
  let f₁ : s₁ ↓ₑ s₂' := ⟨ha₁, ht₁, a₁⟩
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.indep_triggers_iff h |>.not.mp e₁.not_triggers_rcn
  let s₃' := s₂'.record e₁.rcn
  let f₂ : s₂' ↓ₛ s₃' := ⟨ha₂, ht₂⟩
  refine ⟨_, _, .exec f₁, .skip f₂, rfl, rfl, ?_⟩
  simp [e₂.dst_eq, f₂.dst_eq]
  rw [State.record_comm]
  congr!
  have a₂ := e₂.apply
  simp [e₁.dst_eq] at a₂
  exact a₁.comm_record a₂
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
case exec.skip e₁ e₂ =>
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.indep_triggers_iff h.symm |>.not.mpr e₂.not_triggers_rcn
  let s₂' := s₁.record e₂.rcn
  let f₁ : s₁ ↓ₛ s₂' := ⟨ha₁, ht₁⟩
  have ⟨z₃, a₂⟩ := Step.Apply.RTC.construct s₂' (s₂'.output e₁.rcn)
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.triggers_iff.mp e₁.triggers_rcn
  let s₃' := z₃.record e₁.rcn
  let f₂ : s₂' ↓ₑ s₃' := ⟨ha₂, ht₂, a₂⟩
  refine ⟨_, _, .skip f₁, .exec f₂, rfl, rfl, ?_⟩
  simp [e₂.dst_eq, e₁.dst_eq]
  rw [State.record_comm]
  congr!
  have a₁ := e₁.apply
  rw [s₁.record_preserves_output] at a₂
  exact a₁.comm_record a₂ |>.symm
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
case exec.exec e₁ e₂ =>
  have ⟨z₂, a₁⟩ := Step.Apply.RTC.construct s₁ (s₁.output e₂.rcn)
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.indep_triggers_iff h.symm |>.mpr e₂.triggers_rcn
  let s₂' := z₂.record e₂.rcn
  let f₁ : s₁ ↓ₑ s₂' := ⟨ha₁, ht₁, a₁⟩
  have ⟨z₃, a₂⟩ := Step.Apply.RTC.construct s₂' (s₂'.output e₁.rcn)
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.indep_triggers_iff h |>.mp e₁.triggers_rcn
  let s₃' := z₃.record e₁.rcn
  let f₂ : s₂' ↓ₑ s₃' := ⟨ha₂, ht₂, a₂⟩
  refine ⟨_, _, .exec f₁, .exec f₂, rfl, rfl, ?_⟩
  exact Step.Exec.indep_comm e₁ e₂ f₁ f₂ rfl rfl h |>.symm
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ht₁ := e₁.triggers_iff.not.mpr e₂.not_triggers_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let s₂' := s₁.record e₂.rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let f₁ : s₁ ↓ₛ s₂' := ⟨ha₁, ht₁⟩
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ht₂ := f₁.triggers_iff.not.mp e₁.not_triggers_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let s₃' := s₂'.record e₁.rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let f₂ : s₂' ↓ₛ s₃' := ⟨ha₂, ht₂⟩
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
refine ⟨_, _, .skip f₁, .skip f₂, rfl, rfl, ?_⟩
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ s₃' = s₃
Tactic:
exact Step.Skip.comm e₁ e₂ f₁ f₂ rfl rfl |>.symm
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ⟨z₂, a₁⟩ := Step.Apply.RTC.construct s₁ (s₁.output e₂.rcn)
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ht₁ := e₁.triggers_iff.mpr e₂.triggers_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let s₂' := z₂.record e₂.rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let f₁ : s₁ ↓ₑ s₂' := ⟨ha₁, ht₁, a₁⟩
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ht₂ := f₁.indep_triggers_iff h |>.not.mp e₁.not_triggers_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃