book/TPiL/InductionAndRecursion.lean

GitHub source file

191 declarations, 7 contain sorry, 0 declared as axioms

Imports (2)
  1. def sub1 line 60 source
  2. def isZero line 64 source
  3. def sub1 line 73 source
  4. def isZero line 76 source
  5. example (example at line 80) line 80 source

    Source comment

    ----
    example : sub1 0 = 0 := rfl

    Mentions: sub1

  6. example (example at line 81) line 81 source
  7. example (example at line 83) line 83 source
  8. example (example at line 84) line 84 source
  9. example (example at line 86) line 86 source
  10. example (example at line 87) line 87 source
  11. def sub1 line 95 source

    Source comment

    ------
    def sub1 : Nat → Nat
  | 0     => 0
  | x + 1 => x

    Mentions: x

  12. def isZero line 99 source
  13. def swap line 112 source
  14. def foo line 115 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

  15. def bar line 118 source
  16. def Hidden.not line 129 source

    Source comment

    ----
    def not : Bool → Bool
  | true  => false
  | false => true
  17. theorem Hidden.not_not line 133 source
  18. example (example at line 143) line 143 source
  19. example (example at line 146) line 146 source
  20. def sub2 line 158 source
  21. def sub2 line 173 source
  22. example (example at line 178) line 178 source

    Source comment

    ----
    example : sub2 0 = 0 := rfl

    Mentions: sub2

  23. example (example at line 179) line 179 source
  24. example (example at line 180) line 180 source
  25. example (example at line 182) line 182 source
  26. def sub2 line 187 source
  27. def sub2 line 199 source
  28. example (example at line 212) line 212 source

    Source comment

    ------
    example (p q : α → Prop) :
        (∃ x, p x ∨ q x) →
        (∃ x, p x) ∨ (∃ x, q x)
  | Exists.intro x (Or.inl px) => Or.inl (Exists.intro x px)
  | Exists.intro x (Or.inr qx) => Or.inr (Exists.intro x qx)

    Mentions: α, x

  29. def foo line 218 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

  30. example (example at line 225) line 225 source
  31. def foo line 231 source

    Source comment

    ------

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

    def foo : Nat → Nat → Nat
  | 0,     n     => 0
  | m + 1, 0     => 1
  | m + 1, n + 1 => 2
```

Here is another example:

```lean
set_option linter.unusedVariables false
--------

    Mentions: n, m, is

  32. def bar line 242 source

    Source comment

    ------
    def bar : List Nat → List Nat → Nat
  | [],      []      => 0
  | a :: as, []      => a
  | [],      b :: bs => b
  | a :: as, b :: bs => a + b
```

Note that the patterns are separated by commas.

In each of the following examples, splitting occurs on only the first
argument, even though the others are included among the list of
patterns.
…

    Mentions: as, b, bs

  33. def Hidden.and line 259 source

    Source comment

    ----
    def and : Bool → Bool → Bool
  | true,  a => a
  | false, _ => false
  34. def Hidden.or line 263 source
  35. def Hidden.cond line 267 source
  36. def tail line 288 source

    Source comment

    ------
    def tail : List α → List α
  | []      => []
  | a :: as => as
```

:::leanFirst
As described in {ref "inductive-types"}[Inductive Types],

    Mentions: α, as, in

  37. inductive data line 295 source

    Distinct definitions of this name: book/TPiL/StructuresAndRecords.lean:44 (different declaration text). Qualify references as data@path.

  38. def tail1 line 304 source

    Source comment

    ------
    def tail1 {α : Type u} : List α → List α
  | []      => []
  | a :: as => as

    Mentions: α, as

  39. def tail2 line 308 source
  40. def foo line 334 source

    Source comment

    ------

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

    def foo : Nat → Nat → Nat
  | 0,     n     => 0
  | m + 1, 0     => 1
  | m + 1, n + 1 => 2
