Chain Reasoning

我會用了！整個 ChainReasoning module 的精神是簡化 transitivity 的使用（透過 operator ===）並要求中間項適時地出現（由 operator by 達成）。之前證得超複雜的 lemma 現在變成

lemma : {n₁ n₂ n₃ : Nat} ->
          suc (parity p + (n₁ + n₂) + n₃) ≡ parity p + n₁ + suc (n₂ + n₃)
lemma {n₁} {n₂} {n₃} =
  chain> suc (parity p + (n₁ + n₂) + n₃)
     === suc (parity p + (n₁ + n₂ + n₃))
           by cong suc (sym (+assoc (parity p) (n₁ + n₂) n₃))
     === parity p + suc (n₁ + n₂ + n₃)
           by sym (+suc (parity p) (n₁ + n₂ + n₃))
     === parity p + (n₁ + suc (n₂ + n₃)) by cong (\x -> parity p + x)
         ( chain> suc (n₁ + n₂ + n₃)
              === suc (n₁ + (n₂ + n₃)) by cong suc (sym (+assoc n₁ n₂ n₃))
              === n₁ + suc (n₂ + n₃) by sym (+suc n₁ (n₂ + n₃)) )
     === parity p + n₁ + suc (n₂ + n₃)
           by +assoc (parity p) n₁ (suc (n₂ + n₃))

因為 intermediate expressions 出現得夠多，就不會一堆 proof terms 疊在一起看起來很嚇人，應該有好看一點 XD。

然後我試著要把 by 的引數順序反過來，就可以變成 scm 老師心目中理想的長相：

chain> suc (parity p + (n₁ + n₂) + n₃)
   === [ cong suc (sym (+assoc (parity p) (n₁ + n₂) n₃)) ]
       suc (parity p + (n₁ + n₂ + n₃))
   === ...

可惜試到最後還是弄不出來，而且做到覺得不可能成功，所以就放棄了 XD。最後的版本是

data Indeed {A : Set} : A -> Set where
  indeed : (x : A) -> Indeed x

[_ : {A : Set}{x y : A} -> x == y -> Indeed y -> x == y
[ eq = \_ -> eq

]_ : {A : Set} -> (y : A) -> Indeed y
] y = indeed y

如果加幾組括號進去是會 work，但如果加括號整個形式就爛掉了 XD。

--
從明天開始暫時不能玩 Agda 了 XD。

---

會用 chain reasoning（而且證過上面那個 lemma）之後，scm 老師出的第一個作業就變得 trivial 了 XD。

half : (n : Nat) -> (Nat ⋮ \m -> n ≡ m + m) \/ 
                    (Nat ⋮ \m -> n ≡ 1 + (m + m))
...
half (suc n) | \/-IR (sub m p) = \/-IL (sub (1 + m) (proof n m p))
  where 
    proof : (n : Nat) -> (m : Nat) -> 
              (n ≡ 1 + (m + m)) -> (1 + n ≡ (1 + m) + (1 + m))
    proof n m p =
      chain> 1 + n
         === 1 + (1 + m + m) by cong suc p
         === (1 + m) + (1 + m) by sym (+suc (1 + m) m)

--
第一個想到可以這樣搞證明的人真的很神！XD