Back to the Equations

寫完 summation 的 congruence rules 和 commutativity，現在可以做「勉強算是 non-trivial」的 equational reasoning 了：

test : ∀ {a b : Set} {x : Chan a} {y : Chan b} {p q r s z w} →
  p ≈ q  →  r ≈ s  →  (x ! z · p) + (y ! w · r) ≈ (x ! z · q) + (y ! w · s)
test {a}{b}{x}{y}{p}{q}{r}{s}{z}{w} p≈q r≈s =
  ≈-begin
     (x ! z · p) + (y ! w · r)
  ≈⟨ +-cong₁ p≈q ⟩
     (x ! z · q) + (y ! w · r)
  ≈⟨ +-comm ⟩
     (y ! w · r) + (x ! z · q)
  ≈⟨ +-cong₁ r≈s ⟩
     (y ! w · s) + (x ! z · q)
  ≈⟨ +-comm ⟩
     (x ! z · q) + (y ! w · s)
  ≈∎

看到漂亮的 equational reasoning 就覺得前途一片光明啊 XD。

--
睡醒再戰 XD。