18
$\begingroup$

The most well-known tutorials/learning materials, including Book 1, Chapter 2 of Software Foundations for Coq and the Natural Number Game for Lean, use natural numbers to introduce induction. But there are multiple complaints by new learners that having to prove trivial facts of natural numbers via induction feels unintuitive and intimidating (one example).

Has there been any attempt at a tutorial that doesn't start with natural numbers? I can imagine using monomorphic lists instead, say a list of booleans. For example, proving associativity of list concatenation (a ++ b) ++ c = a ++ (b ++ c) should feel less intimidating (because it is no longer a "trivial" property of natural numbers the students would have taken as granted) and more interesting than proving associativity of addition on natural numbers. And then the properties of natural numbers could be introduced by pointing to similarities with list operations.

Improve this question
$\endgroup$
2
  • $\begingroup$ Some people have worked on Real Number Game for Lean, but I think it has NNG as a "prerequisite", so probably doesn't quite classify as an answer. $\endgroup$
    – Wojowu
    Feb 8, 2022 at 23:57
  • 1
    $\begingroup$ To me associativity of list concatenation seems more trivial that associativity of addition of natural numbers. It's not really possible to understand the statement of associativity of list concatenation without understanding why it's true, while that is possible for associativity of addition of natural numbers. $\endgroup$
    – Will Sawin
    Feb 8, 2022 at 23:57

2 Answers 2

Reset to default
17
$\begingroup$

Patrick Massot's very nice tutorial for Lean takes place in the domain of elementary (epsilon-delta) real analysis. As a mathematician but not a mathematician focused on foundations, this to me feels like a very sensible place to start.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Your answer could be improved with additional supporting information. Please edit to add further details, such as citations or documentation, so that others can confirm that your answer is correct. You can find more information on how to write good answers in the help center. $\endgroup$
    – Community Bot
    Feb 9, 2022 at 0:10
  • 1
    $\begingroup$ At this length, the answer could easily be a comment, and could by some people be considered a "link-only" answer. I upvoted you, but I also encourage you to expand the answer a bit! $\endgroup$
    – Nike Dattani
    Feb 9, 2022 at 0:11
  • 1
    $\begingroup$ @NikeDattani, sure, what would you like to know? $\endgroup$
    – macbeth
    Feb 9, 2022 at 0:16
  • $\begingroup$ I had nothing specific in mind. Please see this comment by Slate which indicates that I'm not the only one encouraging more detailed answers. $\endgroup$
    – Nike Dattani
    Feb 9, 2022 at 0:19
  • $\begingroup$ I guess "don't teach induction at all" is probably a valid answer (I checked the entire repo and induction is used only once for a given lemma), but I'd prefer one that actually teaches induction but not with natural numbers (if such a thing exists). $\endgroup$
    – Bubbler
    Feb 9, 2022 at 0:20
10
$\begingroup$

Joseph Hua, Ken Lee, and Bendit Chan have recently released the HoTT Game, designed as an introduction to Cubical Agda for mathematicians with no proof verification experience. The two parts of this tutorial are Trinitarianism (nicely summarized here) which introduces all the basic notions of (homotopy) type theory, and Fundamental Group of the Circle, whose goal is showing that $\pi_1(S^1)\cong\mathbb Z$.

Granted, at some points working with $\mathbb Z$ reduces to working with (two copies of) $\mathbb N$, but unlike the tutorials mentioned in the original post, the theorems of this tutorial are not about arithmetic of $\mathbb N$.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ This one looks great - and I should take another try to get into cubical agda with this :) $\endgroup$
    – Bubbler
    Feb 10, 2022 at 23:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.