Enforcing a stronger difference between the two syntaxes "simpl

reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.

In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
  head symbol is written "+" (in the toplevel scope); idem for
  vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
  implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
  native_compute with functor application should now work (i.e.
  vm_compute and native_compute are now taken into account in
  tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
  eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.

By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").

1 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index 271e6ef76..66a92ea41 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -45,3 +45,37 @@ Goal forall A B (a:A) l f (i:B), fold_right f i ((a :: l))=i.
 simpl.
 admit.
 Qed. (* Qed will fail if simplification is incorrect (de Bruijn!) *)
+
+(* Check that maximally inserted arguments do not break interpretation
+   of references in simpl, vm_compute etc. *)
+
+Arguments fst {A} {B} p.
+
+Goal fst (0,0) = 0.
+simpl fst.
+Fail set (fst _).
+Abort.
+
+Goal fst (0,0) = 0.
+vm_compute fst.
+Fail set (fst _).
+Abort.
+
+Goal let f x := x + 0 in f 0 = 0.
+intro.
+vm_compute f.
+Fail set (f _).
+Abort.
+
+(* This is a compatibility test with a non evaluable reference, maybe
+   not to be kept for long *)
+Goal 0+0=0.
+simpl @eq.
+Abort.
+
+(* Check reference by notation in simpl *)
+
+Goal 0+0 = 0.
+simpl "+".
+Fail set (_ + _).
+Abort.