```

An alternative presentation is:

```lean
set_option linter.unusedVariables false
--------

    Mentions: n, m, is

  41. def foo line 345 source

    Source comment

    ------

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

    def foo : Nat → Nat → Nat
  | 0, n => 0
  | m, 0 => 1
  | m, n => 2
```

In the second presentation, the patterns overlap; for example, the
pair of arguments {lit}`0, 0` matches all three cases. But Lean handles
the ambiguity by using the first applicable equation, so in this example
the net result is the same. In particular, the following equations hold
definitionally:
…

    Mentions: n, m, in, is

  42. def foo line 358 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

  43. example (example at line 363) line 363 source

    Source comment

    ----
    example : foo 0       0       = 0 := rfl
  44. example (example at line 364) line 364 source
  45. example (example at line 365) line 365 source
  46. example (example at line 366) line 366 source
  47. def foo line 372 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

  48. class (class at line 390) line 390 source
  49. def f1 line 405 source
  50. example (example at line 410) line 410 source
  51. example (example at line 411) line 411 source
  52. example (example at line 412) line 412 source
  53. example (example at line 413) line 413 source
  54. def f2 line 415 source
  55. example (example at line 420) line 420 source
  56. example (example at line 421) line 421 source
  57. example (example at line 422) line 422 source
  58. example (example at line 423) line 423 source
  59. def bar line 431 source
  60. def foo line 445 source

    Source comment

    -----

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

    def foo : Char → Nat
  | 'A' => 1
  | 'B' => 2
  | _   => 3

#print foo.match_1
```

# Structural Recursion and Induction
%%%
tag := "structural-recursion-and-induction"
…
  61. def foo line 469 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

  62. def add line 505 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:600 (different declaration text), book/TPiL/InteractingWithLean.lean:231 (different declaration text). Qualify references as add@path.

  63. theorem add_zero line 509 source
  64. theorem add_succ line 510 source
  65. theorem zero_add line 512 source
  66. def mul line 516 source
  67. def add line 537 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:600 (different declaration text), book/TPiL/InteractingWithLean.lean:231 (different declaration text). Qualify references as add@path.

  68. theorem zero_add line 541 source

    Source comment

    ---
    theorem zero_add : ∀ n, add zero n = n
  | zero   => by simp [add]
  | succ n => by simp [add, zero_add]
```

As with definition by pattern matching, parameters to a structural
recursion or induction may appear before the colon. Such parameters
are simply added to the local context before the definition is
processed. For example, the definition of addition may also be written
as follows:

```lean
…

    Mentions: n, is, as

  69. def add line 554 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:600 (different declaration text), book/TPiL/InteractingWithLean.lean:231 (different declaration text). Qualify references as add@path.

  70. def add line 563 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:600 (different declaration text), book/TPiL/InteractingWithLean.lean:231 (different declaration text). Qualify references as add@path.

  71. def fib line 573 source
  72. example (example at line 578) line 578 source
  73. example (example at line 580) line 580 source
  74. example (example at line 582) line 582 source
  75. example (example at line 584) line 584 source
  76. def fibFast line 602 source
  77. def fibFast line 615 source
  78. def fib line 659 source
  79. def append line 677 source
  80. example (example at line 681) line 681 source
  81. def listAdd line 688 source
  82. def replicate line 706 source
  83. def replicate line 725 source
  84. theorem length_replicate line 731 source

    Source comment

    ----
    theorem length_replicate (n : Nat) (a : α) :
    (replicate n a).length = n := by
…

    Mentions: n, α, replicate

  85. def replicate line 745 source
  86. theorem length_replicate line 752 source
  87. example (example at line 796) line 796 source
  88. def r' line 805 source
  89. example (example at line 807) line 807 source
  90. example (example at line 808) line 808 source
  91. def f line 833 source

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

  92. theorem div_lemma line 878 source
  93. def div.F line 881 source
  94. def div line 887 source
  95. theorem div_lemma line 902 source
  96. def div.F line 905 source
  97. def div line 911 source
  98. example (example at line 913) line 913 source

    Source comment

    ---
    example : div 8 2 = 4 := by rfl
