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:

  • filtrev has an accumulator, rev (at least apparently) does not.
  • which is the invariant linking the accumulator acc and p in the code of filtrev? Depending on how you expose the accumulator on the right hand side of the goal, such invariant may need to be taken into account by the induction.

Relevant keywords for Search are: rev cons cat filter rcons Hint: it is perfectly fine to state intermediate lemmas

Prove that if (s1 :|: s2) is disjoint from (s1 :|: s3) then s1 is empty

Prove the equivalence of these two sums. E.g. (n=8)

    1 + 3 + 5 + 7 = 7-0 + 7-2 + 7-4 + 7-6

Now, some algebra.

We remind what Gauss integer are and recall some theory about it.

Prove these two facts. (Hint: conjugation is a morphism)

Question: Prove that GI euclidean for the stasm gaussNorm.

  • i.e. ∀ (a, b) ∈ GI × GI*, ∃ (q, r) ∈ GI² s.t. a = q b + r and φ(r) < φ(b)
  • Suggested strategy: sketch the proof on a paper first, don't let Coq divert you from your proofsketch
  • We first sketch the paper proof here and then do it in Coq:
    • take a / b = x + i y
    • take u the closest integer to x, and v the closest integer to y
    • satisfy the existential with q = u + i v and r = a - q b, which are both Gauss integers.
    • We want to show that |a - q b|² < |b|².
    • It suffices to show |a / b - q|² < 1
    • But |a / b - q|² = (u - x)² + (v - x)² ≤ ‌½² + ½² < 1
  • Now we give a Coq proof with holes, fill in the holes.

Definition and properties of lagrange polynomials.

You can prove only one of the following lemmas

Endomorphisms u such that Ker u ⊕ Im u = E.

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.

  • Assume u o v = 0 and v + u is invertible,
    • we have rank (v + u) = n
    • we have rank v + rank u = n and we have Im v ⊂ Ker u
    • Hence we have Im v = Ker u
    • We deduce that Ker u ⊕ Im u = Im v ⊕ Im u = E

save script