book/TPiL/Tactics.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Theorem Proving in Lean documentation, Pinned Theorem Proving in Lean 4 book index

147 declarations, 3 contain sorry, 0 declared as axioms

Imports (2)
  1. example (example at line 25) line 25 source
  2. theorem test sorry line 45 source
  3. theorem test line 73 source
  4. example above line 82 source
  5. theorem test line 85 source
  6. theorem test line 129 source
  7. theorem test line 154 source
  8. theorem test line 162 source
  9. theorem test line 172 source
  10. example (example at line 177) line 177 source
  11. theorem test line 185 source
  12. theorem test line 200 source
  13. theorem test line 233 source
  14. example (example at line 253) line 253 source
  15. example (example at line 285) line 285 source
  16. example (example at line 289) line 289 source
  17. example (example at line 297) line 297 source
  18. example (example at line 315) line 315 source
  19. example (example at line 323) line 323 source
  20. example (example at line 342) line 342 source
  21. example (example at line 354) line 354 source
  22. example (example at line 365) line 365 source
  23. example (example at line 380) line 380 source
  24. example (example at line 395) line 395 source
  25. example (example at line 410) line 410 source
  26. example (example at line 419) line 419 source
  27. example (example at line 432) line 432 source
  28. example (example at line 458) line 458 source
  29. example (example at line 492) line 492 source
  30. example (example at line 512) line 512 source
  31. example (example at line 533) line 533 source
  32. example (example at line 559) sorry line 559 source
  33. example (example at line 574) line 574 source
  34. example (example at line 604) line 604 source
  35. example (example at line 616) line 616 source
  36. example (example at line 627) line 627 source
  37. example (example at line 640) line 640 source
  38. example (example at line 650) line 650 source
  39. example (example at line 659) line 659 source
  40. example (example at line 667) line 667 source
  41. example (example at line 677) line 677 source
  42. example (example at line 693) line 693 source
  43. example from line 718 source
  44. example (example at line 721) line 721 source
  45. example (example at line 748) line 748 source
  46. example (example at line 763) line 763 source
  47. example (example at line 772) line 772 source
  48. def swap_pair Tactics can define data: swapping a pair line 786 source

    L4DEL explanation

    The same tactic script that proves p and q implies q and p also builds a function that swaps the two components of a pair.

    1. The type is α × β → β × α, a function type for products.
    2. intro p introduces the argument; cases p splits the pair into its two components.
    3. constructor <;> assumption builds the new pair, and for each of its two parts assumption finds the matching component in the context.
    4. The book remarks that, up to variable names, this is identical to the proof for conjunction.

    See also: swap_sum

    Sources and attribution: Pinned Lean source (4e28129fdd58)

    def swap_pair : α × β → β × α := by
…

    Mentions: α, β

  49. def swap_sum Swapping the two sides of a sum type line 791 source

    L4DEL explanation

    cases splits on which side of the sum we are in, and each branch rebuilds the value on the opposite side.

    1. The type is Sum α β → Sum β α.
    2. intro p and cases p give one goal per constructor of Sum.
    3. In the first branch apply Sum.inr; assumption wraps the left value on the right; in the second, apply Sum.inl; assumption does the reverse.
    4. The book remarks that this matches the proof of commutativity of disjunction.

    See also: swap_pair

    Sources and attribution: Pinned Lean source (4e28129fdd58)

    cases: the tactic that splits a value or hypothesis by its constructors and gives one goal for each.

    def swap_sum : Sum α β → Sum β α := by
…

    Mentions: α, β

  50. example (example at line 805) line 805 source
  51. example (example at line 820) line 820 source
  52. example (example at line 831) line 831 source
  53. example (example at line 852) line 852 source
  54. structure to line 875 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:526 (different declaration text). Qualify references as to@path.

  55. example (example at line 888) line 888 source
  56. example (example at line 903) line 903 source
  57. example (example at line 922) line 922 source
  58. example (example at line 946) line 946 source
  59. example (example at line 954) line 954 source
  60. example (example at line 973) line 973 source
  61. example (example at line 995) line 995 source
  62. example (example at line 1013) line 1013 source
  63. example (example at line 1032) line 1032 source
  64. theorem (theorem at line 1053) line 1053 source
  65. example (example at line 1093) line 1093 source
  66. example (example at line 1105) line 1105 source
  67. example (example at line 1116) line 1116 source
  68. example (example at line 1119) line 1119 source
  69. example (example at line 1127) line 1127 source
  70. example (example at line 1130) line 1130 source
  71. example (example at line 1133) line 1133 source
  72. example (example at line 1155) line 1155 source
  73. example (example at line 1168) line 1168 source
  74. example (example at line 1179) line 1179 source
  75. example (example at line 1189) line 1189 source
  76. example (example at line 1198) line 1198 source
  77. theorem add_comm line 1220 source
  78. example (example at line 1239) line 1239 source
  79. example (example at line 1256) line 1256 source
  80. example (example at line 1269) line 1269 source
  81. example (example at line 1281) line 1281 source
  82. example (example at line 1296) line 1296 source
  83. example (example at line 1299) line 1299 source
  84. example (example at line 1302) line 1302 source
  85. example (example at line 1325) line 1325 source
  86. def Tuple line 1338 source
  87. example (example at line 1341) line 1341 source
  88. example (example at line 1359) line 1359 source
  89. example (example at line 1362) line 1362 source
  90. example (example at line 1378) line 1378 source
  91. example (example at line 1382) line 1382 source
  92. example (example at line 1390) line 1390 source
  93. example (example at line 1401) line 1401 source
  94. example (example at line 1405) line 1405 source
  95. example (example at line 1440) line 1440 source

    Source comment

    ----
    example (w x y z : Nat) (p : Nat → Prop)
        : x * y + z * w * x = x * w * z + y * x := by