…

    Mentions: div

  99. theorem div_lemma line 925 source
  100. def div.F line 928 source
  101. def div line 934 source
  102. example (example at line 936) line 936 source

    Source comment

    ---
    example : div 8 2 = 4 := by
…

    Mentions: div

  103. def div line 946 source
  104. def div line 967 source
  105. example (example at line 974) line 974 source

    Source comment

    ----
    example (x y : Nat) :
    div x y =
    if 0 < y ∧ y ≤ x then
      div (x - y) y + 1
    else 0 := by
…

    Mentions: x, div

  106. example (example at line 983) sorry line 983 source
  107. def natToBin sorry line 998 source
  108. def ack line 1018 source
  109. def ack line 1030 source
  110. instance (instance at line 1045) line 1045 source
  111. def takeWhile line 1055 source
  112. def takeWhile line 1073 source
  113. theorem div_lemma line 1091 source
  114. def div line 1094 source
  115. def ack sorry line 1106 source
  116. def natToBin sorry line 1123 source
  117. def unsound sorry line 1138 source

    Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:328 (different declaration text). Qualify references as unsound@path.

  118. def ack line 1176 source
  119. theorem ack_gt_zero line 1181 source
  120. def ack line 1229 source
  121. theorem ack_gt_zero line 1234 source

    Source comment

    -----------
    theorem ack_gt_zero : ack n m > 0 := by
…

    Mentions: ack, n, m

  122. def f line 1245 source

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

  123. def f line 1257 source

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

  124. theorem f_or sorry line 1264 source

    Source comment

    ----
    theorem f_or : f b1 b2 b3 b4 b5 = (b1 || b2 || b3 || b4 || b5) := by
…

    Mentions: b1, b2

  125. def f line 1324 source

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

  126. theorem f_or line 1331 source

    Source comment

    ----
    theorem f_or : f b1 b2 b3 b4 b5 = (b1 || b2 || b3 || b4 || b5) := by
…

    Mentions: b1, b2

  127. example (example at line 1355) line 1355 source
  128. example (example at line 1358) line 1358 source
  129. theorem even_eq_not_odd line 1361 source
  130. inductive Even line 1389 source
  131. inductive Odd line 1392 source
  132. theorem not_odd_zero line 1398 source
  133. theorem even_of_odd_succ line 1401 source
  134. theorem odd_of_even_succ line 1404 source
  135. inductive Term line 1412 source
  136. inductive Term line 1420 source
  137. def sample line 1436 source
  138. inductive Term line 1447 source
  139. def Term.numConsts line 1452 source
  140. inductive Vect line 1498 source
  141. def map line 1502 source
  142. def zip line 1506 source
  143. def unzip line 1510 source
  144. def tail line 1516 source
  145. inductive families line 1527 source
  146. inductive Vect line 1536 source
  147. inductive Vect line 1568 source
  148. def Vect.tailAux line 1573 source

    Source comment

    ----
    def tailAux (v : Vect α m) : m = n + 1 → Vect α n :=
…

    Mentions: Vect, α, m, n

  149. def Vect.tail line 1580 source
  150. inductive Vect line 1605 source
  151. def Vect.head line 1610 source

    Source comment

    ----
    def head : {n : Nat} → Vect α (n+1) → α
  | n, cons a as => a

    Mentions: n, Vect, α, cons, as

  152. def Vect.tail line 1613 source
  153. theorem Vect.eta line 1616 source
  154. def Vect.map line 1619 source
  155. def Vect.zip line 1623 source
  156. inductive Vect line 1637 source
  157. def Vect.zipWith line 1642 source

    Source comment

    -----
    def zipWith (f : α → β → γ) : {n : Nat} → Vect α n → Vect β n → Vect γ n
  | 0,   nil,       nil       => nil
  | n+1, cons a as, cons b bs => cons (f a b) (zipWith f as bs)

