diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-22 14:58:58 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-22 14:58:58 +0000 |
| commit | 870849c0d4f32e8ff69dd53f81dc1af76ef3c747 (patch) | |
| tree | 40ae5ba5bf4c0cfdda86c23dd91e2ae49605c0f3 /theories/FSets/FSetProperties.v | |
| parent | a81329a241ba18b8c8535576290a0ffa23739d27 (diff) | |
FMap: fold_rec + more permissive transpose hyp + various cleanup
The induction principles for fold are due to S. Lescuyer
The better transpose hyp is a suggestion by P. Casteran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11711 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FSetProperties.v')
| -rw-r--r-- | theories/FSets/FSetProperties.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 291bd558f..a5981663a 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -365,10 +365,10 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). (unfold l; intros; rewrite elements_iff, InA_rev; intuition). clear Pstep; clearbody l; revert s Hsame; induction l. (* empty *) - intros s Hsame; simpl; intros; subst. + intros s Hsame; simpl. apply Pempty. intro x. rewrite Hsame, InA_nil; intuition. (* step *) - intros s Hsame; simpl; intros. + intros s Hsame; simpl. apply Pstep' with (of_list l); auto. inversion_clear Hdup; rewrite of_list_1; auto. red. intros. rewrite Hsame, of_list_1, InA_cons; intuition. @@ -469,7 +469,8 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). (** ** Alternative (weaker) specifications for [fold] *) (** When [FSets] was first designed, the order in which Ocaml's [Set.fold] - takes the set elements was unspecified. This specification reflects this fact: + takes the set elements was unspecified. This specification reflects + this fact: *) Lemma fold_0 : @@ -489,8 +490,8 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). apply fold_1. Qed. - (** An alternate (and previous) specification for [fold] was based on - the recursive structure of a set. It is now lemmas [fold_1] and + (** An alternate (and previous) specification for [fold] was based on + the recursive structure of a set. It is now lemmas [fold_1] and [fold_2]. *) Lemma fold_1 : |