Help for Heterogenous vector · Coq users

Hi, I've spent the day trying to write a type for a heterogenous vector, and I'm out of ideas and energy. What I want is a type hvec depending on a finite family of types T : fin n -> Type such that

hvec {n : nat} (T : Fin.t n -> Type) : Type.
hvec_get {n : nat} {T : Fin.t n -> Type} (v : hvec n T) (i : Fin.t n) : T i.
hvec_func {n : nat} {T : Fin.t n -> Type} (f : forall i, T i) : hvec n T.
hvec_set {n : nat} {T : Fin.t n -> Type} (v : hvec n T) (i : fin n) (t : T i) : hvec n T.

hvec_get (hvec_func f) i = f i
hvec_get (hvec_set v i t) i = t
i ≠ j ->  hvec_get (hvec_set v i t) j = hvec_get v j

In addition, I would like hvec to compute correctly if n and T are fully concrete (e.g. n = 4 and T = fun i → fin (S i)). And I want it to compute reasonably fast, especially if n is small like 4, it will be part of a much larger computation.

It would be sad, but if needed, I can probably define hvec_set from hvec_func and hvec_get by using the decidable equality on Fin.t n.

Do you think it is possible at all? After 8 hours of search, I honestly don't know. I managed to do it in non-computable way using Program Fixpoint but I don't know how to make it computable. The whole point is to have something computationally nice, and not a function that can take a few hvec_set and then be computed with vm_compute and extracted as a plain list. Otherwise, the type f : forall i, T i fits the bill, but it will grow after each hvec_set and will never be flattened by something like vm_compute.

If nobody has any idea, since I'll only need it on 4 and 5, I'll just do T 0 * T 1 * T 2 * T 3, but that is quite sad

Karl Palmskog (Jan 04 2023 at 18:42):

I think the standard advice for nontrivial dependent types + computation these days is something like: use Equations after doing Set Equations Transparent.

Dominique Larchey-Wendling (Jan 04 2023 at 21:11):

Another approach is to follow smallers inversions (see JFM, Types 2022). Notice that the fixpoints below are build using refine and a mix of lambda term style proof and ltac style proofs before cleaning them up.

A lesson that I learned the hard way is that with dependent types, there may exist a proper/smooth path to implement things, but all the other paths are VERY painful.

(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL B FREE SOFTWARE LICENSE AGREEMENT           *)
(**************************************************************)

(* Part of the idx/vec code come from

      https://github.com/DmxLarchey/Kruskal-Trees

   and follows the "Smaller inversions" technique
   of JF Monin, Types 2022

*)

From Coq Require Import Utf8.
From Coq Require Fin Vector.

Set Implicit Arguments.

Notation idx := Fin.t.
Notation idx_fst := Fin.F1.
Notation idx_nxt := Fin.FS.

Notation 𝕆 := idx_fst.
Notation 𝕊 := idx_nxt.

Section idx_rect.

  Inductive idx_shape_O : idx 0 → Type := .

  Inductive idx_shape_S {n} : idx (S n) → Type :=
    | idx_shape_S_fst : idx_shape_S 𝕆
    | idx_shape_S_nxt i : idx_shape_S (𝕊 i).

  Let idx_invert_t n : idx n → Type :=
    match n with
      | O   => idx_shape_O
      | S n => idx_shape_S
    end.

  Definition idx_invert {n} (i : idx n) : idx_invert_t i :=
    match i with
      | 𝕆   => idx_shape_S_fst
      | 𝕊 i => idx_shape_S_nxt i
    end.

  Definition idx_O_rect X (i : idx 0) : X :=
    match idx_invert i with end.

  Variables (n : nat)
            (P : idx (S n) → Type)
            (P_0 : P 𝕆)
            (P_S : ∀i, P (𝕊 i)).

  Definition idx_S_rect i : P i :=
    match idx_invert i with
      | idx_shape_S_fst => P_0
      | idx_shape_S_nxt i => P_S i
    end.

End idx_rect.

Arguments idx_invert {_} _ /.
Arguments idx_S_rect {_ _} _ _ _ /.

