I'm trying to define `list_of_fins`

which would give me list of fins (from 0 to i), but without any adequate success.

Can someone help?

```
Definition fin n := { i | i < n }.
Coercion fin_proj1 n: fin n → nat := λ f, proj1_sig f.
Definition list_of_fins n (i: fin n): list (fin n).
Proof. Admitted.
```

It seems I did it, hoorah.

```
Definition list_of_fins (n: nat) (i: fin n): { L: list (fin n) | map (@fin_proj1 n) L = seq 0 (S i) }.
Proof.
destruct i as [i H]. induction i.
+ exists ((exist (λ x, x < n)%nat _ H) :: nil).
simpl. auto.
+ assert (i < n)%nat by lia. destruct (IHi H0) as [L H1]. simpl in *.
exists (L ++ (exist (λ x, x < n)%nat _ H) :: nil).
rewrite map_app. rewrite H1. simpl. f_equal.
clear H IHi H0 L H1 n.
{ replace (seq 1 i ++ S i :: nil) with (seq 1 (S i)).
replace (1 :: seq 2 i)%nat with (seq 1 (S i)).
auto.
{ simpl. auto. }
{ rewrite seq_S. simpl. auto. } }
Defined.
```

The result of `Eval cbv in list_of_fins 1`

is quite a mess though, so this implementation might give you a hard time further down the road. Also there is no instance of `fin 0`

so that you can't call this function for n=0 to get an empty list.

I would split this into several functional and proof pieces. Say a function which creates a sequence from 0..n-1, a proof that all elements of such a sequence are <n and then a function which uses the sequence and the proof to construct the fin n instances - which is trivial then.

The specification proof `map (@fin_proj1 n) L = seq 0 (S i)`

you can do separately then for the result of the function.

In general one needs to be careful to use dependent types not more than necessary. It is frequently easier to have a simple function and prove its properties than to have a complicated function which includes its properties in a dependent type. The latter only works easily if this property included in the type is the only property you ever want to know about this function, because the function is so complicated that it will be close to impossible to prove anything else about it.

In your case, the property in the type looks pretty complete, though, so you might get along with it - except that it doesn't work for n=0.

I agree

This type might in fact be okay, as long as you Qed all the proof parts; I recommend abstract or Qed’d obligations for that.

@Paolo Giarrusso : the function has an argument (i : fin n). One still has to supply it if n=0, even if the function wouldn't need it because it returns an empty list. What am I missing?

Sorry I read too quickly, you were clear the first time.

It's debatable if using it with n = 0 is desirable, but both options make sense.

Thank you both!

Rewrote it like this. (I'm using the axiom of proof irrelevance.)

```
Definition list_of_fins n (i: fin (S n)): list (fin (S n)).
Proof.
destruct i as [i H]. induction i.
+ exact ((exist (λ x, x < S n)%nat _ H) :: nil).
+ assert (i < S n)%nat by abstract lia.
exact (IHi H0 ++ (exist (λ x, x < S n)%nat _ H) :: nil).
Defined.
Definition list_of_fins_property (n: nat) (i: fin (S n)): map (@fin_proj1 (S n)) (list_of_fins i) = seq 0 (S i).
Proof.
destruct i as [i H]. induction i.
+ simpl. auto.
+ assert (i < S n)%nat by lia. pose proof (IHi H0).
simpl in *. rewrite map_app. simpl.
replace (list_of_fins_subproof H) with H0 by apply ProofIrrelevance.
rewrite H1. simpl. f_equal. rewrite <- seq_S. auto.
Qed.
```

I'm staying with fins as dependent type for now.

Oh, I didn't mean to not use dependent types for fin itself. What I meant is that it might be a good idea to type your function with `list (fin n)`

instead of `map (@fin_proj1 (S n)) (list_of_fins i) = seq 0 (S i).`

and prove that it actually returns this value in a separate lemma (as you did above). Putting this proof inside the computational function itself makes the function substantially more complicated at little gained value. It is usually a good idea to keep computation and proofs separated as much as possible.

Here is an alternative (without the final spec proof - it is more about the evaluated output of the functions):

```
Require Import List.
Require Import Lia.
Definition fin n := { i | i < n }.
Coercion fin_proj1 n: fin n -> nat := fun f => proj1_sig f.
Lemma Forall_Lt_Sn (n : nat) (l : list nat):
Forall (fun i : nat => i < n) l ->
Forall (fun i : nat => i < S n) (map S l).
Proof.
intros H.
induction l.
- constructor.
- constructor; inversion H.
+ lia.
+ apply IHl; assumption.
Qed.
Lemma seq_n_less: forall (n : nat), Forall (fun i => i<n) (seq 0 n).
Proof.
intros n.
induction n.
- constructor.
- constructor.
+ lia.
+ fold seq. rewrite <- seq_shift. apply Forall_Lt_Sn. assumption.
Qed.
Lemma Forall_sig {A : Type} {P : A -> Prop} (l : list A) (F : Forall P l) : list (sig P).
Proof.
induction l.
- exact nil.
- exact (exist P a (Forall_inv F) :: (IHl (Forall_inv_tail F))).
Defined.
Definition list_of_fins' (n : nat) : list (fin n) :=
Forall_sig (seq 0 n) (seq_n_less n).
```

With this `Eval cbv in list_of_fins' 3`

results in:

```
= exist (fun i : nat => S i <= 3) 0 (Forall_inv (seq_n_less 3))
:: exist (fun i : nat => S i <= 3) 1
(Forall_inv (Forall_inv_tail (seq_n_less 3)))
:: exist (fun i : nat => S i <= 3) 2
(Forall_inv (Forall_inv_tail (Forall_inv_tail (seq_n_less 3))))
:: nil
: list (fin 3)
```

This is still not optimal because the term size is quadratic with n, but it is reasonable and shows that it is likely easy to prove something about the function which constructs these terms.

The output of your function (for n=3) is:

```
= exist (fun i : nat => S i <= 3) 0 (Forall_inv (seq_n_less 3))
:: exist (fun i : nat => S i <= 3) 1
(Forall_inv (Forall_inv_tail (seq_n_less 3)))
:: exist (fun i : nat => S i <= 3) 2
(Forall_inv (Forall_inv_tail (Forall_inv_tail (seq_n_less 3))))
:: nil
: list (fin 3)
= fun i : {i : nat | S i <= 4} =>
let (x, p) := i in
(fix F (n : nat) : S n <= 4 -> list {i0 : nat | S i0 <= 4} :=
match
n as n0 return (S n0 <= 4 -> list {i0 : nat | S i0 <= 4})
with
| 0 =>
fun H : 1 <= 4 => exist (fun x0 : nat => S x0 <= 4) 0 H :: nil
| S n0 =>
fun H : S (S n0) <= 4 =>
(fix app (l m : list {i0 : nat | S i0 <= 4}) {struct l} :
list {i0 : nat | S i0 <= 4} :=
match l with
| nil => m
| a :: l1 => a :: app l1 m
end) (F n0 (list_of_fins_subproof 3 n0 H))
(exist (fun x0 : nat => S x0 <= 4) (S n0) H :: nil)
end) x p
: fin 4 -> list (fin 4)
```

which is much better than you initial solution (which had > 1000 lines even for n=1), but still not terribly obvious.

But my point is not really about list_of_fins, your solution is perfectly fine. I am talking about keeping more complicated stuff manageable, and your example is quite nice to discuss different solutions.

Last updated: Jun 15 2024 at 08:01 UTC