To play this document inside your browser use ALT-N and ALT-P.
If you get stack overflow
errors, try to use
Google Chrome
or Chromium
with the command line option --js-flags="--harmony-tailcalls".
You can
inside your browser and (edits are also saved when you close the window). Finally you can the file for offline editing.Classical logic is somewhat surprising! Prove that given two arbitrary propositions a and b, either a implies b or the converse
Enrico is a lazy student. When asked to reverse and filter a list he comes up with the following ugly code.
The teacher asks him to prove that his ugly code is equivalent to the nicer code [seq x <- rev l | p x] he could have written by reusing the seq library.
Such proof is not trivial:
Relevant keywords for Search are: rev cons cat filter rcons Hint: it is perfectly fine to state intermediate lemmas
Prove the equivalence of these two sums. E.g. (n=8)
1 + 3 + 5 + 7 = 7-0 + 7-2 + 7-4 + 7-6
Even the Mathematical Components library misses some theorems, for example the following one.
Would you help us improve the library with this lemma?
Hint: check out the theory of iota
Now, some algebra.
Big operations and zmodType. Now that ring_scope is open we are in an algebraic setting. Think about the meaning of + now, and find the right injectivity lemma.
We remind what Gauss integer are and recall some theory about it.
Prove these two facts. (Hint: conjugation is a morphism)
paper proofhere and then do it in Coq:
Prove only one of the following lemmas
Taylor formula for polynomials
The endomorphisms of a space E of finite dimension n, such that u o v = 0 and v + u is invertible are exactly the endomorphisms such that Ker u ⊕ Im u = E.