# How to get rid of opaque proof-terms in computation

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

Something like

Compute foo [[1;2]; ; [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]; ; [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?

I found a very useful article which solved my problem.

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.

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]; ; [4;5]]%list.
Compute list_vector_from_list 0 1 [[1;2]; ; [4;5]]%list.
Compute list_vector_from_list 0 2 [[1;2]; ; [4;5]]%list.

• I don't think using this would work: you'd still need at some point to use the decision procedure on natural numbers to cast between vector types of equal length, which is the original problem… Feb 17 at 10:56
• but the length of the vector does not come from the length of the list, so all the produced vectors are of same type.
– Lolo
Feb 17 at 12:00
• Yes, but if I understand correctly, the aim of OP's post was to filter a list of lists to only keep those of a certain length, and convert only those to vectors. If you map your function on a list of lists, you'd instead get all lists in the original list, padded or truncated according to the integer. Feb 17 at 12:14
• of course you first need to filter the lists of wrong size, but this is easy it is an operation from list (list nat) to list (list nat)
– Lolo
Feb 17 at 12:19