From 3fe4912b568916676644baeb982a3e10c592d887 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 25 Sep 2014 00:12:26 +0200 Subject: 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. --- theories/Reals/Binomial.v | 7 +++---- theories/Reals/Rlimit.v | 2 ++ 2 files changed, 5 insertions(+), 4 deletions(-) (limited to 'theories/Reals') diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index ad076c488..16f2661fe 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -172,13 +172,12 @@ Proof. apply sum_eq. intros; apply H1. unfold N; apply le_lt_trans with n; [ assumption | apply lt_n_Sn ]. - intros; unfold Bn, Cn. - replace (S N - S i)%nat with (N - i)%nat; reflexivity. + reflexivity. unfold An; fold N; rewrite <- minus_n_n; rewrite H0; simpl; ring. apply sum_eq. - intros; unfold An, Bn; replace (S N - S i)%nat with (N - i)%nat; - [ idtac | reflexivity ]. + intros; unfold An, Bn. + change (S N - S i)%nat with (N - i)%nat. rewrite <- pascal; [ ring | apply le_lt_trans with n; [ assumption | unfold N; apply lt_n_Sn ] ]. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 375cc2752..cf7b91af8 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -174,6 +174,8 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X') Definition R_met : Metric_Space := Build_Metric_Space R R_dist R_dist_pos R_dist_sym R_dist_refl R_dist_tri. +Declare Equivalent Keys dist R_dist. + (*******************************) (** * Limit 1 arg *) (*******************************) -- cgit v1.2.3