Try to define a next function over 'I_n that correspond to the
successor function over the natural plus the special case that
n -1
is mapped to zero
Hint: potentially useful theorems are: ltn_neqAle, ltnS, negbT, ifP
Hint: potentially useful tactics are case, move, rewrite
Hint: you may also need to use the val function (or \val notation)
These should return 3 and 0 respectively.
Show that injectivity is decidable for a function f : aT -> rT when aT is a finite type.
As a first step, we exhibit a boolean formulation of injectivity:
a boolean formula, based on boolean forall
, exists
, and ==>
and
boolean equality, which expresses the property of injectivity.
We then show that this boolean formula is equivalent to th existing notion of injective, which is not injective in general.
Build a function that maps an element of an ordinal to another element of the same ordinal with a p subtracted from it.
Hint: if i has type 'I_n, then i can also be used for type nat and i < n is given by theorem ltn_ord. Others potentially useful theorems are leq_ltn_trans and leq_subr
Prove the following statement by induction in several ways.
2 * (1 + 2 ... + n) = (1 + 2 ... + (n - 1) + n) + (n + (n - 1) ... + 2 + 1) = (1 + n) + (2 + n - 1) + ... + (n + 1) = n * (1 + n)
Try to formalize the following problem
Given a parking where the boolean indicates if the slot is occupied or not
Number of cars at line i
Number of cars at column j
Show that if 0 < n there is always two lines, or two columns, or a column and a line that have the same numbers of cars
Prove the following statement by induction and by using a similar trick as for Gauss noticing that n ^ 3 = n * (n ^ 2)
Prove the following statement using only big operator theorems. big_cat_nat, big_nat_cond, big_mkcondl, big1
building a monoid law