Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hi Nicolas,

at some point it would be useful to have a bit more context to provide a
relevant answer. Yet as a rule of thumb, it often helps defining functions on
data types (product of nats) instead of sigma types (finite ordinals), when
possible.

Here it would boil down to having an auxiliary :

Definition f' := [fun xy : nat * nat =>  0 with (0,0) |-> 42,
                   (0,1) |-> 7,
                   (0,2) |-> 28,
                   (1,0) |-> 2,
                   (1,1) |-> 8,
                   (1,2) |-> 70,
                   (2,0) |-> 116,
                   (2,1) |-> 53,
                   (2,2) |-> 47].

And then for your question 1/:

Definition f1 := [fun xy : 'I_3 * 'I_3 => f' (val xy.1, val xy.2)].

And for your question 2/:

Definition f2 := [fun x : 'I_3 => [fun y : 'I_3 => f' (val x, val y)]].


Kind regards,

assia

Le 28/09/2017 à 11:12, Cyril a écrit :
> To answer Nicolas' question 2 and 1 simultaneously you can do this:
> 
> Definition f' (x : 'I_3) (y : 'I_3) : nat :=
>   [fun _ => 0 with (0,0) |-> 42,
>                    (0,1) |-> 7,
>                    (0,2) |-> 28,
>                    (1,0) |-> 2,
>                    (1,1) |-> 8,
>                    (1,2) |-> 70,
>                    (2,0) |-> 116,
>                    (2,1) |-> 53,
>                    (2,2) |-> 47] (val x, val y).
> which type is 'I_3 -> 'I_3 -> nat.
> 
> Except if you really need simpl_fun, in which case you can do:
> Definition f' := [fun x : 'I_3 => [fun y : 'I_3 =>
>   [fun _ => 0 with (0,0) |-> 42,
>                    (0,1) |-> 7,
>                    (0,2) |-> 28,
>                    (1,0) |-> 2,
>                    (1,1) |-> 8,
>                    (1,2) |-> 70,
>                    (2,0) |-> 116,
>                    (2,1) |-> 53,
>                    (2,2) |-> 47] (val x, val y)]].
> which type is simpl_fun 'I_3 (simpl_fun 'I_3 nat)
> 
> Best,