Section idx_nxt_inj.

  Variable (n : nat).

  Definition idx_S_inv : idx (S n) → option (idx n) := idx_S_rect None Some.

  Fact idx_S_inv_fst : idx_S_inv 𝕆 = None.            Proof. reflexivity. Qed.
  Fact idx_S_inv_nxt i : idx_S_inv (𝕊 i) = Some i.    Proof. reflexivity. Qed.

  Fact idx_nxt_inj (i j : idx n) (H : 𝕊 i = 𝕊 j) : i = j.
  Proof.
    apply f_equal with (f := idx_S_inv) in H.
    cbn in H; now inversion H.
  Qed.

End idx_nxt_inj.

Arguments idx_S_inv {_} i /.

#[local] Reserved Notation "v ⦃ p ⦄" (at level 1, format "v ⦃ p ⦄").
#[local] Reserved Notation "x '##' y" (at level 60, right associativity).

Notation vec := Vector.t.
Notation vec_nil := Vector.nil.
Notation vec_cons := Vector.cons.

Arguments vec_nil {A}.
Arguments vec_cons {A} _ {n}.

#[local] Notation "∅" := vec_nil.
#[local] Infix "##" := vec_cons.

Section vec_prj.

  Variable (X : Type).

  Fixpoint vec_prj n (v : vec _ n) : idx n → X :=
    match v with
      | ∅    => idx_O_rect _
      | x##v => λ i,
      match idx_S_inv i with
        | None   => x
        | Some j => v⦃j⦄
      end
    end
  where "v ⦃ i ⦄" := (@vec_prj _ v i).

  Goal ∀n x (v : vec _ n),   (x##v)⦃𝕆⦄   = x.   Proof. reflexivity. Qed.
  Goal ∀n x (v : vec _ n) i, (x##v)⦃𝕊 i⦄ = v⦃i⦄. Proof. reflexivity. Qed.

End vec_prj.

Arguments vec_prj {X n}.

#[local] Notation "v ⦃ i ⦄" := (vec_prj v i).

Section hvec.

  Inductive hvec : forall {n}, vec Type n → Type :=
    | hvec_nil : hvec ∅
    | hvec_cons {n X V} : X → @hvec n V → hvec (X##V).

  Fixpoint hvec_prj {n V} (v : @hvec n V) : ∀i, V⦃i⦄ :=
    match v with
      | hvec_nil      => λ i, idx_O_rect _ i
      | hvec_cons x v => λ i,
      match idx_invert i in idx_shape_S j return (_##_)⦃j⦄  with
        | idx_shape_S_fst   => x
        | idx_shape_S_nxt j => hvec_prj v j
      end
    end.

  Fixpoint hvec_func {n} (V : vec Type n) : (∀i, V⦃i⦄) → hvec V :=
    match V with
      | ∅    => λ _, hvec_nil
      | X##V => λ f, hvec_cons (f 𝕆) (hvec_func V (λ i, f (𝕊 i)))
    end.

  Fact hvec_prj_func n (V : vec Type n) f i : hvec_prj (hvec_func V f) i = f i.
  Proof.
    induction V as [ | n X V IHV ] in f, i |- *; simpl; destruct (idx_invert i); auto.
    apply IHV.
  Qed.

  Fixpoint hvec_set {n} {V : vec Type n} (v : hvec V) : ∀i, V⦃i⦄ → hvec V :=
    match v with
      | hvec_nil      => λ i _, hvec_nil
      | @hvec_cons _ X _ x v => λ i,
      match idx_invert i in idx_shape_S j return (_##_)⦃j⦄ → hvec (X##_) with
        | idx_shape_S_fst   => λ y, hvec_cons y v
        | idx_shape_S_nxt j => λ y, hvec_cons x (hvec_set v j y)
      end
    end.

  Fact hvec_set_eq n V v i x : hvec_prj (@hvec_set n V v i x) i = x.
  Proof.
    induction v as [ | n X V y v IHv ] in i, x |- *; simpl; destruct (idx_invert i); auto.
    apply IHv.
  Qed.

  Fact hvec_set_neq n V v i j x : i ≠ j → hvec_prj (@hvec_set n V v i x) j = hvec_prj v j.
  Proof.
    induction v as [ | n X V y v IHv ] in i, j, x |- *; simpl;
      destruct (idx_invert i); destruct (idx_invert j) as [ | j ]; simpl; auto.
    + intros []; auto.
    + intros H; apply IHv; contradict H; subst; auto.
  Qed.

End hvec.

Meven Lennon-Bertrand (Jan 05 2023 at 00:09):

For the record, here is such an Equation-based solution. I changed the indexing by a function to one by a vector of types, to avoid going down a funext rabbit hole and make it easier to do clausal definitions. You can transport back to get functions with the signature that you want, with the cost of extra transports, as I show at the end, but not sure this is a good idea…

Require Import Fin Vector.
Import VectorNotations.

From Equations Require Import Equations.
Set Equations Transparent.

Inductive _hvec : forall {n : nat} (T : Vector.t Type n), Type :=
  | hnil {T : Vector.t Type 0} : _hvec T
  | hcons {A : Type} (hd : A) {n} {T : Vector.t Type n} (tl : _hvec T) : @_hvec (S n) (A :: T).

Derive NoConfusion for nat.
Derive Signature NoConfusion NoConfusionHom for Vector.t.
Derive Signature NoConfusion NoConfusionHom for _hvec.

Equations _hvec_get {n : nat} {T : Vector.t Type n} (v : _hvec T) (i : Fin.t n) : Vector.nth T i :=
  _hvec_get hnil ! ;
  _hvec_get (hcons hd _) F1 := hd ;
  _hvec_get (hcons _ tl) (FS m) := _hvec_get tl m.

Equations _hvec_func (n : nat) {T : Vector.t Type n} (f : forall i, Vector.nth T i) : _hvec T :=
  _hvec_func 0 _ := hnil ;
  _hvec_func (S n') (T := _ :: _) f := hcons (f F1) (_hvec_func n' (fun i => f (FS i))).

Equations _hvec_set {n : nat} {T : Vector.t Type n} (v : _hvec T) (i : Fin.t n) (t : Vector.nth T i) : _hvec T :=
  _hvec_set (n := 0) hnil ! _ ;
  _hvec_set (n := S _) (T := _ :: _) (hcons _ tl) F1 t := hcons t tl ;
  _hvec_set (n := S _) (T := _ :: _) (hcons hd tl) (FS i') t := hcons hd (_hvec_set tl i' t).

Fact get_f n (T : Vector.t Type n) (f : forall i, Vector.nth T i) i : _hvec_get (_hvec_func n f) i = f i.
Proof.
  funelim (_hvec_func n f).
  - inversion i.
  - simp _hvec_func.
    funelim (_hvec_get (hcons _ _) _).
    all: simp _hvec_get.
    reflexivity.
Qed.

Fact get_set n (T : Vector.t Type n) (v : _hvec T) (i : Fin.t n) (t : Vector.nth T i) : _hvec_get (_hvec_set v i t) i = t.
Proof.
  funelim (_hvec_set v i t).
  all: simp _hvec_set _hvec_get.
  reflexivity.
Qed.

Lemma Fpred (n : nat) (j : Fin.t (S n)) : F1 <> j -> {j' & j = FS j'}.
Proof.
  pattern j.
  apply Fin.caseS'.
  - congruence.
  - intros ? _.
    eexists.
    reflexivity.
Defined.

Lemma Fpred' (n : nat) (i' : Fin.t n) (j : Fin.t (S n)) : FS i' <> j -> (j = F1) + {j' & (j = FS j')*(i' <> j')}%type.
Proof.
  pattern j.
  apply Fin.caseS'.
  - left. reflexivity.
  - intros j' ?.
    right.
    exists j'.
    split ; congruence.
Defined.

Fact get_diff n (T : Vector.t Type n) (v : _hvec T) (i j : Fin.t n) (t : Vector.nth T i) (ne : i <> j) :
  _hvec_get (_hvec_set v i t) j = _hvec_get v j.
Proof.
  funelim (_hvec_set v i t).
  all: simp _hvec_set.
  - apply Fpred in ne as [? ->].
    now simp _hvec_get.
  - apply Fpred' in ne as [-> | [? [-> ne]]].
    + now simp _hvec_get.
    + simp _hvec_get.
Qed.



Equations to_vect {A : Type} {n : nat} (f : Fin.t n -> A) : Vector.t A n :=
  to_vect (n := 0) f := [] ;
  to_vect (n := S _) f := (f F1) :: (to_vect (fun m => f (FS m))).

Fact to_vect_nth {A n} (f : Fin.t n -> A) m : Vector.nth (to_vect f) m = f m.
Proof.
  funelim (to_vect f).
  all: simp to_vect.
  - inversion m.
  - pattern m.
    apply Fin.caseS'.
    1: reflexivity.
    intros m'.
    now apply H.
Qed.

Definition hvec {n : nat} (T : Fin.t n -> Type) : Type := _hvec (to_vect T).
Definition hvec_get {n : nat} {T : Fin.t n -> Type} (v : hvec T) (i : Fin.t n) : T i.
Proof.
  rewrite <- to_vect_nth.
  exact (_hvec_get v i).
Defined.
Definition hvec_func {n : nat} {T : Fin.t n -> Type} (f : forall i, T i) : hvec T.
Proof.
  apply _hvec_func.
  intros i.
  rewrite to_vect_nth.
  exact (f i).
Defined.
Definition hvec_set {n : nat} {T : Fin.t n -> Type} (v : hvec T) (i : Fin.t n) (t : T i) : hvec T.
Proof.
  eapply _hvec_set.
  1: exact v.
  rewrite to_vect_nth.
  exact t.
Defined.

Meven Lennon-Bertrand (Jan 05 2023 at 00:44):

Another solution, which is very smooth: define hvec by induction on its length, rather than as an indexed inductive type. It is very smooth compared to the head-banging, inductive ones.

Require Import Fin.

Infix "×" := prod (at level 50).

Fixpoint hvec {n : nat} : (Fin.t n -> Type) -> Type :=
  match n with
    | 0 => fun _ => unit
    | S n' => fun T => (T F1) × (@hvec n' (fun m => T (FS m)))
  end.

Fixpoint hvec_get {n : nat} (i : Fin.t n) : forall {T : Fin.t n -> Type} (v : hvec T), T i :=
  match i with
    | F1 => fun T v => fst v
    | FS i' => fun T v => hvec_get i' (snd v)
  end.

Fixpoint hvec_func (n : nat) : forall {T : Fin.t n -> Type} (f : forall i, T i), hvec T :=
  match n with
    | 0 => fun _ _ => tt
    | S _ => fun _ f => ((f F1), (hvec_func _ (fun i => f (FS i))))
  end.

Fixpoint hvec_set {n : nat} (i : Fin.t n) : forall {T : Fin.t n -> Type} (v : hvec T) (t : T i), hvec T :=
  match i with
    | F1 => fun _ v t => (t, snd v)
    | FS i' => fun _ v t => (fst v, hvec_set i' (snd v) t)
  end.

Fact get_f n (T : Fin.t n -> Type) (f : forall i, T i) i : hvec_get i (hvec_func n f) = f i.
Proof.
  induction i ; cbn.
  1: reflexivity.
  now rewrite IHi.
Qed.

Fact get_set n (T : Fin.t n -> Type) (v : hvec T) (i : Fin.t n) (t : T i) : hvec_get i (hvec_set i v t) = t.
Proof.
  induction i ; cbn.
  1: reflexivity.
  now rewrite IHi.
Qed.

Lemma Fpred (n : nat) (j : Fin.t (S n)) : j <> F1 -> {j' & j = FS j'}.
Proof.
  pattern j.
  apply Fin.caseS'.
  - congruence.
  - intros ? _.
    eexists.
    reflexivity.
Defined.

Lemma Fpred' (n : nat) (i' : Fin.t n) (j : Fin.t (S n)) : j <> FS i' -> (j = F1) + {j' & (j = FS j')*(j' <> i')}%type.
Proof.
  pattern j.
  apply Fin.caseS'.
  - left. reflexivity.
  - intros j' ?.
    right.
    exists j'.
    split ; congruence.
Defined.


Fact get_diff n (T : Fin.t n -> Type) (v : hvec T) (i j : Fin.t n) (t : T i) (ne : i <> j) :
  hvec_get j (hvec_set i v t) = hvec_get j v.
Proof.
  induction j ; cbn.
  - apply Fpred in ne as [? ->].
    reflexivity.
  - apply Fpred' in ne as [-> | [? [-> ne]]].
    1: reflexivity.
    cbn.
    now rewrite IHj.
Qed.

Dominique Larchey-Wendling (Jan 05 2023 at 09:11):

Complementary to @Meven Lennon-Bertrand remark about the product approach, it is nice/natural indeed but it may have a drawback depending on the use case: it does not nest within another inductive type, because Fixpoint are not compatible with the strict positivity criterium.

The typical use case is to represent dependent, vector based, proof trees as below. Notice that

hvec_i , hvec_p :  ∀X, (X → Type) → ∀n, vec X n → Type

are slightly specialized types compared to the more general type hvec : ∀n, vec Type n → Type above.

Section hvec.

  Variables (X : Type) (P : X → Type).

  Inductive hvec_i : forall {n}, vec X n → Type :=
    | hvec_nil : hvec_i ∅
    | hvec_cons {n x v} : P x → @hvec_i n v → hvec_i (x##v).

  Fixpoint hvec_p {n} (v : vec X n) : Type :=
    match v with
      | ∅    => unit
      | x##v => prod (P x) (hvec_p v)
    end.

End hvec.

Section proof.

  Variables (stm : Type) (rule : forall {n}, vec stm n → stm → Type).

  Inductive proof_i : stm → Type :=
    | proof_i_cons n (h : vec _ n) c : rule h c → hvec_i proof_i h → proof_i c.

  (* The one below fails on strict positivity *)
  Inductive proof_p : stm → Type :=
    | proof_p_cons n (h : vec _ n) c : rule h c → hvec_p proof_p h → proof_p c.

End proof.

Dominique Larchey-Wendling (Jan 05 2023 at 09:18):

Another remark about indexing hvec with function based vectors of type idx n → Type instead of inductive vectors (as above) is that functions somehow tend to refuse to be provably equal even if you want them to, no matter how hard you want this.

As a consequence, building an isomorphism between the types hvec v and hvec w becomes painful when you just have that v and w are extensionnally equal. Hence the funext"rabbit hole" of @Meven Lennon-Bertrand .

Thibaut Pérami (Jan 05 2023 at 10:15):

Thank you all for your help and especially @Meven Lennon-Bertrand. I'm going to use the tuple approach. I find it amazing because I found an isomorphic solution yesterday evening after sending the message without having your answers. Maybe there is indeed only one non-headache solution for dependent type problems. In my use case a few individual functions fin n -> T are defined at the top level for concrete values of nand used everywhere, so there won't be any extensionality problem. I also don't intend to use them in the definition of other inductive types.

Furthermore, not having any transport is one of the main goal for this specific problem because it helps performance quite a bit. Also, not depending on coq-equation is nice, because it means I can send move that code to some other library that cannot add dependencies if needed.

Notification Bot (Jan 05 2023 at 10:15):

Meven Lennon-Bertrand (Jan 05 2023 at 10:15):

On this, I want to add that you can run into similar issues even with vectors of types as indices. The problem is the same: equality of types in raw CIC is highly underspecified, just as equality of functions (this is the whole point of HoTT). The standard solution is to introduce codes, a datatype meant to represent the types that you will be manipulating, together with a decoding function El : codes -> Type. Rather than indexing by a vector of types, you then index by a vector of codes, using El when needed to turn a code back to a type. The important point is that now your index is a real datatype, which has a well-behaved equality.

Meven Lennon-Bertrand (Jan 05 2023 at 10:17):

Another down point of the Fixpoint-based approach is that it is based on large elimination (defining a type by recursion), which does not play very well with extraction, as non-dependent type systems do not have this feature. Thus if you ever want to extract to OCaml, the Fixpoint version will likely extract to code riddled with Obj.magic…

Dominique Larchey-Wendling (Jan 05 2023 at 10:19):

Indeed El : codes -> Type corresponds to P : X -> Type is the definitions of hvec_i and hvec_p above.

Meven Lennon-Bertrand (Jan 05 2023 at 10:19):

Thibaut Pérami (Jan 05 2023 at 10:21):

In some sense that is also what I want, except that codes/X is exactly fin n in my case and the vector of codes I want is exactly [0;...;n-1].

Thibaut Pérami (Jan 05 2023 at 10:22):

The important part is thus that whatever code/ value of type fin n, I know it is in the heterogenous vector because all of them are, so I don't need an option when accessing a value.

Dominique Larchey-Wendling (Jan 05 2023 at 10:47):

From Coq Require Import Utf8.
From Coq Require Fin Vector.

Set Implicit Arguments.

Arguments Vector.nil {A}.
Arguments Vector.cons {A} _ {n}.

#[local] Notation "∅" := Vector.nil.
#[local] Infix "##" := Vector.cons (at level 60, right associativity).

Section hvec.

  Variables (k : nat) (P : Fin.t k → Type).

  Inductive hvec : ∀{n}, Vector.t (Fin.t k) n → Type :=
    | hvec_nil : hvec ∅
    | hvec_cons {n x v} : P x → @hvec n v → hvec (x##v).

End hvec.

Notice that k and n need not be the same, and I strongly suggest them not to be forced equal if you do not want to enter into another rabbit hole, much worse than the funext one :wink: .

Thibaut Pérami (Jan 05 2023 at 10:51):

(* Fin.t notations *)
Definition fin := Fin.t.
Notation FS := Fin.FS.
Declare Scope fin_scope.
Delimit Scope fin_scope with fin.
Global Arguments Fin.FS _ _%fin : assert.
Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.


Fixpoint hvec (n : nat) : (fin n -> Type) -> Type :=
  match n with
  | 0%nat => fun _ => unit
  | S m => fun T => ((T 0%fin) * hvec m (fun x => T (FS x)))%type
  end.
Arguments hvec {n} T.

Fixpoint hget {n : nat} (i : fin n) : forall T : fin n -> Type, hvec T -> T i :=
  match i with
  | 0%fin => fun _ v => v.1
  | FS p => fun _ v => hget p _ v.2
  end.
Arguments hget {n} i {T} v.

Fixpoint hvec_func {n : nat} : forall T : fin n -> Type, (forall i, T i) -> hvec T :=
  match n with
  | 0%nat => fun _ f => ()
  | S m => fun _ f => (f 0%fin, hvec_func _ (fun x => f (FS x)))
  end.
Arguments hvec_func {n T} f.

Fixpoint hset {n : nat} (i : fin n) : forall T : fin n -> Type, T i -> hvec T -> hvec T :=
  match i with
  | 0%fin => fun _ nv v => (nv, v.2)
  | FS p => fun _ nv v => (v.1, hset p _ nv v.2)
  end.
Arguments hset {n} i {T} nv v.

Lemma hvec_get_func {n : nat} {T : fin n -> Type} (i : fin n) (f : forall i, T i) :
  hget i (hvec_func f) = f i.
Proof. induction i; hauto. Qed.

Lemma hvec_get_set_same {n : nat} {T : fin n -> Type}
  (v : hvec T) (i : fin n) (nv : T i) :
  hget i (hset i nv v) = nv.
Proof. induction i; hauto. Qed.

Lemma hvec_get_set_diff {n : nat} {T : fin n -> Type}
  (v : hvec T) (i j : fin n) (nv : T j) :
  i ≠ j -> hget i (hset j nv v) = hget i v.
Proof. induction i; sauto dep:on. Qed.

Thibaut Pérami (Jan 05 2023 at 11:08):

I decided to rename hvec_get into hget and hvec_set into hset because I'm lazy

Paolo Giarrusso (Jan 05 2023 at 20:16):

Just one note on finite functions: proving equality of finite functions needs funext, but it's only used in "irrelevant" positions: so they have decidable equality and it computes correctly

Paolo Giarrusso (Jan 05 2023 at 20:18):

Mukesh Tiwari (Jan 10 2023 at 10:21):

@Dominique Larchey-Wendling How can I invert the term X : X: Hvect (rx :: rv) to something like ∃ (x : rx) (w : @Hvect n rv), X = @Hcon rx n rv x w) to avoid opaque terms in construct_n_move_sigma function?

From Coq Require Import
  Vector Utf8.
Import VectorNotations.

Section Util.

  Context {R : Type}.

  Lemma vector_inv_0 (v : Vector.t R 0) :
    v = @Vector.nil R.
  Proof.
    refine (match v with
            | @Vector.nil _ => _
            end).
    reflexivity.
  Defined.

  Lemma vector_inv_S {n : nat} (v : Vector.t R (S n)) :
    {x & {v' | v = @Vector.cons _ x _ v'}}.
  Proof.
    refine (match v with
            | @Vector.cons _ x _ v' =>  _
            end);
    eauto.
  Defined.

End Util.

Section Hvect.

  Inductive Hvect : ∀ {n : nat}, Vector.t Type n -> Type :=
  | Hnil : @Hvect 0 []
  | Hcon {A : Type} {n : nat} {v : Vector.t Type n} :
      A -> @Hvect n v -> @Hvect (1 + n) (A :: v).

  Check [nat; nat; bool].
  Check [Vector.t nat 1; Vector.t nat 1; Vector.t bool 1].
  Check Hcon 1 (Hcon 2 (Hcon true Hnil)).
  Check Hcon [1] (Hcon [2] (Hcon [true] Hnil)).


  Theorem construct_n_move_sigma :
    forall {n : nat} {r : Vector.t Type n},
    @Hvect n r -> @Hvect n
      (Vector.map (fun x => Vector.t x 1) r).
  Proof.
    induction n as [|n IHn].
    +
      intros ? X.
      pose proof (vector_inv_0 r) as Ha;
      subst; simpl.
      exact Hnil.
    +
      intros ? X.
      destruct (vector_inv_S r) as (rx & rv & Ha);
      subst; simpl.
      (*
      I want to invert this cleanly.
      assert (Ha : ∃ (x : rx) (w : @Hvect n rv),
        X = @Hcon rx n rv x w).
      admit.

      *)
      inversion X as [|A nt v x Xt Ha Hb].
      refine (Hcon [x] (IHn _ _)).
      eapply Coq.Logic.Eqdep_dec.inj_pair2_eq_dec in H;
      subst; [exact Xt | exact Coq.Arith.Peano_dec.eq_nat_dec].
  Defined.

  Print Opaque Dependencies construct_n_move_sigma.
  Eval compute in construct_n_move_sigma
    (Hcon 1 (Hcon 2 (Hcon true Hnil))).

End Hvect.

Li-yao (Jan 10 2023 at 10:31):

This would be easier by induction on the Hvect directly instead of on the length.

Mukesh Tiwari (Jan 10 2023 at 10:43):

Notification Bot (Jan 10 2023 at 12:48):

Dominique Larchey-Wendling (Jan 10 2023 at 12:50):

@Mukesh Tiwari and @Li-yao Indeed induction on Hvect is preferable in this case, but of course it is not always possible to do so when two parameters share one or more dependent arguments. So here is a version based on inversion, implemented following the previously mentionned smaller inversions (JFM TYPES 2022)

From Coq Require Import
  Vector Utf8.
Import VectorNotations.

Section Util.

  Context {R : Type}.

  Inductive vec_shape_0 : Vector.t R 0 -> Type :=
  | vec_shaphe_0_intro : vec_shape_0 [].

  Inductive vec_shape_S {n} : Vector.t R (S n) -> Type :=
  | vec_shape_S_intro r v : vec_shape_S (r::v).

  Definition vec_invert_t {n} : Vector.t R n -> Type :=
    match n with
    | 0   => vec_shape_0
    | S n => vec_shape_S
    end.

  Definition vec_invert {n} (v : Vector.t R n) : vec_invert_t v :=
    match v return vec_invert_t v with
    | []   => vec_shaphe_0_intro
    | r::v => vec_shape_S_intro r v
    end.

End Util.

Section Hvect.

  Inductive Hvect : ∀ {n : nat}, Vector.t Type n -> Type :=
  | Hnil : @Hvect 0 []
  | Hcon {A : Type} {n : nat} {v : Vector.t Type n} :
      A -> @Hvect n v -> @Hvect (1 + n) (A :: v).

  Inductive Hvect_shape_0 : @Hvect 0 [] -> Type :=
  | Hvect_shape_0_intro : Hvect_shape_0 Hnil.

  Inductive Hvect_shape_S {n X V} : @Hvect (S n) (X::V) -> Type :=
  | Hvect_shape_S_0 x w : @Hvect_shape_S _ X V (Hcon x w).

  Definition Hvec_invert_t {n} {V : Vector.t Type n} : @Hvect n V -> Type :=
    match V with
    | [] => Hvect_shape_0
    | X::V => @Hvect_shape_S _ X V
    end.

  Definition Hvec_invert {n V} (w : @Hvect n V) : Hvec_invert_t w :=
    match w return Hvec_invert_t w with
    | Hnil => Hvect_shape_0_intro
    | Hcon a w => Hvect_shape_S_0 a w
    end.

  Theorem construct_n_move_sigma_ind_Hvect :
    forall {n : nat} {r : Vector.t Type n},
    @Hvect n r -> @Hvect n
      (Vector.map (fun x => Vector.t x 1) r).
  Proof.
    induction 1; simpl; constructor; auto.
    repeat constructor; auto.
  Qed.

  Theorem construct_n_move_sigma_ind_n :
    forall {n : nat} {r : Vector.t Type n},
    @Hvect n r -> @Hvect n
      (Vector.map (fun x => Vector.t x 1) r).
  Proof.
    induction n as [ | n IHn ]; intros V w.
    + destruct (vec_invert V).
      destruct (Hvec_invert w).
      simpl; constructor.
    + destruct (vec_invert V) as [ X V ].
      destruct (Hvec_invert w) as [ x w ].
      simpl; constructor.
      * repeat constructor; trivial.
      * apply IHn, w.
  Qed.

End Hvect.

Dominique Larchey-Wendling (Jan 10 2023 at 13:03):

I forgot to say that both below Eval work after closing the two theorems construct_n_move_sigma_ind_Hvect and construct_n_move_sigma_ind_n with Defined in place of Qed:

  Eval compute in construct_n_move_sigma_ind_Hvect
    (Hcon 1 (Hcon 2 (Hcon true Hnil))).

  Eval compute in construct_n_move_sigma_ind_n
    (Hcon 1 (Hcon 2 (Hcon true Hnil))).

Mukesh Tiwari (Jan 11 2023 at 00:48):

Thanks @Dominique Larchey-Wendling! I am trying to learn the small inversions trick, but it seems I don't understand it enough. Do you know why my fin_inver function fails?

  Inductive fin_shape_0 : Fin.t 0 -> Type :=.

  Inductive fin_shape_1 : Fin.t 1 -> Type :=
  | fin_shape_1_intro : fin_shape_1 F1.

  Inductive fin_shape_S {n : nat} : Fin.t (S (S n)) -> Type :=
  | fin_shape_S_intro s : fin_shape_S (FS s).


  Definition fin_invert_t {n : nat} : Fin.t n -> Type :=
    match n with
    | O => fin_shape_0
    | S O => fin_shape_1
    | S (S n') => fin_shape_S
    end.

  Fail Definition fin_invert
    {n : nat} (f : Fin.t n) : fin_invert_t f :=
    match f with
    | F1 => fin_shape_1_intro
    | FS s => fin_shape_S_intro s
    end.

Mukesh Tiwari (Jan 11 2023 at 01:53):

I just found that Thomas Braibant and Pierre Boutillier wanted to implement the small inversion method as a tactic in Coq (http://gallium.inria.fr/blog/a-new-Coq-tactic-for-inversion/ ). It would be super nice feature to have in Coq because it makes the dependent type inversion painless.

Dominique Larchey-Wendling (Jan 11 2023 at 06:43):

@Mukesh Tiwari your inversion patterns are incomplete. Indeed @F1 1 : Fin.t 2 is not captured so you cannot prove the goal. I did give the small inversion patterns for Fin.t/idx above in that very thread.

Meven Lennon-Bertrand (Jan 11 2023 at 10:19):

There has been ongoing work on this by @Hugo Herbelin and Thierry Martinez for some time now (more precisely, on using small inversion to make Coq's pattern-matching compilation smarter), but I am not sure of the exact state of it… Also, quite a bit of this pattern-matching juggling is part of Equations these days.

Stream: Coq users

Topic: Help for Heterogenous vector

Thibaut Pérami (Jan 04 2023 at 18:14):