From 6477ab0f7ea03a0563ca7ba2731d6aae1d3aa447 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 8 Jan 2010 17:36:28 +0000 Subject: Numbers: BigN and BigZ get instantiations of all properties about div and mod NB: for declaring div and mod as a morphism, even when divisor is zero, I've slightly changed the definition of div_eucl: it now starts by a check of whether the divisor is zero. Not very nice, but this way we can say that BigN.div and BigZ.div _always_ answer like Zdiv.Zdiv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12646 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/BigN/NMake_gen.ml | 27 +++++++++++++++++++-------- 1 file changed, 19 insertions(+), 8 deletions(-) (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml') diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 769d804d7..b8e879c66 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1956,6 +1956,7 @@ let _ = pr ""; pr " Definition div_eucl x y :="; + pr " if eq_bool y zero then (zero,zero) else"; pr " match compare x y with"; pr " | Eq => (one, zero)"; pr " | Lt => (zero, x)"; @@ -1964,7 +1965,6 @@ let _ = pr ""; pr " Theorem spec_div_eucl: forall x y,"; - pr " 0 < [y] ->"; pr " let (q,r) := div_eucl x y in"; pr " ([q], [r]) = Zdiv_eucl [x] [y]."; pa " Admitted."; @@ -1973,8 +1973,13 @@ let _ = pp " exact (spec_0 w0_spec)."; pp " assert (F1: [one] = 1)."; pp " exact (spec_1 w0_spec)."; - pp " intros x y H; generalize (spec_compare x y);"; - pp " unfold div_eucl; case compare; try rewrite F0;"; + pp " intros x y. unfold div_eucl."; + pp " generalize (spec_eq_bool y zero). destruct eq_bool; rewrite F0."; + pp " intro H. rewrite H. destruct [x]; auto."; + pp " intro H'."; + pp " assert (0 < [y]) by (generalize (spec_pos y); auto with zarith)."; + pp " clear H'."; + pp " generalize (spec_compare x y); case compare; try rewrite F0;"; pp " try rewrite F1; intros; auto with zarith."; pp " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))"; pp " (Z_mod_same [y] (Zlt_gt _ _ H));"; @@ -1994,10 +1999,10 @@ let _ = pr ""; pr " Theorem spec_div:"; - pr " forall x y, 0 < [y] -> [div x y] = [x] / [y]."; + pr " forall x y, [div x y] = [x] / [y]."; pa " Admitted."; pp " Proof."; - pp " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);"; + pp " intros x y; unfold div; generalize (spec_div_eucl x y);"; pp " case div_eucl; simpl fst."; pp " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; "; pp " injection H; auto."; @@ -2099,6 +2104,7 @@ let _ = pr ""; pr " Definition modulo x y := "; + pr " if eq_bool y zero then zero else"; pr " match compare x y with"; pr " | Eq => zero"; pr " | Lt => x"; @@ -2107,15 +2113,20 @@ let _ = pr ""; pr " Theorem spec_modulo:"; - pr " forall x y, 0 < [y] -> [modulo x y] = [x] mod [y]."; + pr " forall x y, [modulo x y] = [x] mod [y]."; pa " Admitted."; pp " Proof."; pp " assert (F0: [zero] = 0)."; pp " exact (spec_0 w0_spec)."; pp " assert (F1: [one] = 1)."; pp " exact (spec_1 w0_spec)."; - pp " intros x y H; generalize (spec_compare x y);"; - pp " unfold modulo; case compare; try rewrite F0;"; + pp " intros x y. unfold modulo."; + pp " generalize (spec_eq_bool y zero). destruct eq_bool; rewrite F0."; + pp " intro H; rewrite H. destruct [x]; auto."; + pp " intro H'."; + pp " assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith)."; + pp " clear H'."; + pp " generalize (spec_compare x y); case compare; try rewrite F0;"; pp " try rewrite F1; intros; try split; auto with zarith."; pp " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith."; pp " apply sym_equal; apply Zmod_small; auto with zarith."; -- cgit v1.2.3