Configurable simpl tactic

The problem that this patch tries to solve is that sometimes the
unfolding behaviour of simpl is too aggressive, frequently exposing
match constructs. Moreover one may want some constants to never be
unfolded by simpl (like in the Math-Comp library where the nosimpl hack
is pervasive). Finally, one may want some constants to be volatile,
always unfolded by simple when applied to enough arguments, even if they
do not hide a fixpoint or a match.

A new vernacular command to be indroduced in a following patch attaches
to constants an extra-logical piece of information. It declares wich
arguments must be checked to evaluate to a constructor before performing
the unfolding of the constant (in the same spirit simpl considers as
such the recursive argument of an inner fixpoint).

Examples:

Arguments minus !x !y.
  (* x and y must evaluate to a constructor for simpl to unfold minus *)

  (S x - y)   --- simpl ---> (S x - y)
  (S x - S y) --- simpl ---> (x - y)

Definition fcomp A B C (f : B -> C) (g : A -> B) x := f (g x).
Arguments fcomp A B C f g x /.
Infix "\o" := fcomp (at level 50, left associativity) : nat_scope.
  (* fcomp hides no fix, but simpl will unfold if applied to 6 arguments *)

  (fun x => (f \o g) x) = f \o g  --- simpl ---> (fun x => f (g x)) = f \o g

Arguments minus x y : simpl never.
  (* simpl will never unfold minus *)

  (S x - S y) --- simpl ---> (S x - S y)

Definition nid (x : nat) := x.
Arguments nid / x.
  (* nid is volatile, unfolded by simpl when applied to 0 or more arguments *)

  nid   --- simpl ---> (fun x => x)

Arguments minus x y : simpl nomatch.
  (* triggers for minus the "new" simpl heuristic I discussed with Hugo:

       if reducing the fix would leave a match in "head" position
       then don't unfold

     a suggestion for a better name (for "nomatch") would be appreciated *)

  (0 - y)  --- simpl ---> 0
  (S x - y)  --- simpl ---> (S x - y)
  (S x - S y) --- simpl ---> (x - y)

  (minus 0) --- simpl ---> (minus 0)

  (* This last test does not work as one may expect, i.e.

  (minus 0) --- simpl ---> (fun _ => 0)

  The point is that simpl is implemented as "strong whd_simpl"
  and after unfolding minus you have

    (fun m => match 0 => 0 | S n' => ...n' - m'... end)

  that is already in whd and exposes a match, that of course "strong"
  would reduce away but at that stage we don't know, and reducing by
  hand under the lambda is against whd reduction. So further discussion
  on that idea is needed. *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14716 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions