internlm/Lean-Github huggingface dataset:
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₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec 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 (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₃' : State α := record s₂' (Step.Skip.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₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.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₂⟩
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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ 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₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
refine ⟨_, _, .exec 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 (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₃' : 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 (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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ s₃' = s₃
Tactic:
simp [e₂.dst_eq, f₂.dst_eq]
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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record s₂' (Step.Skip.rcn f₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)
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₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record s₂' (Step.Skip.rcn f₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)
Tactic:
rw [State.record_comm]
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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record (record z₂ (Step.Skip.rcn f₂)) (Step.Exec.rcn e₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)
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₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record (record z₂ (Step.Skip.rcn f₂)) (Step.Exec.rcn e₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)
Tactic:
congr!
Proof state after:
case h.e'_2
α : 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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
case h.e'_2
α : 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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Tactic:
have a₂ := e₂.apply
Proof state after:
case h.e'_2
α : 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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
a₂ : s₂ -[output s₂ (Step.Exec.rcn e₂)]→ (Step.Exec.applied e₂)
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
case h.e'_2
α : 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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
a₂ : s₂ -[output s₂ (Step.Exec.rcn e₂)]→ (Step.Exec.applied e₂)
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Tactic:
simp [e₁.dst_eq] at a₂
Proof state after:
case h.e'_2
α : 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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
a₂ : (record s₁ (Step.Skip.rcn e₁)) -[output (record s₁ (Step.Skip.rcn e₁)) (Step.Exec.rcn e₂)]→ (Step.Exec.applied e₂)
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof state before:
case h.e'_2
α : 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₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
a₂ : (record s₁ (Step.Skip.rcn e₁)) -[output (record s₁ (Step.Skip.rcn e₁)) (Step.Exec.rcn e₂)]→ (Step.Exec.applied e₂)
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Tactic:
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:
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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ht₁ := e₁.indep_triggers_iff h.symm |>.not.mpr e₂.not_triggers_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip 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 (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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip 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 (exec 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ht₂ := f₁.triggers_iff.mp e₁.triggers_rcn
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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 (skip 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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 (skip e₂) ∧ rcn e₂' = rcn (exec 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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 (skip 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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 (skip e₂) ∧ rcn e₂' = rcn (exec 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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 (skip 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 (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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 (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
refine ⟨_, _, .skip f₁, .exec f₂, rfl, rfl, ?_⟩
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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₃
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₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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₃
Tactic:
simp [e₂.dst_eq, e₁.dst_eq]
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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₃' = record (record (Step.Exec.applied e₁) (Step.Exec.rcn e₁)) (Step.Skip.rcn e₂)
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₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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₃' = record (record (Step.Exec.applied e₁) (Step.Exec.rcn e₁)) (Step.Skip.rcn e₂)
Tactic:
rw [State.record_comm]
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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₃' = record (record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)) (Step.Exec.rcn e₁)
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₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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₃' = record (record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)) (Step.Exec.rcn e₁)
Tactic:
congr!
Proof state after:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
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₂
⊢ z₃ = record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)