Keyed unification option, compiling the whole standard library

(but deactivated still).

Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.

Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:

Declare Equivalent Keys f g.

This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.

For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.

INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.

5 files changed, 19 insertions, 10 deletions

diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index d65c60167..50197872c 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -93,6 +93,7 @@ Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
 Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
 
 Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp.
+Declare Equivalent Keys gen_order_phi_Z gen_phiZ.
 
 Notation phi_pos := (gen_phiPOS 1 rplus rtimes).
 Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes).
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 78837d4cd..c982db393 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -155,12 +155,16 @@ Proof.
 Qed.
 
 Definition psub  := psub Z0  Z.add Z.sub Z.opp Zeq_bool.
+Declare Equivalent Keys psub RingMicromega.psub.
 
 Definition padd  := padd Z0  Z.add Zeq_bool.
+Declare Equivalent Keys padd RingMicromega.padd.
 
 Definition norm  := norm 0 1 Z.add Z.mul Z.sub Z.opp Zeq_bool.
+Declare Equivalent Keys norm RingMicromega.norm.
 
 Definition eval_pol := eval_pol Z.add Z.mul (fun x => x).
+Declare Equivalent Keys eval_pol RingMicromega.eval_pol.
 
 Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub  lhs rhs) = eval_pol env lhs - eval_pol env rhs.
 Proof.
@@ -202,11 +206,10 @@ Definition normalise (t:Formula Z) : cnf (NFormula Z) :=
 
 Lemma normalise_correct : forall env t, eval_cnf eval_nformula env (normalise t) <-> Zeval_formula env t.
 Proof.
-  Opaque padd.
-  unfold normalise, xnormalise  ; simpl; intros env t.
+  unfold normalise, xnormalise; cbn -[padd]; intros env t.
   rewrite Zeval_formula_compat.
   unfold eval_cnf, eval_clause.
-  destruct t as [lhs o rhs]; case_eq o; simpl;
+  destruct t as [lhs o rhs]; case_eq o; cbn -[padd];
     repeat rewrite eval_pol_sub;
       repeat rewrite eval_pol_add;
       repeat rewrite <- eval_pol_norm ; simpl in *;
@@ -216,7 +219,6 @@ Proof.
   generalize (eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
     (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst;
     intuition (auto with zarith).
-  Transparent padd.
 Qed.
 
 Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z)  :=
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index ad7fbd871..16f9b9723 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1168,7 +1168,8 @@ induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl;
   assert (U2 := split_ok_r (num F1) (num F2) l).
   assert (U3 := split_ok_l (denum F1) (denum F2) l).
   assert (U4 := split_ok_r (denum F1) (denum F2) l).
-  rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4; apply rdiv7b;
+  rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4.
+  simpl in U2, U3, U4. apply rdiv7b;
    rewrite <- ?U2, <- ?U3, <- ?U4; try apply Pcond_Fnorm; trivial.
 
 - rewrite !NPEpow_ok. simpl. rewrite !rpow_pow, (IHfe Hc).
@@ -1274,6 +1275,9 @@ Qed.
 (* simplify a field equation : generate the crossproduct and simplify
    polynomials *)
 
+(** This allows rewriting modulo the simplification of PEeval on PMul *)
+Declare Equivalent Keys PEeval rmul.
+
 Theorem Field_simplify_eq_correct :
  forall n l lpe fe1 fe2,
     Ninterp_PElist l lpe ->
@@ -1294,8 +1298,7 @@ rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3.
 simpl.
 rewrite !rmul_assoc.
 apply rmul_ext; trivial.
-rewrite
- (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
+rewrite (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
  (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl).
 rewrite Hlmp.
 apply Hcrossprod.
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 528ad4f17..40748c044 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -192,6 +192,7 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x].
  Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
  Proof. intros;subst;reflexivity. Qed.
 
+Declare Equivalent Keys bracket gen_phiZ.
 (*proof that [.] satisfies morphism specifications*)
 Global Instance gen_phiZ_morph :
 (@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*)
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 5ec73950b..3e0e931b6 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1033,16 +1033,18 @@ Section POWER.
   now destruct pe.
   Qed.
 
+  Arguments norm_aux !pe : simpl nomatch.
+
   Lemma norm_aux_spec l pe :
     PEeval l pe == (norm_aux pe)@l.
   Proof.
    intros.
-   induction pe.
-   - now rewrite (morph0 CRmorph).
+   induction pe; cbn.
+   - now rewrite (morph0 CRmorph). 
    - now rewrite (morph1 CRmorph).
    - reflexivity.
    - apply mkX_ok.
-   - simpl PEeval. rewrite IHpe1, IHpe2.
+   - rewrite IHpe1, IHpe2.
      assert (H1 := norm_aux_PEopp pe1).
      assert (H2 := norm_aux_PEopp pe2).
      rewrite norm_aux_PEadd.