more readable match patterns for very dependent types

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4575 From: @jonleivent Reported version: 8.5 CC: coq-bugs-redist@lists.gforge.inria.fr

[coqbot]

Comment author: @jonleivent

Due to very dependent types, match patterns can become onerous. Consider ones like the following (an actual case):

  match lt with
  | Missing _ _ _ _ _ _ _ _ _ => ...
  | Node _ _ _ _ _ _ _ _ lc d _ rc _ _ _ =>
    match rc with
    | Missing _ _ _ _ _ _ _ _ _ => ...
    | Node _ _ _ _ _ rg _ _ _ _ _ _ _ _ _ => ...

The difference between how bad this looks by default and when Asymmetric Patterns is set is not significant, so that is not much help.

However, suppose the parser could accept patterns that borrow syntactically from tactics like apply, and look like so:

  match lt with
  | Missing (_:=_) => ...
  | Node (lc:=lc) (d:=d) (rc:=rc) =>
    match rc with
    | Missing (_:=_) => ...
    | Node (ug:=rg) => ...

Of course, instead of providing values to parameters by name, the (x:=y) form here declares a binding y for the formal parameter x. The rule would be that if any (x:=y) is given, then any parameters not named that way will be bound with _. The (_:=_) pattern then just says to use _ for all parameters. Also, unnamed non-dependent products could be referred to by number (3:=z), just as with tactics like apply.

If := is too reminiscent of assignment, one can instead use some other notation, for instance (x as y) instead of (x:=y).

[Alizter]

cc @herbelin How difficult would it be to add "(x:=y)" to the match syntax?

[herbelin]

We could support giving arguments of constructors by position in patterns too. The syntax x as y is already taken, but (x:=y) would a priori be possible (or even (x:=y as z) to include the ability to rebind any pattern). It would be parsed and interpreted the same way as for ordinary applications.