Stream: Coq users

Topic: What's the best way to get list of fins


view this post on Zulip Lessness (Nov 24 2021 at 07:46):

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.

view this post on Zulip Lessness (Nov 24 2021 at 09:36):

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.

view this post on Zulip Michael Soegtrop (Nov 24 2021 at 10:11):

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.

view this post on Zulip Michael Soegtrop (Nov 24 2021 at 10:16):

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.

view this post on Zulip Michael Soegtrop (Nov 24 2021 at 10:17):

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.

view this post on Zulip Paolo Giarrusso (Nov 24 2021 at 11:20):

I agree

view this post on Zulip Paolo Giarrusso (Nov 24 2021 at 11:23):

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.

view this post on Zulip Michael Soegtrop (Nov 24 2021 at 11:33):

@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?

view this post on Zulip Paolo Giarrusso (Nov 24 2021 at 11:47):

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

view this post on Zulip Paolo Giarrusso (Nov 24 2021 at 11:48):

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

view this post on Zulip Lessness (Nov 24 2021 at 16:43):

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.

view this post on Zulip Lessness (Nov 24 2021 at 16:44):

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

view this post on Zulip Michael Soegtrop (Nov 24 2021 at 18:57):

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.

view this post on Zulip Michael Soegtrop (Nov 24 2021 at 20:44):

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: Mar 28 2024 at 12:01 UTC