如何證明加法交換律？

12-02

對於任意x， y ∈ N; x + y = y + x

Lemma plus_comm_z : forall b : nat, 0 + b = b + 0. Proof. intros. induction b. reflexivity. simpl. rewrite &<- IHb. simpl. reflexivity. Qed. Lemma plus_comm_s : forall a b : nat, S (b + a) = b + S a. Proof. intros. induction b. simpl. reflexivity. simpl. rewrite IHb. reflexivity. Qed. Theorem plus_comm : forall a b : nat, a + b = b + a. Proof. intros. induction a. apply plus_comm_z. simpl. rewrite IHa. apply plus_comm_s. Qed.

引自陶哲軒《實分析》第21頁，全書下載在新浪微盤搜
當然了，僅僅是這張圖片還不夠，陶從皮亞諾公理開始做到了這步要有不少中間過程的。

{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}


module AdditionCommutes

  ( plusCommutes ) where
-- | The natural numbers.

data Z

data S n
-- | Predicate describing natural numbers.

-- | This allows us to reason with `Nat`s.

data Natural :: * -&> * where

    NumZ :: Natural Z

    NumS :: Natural n -&> Natural (S n)
-- | Predicate describing equality of natural numbers.

data Equal :: * -&> * -&> * where

    EqlZ :: Equal Z Z

    EqlS :: Equal n m -&> Equal (S n) (S m)
-- | Peano definition of addition.

type family (:+:) (n :: *) (m :: *) :: *

type instance Z :+: m = m

type instance S n :+: m = S (n :+: m)
-- | if a = b and b = c, then a = c.

transitive :: Equal a b -&> Equal b c -&> Equal a c

transitive EqlZ EqlZ = EqlZ

transitive (EqlS e1) (EqlS e2) = EqlS $ transitive e1 e2
-- | a + (b ++) = (a + b) ++

lemma :: Natural m -&> Natural n -&> Equal (m :+: S n) (S (m :+: n))

lemma NumZ NumZ = EqlS EqlZ

lemma NumZ (NumS n) = EqlS $ lemma NumZ n

lemma (NumS m) n = EqlS $ lemma m n

-- | a + zero = zero + a -- | a + (b ++) = (a + b) ++ -- | (b ++) + a = (b + a) ++ -- | then a + b = b + a plusCommutes :: Natural a -&> Natural b -&> Equal (a :+: b) (b :+: a) plusCommutes NumZ NumZ = EqlZ plusCommutes (NumS m) NumZ = EqlS $ plusCommutes m NumZ plusCommutes m (NumS n) = transitive (lemma m n) $ EqlS $ plusCommutes m n

這是 codewars 上的一道題，剛做了，就來答一下。