Stream: Coq users

Topic: Make a multiargument function

Ali Caglayan (Nov 16 2021 at 15:00):

I have some terms like this:

{P : Fin.t n -> Type}
{Q : (forall x, P x) -> Type}
(f : forall (x : forall (y : Fin.t n), P y), Q x)

I want to treat f like a function which takes multiple arguments. For this I need to define some sort of app but it is pretty tricky to write down. I would like to be able to write app f a b c which would be translated to f g where g maps each element of Fin.t 3 to a, b and c respectively.

Ali Caglayan (Nov 16 2021 at 15:01):

It seems the target type of f should depend on the n, and I guess for n = 0 we should just return Q (Fin.case0 P). Not sure how to write down the successor case however. It would need to be P Fin.F1 -> _ or something.

Ali Caglayan (Nov 16 2021 at 15:03):

And that's just the type of app....

Gaëtan Gilbert (Nov 16 2021 at 15:08):

why not write something like

Notation "[ x ; y ; .. ; z ]" :=  (some stuff to build the Fin.t with x y z) : list_scope.

and then f [a;b;c]?
seems easier than trying to make application syntax work

Ali Caglayan (Nov 16 2021 at 15:15):

Ah ok that seems easier

Ali Caglayan (Nov 16 2021 at 15:16):

I've tried something like this but Coq isn't happy with it:

Notation "[ x ; y ; .. ; z ]" :=
  (fun n =>
    match n with
    | Fin.F1 => x
    | Fin.FS n =>
      match n with
      | Fin.F1 => y
      | Fin.FS n => ..
        z
        ..
      end
    end).

Ali Caglayan (Nov 16 2021 at 15:18):

Alright got this to work:

Notation "[ x ; y ; .. ; w ; z ]" :=
  (fun n =>
    match n with
    | Fin.F1 => x
    | Fin.FS n =>
      match n with
      | Fin.F1 => y
      | Fin.FS n => ..
        match n with
        | Fin.F1 => w
        | Fin.FS n => z
        end
        ..
      end
    end).

Ali Caglayan (Nov 16 2021 at 15:18):

Thanks!

Paolo Giarrusso (Nov 16 2021 at 18:28):

I would have considered some (fun i : Fin.t n => vector_lookup <build vector with a, b, c> i)

Paolo Giarrusso (Nov 16 2021 at 18:29):

(which I’ve only eta-expanded for clarity)

Paolo Giarrusso (Nov 16 2021 at 18:30):

for a suitable vector_lookup : Vector.t A n -> Fin.t n -> A — I forget the right name (Vector.lookup?)

Paolo Giarrusso (Nov 16 2021 at 18:32):

your notation produces an inlined version and it’s fine, but I’d be worried it’d be harder/slower to reason about

Ali Caglayan (Nov 16 2021 at 22:05):

It's called nth.

Ali Caglayan (Nov 16 2021 at 22:08):

But that seems to be exactly what I am looking for. Thanks!

Last updated: Oct 13 2024 at 01:02 UTC