BT002U

gcd_exists_up_to

Stable · empty-context checked

Bounded induction constructs a relational gcd whenever the right input is at most the bound.

Exact expanded PA statement

forall B b. (exists t. t + b = B) -> forall a. exists d. (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

Structural proof guide

Bounded induction constructs a relational gcd whenever the right input is at most the bound.

Direct prerequisites: multiple_refl, le_zero, le_eq_or_lt, le_of_succ_le_succ, division_remainder_exists, is_gcd_euclid_forward. The authored body proceeds by structural induction (1), case analysis (5), intermediate claims (9), equality transport (1).

Proof neighborhood

Direct dependencies

BT0028 multiple_refl BT000Y le_zero BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT001P division_remainder_exists BT002S is_gcd_euclid_forward

Direct dependents

BT002V gcd_exists_relational

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro B
  2. 0002induction B
  3. 0003intro b
  4. 0004intro hb
  5. 0005intro a
  6. 0006have hb0 : b = 0
  7. 0007apply le_zero
  8. 0008exact hb
  9. 0009exists a
  10. 0010split
  11. 0011split
  12. 0012specialize multiple_refl a
  13. 0013exact multiple_refl
  14. 0014exists 0
  15. 0015trans 0
  16. 0016exact hb0
  17. 0017symm
  18. 0018apply PA5
  19. 0019intro c
  20. 0020intro hca
  21. 0021intro hcb
  22. 0022exact hca
  23. 0023intro b
  24. 0024intro hb
  25. 0025intro a
  26. 0026specialize le_eq_or_lt b
  27. 0027specialize le_eq_or_lt (S B)
  28. 0028have hsplit : b = S B \/ exists k. k + S b = S B
  29. 0029apply le_eq_or_lt
  30. 0030exact hb
  31. 0031cases hsplit
  32. 0032have hb0 : ~(b = 0)
  33. 0033intro hzero
  34. 0034apply PA1
  35. 0035trans b
  36. 0036symm
  37. 0037exact hsplit_left
  38. 0038exact hzero
  39. 0039have hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
  40. 0040apply division_remainder_exists
  41. 0041exact hb0
  42. 0042cases hdiv
  43. 0043cases hdiv_witness
  44. 0044cases hdiv_witness_witness
  45. 0045have hrB : exists k. k + x1 = B
  46. 0046apply le_of_succ_le_succ
  47. 0047rewrite hsplit_left at hdiv_witness_witness_right
  48. 0048exact hdiv_witness_witness_right
  49. 0049have hsmall : exists d. (((exists u. b = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. b = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
  50. 0050specialize IH x1
  51. 0051have hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
  52. 0052apply IH
  53. 0053exact hrB
  54. 0054specialize hall b
  55. 0055exact hall
  56. 0056cases hsmall
  57. 0057exists x2
  58. 0058specialize is_gcd_euclid_forward x2
  59. 0059specialize is_gcd_euclid_forward a
  60. 0060specialize is_gcd_euclid_forward b
  61. 0061specialize is_gcd_euclid_forward x
  62. 0062specialize is_gcd_euclid_forward x1
  63. 0063apply is_gcd_euclid_forward
  64. 0064exact hdiv_witness_witness_left
  65. 0065exact hsmall_witness
  66. 0066have hbB : exists k. k + b = B
  67. 0067apply le_of_succ_le_succ
  68. 0068exact hsplit_right
  69. 0069specialize IH b
  70. 0070have hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. b = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. b = c * t) -> exists w. d = c * w)
  71. 0071apply IH
  72. 0072exact hbB
  73. 0073specialize hall a
  74. 0074exact hall