diff options
Diffstat (limited to 'theories/Numbers/Natural/Axioms/NTimes.v')
| -rw-r--r-- | theories/Numbers/Natural/Axioms/NTimes.v | 162 |
1 files changed, 162 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v new file mode 100644 index 0000000000..a470700832 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NTimes.v @@ -0,0 +1,162 @@ +Require Export NPlus. + +Module Type TimesSignature. +Declare Module Export PlusModule : PlusSignature. + +Parameter Inline times : N -> N -> N. + +Notation "x * y" := (times x y). + +Add Morphism times with signature E ==> E ==> E as times_wd. + +Axiom times_0_n : forall n, 0 * n == 0. +Axiom times_Sn_m : forall n m, (S n) * m == m + n * m. + +End TimesSignature. + +Module TimesProperties (Export TimesModule : TimesSignature). + +Module Export PlusPropertiesModule := PlusProperties PlusModule. + +Theorem mult_0_r : forall n, n * 0 == 0. +Proof. +induct n. +now rewrite times_0_n. +intros x IH. +rewrite times_Sn_m; now rewrite plus_0_n. +Qed. + +Theorem mult_0_l : forall n, 0 * n == 0. +Proof. +intro n; now rewrite times_0_n. +Qed. + +Theorem mult_plus_distr_r : forall n m p, (n + m) * p == n * p + m * p. +Proof. +intros n m p; induct n. +rewrite mult_0_l. +now do 2 rewrite plus_0_l. +intros x IH. +rewrite plus_Sn_m. +do 2 rewrite times_Sn_m. +rewrite IH. +apply plus_assoc. +Qed. + +Theorem mult_plus_distr_l : forall n m p, n * (m + p) == n * m + n * p. +Proof. +intros n m p; induct n. +do 3 rewrite mult_0_l; now rewrite plus_0_l. +intros x IH. +do 3 rewrite times_Sn_m. +rewrite IH. +(* Now we have to rearrange the sum of 4 terms *) +rewrite <- (plus_assoc m p (x * m + x * p)). +rewrite (plus_assoc p (x * m) (x * p)). +rewrite (plus_comm p (x * m)). +rewrite <- (plus_assoc (x * m) p (x * p)). +apply (plus_assoc m (x * m) (p + x * p)). +Qed. + +Theorem mult_assoc : forall n m p, n * (m * p) == (n * m) * p. +Proof. +intros n m p; induct n. +now do 3 rewrite mult_0_l. +intros x IH. +do 2 rewrite times_Sn_m. +rewrite mult_plus_distr_r. +now rewrite IH. +Qed. + +Theorem mult_1_l : forall n, 1 * n == n. +Proof. +intro n. +rewrite times_Sn_m; rewrite times_0_n. now rewrite plus_0_r. +Qed. + +Theorem mult_1_r : forall n, n * 1 == n. +Proof. +induct n. +now rewrite times_0_n. +intros x IH. +rewrite times_Sn_m; rewrite IH; rewrite plus_Sn_m; now rewrite plus_0_n. +Qed. + +Theorem mult_comm : forall n m, n * m == m * n. +Proof. +intros n m. +induct n. +rewrite mult_0_l; now rewrite mult_0_r. +intros x IH. +rewrite times_Sn_m. +assert (H : S x == S 0 + x). +rewrite plus_Sn_m; rewrite plus_0_n; reflexivity. +rewrite H. +rewrite mult_plus_distr_l. +rewrite mult_1_r; rewrite IH; reflexivity. +Qed. + +Theorem times_eq_0 : forall n m, n * m == 0 -> n == 0 \/ m == 0. +Proof. +induct n; induct m. +intros; now left. +intros; now left. +intros; now right. +intros m IH H1. +rewrite times_Sn_m in H1; rewrite plus_Sn_m in H1; now apply S_0 in H1. +Qed. + +Definition times_eq_0_dec (n m : N) : bool := + recursion true (fun _ _ => recursion false (fun _ _ => false) m) n. + +Lemma times_eq_0_dec_wd_step : + forall y y', y == y' -> + eq_bool (recursion false (fun _ _ => false) y) + (recursion false (fun _ _ => false) y'). +Proof. +intros y y' Eyy'. +apply recursion_wd with (EA := eq_bool). +now unfold eq_bool. +unfold eq_fun2. intros. now unfold eq_bool. +assumption. +Qed. + +Add Morphism times_eq_0_dec with signature E ==> E ==> eq_bool +as times_eq_0_dec_wd. +unfold fun2_wd, times_eq_0_dec. +intros x x' Exx' y y' Eyy'. +apply recursion_wd with (EA := eq_bool). +now unfold eq_bool. +unfold eq_fun2; intros. now apply times_eq_0_dec_wd_step. +assumption. +Qed. + +Theorem times_eq_0_dec_correct : + forall n m, n * m == 0 -> + (times_eq_0_dec n m = true -> n == 0) /\ + (times_eq_0_dec n m = false -> m == 0). +Proof. +nondep_induct n; nondep_induct m; unfold times_eq_0_dec. +rewrite recursion_0; split; now intros. +intro n; rewrite recursion_0; split; now intros. +intro; rewrite recursion_0; rewrite (recursion_S eq_bool); +[split; now intros | now unfold eq_bool | unfold fun2_wd; unfold eq_bool; now intros]. +intro m; rewrite (recursion_S eq_bool). +rewrite times_Sn_m. rewrite plus_Sn_m. intro H; now apply S_0 in H. +now unfold eq_bool. +unfold fun2_wd; intros; now unfold eq_bool. +Qed. + +Theorem times_eq_1 : forall n m, n * m == 1 -> n == 1 /\ m == 1. +Proof. +nondep_induct n; nondep_induct m. +intro H; rewrite times_0_n in H; symmetry in H; now apply S_0 in H. +intros n H; rewrite times_0_n in H; symmetry in H; now apply S_0 in H. +intro H; rewrite mult_0_r in H; symmetry in H; now apply S_0 in H. +intros m H; rewrite times_Sn_m in H; rewrite plus_Sn_m in H; +apply S_inj in H; rewrite mult_comm in H; rewrite times_Sn_m in H; +apply plus_eq_0 in H; destruct H as [H1 H2]; +apply plus_eq_0 in H2; destruct H2 as [H3 _]; rewrite H1; rewrite H3; now split. +Qed. + +End TimesProperties. |