Define smart constructors for data types as notations

[MarvinLira]

Description

Currently for each constructor of each data type a smart constructor is defined that lifts the return value of that constructor into a monadic value.

Definition MyPair_ (Shape : Type) (Pos : Shape -> Type) {a b : Type} (x : Free Shape Pos a) (y : Free Shape Pos b)
   : Free Shape Pos (MyPair Shape Pos a b) :=
  pure (myPair_ x y).

It would be nice if those smart constructors would be implemented as Notation instead of Definition.

Motivation

The approach with the Definition has two disadvantages:

• The smart constructor is not automatically used by Coq for output.
  Destructing a Free Shape Pos (MyPair Shape Pos a b) twice yields a pure (myPair_ fx fy) instead of a MyPair_ fx fy.
• Some simple tactics of coq fail because they do not unfold smart constructors.

  Lemma lem1 : forall (p : MyPair Shape Pos a b),
    f (pure p) = C.
  Proof. Admitted.
  
  Lemma lem2 : forall (fx : Free Shape Pos a) (fy : Free Shape Pos b),
    f (MyPair_ Shape Pos fx fy) = C.
  Proof.
    intros fx fy.
    Fail rewrite lem1.
  Admitted.
  
  Lemma lem3 : forall (fx : Free Shape Pos a) (fy : Free Shape Pos b),
    f (pure (myPair_ fx fy)) = C.
  Proof.
    intros fx fy.
    Fail rewrite lem2.
  Admitted.

Both points do not apply if a Notation is used.

[MarvinLira]

Issue #178 evaluates whether notation scopes should be used to qualify smart constructor notations.