Structural Recursion · Coq users

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

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

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

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.

    + 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!

Stream: Coq users

Topic: Structural Recursion