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 inside your browser and . Finally, you can 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!