…

    Mentions: x

  96. example (example at line 1444) line 1444 source
  97. def f line 1457 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:340 (different declaration text), book/TPiL/DependentTypeTheory.lean:416 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/InteractingWithLean.lean:468 (different declaration text). Qualify references as f@path.

  98. example (example at line 1460) line 1460 source
  99. example (example at line 1469) line 1469 source
  100. example (example at line 1480) line 1480 source
  101. example (example at line 1488) line 1488 source
  102. example (example at line 1500) line 1500 source
  103. example (example at line 1503) line 1503 source
  104. example (example at line 1506) line 1506 source
  105. example (example at line 1516) line 1516 source

    Source comment

    ----
    example (u w x x' y y' z : Nat) (p : Nat → Prop)
        (h₁ : x + 0 = x') (h₂ : y + 0 = y')
        : x + y + 0 = x' + y' := by
…

    Mentions: x

  106. def mk_symm line 1529 source
  107. def mk_symm line 1538 source
  108. theorem reverse_mk_symm line 1541 source

    Source comment

    ----
    theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
…

    Mentions: α, mk_symm

  109. def mk_symm line 1550 source
  110. theorem reverse_mk_symm line 1552 source
  111. example (example at line 1556) line 1556 source

    Source comment

    ----
    example (xs ys : List Nat)
        : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
…

    Mentions: mk_symm

  112. example (example at line 1560) line 1560 source
  113. def mk_symm line 1572 source
  114. theorem reverse_mk_symm line 1575 source

    Source comment

    ----
    @[simp] theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
…

    Mentions: α, mk_symm

  115. example (example at line 1579) line 1579 source
  116. example (example at line 1583) line 1583 source
  117. def mk_symm line 1593 source
  118. theorem reverse_mk_symm line 1596 source

    Source comment

    ----
    theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
…

    Mentions: α, mk_symm

  119. example (example at line 1602) line 1602 source
  120. example (example at line 1606) line 1606 source
  121. def mk_symm line 1615 source
  122. theorem reverse_mk_symm line 1618 source

    Source comment

    ----
    theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
…

    Mentions: α, mk_symm

  123. example (example at line 1622) line 1622 source
  124. example (example at line 1628) line 1628 source
  125. def mk_symm line 1642 source
  126. theorem reverse_mk_symm line 1645 source

    Source comment

    ----
    theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
…

    Mentions: α, mk_symm

  127. example (example at line 1652) line 1652 source
  128. example (example at line 1656) line 1656 source
  129. def mk_symm line 1682 source
  130. theorem reverse_mk_symm line 1684 source
  131. example (example at line 1688) line 1688 source
  132. example (example at line 1693) line 1693 source
  133. example (example at line 1698) line 1698 source
  134. example (example at line 1708) line 1708 source
  135. example (example at line 1716) line 1716 source
  136. example (example at line 1724) line 1724 source
  137. def f line 1742 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:340 (different declaration text), book/TPiL/DependentTypeTheory.lean:416 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/InteractingWithLean.lean:468 (different declaration text). Qualify references as f@path.

  138. example (example at line 1749) line 1749 source
  139. def f line 1763 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:340 (different declaration text), book/TPiL/DependentTypeTheory.lean:416 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/InteractingWithLean.lean:468 (different declaration text). Qualify references as f@path.

  140. example (example at line 1770) line 1770 source

    Source comment

    ----
    example (x y z : Nat) :
  x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w →
  f x y w = 1 := by
…

    Mentions: x

  141. def g line 1781 source

    Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:341 (different declaration text), book/TPiL/DependentTypeTheory.lean:417 (different declaration text). Qualify references as g@path.

  142. example (example at line 1787) line 1787 source
  143. example (example at line 1809) line 1809 source
  144. example (example at line 1821) line 1821 source
  145. example (example at line 1824) line 1824 source
  146. example (example at line 1830) line 1830 source
  147. example (example at line 1848) sorry line 1848 source