Ssreflect Users Discussion List

[Nicolas Magaud <>]

Emilio, Assia, Cyril and Yves,

Thank you for your inputs. 

I try and define finite functions as an exercice to better understand how to 
use ssreflect and the mathcomp library.
One of my main concerns is that once the function is defined I want to 
compute with it.

E.g., using Yves’ suggested notation, I expect "Eval compute in (f’ ['0] 
['2])" to return 28. 

So far, I have no performance issues in mind. But I’ll keep investigating and 
I’ll keep you posted.

Nicolas Magaud


> On 28 Sep 2017, at 17:10, Assia Mahboubi 
> <>
>  wrote:
> 
> 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,