diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-10 11:19:48 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-10 11:19:48 +0000 |
| commit | c46a640aaf9ec4fec52c5b76d32fce68414f6e7d (patch) | |
| tree | 697390d219b64dcc7ff979a7b8dad161da690359 /theories/Numbers/Natural/BigN/NMake_gen.ml | |
| parent | e8b2255678a7fa1c140c4a50dca26cc94ac1a6e0 (diff) | |
SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax
To retrieve the old behavior of spec_sub0 and spec_sub with
precondition on order, just chain spec_sub with Zmax_r or Zmax_l.
Idem with spec_pred0 and spec_pred.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12490 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index c22680be3..769d804d7 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1129,7 +1129,7 @@ let _ = pr " end."; pr ""; - pr " Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1."; + pr " Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1."; pa " Admitted."; pp " Proof."; pp " intros x; case x; unfold pred."; @@ -1172,8 +1172,17 @@ let _ = pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith."; pp " intros; exact (spec_0 w0_spec)."; pp " Qed."; - pr " "; + pr ""; + pr " Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1)."; + pa " Admitted."; + pp " Proof."; + pp " intros. destruct (Zle_lt_or_eq _ _ (spec_pos x))."; + pp " rewrite Zmax_r; auto with zarith."; + pp " apply spec_pred_pos; auto."; + pp " rewrite <- H; apply spec_pred0; auto."; + pp " Qed."; + pr ""; pr " (***************************************************************)"; pr " (* *)"; @@ -1238,7 +1247,7 @@ let _ = pr "subn)."; pr ""; - pr " Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y]."; + pr " Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y]."; pa " Admitted."; pp " Proof."; pp " unfold sub."; @@ -1286,6 +1295,16 @@ let _ = pp " Qed."; pr ""; + pr " Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y])."; + pa " Admitted."; + pp " Proof."; + pp " intros. destruct (Zle_or_lt [y] [x])."; + pp " rewrite Zmax_r; auto with zarith. apply spec_sub_pos; auto."; + pp " rewrite Zmax_l; auto with zarith. apply spec_sub0; auto."; + pp " Qed."; + pr ""; + + pr " (***************************************************************)"; pr " (* *)"; |