#print zipWith
#print zipWith.match_1
------
end Vect
```

:::setup
```

    Mentions: α, β, n, Vect, cons, as, b, bs

  158. inductive Vect line 1654 source
  159. inductive ImageOf line 1695 source
  160. def inverse line 1700 source
  161. def inverse' line 1703 source
  162. inductive Vect line 1719 source
  163. def Vect.add line 1723 source
  164. inductive Vect line 1744 source
  165. def Vect.add line 1749 source

    Source comment

    ----
    def add [Add α] : {n : Nat} → Vect α n → Vect α n → Vect α n
  | .(_), nil,       nil       => nil
  | .(_), cons a as, cons b bs => cons (a + b) (add as bs)
-------
end Vect
```

Marking the position as an inaccessible pattern tells the
equation compiler first, that the form of the argument should be
inferred from the constraints posed by the other arguments, and,
second, that the first argument should _not_ participate in pattern
matching.
…

    Mentions: α, n, Vect, cons, as, b, bs, from, in

  166. inductive Vect line 1765 source
  167. def Vect.add line 1770 source

    Source comment

    ----
    def add [Add α] : {n : Nat} → Vect α n → Vect α n → Vect α n
  | _, nil,       nil       => nil
  | _, cons a as, cons b bs => cons (a + b) (add as bs)
-------
end Vect
```

As we mentioned above, the argument {leanRef}`{n : Nat}` is part of the
pattern matching, because it cannot be held fixed throughout the
definition. Rather than requiring that these discriminants be provided explicitly, Lean implicitly includes
these extra discriminants automatically for us.
…

    Mentions: α, n, Vect, cons, as, b, bs, above, is

  168. inductive Vect line 1783 source
  169. def Vect.add line 1788 source

    Source comment

    ----
    def add [Add α] {n : Nat} : Vect α n → Vect α n → Vect α n
  | nil,       nil       => nil
  | cons a as, cons b bs => cons (a + b) (add as bs)
-------
end Vect
```

When combined with the _auto bound implicits_ feature, you can simplify
the declare further and write:

```lean

    Mentions: α, n, Vect, cons, as, b, bs

  170. inductive Vect line 1799 source
  171. def Vect.add line 1804 source

    Source comment

    ----
    def add [Add α] : Vect α n → Vect α n → Vect α n
  | nil,       nil       => nil
  | cons a as, cons b bs => cons (a + b) (add as bs)
-------
end Vect
```

Using these new features, you can write the other vector functions defined
in the previous sections more compactly as follows:

```lean
set_option linter.unusedVariables false

    Mentions: α, Vect, n, cons, as, b, bs, in

  172. inductive Vect line 1816 source
  173. def Vect.head line 1821 source

    Source comment

    ----
    def head : Vect α (n+1) → α
  | cons a as => a

    Mentions: Vect, α, n, cons, as

  174. def Vect.tail line 1824 source
  175. theorem Vect.eta line 1827 source
  176. def Vect.map line 1830 source
  177. def Vect.zip line 1834 source
  178. def isNotZero line 1852 source

    Source comment

    ----
    def isNotZero (m : Nat) : Bool :=
…

    Mentions: m

  179. def isNotZero line 1865 source

    Source comment

    -----
    def isNotZero (m : Nat) : Bool :=
…

    Mentions: m

  180. def filter line 1870 source
  181. example (example at line 1877) line 1877 source
  182. def foo line 1883 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InteractingWithLean.lean:784 (different declaration text). Qualify references as foo@path.

  183. example (example at line 1892) line 1892 source
  184. def bar₁ line 1899 source
  185. def bar₂ line 1902 source
  186. def bar₃ line 1906 source
  187. def bar₄ line 1909 source
  188. example (example at line 1918) line 1918 source
  189. example (example at line 1921) line 1921 source
  190. example (example at line 1926) line 1926 source
  191. example (example at line 1929) sorry line 1929 source