Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Dear Nicolas,

Nicolas Magaud 
<>
 writes:

> (* 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].

In Coq 8.7 the "fun '(x,y) => E" is supported, however that won't work
with this notation; I am unsure what the problem is, likely Coq needs
more improvement as to correctly support this feature in the notation
syntax.

On the other hand, you write down the graph for such functions and
derive the finite function rather easily I think:

Definition Symb := 'I_3.

Definition f_graph : seq ((Symb * Symb) * nat) :=
  map (fun '((x,y), n) => ((inord x, inord y),n))
  [:: ((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) ].

Definition memq (T : eqType) U (d : U) x :=
  fix memq (l : seq (T*U)) :=
    if l is y :: ys then
      if y.1 == x then y.2 else memq ys
    else d.

Definition fun_f := [ffun x : Symb * Symb => memq 0 x f_graph].

Best,
Emilio