How to write heavily indexed proofs?

Question

I've been playing with hereditary substitution. However, things get very awkward because substitution isn't total unless you index by the environment somehow.

In my old approach terms were not indexed by environment or type but instead there were separate typing judgements. Hereditary substitution simply returned v_tt for invalid cases.

Instead of something like {v: intro | G |- v: t} I'm trying out a different approach of explicitly indexing everything like intro G t. However, in some cases explicit indexing becomes quite awkward to work with.

I'm not sure how to simplify lookup further and prove simple cases like the associativity of hereditary substitution.

Can you help me write proofs over an explicitly indexed style?

Require Import Coq.Unicode.Utf8.
Require Coq.Bool.Bool.
Require Coq.Lists.List.

Import IfNotations.
Import List.ListNotations.

Require Import FunInd.

Definition var := nat.

Implicit Types x y: var.

Function eqb_var (x y: var): bool :=
  match x, y with
  | O, O => true
  | S x', S y' => eqb_var x' y'
  | _, _ => false
  end.

Inductive type :=
| t_var (A: var)
| t_unit
| t_prod (t1 t2: type).

Implicit Type t: type.

Definition environment := list (var * type).

Implicit Type Γ: environment.
Bind Scope list_scope with environment.

Function eqb_type t t' :=
  match t, t' with
  | t_var A, t_var A' => eqb_var A A'
  | t_unit, t_unit => true
  | t_prod t1 t2, t_prod t1' t2' => eqb_type t1 t1' && eqb_type t2 t2'
  | _, _ => false
  end %bool.

Lemma eqb_var_sound {A A'}: Bool.Is_true (eqb_var A A') → A = A'.
Proof.
  functional induction (eqb_var A A').
  all: try contradiction.
  all: auto.
Qed.

Lemma eqb_type_sound {t t'}: Bool.Is_true (eqb_type t t') → t = t'.
Proof.
  functional induction (eqb_type t t').
  all: cbn.
  all: auto.
  all: try contradiction.
  - intro p.
    rewrite (eqb_var_sound p).
    reflexivity.
  - destruct eqb_type, eqb_type.
    all: try contradiction.
    rewrite (IHb I), (IHb0 I).
    auto.
Qed.

Function ismem x t Γ :=
  if Γ is cons (y, t') Γ'
  then
    if eqb_var x y
    then
      eqb_type t t'
    else
      ismem x t Γ'
  else
    false.

Inductive elim Γ: type → Set :=
| V_var x t: Bool.Is_true (ismem x t Γ) → elim Γ t
| V_fst {t1 t2}: elim Γ (t_prod t1 t2) → elim Γ t1
| V_snd {t1 t2}: elim Γ (t_prod t1 t2) → elim Γ t2
.
Inductive intro Γ: type → Set :=
| v_neu A: elim Γ (t_var A) → intro Γ (t_var A)
| v_tt: intro Γ t_unit
| v_fanout {t1 t2}: intro Γ t1 → intro Γ t2 → intro Γ (t_prod t1 t2)
.

Arguments V_var {Γ}.
Arguments V_fst {Γ t1 t2}.
Arguments V_snd {Γ t1 t2}.

Arguments v_neu {Γ A}.
Arguments v_tt {Γ}.
Arguments v_fanout {Γ t1 t2}.

Inductive subst Γ: environment → Set :=
| subst_cons {Γ'} x t: intro Γ t → subst Γ Γ' → subst Γ ((x, t) :: Γ')
| subst_nil: subst Γ []
.

Arguments subst_cons {Γ Γ'}.
Arguments subst_nil {Γ}.

Fixpoint eta {Γ t} {struct t}: elim Γ t → intro Γ t :=
  match t with
  | t_var A => λ V, v_neu V
  | t_unit => λ _, v_tt
  | t_prod t1 t2 => λ V, v_fanout (eta (V_fst V)) (eta (V_snd V))
  end.

Definition head {x t Γ Γ'} (ρ: subst Γ ((x, t) :: Γ')): intro Γ t :=
  match ρ with
  | subst_cons _ _ v _ => v
  end.

Definition tail {x t Γ Γ'} (ρ: subst Γ ((x, t) :: Γ')): subst Γ Γ':=
  match ρ with
  | subst_cons _ _ _ ρ' => ρ'
  end.

Fixpoint lookup x t {Γ'}: Bool.Is_true (ismem x t Γ') → ∀ {Γ}, subst Γ Γ' → intro Γ t.
Proof.
  destruct Γ' as [|p Γ'].
  - intros q.
    destruct q.
  - destruct p as [y t'].
    cbn.
    destruct eqb_var.
    + destruct eqb_type eqn:q2.
      * assert (q' := @eqb_type_sound t t').
        rewrite q2 in q'.
        rewrite (q' I).
        intros ? ? ρ.
        apply (head ρ).
      * intro q.
        destruct q.
    + intros q ? ρ.
      apply (lookup x t Γ' q).
      apply (tail ρ).
Defined.

Fixpoint hsubst_elim {Γ Γ' t} (ρ: subst Γ Γ') (V: elim Γ' t): intro Γ t :=
  match V with
  | V_var x t q => lookup x t q ρ
  | V_fst V =>
      let ' v_fanout v1 _ := hsubst_elim ρ V in
      v1
  | V_snd V =>
      let ' v_fanout _ v2 := hsubst_elim ρ V in
      v2
  end.

Fixpoint hsubst_intro {Γ Γ' t} (ρ: subst Γ Γ') (v: intro Γ' t): intro Γ t :=
  match v with
  | v_neu e => hsubst_elim ρ e
  | v_tt => v_tt
  | v_fanout v1 v2 => v_fanout (hsubst_intro ρ v1) (hsubst_intro ρ v2)
  end.

Notation "V · ρ" := (hsubst_elim ρ V) (at level 30).
Notation "v ∘ ρ" := (hsubst_intro ρ v) (at level 30).

Fixpoint hsubst_elim_assoc {A B} {x y} {f: elim _ A}:
  ∀ {Γ C} {g: intro _ B} {h: intro Γ C},
    f · (subst_cons x _ (g ∘ subst_cons y _ h subst_nil) subst_nil)
    =
      (f · subst_cons x _ g subst_nil) ∘ subst_cons y _ h subst_nil.
Proof.
  admit.
Admitted.

Fixpoint hsubst_intro_assoc {A B} {x y} {f: intro _ A}:
  ∀ {Γ C} {g: intro _ B} {h: intro Γ C},
    f ∘ (subst_cons x _ (g ∘ subst_cons y _ h subst_nil) subst_nil)
    =
      (f ∘ subst_cons x _ g subst_nil) ∘ subst_cons y _ h subst_nil.
Proof.
  induction f.
  all: cbn.
  all: intros.
  all: auto.
  all: repeat rewrite hsubst_intro_assoc.
  all: auto.
  rewrite hsubst_elim_assoc.
  auto.
Qed.