https://leanprover.github.io/live/3.4.1/#code=--%20Math%202001%20--%20HW%2013%20--%20Teamwork%204%0A%0A--%20Due:%20Friday,%2014%20December%202018**%0A%0A--%20Below%20you%20will%20be%20asked%20to%20prove%20some%20facts%20about%20natural%20numbers%20from%20Sections%2017.4%20and%2017.5.%0A--%20First,%20here%20are%20some%20examples.%20(You%20can%20use%20these%20theorems%20in%20your%20own%20proofs).%0A%0Aopen%20nat%0A%0Avariables%20m%20n%20:%20%E2%84%95%0Aexample%20:%20m%20+%200%20=%20m%20:=%20add_zero%20m%0Aexample%20:%20m%20+%20succ%20n%20=%20succ%20(m%20+%20n)%20:=%20add_succ%20m%20n%0A%0A--%20Similarly,%20we%20have%20the%20defining%20equations%20for%20the%20predecessor%20function%20and%20multiplication:%0A#check%20@pred_zero%0A#check%20@pred_succ%0A#check%20@mul_zero%0A#check%20@mul_succ%0A%0A--%20Here%20are%20five%20propositions%20proved%20in%2017.4:%0Anamespace%20hidden%0A%0A%20theorem%20succ_pred%20(n%20:%20%E2%84%95)%20:%20n%20%E2%89%A0%200%20%E2%86%92%20succ%20(pred%20n)%20=%20n%20:=%0A%20nat.rec_on%20n%0A%20%20%20(assume%20H%20:%200%20%E2%89%A0%200,%0A%20%20%20%20%20show%20succ%20(pred%200)%20=%200,%20from%20absurd%20rfl%20H)%0A%20%20%20(assume%20n,%0A%20%20%20%20%20assume%20ih,%0A%20%20%20%20%20assume%20H%20:%20succ%20n%20%E2%89%A0%200,%0A%20%20%20%20%20show%20succ%20(pred%20(succ%20n))%20=%20succ%20n,%0A%20%20%20%20%20%20%20by%20rewrite%20pred_succ)%0A%0A%20theorem%20zero_add%20(n%20:%20nat)%20:%200%20+%20n%20=%20n%20:=%0A%20nat.rec_on%20n%0A%20%20%20(show%200%20+%200%20=%200,%20from%20rfl)%0A%20%20%20(assume%20n,%0A%20%20%20%20%20assume%20ih%20:%200%20+%20n%20=%20n,%0A%20%20%20%20%20show%200%20+%20succ%20n%20=%20succ%20n,%20from%20calc%0A%20%20%20%20%20%20%200%20+%20succ%20n%20=%20succ%20(0%20+%20n)%20:%20rfl%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20succ%20n%20:%20by%20rw%20ih)%0A%0A%20theorem%20succ_add%20(m%20n%20:%20nat)%20:%20succ%20m%20+%20n%20=%20succ%20(m%20+%20n)%20:=%0A%20nat.rec_on%20n%0A%20%20%20(show%20succ%20m%20+%200%20=%20succ%20(m%20+%200),%20from%20rfl)%0A%20%20%20(assume%20n,%0A%20%20%20%20%20assume%20ih%20:%20succ%20m%20+%20n%20=%20succ%20(m%20+%20n),%0A%20%20%20%20%20show%20succ%20m%20+%20succ%20n%20=%20succ%20(m%20+%20succ%20n),%20from%20calc%0A%20%20%20%20%20%20%20succ%20m%20+%20succ%20n%20=%20succ%20(succ%20m%20+%20n)%20:%20rfl%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20succ%20(succ%20(m%20+%20n))%20:%20by%20rw%20ih%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20succ%20(m%20+%20succ%20n)%20:%20rfl)%0A%0A%20theorem%20add_assoc%20(m%20n%20k%20:%20nat)%20:%20m%20+%20n%20+%20k%20=%20m%20+%20(n%20+%20k)%20:=%0A%20nat.rec_on%20k%0A%20%20%20(show%20m%20+%20n%20+%200%20=%20m%20+%20(n%20+%200),%20by%20rw%20%5Badd_zero,%20add_zero%5D)%0A%20%20%20(assume%20k,%0A%20%20%20%20%20assume%20ih%20:%20m%20+%20n%20+%20k%20=%20m%20+%20(n%20+%20k),%0A%20%20%20%20%20show%20m%20+%20n%20+%20succ%20k%20=%20m%20+%20(n%20+%20(succ%20k)),%20from%20calc%0A%20%20%20%20%20%20%20m%20+%20n%20+%20succ%20k%20=%20succ%20(m%20+%20n%20+%20k)%20%20%20:%20by%20rw%20add_succ%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20succ%20(m%20+%20(n%20+%20k))%20:%20by%20rw%20ih%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20m%20+%20(n%20+%20succ%20k)%20%20%20:%20by%20rw%20add_succ)%0A%0A%20theorem%20add_comm%20(m%20n%20:%20nat)%20:%20m%20+%20n%20=%20n%20+%20m%20:=%0A%20nat.rec_on%20n%0A%20%20%20(show%20m%20+%200%20=%200%20+%20m,%20by%20rewrite%20%5Badd_zero,%20zero_add%5D)%0A%20%20%20(assume%20n,%0A%20%20%20%20%20assume%20ih%20:%20m%20+%20n%20=%20n%20+%20m,%0A%20%20%20%20%20show%20m%20+%20succ%20n%20=%20succ%20n%20+%20m,%20from%20calc%0A%20%20%20%20%20%20%20m%20+%20succ%20n%20=%20succ%20(m%20+%20n)%20:%20by%20rw%20add_succ%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20succ%20(n%20+%20m)%20:%20by%20rw%20ih%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20succ%20n%20+%20m%20%20%20:%20by%20rw%20succ_add)%0A%0A%0A%0A%20--EXERCISES--%0A%0A%20--1.%20Prove%20the%20following%20identities%20from%2017.4%20by%20replacing%20each%20%60sorry%60%20with%20a%20proof.%0A%0A%20--1.a.%0A%20theorem%20mul_distr%20:%20%E2%88%80%20m%20n%20k%20:%20nat,%20m%20*%20(n%20+%20k)%20=%20m%20*%20n%20+%20m%20*%20k%20:=%0A%20assume%20m%20n%20k,%0A%20nat.rec_on%20k%0A%20--base%20case%0A%20(%20show%20m%20*%20(n+0)%20=%20m%20*%20n%20+%20m%20*%200,%20from%0A%20%20%20have%20h1%20:%20n%20+%200%20=%20n,%20from%20add_zero%20n,%0A%20%20%20have%20h2%20:%20m%20*%200%20=%200,%20from%20mul_zero%20m,%0A%20%20%20calc%0A%20%20%20m%20*%20(n+0)%20=%20m%20*%20n%20:%20by%20rewrite%20h1%0A%20%20%20%20%20%20%20%20%20%20%20...%20=%20m%20*%20n%20+%200%20:%20add_zero%20(m%20*%20n)%0A%20%20%20%20%20%20%20%20%20%20%20...%20=%20m%20*%20n%20+%20m%20*%200%20:%20by%20rw%20h2%0A%20%20%20)%0A%20--%20induction%20step%0A%20(%20assume%20k,%0A%20%20%20assume%20ih%20:%20m%20*%20(n%20+%20k)%20=%20m%20*%20n%20+%20m%20*%20k,%0A%20%20%20show%20m%20*%20(n%20+%20succ%20k)%20=%20m%20*%20n%20+%20m%20*%20succ%20k,%20from%0A%20%20%20calc%20m%20*%20(n%20+%20succ%20k)%20=%20m%20*%20succ%20(n%20+%20k)%20:%20by%20rw%20add_succ%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20m%20*%20(n%20+%20k)%20+%20m%20:%20mul_succ%20m%20(n%20+%20k)%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20m%20*%20n%20+%20m%20*%20k%20+%20m%20:%20by%20rw%20ih%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20m%20*%20n%20+%20m%20*%20succ%20k%20:%20by%20simp%20%5Bmul_succ%5D)%0A%0A%20--1.b.%0A%20example%20:%20%E2%88%80%20n%20:%20nat,%200%20*%20n%20=%200%20:=%0A%20assume%20n,%0A%20nat.rec_on%20n%0A%20(show%200%20*%200%20=%200%20,from%20mul_zero%200%0A%20%20)%0A%20(assume%20n,%0A%20assume%20ih:%200%20*%20n%20=%200,%0A%20show%200%20*%20succ%20n%20=%200%20,from%20calc%0A%20%200%20*%20succ%20n%20=%200%20*%20n%20%20+%200:%20mul_succ%200%20n%0A%20%20%20%20%20%20%20%20%20...%20=%200%20*%20n%20:%20add_zero%20(0%20*%20n)%0A%20%20%20%20%20%20%20%20%20...%20=%200%20:%20by%20simp%20%5Bmul_zero%5D%20)%0A%0A%20--1.c.%0A%20example%20:%20%E2%88%80%20n%20:%20nat,%201%20*%20n%20=%20n%20:=%0A%20assume%20n%20,%0A%20nat.rec_on%20n%0A%20(show%201%20*%200%20=%200,%20from%20mul_zero%201%0A%20)%0A%20(assume%20n,%0A%20assume%20ih:%201%20*%20n%20=%20n,%0A%20show%20%201%20*%20succ%20n%20=%20succ%20n,%20from%0A%20calc%0A%20%20%201%20*%20succ%20n%20=%201%20*%20n%20+%201%20*%201%20:%20mul_succ%201%20n%0A%20%20%20%20%20%20%20%20%20%20...%20=%201%20*%20n%20+%201%20:%20add_one%20(1%20*%20n)%0A%20%20%20%20%20%20%20%20%20%20...%20=%20n%20+%201%20:%20by%20simp%20%5Bmul_one%5D%0A%20%20%20%20%20%20%20%20%20%20%20)%0A%0A%20--1.d.%0A%20example%20:%20%E2%88%80%20m%20n%20k%20:%20nat,%20(m%20*%20n)%20*%20k%20=%20m%20*%20(n%20*%20k)%20:=%0A%20assume%20m%20n%20k,%0A%20nat.rec_on%20k%0A%20--base%20case%0A%20(show%20(m%20*%20n)%20%20*%200%20=%20m%20*%20(n%20*%200),%20from%0A%20%20%20calc%0A%20%20%20%20%20(m%20*%20n)%20*%200%20=%200%20:%20mul_zero%20(m%20*%20n)%0A%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20n%20*%200%20:%20mul_zero%20n%0A%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20m%20*%20(n%20*%200)%20:%20by%20rw%20(mul_zero%20m)%0A%0A%20--induction%20step%0A%20(assume%20k,%0A%20%20assume%20ih%20:%20(m%20*%20n)%20*%20k%20=%20m%20*%20(n%20*%20k),%0A%20%20show%20(m%20*%20n)%20*%20succ%20k%20=%20m%20*%20(n%20*%20succ%20k),%20from%0A%20%20Sorry%20)%0A%0A%20--1.e.%0A%20example%20:%20%E2%88%80%20m%20n%20:%20nat,%20m%20*%20n=%20n%20*%20m%20:=%20sorry%0A%0A%0A%0A%20--2.%20Prove%20the%20remaining%20identities%20from%2017.5%20by%20replacing%20each%20%60sorry%60%20with%20a%20proof.%0A%0A%20--2.a.%0A%20example%20:%20%E2%88%80%20m%20n%20k%20:%20nat,%20n%20%E2%89%A4%20m%20%E2%86%92%20n%20+%20k%20%E2%89%A4%20m%20%20+%20k%20:=%0A%20assume%20m%20n%20k,%0A%20assume%20h%20:%20n%20%E2%89%A4%20m,%20show%20n+%20k%20%E2%89%A4%20m%20+%20k,%20from%20%0A%20nat.rec_on%20k%0A%20(show%20n%20+%200%20%E2%89%A4%20m%20+%200,%20from%0A%20calc%20n%20+%200%20=%20n%20:%20add_zero%20n%0A%20%20%20%20%20%20%20%20%20%20%20...%E2%89%A4%20m%20:%20h%0A%20%20%20%20%20%20%20%20%20%20%20...=%20m%20+%200%20:%20add_zero%20m)%0A%20(assume%20k,%0A%20%20%20assume%20ih%20:%20n%20+%20k%20%E2%89%A4%20m%20+%20k,%0A%20%20%20show%20n%20+%20succ%20k%20%E2%89%A4%20m%20+%20succ%20k,%20from%0A%20%20%20%20%20%20%20(calc%20n%20+%20succ%20k%20=%20succ%20(n%20+%20k)%20:%20add_succ%20n%20k%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20%E2%89%A4%20succ%20(m%20+%20k)%20:%20by%20simp%20%5Bsucc_le_succ%20ih%5D))%0A%20--2.b.%0A%20%20lemma%20succ_le_le%20:%20%E2%88%80%20m%20n%20:%20nat,%20succ%20m%20%E2%89%A4%20succ%20n%20%E2%86%92%20m%20%E2%89%A4%20n%20:=%0Aassume%20m%20n,%0Anat.rec_on%20m%0A(%20show%20succ%200%20%E2%89%A4%20succ%20n%20%E2%86%92%200%20%E2%89%A4%20n,%20from%0A%20assume%20h%20:%20succ%200%20%E2%89%A4%20succ%20n,%20zero_le%20n)%0A(%20assume%20m,%0A%20assume%20ih%20:%20succ%20m%20%E2%89%A4%20succ%20n%20%E2%86%92%20m%20%E2%89%A4%20n,%0A%20show%20succ%20(succ%20m)%20%E2%89%A4%20succ%20n%20%E2%86%92%20succ%20m%20%E2%89%A4%20n,%20from%0A%20%20%20assume%20h%E2%82%81%20:%20succ%20(succ%20m)%20%E2%89%A4%20succ%20n,%0A%20%20%20have%20h%E2%82%82%20:%20succ%20m%20%3C%20succ%20n,%20from%20lt_of_succ_le%20h%E2%82%81,%0A%20%20%20le_of_lt_succ%20h%E2%82%82)%0A%0A%0A%20example%20:%20%E2%88%80%20m%20n%20k%20:%20nat,%20n%20+%20k%20%E2%89%A4%20m%20+%20k%20%E2%86%92%20n%20%E2%89%A4%20m%20:=%0A%20%20%20assume%20m%20n%20k,%0A%20%20%20nat.rec_on%20k%0A%20%20%20(%20show%20n%20+%200%20%E2%89%A4%20m%20+%200%20%E2%86%92%20n%20%E2%89%A4%20m,%20from%0A%20%20%20%20%20%20%20assume%20h%20:%20n%20+%200%20%E2%89%A4%20m%20+%200,%0A%20%20%20%20%20%20%20show%20)%0A%20%20%20(%20assume%20k,%0A%20%20%20assume%20ih%20:%20n%20+%20k%20%E2%89%A4%20m%20+%20k%20%E2%86%92%20n%20%E2%89%A4%20m,%0A%20%20%20show%20n%20+%20succ%20k%20%E2%89%A4%20m%20+%20succ%20k%20%E2%86%92%20n%20%E2%89%A4%20m,%20from%0A%20%20%20%20%20%20%20assume%20h%20:%20n%20+%20succ%20k%20%E2%89%A4%20m%20+%20succ%20k,%0A%20%20%20%20%20%20%20show%20n%20%E2%89%A4%20m,%20from%0A%20%20%20%20%20%20%20have%20h%E2%82%81%20:%20succ%20(n%20+%20k)%20%E2%89%A4%20succ%20(m%20+%20k),%20from%0A%20%20%20%20%20%20%20%20%20%20%20calc%20succ%20(n%20+%20k)%20=%20n%20+%20succ%20k%20%20%20:%20add_succ%20n%20k%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20%E2%89%A4%20m%20+%20succ%20k%20%20%20:%20h%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20...%20=%20succ%20(m%20+%20k)%20:%20add_succ%0A%20m%20k,%20%20%20%20%20%20%20have%20h%20:%20n%20+%20k%20%E2%89%A4%20m%20+%20k,%20from%20succ_le_le%20(n+k)%20(m+k)%20h,%0A%20%20%20%20%20%20%20show%20n%20%E2%89%A4%20m,%20from%0A%20%20%20%20%20%20%20have%20h%E2%82%82%20:%20)%0A%0Aend%20hidden%0A%0A%0A%0A