What would be a good (for some definiton of "good") way to convince Coq that looking up an element in a list results in a substructure on that list so that recursion can be performed on these elements?

Continuation-passing style can be useful for this.

Could you elaborate on this?: I am not seeing the connection.

You can write the lookup function in CPS: instead of returning the element, you apply a continuation to it. Then when you write a `Fixpoint`

, you make the recursive call in the continuation. If things are set up correctly, then by beta-reduction your recursive call ends up being syntactically applied to the list element.

For this to work, the continuation must not be a Fixpoint argument of the lookup function though, so you have to do a weird dance with sections or use `fix`

directly. `fix lookup k l := ...`

is not the same as `fun k => fix lookup l := ...`

This technique doesn't seem to work for my use-case. I have demonstrated a minimal example of what I want to achieve here (https://pastebin.com/FQgJiwEC).

You can define a slightly more dependent version of LookupCPS like

```
Definition Lookup_Map {T : Type} {R : T -> Type} (k : forall t, R t)
: forall {n : Nat} {v : Vec T n} {i : Fin n}, R (Lookup v i).
Proof.
refine (fix f n v i {struct v} := _).
refine (
match i in (Fin n') return (forall v, R (Lookup v i)) with
| FZ n' => _
| FS n' j => _
end v
); clear v; intros v.
- refine (match v in (Vec _ m) return (match m return Vec T m -> Type with | Zero => fun _ => Unit | Succ m' => fun v => R (Lookup v (FZ m')) end v) with
| Nil => __
| Cons t v => k t
end).
- refine (match v in (Vec _ m) return (match m return Vec T m -> Type with | Zero => fun _ => Unit | Succ m' => fun v => forall i : Fin m', R (Lookup v (FS _ i)) end v) with
| Nil => __
| Cons _ v' => fun j' => f _ v' j'
end j).
Defined.
```

And then the last case of `RelRefl`

becomes

```
+ simpl. intros i.
eapply (Lookup_Map (R := fun x => Rel x x)).
eapply RelRefl.
```

I tried defining the dependent version you gave but could not see how to make it work. Thanks!

Last updated: Jun 20 2024 at 11:02 UTC