The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

You could do something along the following line (caveat below the example)

Definition extension2 {A} (f:A->A->option A) (x y:option A) : option A :=
  match x , y with
  | Some x' , Some y' => f x' y'
  | _ , _ => None
  end
.

Parameter A : Type.
Parameter f : A -> A -> option A.

Definition retA : A -> option A := @Some A.
Coercion retA : A >-> option.

Notation "a * b" := (extension2 f a b).

Check forall a b c d x, a * b * c * d = x.

The implicit coercion mechanism of Coq only works with specific types, i.e. there is no way to specify that Some is a coercion from X to option X in general. I find it's often a pity. So here, the example works because we have fixed a type A. If you are not in this sweet spot, you will have to either manually write Some for every atom:

Check forall a b c d x, Some a * Some b * Some c * Some d = x.

You can also give a notation for Some which will make this _expression_ slimmer, but you will have to write something.


Arnaud

On 13 January 2014 08:40, Anders Lundstedt <anders AT anderslundstedt.se> wrote:

Dear all,

given a partial binary operation

f : A -> A -> option A

is there a convenient way to write partial expressions (with left associativity)? I would like to be able to write e.g.

a*b*c*d

which would be equal to Some e if

a*b=Some x

x*c=Some y

y*d=Some e

for some x y : A, otherwise we would have a*b*c*d = None.

Best regards,

Anders Lundstedt