# Equations

Matthieu Sozeau

In these exercises we will practice equations by working with different implementations of vectors and matrices. The exercises are marked with stars, where 1 star exercises are the simplest and exercises with more start are more complicated. In order to complete some of the exercises you may need to define your own additional definitions/lemmas.
Recall our definition of [vec] as an inductive type.
We derive [Signature] for [vec] here, so that the equations plugin will not reprove this every time it is needed.
We will be using the following notations for convenience.
Recall our definitions of [head], [tail] and [decompose].

### Exercise, 2 star:

Finish the following proof that a vector with zero elements is [nil].

### Exercise, 3 star:

Finish the definition of [rev], the function which reverses a vector.

### Exercise, 1 star:

Show that [rev] satisfies the examples [rev_0] and [rev_3] below.

### Exercise, 3 star:

Prove that [rev] is an involution [rev_involution].
We can implement the type [fin n] of numbers strictly less than [n : nat] with the following inductive definition.
For example, [fin 3] has the following inhabitants:
But [fS (fS (fS f0))] is not an inhabitant of [fin 3]:
The following definition [fvec] is an alternative way to define a vector data type.
The head of an [fvec] is given by the element at [f0].
The definition [ftail] gives the tail of an [fvec].
Notice that the following check succeeds.

### Exercise, 2 star:

Finish the following definition of [fnil], which is the [fvec A 0] corresponding to [nil : vec A 0].
The following check should succeed.

### Exercise, 2 star:

Finish the following definition of [fcons], which is the [fvec A (S n)] corresponding to [cons : vec A (S n)].
The following check should succeed.

### Exercise, 1 star:

To test your implementation of [fnil] and [fcons], prove the examples [fidx_0], [fidx_1], [fidx_2].

### Exercise, 2 star:

Finish the definition of [idx], which is the function for indexing a [vec], i.e. [idx v f] is the element at index [f] in vector [v].
Notice that [@idx A n] is a function from [vec A n] to [fvec A n].

### Exercise, 1 star:

To test, prove the examples [idx_0], [idx_1], [idx_2].

### Exercise, 3 star:

Finish [unidx], the inverse of [idx]. It is the unique function satisfying the Lemmas [unidx_idx] and [idx_unidx].

### Exercise, 3 star:

Finish the following Lemma [unidx_idx].

### Exercise, 3 star:

Finish Lemma [idx_unidx'].

### Exercise, 2 star:

Finish Lemma [idx_unidx]. Hint: Look at the imports in the top of this file.

### Exercise, 3 star:

The Lemmas [idx_unidx] and [unidx_idx] show that there is a bijective correspondence between [vec A n] and [fvec A n]. Finish the examples [nil_to_fnil], [cons_to_fcons], [fnil_to_nil] and [fcons_to_cons] to show that your implementation of [fnil] and [fcons] corresponds to [nil] and [cons], respectively, under this bijective correspondence.
We define a matrix [mtx] as a vector of vectors.
We think of [mtx A m n] as an m by n matrix. For example:
Similarly, an [fmtx] is an fvector of fvectors.

### Exercise, 2 star:

Finish the following definition of [midx]. It is supposed to satisfy that [midx M f g] is the matrix entry at (f,g).

### Exercise, 1 star:

Test your definition of [midx] by finishing the examples [midx_0_0], [midx_0_1], [midx_1_1], [midx_1_2].
Notice that [@midx A m n] is a function from [mtx A m n] to [fmtx A m n].

### Exercise, 3 star:

Finish the definition of [unmidx], the inverse function of [midx], satisfying Lemmas [unmidx_midx] and [midx_unmidx].

### Exercise, 4 star:

Prove Lemma [unmidx_midx].

### Exercise, 4 star:

Prove Lemma [midx_unmidx'].

### Exercise, 2 star:

Prove Lemma [midx_unmidx].

### Exercise, 2 star:

Finish definition [transpose_fmtx] to compute the transpose of an [fmtx].

### Exercise, 2 star:

Show that [transpose_fmtx] is correct by proving Lemma [transpose_fmtx_is_transpose].

### Exercise, 4 star:

Define the transpose of an [mtx]. Consider the strong relationship [unmidx_midx], [midx_unmidx] we have between [mtx] and [fmtx]. Name your definition [transpose_mtx]. Implement [transpose_mtx : forall {A m n}, mtx A m n -> mtx n m] below here.

### Exercise, 4 star:

Show that your [transpose_mtx] definition is correct by proving Lemma [transpose_mtx_is_transpose].