internlm/Lean-Github huggingface dataset:
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
rcn✝ : ID
s₂ : State α
a✝³ : Allows s rcn✝
a✝² : Triggers s rcn✝
a₂ : s -[output s rcn✝]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) = output (record s₂ rcn✝) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
hr₂ : Execution.Step.Exec.rcn (mk a✝³ a✝² a₂) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a₁₂)
s₂₁ : State α
a✝¹ : Allows (record s₂ rcn✝) rcn₁
a✝ : Triggers (record s₂ rcn✝) rcn₁
a₂₁ : (record s₂ rcn✝) -[output (record s₂ rcn✝) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
cases hr₂
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) = output (record s₂ rcn₂) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) = output (record s₂ rcn₂) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
simp [Exec.rcn] at *
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
have ⟨z₁₂, f₁₂⟩ := Apply.RTC.construct s₁ (s.output rcn₂)
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
have ⟨z₂₁, f₂₁⟩ := Apply.RTC.construct s₂ (s.output rcn₁)
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
rw [←ho₁] at a₁₂
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
rw [←ho₂] at a₂₁
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
cases f₁₂.comm_record a₁₂
Proof state after:
case refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
⊢ record (record z₁₂ rcn₁) rcn₂ = record s₂₁ rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
⊢ record (record z₁₂ rcn₁) rcn₂ = record s₂₁ rcn₁
Tactic:
cases f₂₁.comm_record a₂₁
Proof state after:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₁) rcn₂ = record (record z₂₁ rcn₂) rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₁) rcn₂ = record (record z₂₁ rcn₂) rcn₁
Tactic:
rw [record_comm]
Proof state after:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₂) rcn₁ = record (record z₂₁ rcn₂) rcn₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₂) rcn₁ = record (record z₂₁ rcn₂) rcn₁
Tactic:
congr
Proof state after:
case refl.refl.refl.refl.e_s.e_s
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ z₁₂ = z₂₁
Theorem: Execution.Step.Exec.indep_comm
Proof state before:
case refl.refl.refl.refl.e_s.e_s
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ z₁₂ = z₂₁
Tactic:
exact Apply.RTC.disjoint_targets_comm (s.indep_output_disjoint_targets hi) a₁ f₁₂ a₂ f₂₁
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
⊢ Triggers s₁ i ↔ Triggers s₂ i
Tactic:
constructor <;> intro ⟨ho, ht⟩
Proof state after:
case mp
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₂ i

case mpr
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₁ i
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₂ i
Tactic:
case mp =>
  have ho' := Equivalent.obj?_rcn_eq e.equiv ▸ ho
  have ht' := e.indep_input_eq hi.symm ‹_› ‹_› ▸ ht
  exact ⟨ho', ht'⟩
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₁ i
Tactic:
case mpr =>
  have ho' := Equivalent.obj?_rcn_eq e.equiv |>.symm ▸ ho
  have ht' := e.indep_input_eq hi.symm ‹_› ‹_› |>.symm ▸ ht
  exact ⟨ho', ht'⟩
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₂ i
Tactic:
have ho' := Equivalent.obj?_rcn_eq e.equiv ▸ ho
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
⊢ Triggers s₂ i
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
⊢ Triggers s₂ i
Tactic:
have ht' := e.indep_input_eq hi.symm ‹_› ‹_› ▸ ht
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₂ i
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₂ i
Tactic:
exact ⟨ho', ht'⟩
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₁ i
Tactic:
have ho' := Equivalent.obj?_rcn_eq e.equiv |>.symm ▸ ho
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
ho' : s₁.rtr[Component.rcn][i] = some rcn✝
⊢ Triggers s₁ i
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
ho' : s₁.rtr[Component.rcn][i] = some rcn✝
⊢ Triggers s₁ i
Tactic:
have ht' := e.indep_input_eq hi.symm ‹_› ‹_› |>.symm ▸ ht
Proof state after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
ho' : s₁.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₁ i
Theorem: Execution.Step.Exec.indep_triggers_iff
Proof state before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₂.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₂ i)
ho' : s₁.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₁ i)
⊢ Triggers s₁ i
Tactic:
exact ⟨ho', ht'⟩
Proof state after:
no goals
Theorem: Execution.Step.Apply.preserves_tag
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
⊢ s₁.tag = s₂.tag
Tactic:
cases e <;> simp [schedule_preserves_tag]
Proof state after:
no goals
Theorem: Execution.Step.Apply.preserves_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
⊢ s₁.progress = s₂.progress
Tactic:
cases e <;> simp [schedule_preserves_progress]
Proof state after:
no goals