1樓：喚醒感覺和意識
兩個數相加就意味著把這兩個數放到一起，那麼不管先放哪乙個，後放哪乙個，結果都是一樣的，都是這兩個數在一起.也就是說當兩個數相加時，這兩個數可以交換順序.
2樓：非構造性雨軒菌
module
AdditionCommutes
data
PeanoNat=Z
|SPeanoNat
total
plus
:(n, m :
PeanoNat
)->PeanoNat
plus Z n = n
plus (
S n) m =
S(plus n m)
total
plus_right
:(n, m :
PeanoNat
)->S(plus n m)
= plus n (
S m)
plus_right Z n =
Refl
plus_right (
S n) m =
rewrite plus_right n m inRefl
total
plus_commutes
:(n, m :
PeanoNat
)-> plus n m = plus m nplus_commutes ZZ=
Refl
plus_commutes Z
(S n)
= cong (plus_commutes Z n)plus_commutes (
S n) m =
rewrite plus_commutes n m inrewrite plus_right m n inRefl
還能來個idris（逃
3樓：Narc
module
AdditionCommutes
(plusCommutes
)where
-- | The natural numbers.
data
ZdataSn
-- | Predicate describing natural numbers.
-- | This allows us to reason with `Nat`s.
data
Natural::*
->*where
NumZ
::Natural
ZNumS
::Natural
n->Natural(S
n)-- | Predicate describing equality of natural numbers.
data
Equal::*
->*->*where
EqlZ
::EqualZZ
EqlS
::Equalnm
->Equal(S
n)(S
m)-- | Peano definition of addition.
type
family
(:+:)(
n::*)
(m::*
)::*type
instance
Z:+:m=
mtype
instanceSn
:+:m=S
(n:+:m
)-- | if a = b and b = c, then a = c.
transitive
::Equalab
->Equalbc
->Equalac
transitive
EqlZ
EqlZ
=EqlZ
transitive
(EqlSe1)
(EqlSe2)
=EqlS
$transitive
e1e2
-- | a + (b ++) = (a + b) ++
lemma
::Natural
m->Natural
n->Equal(m
:+:Sn)
(S(m
:+:n
))lemma
NumZ
NumZ
=EqlS
EqlZ
lemma
NumZ
(NumSn)
=EqlS
$lemma
NumZ
nlemma
(NumSm)
n=EqlS
$lemmamn
-- | 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
(NumSm)
NumZ
=EqlS
$plusCommutes
mNumZ
plusCommutesm(
NumSn)
=transitive
(lemmamn
)$EqlS
$plusCommutesmn
這是 codewars 上的一道題，剛做了，就來答一下。
最近在學 Agda，於是又寫了乙個 Agda 版的。
lemma-+zero : a -> a + zero ≡ a
lemma-+zero zero = refl
lemma-+zero (succ n) rewrite lemma-+zero n = refl
lemma-+succ : a b -> succ a + b ≡ a + succ b
lemma-+succ zero b = refl
lemma-+succ (succ a) b rewrite lemma-+succ a b = refl
+-common : a b -> a + b ≡ b + a
+-common zero b rewrite lemma-+zero b = refl
+-common (succ a) b rewrite +-common a b | lemma-+succ b a = refl
簡潔多了，定理證明 Haskell 確實還是外行。
4樓：Belleve
Lemma
plus_comm_z
:forallb:
nat,0+
b=b+
0.Proof
.intros
.inductionb.
reflexivity
.simpl
.rewrite
<-IHb.
simpl
.reflexivity
.Qed
.Lemma
plus_comm_s
:forallab
:nat,S
(b+a
)=b+
Sa.Proof
.intros
.inductionb.
simpl
.reflexivity
.simpl
.rewrite
IHb.
reflexivity
.Qed
.Theorem
plus_comm
:forallab
:nat,a
+b=b
+a.Proof
.intros
.inductiona.
plus_comm_z
.simpl
.rewrite
IHa.
plus_comm_s
.Qed.
加法交換律 a b b a 是怎麼證明的？
如果是實數的加法，那麼定義實數的時候通常要求實數集合是乙個域，交換律是公理 如果是自然數的加法，自然數是用peano公理定義的，加法交換律可以用peano公理推出來，好像有人寫了。 Egregium 這個問題比較複雜，需要牽扯到自然數的定義，我們一步步來。一 自然數的定義和Peano公理 所謂自然數...
對於兩個共線向量，怎麼證明滿足加法交換律？
都督水水炮 共線情況實際上更簡單一些。適用平行四邊形定則的向量是有向線段的定義，共線時方向可以使用正負號替代，線段長度計算滿足實數加減法，因此從向量加法退化為實數加法，交換律自然適用。 困泡 認真答題 要求滿足分配律,同時用到實數的交換律 a b a a 分配律 1 a 1 a b a 但這題沒有啥...
加法的交換律和結合律有什麼用呢？為什麼會有這些性質？
Rara 我想加法的交換率結合率就是要告訴你東西不會因為你數數的先後順序在數量上變多變少。你最開始有5顆奶糖，後來小明給了你6顆，然後小紅特別喜歡你就給了你7顆，最後你要數自己一共有多少顆糖呢。不管你是先數哪一堆，然後數另外哪一堆，最後再數剩下那一堆，糖的數量永遠是18顆，不會改變。從另一角度也算是...