Equations and Obligations

[spitters]

The definition of fvec_to_vec below, is non-idiomatic, but I believe should give better error messages. Coq complains:

Functional induction principle could not be proved automatically, it is left as an obligation.

But Next Obligation, says there are no obligations left. I'm using 8.19.2

Is this expected?

From Equations Require Import Equations.

Inductive vec (A:Type) : nat -> Type :=
  | nil : vec A 0
  | cons : forall n, A -> vec A n -> vec A (S n).

Arguments nil {A}.
Arguments cons {A n}.
Derive Signature for vec.

(** We will be using the following notations for convenience. *)

Notation "x :: v" := (cons x v).
Notation "[ ]" := nil.
Notation "[ x ]" := (cons x nil).
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) .. )).

(** Recall our definitions of [head], [tail] and [decompose]. *)

Equations head {A n} (v : vec A (S n)) : A :=
head (x :: _) := x.

Equations tail {A n} (v : vec A (S n)) : vec A n :=
tail (_ :: v) := v.

Inductive fin : nat -> Set :=
  | f0 : forall n, fin (S n)
  | fS : forall n, fin n -> fin (S n).

Derive Signature for fin.

Arguments f0 {n}.
Arguments fS {n}.

Definition fvec (A:Type) (n : nat) : Type := fin n -> A.

Definition fhead {A:Type} {n} (v : fvec A (S n)) : A := v f0.

(** The definition [ftail] gives the tail of an [fvec]. *)

Definition ftail {A} {n} (v : fvec A (S n)) (i : fin n) : A := v (fS i).

(* Open Obligation, but Next Obligation misses it.*)
Equations fvec_to_vec {A:Type} {n} (v : fvec A n) : vec A n:=
  fvec_to_vec v with n :=
  | 0 := nil ;
  | (S m) := fhead v :: fvec_to_vec (ftail v).
  Next Obligation.