Nested types

[sarahzrf]

I'm trying to formalize first-order logic in Coq using Autosubst, and I'm running into a difficulty. Function symbols have a fixed arity, so I'm doing something like this:

Inductive term :=
| idx (v : var)
| app {n : arity} (f : function_symbol n) (a : vec term n).

Unfortunately, Autosubst now doesn't substitute in arguments of an application, presumably because of the nested recursion. I've also tried using a mutually inductive type; that didn't work either. How should I approach this?

[sfs]

Autosubst has limited support for dealing with nested recursion using MMap instances.

MMap A B is just a shorthand for mmap : (A -> A) -> B -> B, e.g., replace all As occurring in a B. For your type you need an instance of the form MMap A (vec B n) to traverse under vec.

I'm saying that there is limited support for this, because the mmap functions need to be written in a particular way to appease Coq's termination checker. In many cases you can just use derive to generate a proplery written instance, but this fails with dependent types like in your example.

Here's a full example of providing an MMap instance for vectors.

From Autosubst Require Import Autosubst.

Definition arity := nat.
Variable function_symbol : arity -> Type.

(** Allow nested recursion with Coq vectors. *)

Require Import Coq.Vectors.Vector.

Notation vec := VectorDef.t.
Import VectorDef.VectorNotations.

Section MMapVectors.
  Variable (A B : Type).
  Variable (MMap_A_B : MMap A B).
  Variable (MMapLemmas_A_B : MMapLemmas A B).
  Variable (MMapExt_A_B : MMapExt A B).

  Global Instance mmap_vec : forall n, MMap A (vec B n) :=
    fun n (f : A -> A) (v : vec B n) =>
      (fix rec n (v : vec B n) :=
         match v with
         | [] => []
         | VectorDef.cons _ hd _ tl => mmap f hd :: rec _ tl
         end) n v.

  Global Instance mmapLemmas_vec n : MMapLemmas A (vec B n). derive. Qed.

  Global Instance mmapExt_vec n : MMapExt A (vec B n).
    intros f g E v. induction v. reflexivity. cbn. f_equal.
    now apply mmap_ext. exact IHv.
  Defined.
End MMapVectors.

(** First-order terms containing vectors. *)

Module FOTermsV.
  Inductive term :=
  | idx (v : var)
  | app {n : arity} (f : function_symbol n) (a : vec term n).

  Instance Ids_term : Ids term. derive. Defined.
  Instance Rename_term : Rename term. derive. Defined.
  Instance Subst_term : Subst term. derive. Defined.
  Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

  (** With the MMap instance, instantiation recurses under vectors *)
  Variable two : function_symbol 2.
  Definition test : term :=
    app two [idx 0; idx 1].
  Compute test.[ren (+1)].
End FOTermsV.

In this particular example, though, I would rather suggest that you represent vectors as functions from a finite type instead:

  Inductive term :=
  | idx (v : var)
  | app {n : arity} (f : function_symbol n) (a : fin n -> term).

There's already an MMap instance for function types, and under functional extensionality the types vec A n and fin n -> A are equivalent.

For example, you could use:

(** First-order terms with fintypes. *)

Fixpoint fin (n : nat) : Type :=
  match n with
  | 0 => False
  | S m => option (fin m)
  end.

Module FOTermsF.
  Inductive term :=
  | idx (v : var)
  | app {n : arity} (f : function_symbol n) (a : fin n -> term).

  Instance Ids_term : Ids term. derive. Defined.
  Instance Rename_term : Rename term. derive. Defined.
  Instance Subst_term : Subst term. derive. Defined.
  Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

  Lemma term_inst_app n (f : function_symbol n) (a : fin n -> term) (sigma : var -> term) :
    (app f a).[sigma] = app f (fun x => (a x).[sigma]).
  Proof. reflexivity. Qed.
End FOTermsF.