How to get rid of opaque proof-terms in computation

Question

My goal is to construct list of vectors from filtered by length list of lists

Something like

Compute foo [[1;2]; [3]; [4;5]]. (* [[1;2]%vector; [4;5]%vector] *)

My approach is this:

Require Import Coq.Program.Wf.
Require Import List.
Import ListNotations.
Require Import PeanoNat.
Require Import Vectors.VectorDef.
Import VectorNotations.

Program Definition list_and_proof_to_vec {A n} (l: list A) (H: List.length l = n) : t A n :=
  match n with
  | 0 => []%vector
  | S n => _
  end
.
Next Obligation.
  rewrite Heq_n.
  refine (of_list l).
Defined.
Fail Next Obligation.

Program Fixpoint filter_by_length_with_proof {A} n (l: list (list A))
  : list {l': list A & List.length l' = n} :=
  match l with
  | []%list => []
  | (x :: xs)%list =>
      match (List.length x =? n) with
      | true => existT (fun q => List.length q = n) x _ :: filter_by_length_with_proof n xs
      | false => filter_by_length_with_proof n xs
      end
  end
.
Next Obligation.
  symmetry in Heq_anonymous.
  apply Nat.eqb_eq in Heq_anonymous.
  exact Heq_anonymous.
Defined.
Fail Next Obligation.

Definition my_list := [[1;2]; [3]; [4;5]]%list.
Definition my_filtered_list := filter_by_length_with_proof 2 my_list.
Definition list_of_vec := List.map (fun x => list_and_proof_to_vec (projT1 x) (projT2 x)) my_filtered_list.

Compute list_of_vec.

The last line, Compute list_of_vec, will show something like this:

     = [match
          match Nat.eqb_eq 2 2 with
          | conj x _ => x
          end eq_refl in (_ = H) return (2 = H -> t nat 2)
        with
        | eq_refl =>
            fun x : 2 = 2 =>
            match
              match x in (_ = H) return (H = 2) with
              | eq_refl => eq_refl
              end in (_ = H) return (t nat H)
            with
            | eq_refl => [1; 2]%vector
            end
        end eq_refl;
        match
          match Nat.eqb_eq 2 2 with
          | conj x _ => x
          end eq_refl in (_ = H) return (2 = H -> t nat 2)
        with
        | eq_refl =>
            fun x : 2 = 2 =>
            match
              match x in (_ = H) return (H = 2) with
              | eq_refl => eq_refl
              end in (_ = H) return (t nat H)
            with
            | eq_refl => [4; 5]%vector
            end
        end eq_refl]%list
     : list (t nat 2)

while I want

[[1;2]%vector; [4;5]%vector]

which is present in | eq_refl => [1; 2]%vector and | eq_refl => [4; 5]%vector

As far as i know there is something about opaqueness: Nat.eqb_eq is opaque, so coq cannot get rid of it in computation

I tried to rewrite Nat.eqb_eq by hand, but ended up with more opaque (and much scarier) terms like Morphisms.iff_impl_subrelation, some of which appeared because of tactics usage in my previous hand(re-)written proofs

I could try to rewrite all opaque terms by hand but i don't know how deep is this rabbit's hole and I genuinely do not want to end up with wall of handwritten (transparent, though) proofs

So i wonder if there some general solution to this kind of problems?

Answer 1

I found a very useful article which solved my problem.

I added this definition:

Definition computational_eq (n m: nat) (H: n = m) : n = m :=
  match Nat.eq_dec n m with
  | left x => x
  | _ => H
  end.

and applied it as follows in filter_by_length_with_proof obligation:

Next Obligation.
  symmetry in Heq_anonymous.
  apply Nat.eqb_eq in Heq_anonymous.
  apply computational_eq in Heq_anonymous. (* !!! this !!! *)
  exact Heq_anonymous.
Defined.

computational_eq transforms a hypothesis of form H: x = y to the exact same form BUT if H is obtained by opaque transformations it makes H transparent and therefore computable.

Answer 2

Another solution would be to never build vector explicitly with proofs and simply use the elements of the list to get the fixed size vectors.

Fixpoint vector_from_list {A : Type} (a : A) (l : list A) (n : nat) : 
   t A n :=
  match n return (t A n) with
  | 0 => []
  | S n1 =>
         match l with
       | []%list => a :: vector_from_list a l n1
       | (b :: l1)%list => b :: vector_from_list a l1 n1
       end 
  end.

Compute (vector_from_list 0 [1; 2]%list 2).

Definition list_vector_from_list {A : Type} (a : A) (n : nat) 
   (l : list (list A)) :=
  List.map (fun l => vector_from_list a l n)
  (filter (fun l => Nat.eqb (length l) n) l).

Compute list_vector_from_list 0 0 [[1;2]; [3]; [4;5]]%list.
Compute list_vector_from_list 0 1 [[1;2]; [3]; [4;5]]%list.
Compute list_vector_from_list 0 2 [[1;2]; [3]; [4;5]]%list.