diff options
| author | coq | 2001-04-20 16:00:43 +0000 |
|---|---|---|
| committer | coq | 2001-04-20 16:00:43 +0000 |
| commit | d857c99c6c985eb36ce8a4b2667dc0b5ccca115c (patch) | |
| tree | 2ea53c80dd3319b24c38b15cb5be5a582c9b302a /theories/IntMap/Map.v | |
| parent | 4837b599b4f158decc91f615a25e3a636c6ced5d (diff) | |
Library doc adjustments (until page 140)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/IntMap/Map.v')
| -rw-r--r-- | theories/IntMap/Map.v | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v index a9093f08d7..05f5612ab4 100644 --- a/theories/IntMap/Map.v +++ b/theories/IntMap/Map.v @@ -78,12 +78,14 @@ Section MapDefs. Unfold MapGet. Intros. Rewrite (ad_eq_correct a). Reflexivity. Qed. - Lemma M1_semantics_2 : (a,a':ad) (y:A) (ad_eq a a')=false -> (MapGet (M1 a y) a')=NONE. + Lemma M1_semantics_2 + : (a,a':ad) (y:A) (ad_eq a a')=false -> (MapGet (M1 a y) a')=NONE. Proof. Intros. Simpl. Rewrite H. Reflexivity. Qed. - Lemma Map2_semantics_1 : (m,m':Map) (eqm (MapGet m) [a:ad] (MapGet (M2 m m') (ad_double a))). + Lemma Map2_semantics_1 + : (m,m':Map) (eqm (MapGet m) [a:ad] (MapGet (M2 m m') (ad_double a))). Proof. Unfold eqm. Induction a; Trivial. Qed. @@ -97,7 +99,8 @@ Section MapDefs. Exact (Map2_semantics_1 m m' a). Qed. - Lemma Map2_semantics_2 : (m,m':Map) (eqm (MapGet m') [a:ad] (MapGet (M2 m m') (ad_double_plus_un a))). + Lemma Map2_semantics_2 + : (m,m':Map) (eqm (MapGet m') [a:ad] (MapGet (M2 m m') (ad_double_plus_un a))). Proof. Unfold eqm. Induction a; Trivial. Qed. @@ -646,7 +649,8 @@ Section MapDefs. Qed. Lemma MapDelta_semantics_1_1 : (a:ad) (y:A) (m':Map) (a0:ad) - (MapGet (M1 a y) a0)=NONE -> (MapGet m' a0)=NONE -> (MapGet (MapDelta (M1 a y) m') a0)=NONE. + (MapGet (M1 a y) a0)=NONE -> (MapGet m' a0)=NONE -> + (MapGet (MapDelta (M1 a y) m') a0)=NONE. Proof. Intros. Unfold MapDelta. Elim (sumbool_of_bool (ad_eq a a0)). Intro H1. Rewrite (ad_eq_complete ? ? H1) in H. Rewrite (M1_semantics_1 a0 y) in H. Discriminate H. @@ -692,7 +696,8 @@ Section MapDefs. Qed. Lemma MapDelta_semantics_2 : (m,m':Map) (a:ad) (y:A) - (MapGet m a)=NONE -> (MapGet m' a)=(SOME y) -> (MapGet (MapDelta m m') a)=(SOME y). + (MapGet m a)=NONE -> (MapGet m' a)=(SOME y) -> + (MapGet (MapDelta m m') a)=(SOME y). Proof. Induction m. Trivial. Exact MapDelta_semantics_2_1. @@ -718,7 +723,8 @@ Section MapDefs. Qed. Lemma MapDelta_semantics_3 : (m,m':Map) (a:ad) (y,y':A) - (MapGet m a)=(SOME y) -> (MapGet m' a)=(SOME y') -> (MapGet (MapDelta m m') a)=NONE. + (MapGet m a)=(SOME y) -> (MapGet m' a)=(SOME y') -> + (MapGet (MapDelta m m') a)=NONE. Proof. Induction m. Intros. Discriminate H. Exact MapDelta_semantics_3_1. |