Lecture Notes, Week 10

• More tactics
  • Resources
  • The simpl tactic
  • Interlude
  • Executive summary
  • A perspicuous use of the injection tactic
  • The do tactic
  • Exercise 01
  • Solution for Exercise 01
  • The repeat tactic
  • DANGER, WILL ROBINSON
  • Resources
  • Version
• Formalizing summations
  • Resources
  • Exercise 02
  • Exercise 03
  • Towards a solution for Exercise 03
  • Resources
  • Version
• The problem with substracting natural numbers
  • Summations
  • A property of non-decreasing nat-valued functions
  • The fundamental theorem of calculus for non-decreasing nat-valued functions
  • The fundamental theorem of calculus for nat-valued functions
  • Exercise 04
  • Solution for Exercise 04
  • Postlude
  • Exercise 06
  • Solution for Exercise 06
  • Post-postlude
  • Acknowledgment
  • Resources
  • Version
• Integers
  • Resources
  • Prelude
  • Summations over integers
  • The fundamental theorem of calculus for int-valued functions
  • Abel’s lemma for int-valued functions
  • Absolute values
  • Two identities about absolute values
  • Divisibility of polynomials
  • Exercise 07
  • Exercise 08
  • Solution for Exercise 08a
  • Exercise 09
  • Exercise 10
  • Interlude
  • Executive summary
  • Exercise 11
  • Exercise 12
  • Exercise 13
  • Acknowledgments
  • Resources
  • Version
• Formalizing two-by-two matrices
  • Resources
  • Exercise 04
  • Exercise 05
  • Resources
  • Version
• A Fibonacci structure
  • Goal
  • Resources
  • The structure
  • The standard Fibonacci function over natural numbers
  • Computing Fibonacci numbers by exponentiating a 2x2 matrix of natural numbers
  • Exercise 06
  • A perhaps unexpected property
  • Another instance of a Fibonacci structure
  • Polymorphic 2x2 matrices
  • Revisiting the 2x2 matrices of natural numbers
  • Layering a Fibonacci structure on top of another
  • Structure vs. nature
  • Structure vs. nature: the base case
  • Structure vs. nature: the induction step
  • The stepping stone
  • Resources
  • Version
• Exercises for Week 10
  • Exercise 00
  • Mandatory exercises
  • Exercise from Week 06
  • Version
• Index of concepts for Week 10
  • Version