Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line. Use ALT-(right-arrow) to go to the cursor. You can save your edits inside your browser and load them back. Finally, you can download your working copy of the file, e.g., for sending it to teachers.

what follows is a slide, it creates an index item next to the scroll bar, just move the mouse there.

Induction and structured proofs

Exercise 1

Let us prove directly formula \[ \sum_{i=0}^{n-1} (2 i + 1) = n ^ 2 \] from lesson 1, slightly modified.

Let us first recall custom sum operator:

  • First prove a very useful lemma about iota (you can use iota_add) (Easy)

  • Then prove a very useful lemma about summation. (Medium)

  • Now use the previous result to get the main result (Easy - Medium)


Exercise 2

Prove that the equation \[ 8y = 6x + 1 \] has no solution. (Easy)

  • Hint 1: take the modulo 2 of the equation (using suff).
  • Hint 2: Search _ "contra" in MC and use the view eqP.
  • Hint 3: Search _ modn addn in MC and Search _ modn muln in MC

Exercise 3:

The ultimate Goal of this exercise is to find the solutions of the equation \[ 2^n = a^2 + b^2,\] where n is fixed and a and b unkwown. We hence study the following predicate:

  • We give the set of solutions for \(n = 0\) or \(1\)

  • Now prove a little lemma that will guarantee that a and b are even. (Medium - Hard)
    • Hint: Search _ (_ ^ 2) (_ + _) in MC.
    • Hint: Search ((_ * _) ^ _) in MC.
    • ...
    • Hint: About divn_eq to substitute a and b (rewrite {1}(div_eq ...))
    • Hint: Search _ modn odd in MC.

  • Do it on paper first!

  • Deduce that if n is greater than 2 and a and b are solutions, then they are even. (HARD)

  • Prove that the solutions for n are the halves of the solutions for n + 2.
    • Hint: Search _ odd double in MC and Search _ "eq" "mul" in MC.

  • Prove there are no solutions for n even (Easy)
    • Hint: Use sol0 and solSS.

  • Certify the only solution when n is odd. (SUPER HARD)
    • Hint 1: Use sol1, solSS and sol_are_even.
    • Hint 2: Really sketch it on paper first!