exercise7

To play this document inside your browser use ALT-N and ALT-P.

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

Exercise 1 :

Prove this statement by induction or
alternatively by using big_morph

Exercise 2 :

Prove this statement by using big_morph

Exercise 3 :

Prove this statement by induction.
Relevant lemmas are
- doubleS odd_double addn0 addnn mulnn
- big_mkcond big_nat_recr big_geq

Exercise 4 :

Prove this statement by induction.
Relevant lemmas are
- doubleD muln2 addn2 big_nat_recr big_geq

In what follows we are going to mimic the proof of Gauss :

       1 +     2 + .....        +  n.-2     + n.-1
 +  n.-1 +  n.-2 +              +     2     +    1

   = n.-1 * n

Exercise 5 :

Prove this statement without induction.
Relevant lemma is big_nat_rev

Exercise 6 :

Prove this statement without induction.
Relevant lemma is addnn

Exercise 7 :

Prove this statement without induction.
Relevant lemma are big_split and eq_big_nat

Exercise 8 :

Prove this statement without induction.
Relevant lemma are sum_nat_const_nat

Exercise 9 :

Prove this statement using exercises 5-8

Exercise 10 :

Prove this statement directly without using the lemmas
defined in exercises 5-9

Now we try to prove the sum of squares.

We first define the property for a function to be increasing

Exercise 11 :

Prove this statement by induction

Exercise 12 :

Prove this statement using exercise 9
Hint : subnK

Exercise 13 :

Proof by induction
Hints : addnCA subnK fincr_leq big_geq

Exercise 14 :

Proof using the previous lemma
Hints : leq_exp2r

We give the proof of a technical result

Exercise 15 :

Hints : big_split sum_mll sum_gauss sum_gauss_const

Exercise 16 :

Hints : big_split sum_mll sum_gauss sum_gauss_const

Another technical lemma

Exercise 17 :

Hint : addIn sum_sum4 sum_tech.

Exercise 18 :

Prove the theorem directly using only sum_gauss and the tactic sring.