Why is Ids_outer necessary for HSubstLemmas?

[sarahzrf]

I'm using HSubst in a case where the outer type doesn't have variables of its own (first-order logic; terms are a separate type, variables are bound by quantifiers in the props). I want to derive HSubstLemmas, but it depends on having an Ids instance for the outer type, even though that's impossible here. I glanced at the source and I don't see any obvious reason why it has that dependency... Can it be removed?

[Ekdohibs]

I'm having the same problem while trying to formalize Peano arithmetic. From the manual, I guess it is necessary to derive the lemma (ids x).|[sigma] = ids x, even though the Ids instance for the outer type is not listed as dependency. Is there any way this can be changed in the future in order to allow the outer type not to have binders?

[sfs]

This is one of the things that we are changing for Autosubst 2 (very preliminary report at: https://www.ps.uni-saarland.de/extras/lfmtp17/).

In Autosubst 1, I think that we are using Ids_outer somewhere to derive HSubstLemmas. I guess it's possible to remove the constraint from the class, but the derive tactic will fail and you will have to provide your own implementation.

A "better" - as in working but hacky - way around this problem can be to use nested types with MMap instances instead.

For example, suppose you want to represent terms for call-by-value reduction. The obvious solution would be to use mutual inductive types:

Inductive term :=
| app (s t : term)
| val (v : value)
with value :=
| var (x : var)
| lam (b : {bind value in term}).

Apart from the fact that we don't even support mutual inductive types at the moment this would fail because instantiation in terms is not a heterogeneous instantiation operation as currently implemented in Autosubst - there are no term variables.

An alternative presentation of the system as a nested inductive type does work though. Here are all the messy details:

Inductive term_of {T} :=
| app (s t : term_of)
| val (v : T).

Inductive value :=
| var (x : var)
| lam (b : {bind value in @term_of value}).

Section MMapTermOf.
  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_term_of : MMap A (@term_of B). derive. Defined.
  Global Instance mmapLemmas_term_of : MMapLemmas A (@term_of B). derive. Qed.
  Global Instance mmapExt_term_of : MMapExt A (@term_of B). derive. Defined.
End MMapTermOf.

Instance Ids_value : Ids value. derive. Defined.
Instance Rename_value : Rename value. derive. Defined.
Instance Subst_value : Subst value. derive. Defined.
Instance SubstLemmas_value : SubstLemmas value. derive. Qed.

Definition test : value :=
  lam (app (val (var 0)) (val (var 1))).
Compute test.[ren (+1)].