## Stream: Coq users

### Topic: Structural Recursion

#### D.G. Berry (Aug 17 2020 at 12:30):

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?

#### Li-yao (Aug 17 2020 at 13:16):

Continuation-passing style can be useful for this.

#### D.G. Berry (Aug 17 2020 at 13:23):

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

#### Li-yao (Aug 17 2020 at 13:29):

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.

#### Li-yao (Aug 17 2020 at 13:31):

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 := ...`

#### D.G. Berry (Aug 17 2020 at 15:18):

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).

#### Jasper Hugunin (Aug 17 2020 at 15:44):

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.
``````

#### D.G. Berry (Aug 17 2020 at 16:08):

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