coq練習問題(3)

coq3.v

Require Import ssreflect.

Lemma plusnS m n : m + S n = S (m + n).
Proof.
  elim: m => /=.
  + done.
  + move => m IH.
    by rewrite IH.
Qed.
Lemma plusSn m n : (S m) + n = S (m + n).
Proof. rewrite /=. done. Show Proof. Qed.

Lemma plusn0 n : n + O = n.
Proof.
  elim: n.
  reflexivity.
  move => n IH.
  cut ((S n + O) = S (n + 0)).
  + move => rm_prns.
  rewrite -> rm_prns.
  rewrite -> IH.
  reflexivity.
  + reflexivity.
  
Qed.

Lemma plusC m n : m + n = n + m.
  elim: m.
  + rewrite plusn0.
  reflexivity.
  + move => m IH.
  rewrite plusSn.
  rewrite -> IH.
  rewrite plusnS.
  reflexivity.
Qed.
Lemma plusA m n p : m + (n + p) = (m + n) + p.
Proof.
  elim: m.
  reflexivity.
  move => m IH.
  rewrite !plusSn.
  rewrite IH.
  reflexivity.
Qed.

Lemma multn0 n : n * 0 = 0.
Proof.
  elim: n.
  reflexivity.
  move => n IH.
  rewrite /=.
  rewrite IH.
  reflexivity.
Qed.
Lemma multnS m n : m * S n = m + (m * n).
Proof.
  elim: m => /= [|m ->] //.
  by rewrite !plusA [n + m]plusC.  
Restart.
  elim: m. 
  reflexivity.
  move => m IH.
  rewrite /=.
  rewrite IH.
  rewrite !plusA.
  rewrite (plusC n m).
  reflexivity.
Qed.

Lemma multC m n : m * n = n * m.
Proof.
  elim: m.
  rewrite multn0; reflexivity.
  move => m IH.
  by rewrite /= multnS IH.
Qed.
Lemma multnDr m n p : (m + n) * p = m * p + n * p.
Proof.
  elim: m.
  reflexivity.
  move => m IH.
  rewrite /=.
  rewrite IH.
  rewrite plusA.
  reflexivity.
Qed.

Lemma multA m n p : m * (n * p) = (m * n) * p.
Proof.
  elim: m.
  reflexivity.
  move => m IH.
  rewrite /= IH multnDr.
  reflexivity.
Qed.

Fixpoint sum n :=
  if n is S m then n + sum m else 0.
Print sum.


Lemma double_sum n : 2 * sum n = n * (n+1).
Proof.
  elim: n.
  rewrite /=.
  reflexivity.
  move => n IH.
  rewrite [(S n + 1)]/=.
  rewrite [sum (S n)]/=.
  rewrite [2 * S(n+sum n)]multnS.
  rewrite [2*(n+sum n)]multC multnDr.
  rewrite [sum n * 2]multC.
  rewrite IH.
  rewrite [n * (n + 1)]multC multnDr.
  rewrite !plusA.
  rewrite [n+1]plusnS [n+0]plusn0.
  simpl.
  rewrite ![n * S(S n)]multnS.
  rewrite [n * (S n)]multnS.
  rewrite !plusA.
  rewrite [n*2]multnS.
  rewrite [n*1]multnS.
  rewrite !multn0.
  rewrite !plusn0.
  rewrite [n + n + n * n]plusC.
  rewrite [n + n + n + n* n]plusC.
  rewrite !plusA.
  reflexivity.
Qed.


Lemma square_eq a b : (a + b) * (a + b) = (a*a) + (2*a*b) + (b*b).
Proof.
  rewrite multnDr.
  rewrite [a * (a+b)]multC.
  rewrite [b * (a+b)]multC.
  rewrite 2!multnDr.
  
  rewrite [b * a]multC.
  simpl.
  rewrite multnDr.
  rewrite plusn0.
  rewrite !plusA.
  reflexivity.
Qed.