fork download
copy 
  1. Require Import Arith.
  2. Require Import Omega.
  3. Open Scope Z_scope.
  4.  
  5. Variables m n: Z.
  6. Lemma l1: exists m0: Z, m = m0 * Z.gcd m n.
  7. apply Z.gcd_divide_l.
  8. Qed.
  9.  
  10. Lemma l2: exists n0: Z, n = n0 * Z.gcd m n.
  11. apply Z.gcd_divide_r.
  12. Qed.
  13.  
  14. Variables m0 n0: Z.
  15.  
  16. Hypothesis hyp1: (0 <> m)%Z.
  17. Hypothesis hyp2: (0 <> n)%Z.
  18. Hypothesis hyp3: m = m0 * Z.gcd m n.
  19. Hypothesis hyp4: n = n0 * Z.gcd m n.
  20. Hypothesis hyp5: Z.gcd m n + Z.lcm m n = m + n.
  21. Hypothesis hyp6: (0 <= m)%Z.
  22. Hypothesis hyp7: (0 <= n)%Z.
  23. Hypothesis hyp8: Z.lcm m n = m0 * n0 * Z.gcd m n.
  24.  
  25. Theorem t1: Z.gcd m n + m0 * n0 * Z.gcd m n = m0 * Z.gcd m n + n0 * Z.gcd m n.
  26. replace (m0 * Z.gcd m n) with m.
  27. replace (n0 * Z.gcd m n) with n.
  28. replace (m0 * n0 * Z.gcd m n) with (Z.lcm m n).
  29. apply hyp5.
  30. apply hyp8.
  31. apply hyp4.
  32. apply hyp3.
  33. Qed.
  34.  
  35. Theorem t2: (1 + m0 * n0)%Z * Z.gcd m n = (m0 + n0)%Z * Z.gcd m n.
  36. replace ((1 + m0 * n0) * Z.gcd m n) with (Z.gcd m n + m0 * n0 * Z.gcd m n).
  37. replace ((m0 + n0) * Z.gcd m n) with (m0 * Z.gcd m n + n0 * Z.gcd m n).
  38. apply t1.
  39. symmetry.
  40. apply Z.mul_add_distr_r.
  41. symmetry.
  42. replace (Z.gcd m n + m0 * n0 * Z.gcd m n) with (1 * Z.gcd m n + m0 * n0 * Z.gcd m n).
  43. apply Z.mul_add_distr_r.
  44. omega.
  45. Qed.
  46.  
  47. Theorem t3: (0 <= Z.gcd m n)%Z.
  48. apply Z.gcd_nonneg.
  49. Qed.
  50.  
  51. Theorem t4: (0 <> Z.gcd m n)%Z.
  52. apply not_eq_sym.
  53. rewrite Z.gcd_eq_0.
  54. red.
  55. intros.
  56. destruct H as (H1, H2).
  57. apply hyp1.
  58. symmetry.
  59. auto.
  60. Qed.
  61.  
  62. Theorem t5: 1 + m0 * n0 = m0 + n0.
  63. assert ((1 + m0 * n0)%Z * Z.gcd m n = (m0 + n0)%Z * Z.gcd m n).
  64. apply t2.
  65. assert (Z.gcd m n <> 0%Z).
  66. apply not_eq_sym.
  67. apply t4.
  68. rewrite <- Z.mul_cancel_r.
  69. eapply H.
  70. apply H0.
  71. Qed.
  72.  
  73. Theorem t6: m0 * (n0 - 1%Z) = n0 - 1%Z.
  74. assert (1 + m0 * n0 = m0 + n0).
  75. apply t5.
  76. replace (m0 * (n0 - 1)) with (m0 * n0 - m0).
  77. omega.
  78. symmetry.
  79. rewrite Z.mul_sub_distr_l.
  80. replace (m0 * 1) with m0.
  81. auto.
  82. symmetry.
  83. apply Z.mul_1_r.
  84. Qed.
  85.  
  86. Theorem t7: n0 * (m0 - 1%Z) = m0 - 1%Z.
  87. assert (1 + m0 * n0 = m0 + n0).
  88. apply t5.
  89. replace (n0 * (m0 - 1)) with (n0 * m0 - n0 * 1).
  90. apply Zeq_plus_swap.
  91. rewrite Z.sub_opp_r.
  92. replace (n0 * 1) with n0.
  93. replace (m0 - 1 + n0) with (m0 + n0 - 1).
  94. apply Zplus_minus_eq.
  95. symmetry.
  96. replace (n0 * m0) with (m0 * n0).
  97. apply H.
  98. apply Z.mul_comm.
  99. omega.
  100. symmetry.
  101. apply Z.mul_1_r.
  102. symmetry.
  103. apply Zmult_minus_distr_l.
  104. Qed.
  105.  
  106. Theorem t8: n0 <> 1 -> m0 = 1.
  107. intros.
  108. assert (m0 * (n0 - 1%Z) = n0 - 1%Z).
  109. apply t6.
  110. assert (n0 - 1 <> 0).
  111. omega.
  112. assert (m0 * (n0 - 1) = 1 * (n0 - 1)).
  113. omega.
  114. apply Z.mul_cancel_r in H2.
  115. apply H2.
  116. apply H1.
  117. Qed.
  118.  
  119. Theorem t9: m0 <> 1 -> n0 = 1.
  120. intros.
  121. assert (n0 * (m0 - 1%Z) = m0 - 1%Z).
  122. apply t7.
  123. assert (m0 - 1 <> 0).
  124. omega.
  125. assert (n0 * (m0 - 1) = 1 * (m0 - 1)).
  126. omega.
  127. apply Z.mul_cancel_r in H2.
  128. apply H2.
  129. apply H1.
  130. Qed.
  131.  
  132. Theorem t10: m0 = 1 \/ n0 = 1.
  133. assert (n0 <> 1 -> m0 = 1).
  134. apply t8.
  135. omega.
  136. Qed.
  137.  
  138. Theorem t11: m = Z.gcd m n \/ n = Z.gcd m n.
  139. assert (m0 = 1 \/ n0 = 1).
  140. apply t10.
  141. assert (m = m0 * Z.gcd m n).
  142. apply hyp3.
  143. assert (n = n0 * Z.gcd m n).
  144. apply hyp4.
  145. case H.
  146. intro.
  147. left.
  148. replace (Z.gcd m n) with (1 * Z.gcd m n).
  149. replace 1 with m0.
  150. apply H0.
  151. apply Z.mul_1_l.
  152. intro.
  153. right.
  154. replace (Z.gcd m n) with (1 * Z.gcd m n).
  155. replace 1 with n0.
  156. apply H1.
  157. apply Z.mul_1_l.
  158. Qed.
  159.  
  160. Theorem t12: (m | n)%Z \/ (n | m)%Z.
  161. assert (m = Z.gcd m n \/ n = Z.gcd m n).
  162. apply t11.
  163. assert (0 <= m%Z).
  164. apply hyp6.
  165. assert (0 <= n%Z).
  166. apply hyp7.
  167. case H.
  168. intro.
  169. left.
  170. apply Z.divide_gcd_iff.
  171. apply H0.
  172. symmetry.
  173. apply H2.
  174. intro.
  175. right.
  176. apply Z.divide_gcd_iff.
  177. apply H1.
  178. symmetry.
  179. replace (Z.gcd n m) with (Z.gcd m n).
  180. apply H2.
  181. apply Z.gcd_comm.
  182. Qed.
  183.  
Not running #stdin #stdout 0s 0KB
comments (?)
stdin
copy 
Standard input is empty
stdout
copy 
Standard output is empty
https://ideone.com/Aa07zr
language:
Text (text 6.10)
created:
9 years ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!