Ssreflect Users Discussion List

[Cyril <>]

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,
--
Cyril

On 28/09/2017 10:26, Yves Bertot wrote:
> Here is my suggestion:
>
> If you know you will work intensively with Í_3, you can help yourself 
> with a small notation.  For instance:
>
>  From mathcomp Require Import all_ssreflect.
> Set Implicit Arguments.
> Unset Strict Implicit.
> Unset Printing Implicit Defensive.
>
> Notation "[' n ]" := (@Ordinal _ n (isT : n < 3)).
>
> Definition f'  :=
>   [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].
>
>
> On 09/28/2017 09:28 AM, Nicolas Magaud wrote:
> > Thanks for this example.
> >
> > This function has type : simpl_fun (prod_eqType nat_eqType nat_eqType) 
> > nat.
> >
> > I have 2 other questions :
> >
> > 1/ Is it possible to have the type  "simpl_fun (prod_eqType ‘I_3 
> > ‘I_3)" nat instead ?
> >
> > 2/ Moreover, is it possible to have a curryfing version of f’ whose 
> > type would be "simpl_fun ‘I_3 (simpl_fun ‘I_3 nat)" ?
> >
> > Nicolas Magaud
> >
> >
> > > On 27 Sep 2017, at 15:09, Cyril 
> > > <>
> > >  wrote:
> > >
> > > Dear Nicolas, your code almost work, because there is no need for a 
> > > pattern matching:
> > >
> > > Definition f' :=
> > >   [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].
> > >
> > > --
> > > Cyril
> > >
> > > On 27/09/2017 14:19, Nicolas Magaud wrote:
> > > > Dear all,
> > > > I have trouble defining finite functions (on finite domains) which 
> > > > have 2 or more arguments using the [] notation.
> > > > Below is a example of what I am trying to do.
> > > > I would like to define the function f’ using pattern matching on a 
> > > > couple or on the 2 separate arguments (in a currified way) but 
> > > > without doing explicit lambda-abstraction.
> > > > Is there a way to do that ? This would make the code more readable 
> > > > once the fun and => keywords are gone.
> > > > Nicolas Magaud
> > > > (* full example *)
> > > > Definition Symb := 'I_3.
> > > > (* code that works *)
> > > > Definition easy := [fun x : Symb => 0 with 0 |-> 16, 1 |-> 18, 2|-> 
> > > > 34].
> > > > Definition f :=
> > > >   [ fun x:Symb =>
> > > >     [ fun y:Symb => 0 with
> > > >     0 |-> [fun x':Symb => 17 with 0 |-> 42, 1 |-> 7, 2 |-> 28] x,
> > > >     1 |-> [fun x':Symb => 34 with 0 |-> 2, 1 |-> 8, 2 |-> 70] x,
> > > >     2 |-> [fun x':Symb => 72 with 0 |-> 116, 1 |-> 53, 2 |-> 47] x]].
> > > > (* code I would like to write or something like that, i.e. with no 
> > > > lambda-abstractions *)
> > > > Definition f' :=
> > > >    [fun (x,y) => 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].
> > > --
> > > Cyril