Coq inductive type with vector parameter lacks sufficient inductive principle

Question

Background/Setting of Problem

I am trying to encode first-order logic in Coq, and have defined a Term as:

Definition name : Type := string.

Inductive V :=       (* "V" for Variable *)
| FVar : name -> V   (* Free variables *)
| BVar : nat -> V.   (* de Bruijn indices for bounded variables *)

Inductive Term : Type :=
| Var : V -> Term
| EConst : nat -> Term
| Fun {n : nat} : name -> Vector.t Term n -> Term.

(I'm using locally nameless variables, but the problem I'm facing appears to stem from using Vector.t Term in Fun.)

So far, so good, right? Well, I want to define an fmap on the variables appearing in a formula.

Fixpoint term_map_var (f : V -> V) (t : Term) : Term :=
match t with
| Var x => Var (f x)
| EConst _ => t
| Fun nm args => Fun nm (Vector.map (fun (arg : Term) => term_map_var f arg) args)
end.

Problem: Induction fails to generate inductive hypothesis

This naively looks fine, so let's prove that forall (t : Term), term_map_var id t = t, shall we?

Lemma term_map_var_id : forall (t : Term),
  term_map_var id t = t.
Proof.
intros. induction t.
- (* Case: [Var] trivial *) simpl; auto.
- (* Case: [EConst] trivial *) simpl; auto.
- (* Case: [Fun] ...not so trivial *) 
  rename t into args.
(* Uh, uh oh, my context and goals are:
1 goal
n : nat
n0 : name
args : t Term n
______________________________________(1/1)
term_map_var id (Fun n0 args) = Fun n0 args 

...let's try induction on args? *)
  induction args.
  + simpl; auto.
  + inversion IHargs.
    apply inj_pair2_eq_dec in H0. 2: decide equality. rewrite H0.
    assert (term_map_var id (Fun n0 (h :: args)) = Fun n0 (Vector.map (fun (arg : Term) => term_map_var id arg) (h :: args))). {
      simpl; auto.
    }
    assert (Vector.map (fun (arg : Term) => term_map_var id arg) (h :: args) 
          = (((fun (arg : Term) => term_map_var id arg) h)::(Vector.map (fun (arg : Term) => term_map_var id arg) args))). {
      unfold Vector.map; simpl; auto.
    }
    rewrite H.
    rewrite H1. rewrite H0.
    (* STUCK! Goal is now: [Fun n0 (term_map_var id h :: args) = Fun n0 (h :: args)] 
and there is no inductive hypothesis in context. *)

What horror have I wrought onto myself? In the Fun f args case of this proof, there was no inductive hypothesis for me to rely upon, which makes it impossible to prove the obvious proposition.

I'm uncertain how best to proceed. Is there a way to salvage this situation? Or do I need a completely different formalization?

(I'm also not sure if there is some argot description of this anti-pattern; so please correct my idiosyncratic phrasing.)

Answer 1

The default induction scheme Term_ind generated when you declare an inductive type where the recursive occurrence is nested in another data type is too weak. The workaround is to construct the induction scheme yourself, as a fixpoint. Use Unset Elimination Schemes to not generate Term_ind and keep the name free.

Unset Elimination Schemes.

Inductive Term : Type :=
| Var : V -> Term
| EConst : nat -> Term
| Fun {n : nat} : name -> Vector.t Term n -> Term.

Definition Term_ind (P : Term -> Prop)
       (HVar : forall v : V, P (Var v))
       (HConst : forall n : nat, P (EConst n))
       (HFun : forall (n : nat) (n0 : name) (t : t Term n),
         Vector.Forall P t -> P (Fun n0 t))
       (* ^ extra hypothesis *)
  : forall t : Term, P t.
Proof.
  fix SELF 1; intros [ | | n m t].
  - apply HVar.
  - apply HConst.
  - apply HFun.
    induction t as [ | ? ? ? IH ]; constructor.
    + apply SELF.
    + apply IH.
Qed.

See also: CPDT: Inductive types: Nested inductive types

Answer 2

I've been dealing with similar challenges in Coq.

It's a pain.

A slightly different approach might be to use Fin.t n -> A as well as Vector.

Something like

Variant format := stream | vector.

Definition container F :=
  match F with
  | stream => fun A n => Fin.t n -> A
  | vector => Vector.t
  end.

Then you define a bunch of functional combinators and conversion functions.

Still a massive pain to work with but sometimes the "stream" format can be more convenient to recurse over.

Also the positivity checker gets cranky without annoying workarounds.

I ultimately decided to drop this approach as too complicated with too little gain.

Some code a long those lines

https://gist.github.com/mstewartgallus/e1a536bc0156b8f8c6d997f4ba53ca81