diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NMiscFunct.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMiscFunct.v | 404 |
1 files changed, 404 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v new file mode 100644 index 0000000000..82a9224533 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMiscFunct.v @@ -0,0 +1,404 @@ +Require Import Bool. (* To get the orb and negb function *) +Require Export NStrongRec. +Require Export NTimesOrder. + +Module MiscFunctFunctor (Import NatMod : NBaseSig). +Module Export StrongRecPropertiesModule := StrongRecProperties NatMod. +Open Local Scope NatScope. + +(*****************************************************) +(** Addition *) + +Definition plus (x y : N) := recursion y (fun _ p => S p) x. + +Lemma plus_step_wd : fun2_wd E E E (fun _ p => S p). +Proof. +unfold fun2_wd; intros _ _ _ p p' H; now rewrite H. +Qed. + +Add Morphism plus with signature E ==> E ==> E as plus_wd. +Proof. +unfold plus. +intros x x' Exx' y y' Eyy'. +apply recursion_wd with (EA := E). +assumption. +unfold eq_fun2; intros _ _ _ p p' Epp'; now rewrite Epp'. +assumption. +Qed. + +Theorem plus_0 : forall y, plus 0 y == y. +Proof. +intro y. unfold plus. +(*pose proof (recursion_0 E y (fun _ p => S p)) as H.*) +rewrite recursion_0. apply (proj1 E_equiv). +Qed. + +Theorem plus_succ : forall x y, plus (S x) y == S (plus x y). +Proof. +intros x y; unfold plus. +now rewrite (recursion_succ E); [|apply plus_step_wd|]. +Qed. + +(*****************************************************) +(** Multiplication *) + +Definition times (x y : N) := recursion 0 (fun _ p => plus p x) y. + +Lemma times_step_wd : forall x, fun2_wd E E E (fun _ p => plus p x). +Proof. +unfold fun2_wd. intros. now apply plus_wd. +Qed. + +Lemma times_step_equal : + forall x x', x == x' -> eq_fun2 E E E (fun _ p => plus p x) (fun x p => plus p x'). +Proof. +unfold eq_fun2; intros; apply plus_wd; assumption. +Qed. + +Add Morphism times with signature E ==> E ==> E as times_wd. +Proof. +unfold times. +intros x x' Exx' y y' Eyy'. +apply recursion_wd with (EA := E). +reflexivity. apply times_step_equal. assumption. assumption. +Qed. + +Theorem times_0_r : forall x, times x 0 == 0. +Proof. +intro. unfold times. now rewrite recursion_0. +Qed. + +Theorem times_succ_r : forall x y, times x (S y) == plus (times x y) x. +Proof. +intros x y; unfold times. +now rewrite (recursion_succ E); [| apply times_step_wd |]. +Qed. + +(*****************************************************) +(** Less Than *) + +Definition lt (m : N) : N -> bool := + recursion (if_zero false true) + (fun _ f => fun n => recursion false (fun n' _ => f n') n) + m. + +(* It would be more efficient to make a three-way comparison, i.e., +return Eq, Lt, or Gt, but since these are no-use default functions, +we define <= as (< or =) *) +Definition le (n m : N) := lt n m || e n m. + +Theorem le_lt : forall n m, le n m <-> lt n m \/ n == m. +Proof. +intros n m. rewrite E_equiv_e. unfold le. +do 3 rewrite eq_true_unfold_pos. +assert (H : lt n m || e n m = true <-> lt n m = true \/ e n m = true). +split; [apply orb_prop | apply orb_true_intro]. +now rewrite H. +Qed. + +Theorem le_intro_left : forall n m, lt n m -> le n m. +Proof. +intros; rewrite le_lt; now left. +Qed. + +Theorem le_intro_right : forall n m, n == m -> le n m. +Proof. +intros; rewrite le_lt; now right. +Qed. + +Lemma lt_base_wd : eq_fun E eq_bool (if_zero false true) (if_zero false true). +unfold eq_fun, eq_bool; intros; apply if_zero_wd; now unfold LE_succet. +Qed. + +Lemma lt_step_wd : + let step := (fun _ f => fun n => recursion false (fun n' _ => f n') n) in + eq_fun2 E (eq_fun E eq_bool) (eq_fun E eq_bool) step step. +Proof. +unfold eq_fun2, eq_fun, eq_bool. +intros x x' Exx' f f' Eff' y y' Eyy'. +apply recursion_wd with (EA := eq_bool); unfold eq_bool. +reflexivity. +unfold eq_fun2; intros; now apply Eff'. +assumption. +Qed. + +Lemma lt_curry_wd : forall m m', m == m' -> eq_fun E eq_bool (lt m) (lt m'). +Proof. +unfold lt. +intros m m' Emm'. +apply recursion_wd with (EA := eq_fun E eq_bool). +apply lt_base_wd. +apply lt_step_wd. +assumption. +Qed. + +Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. +Proof. +unfold eq_fun; intros m m' Emm' n n' Enn'. +now apply lt_curry_wd. +Qed. + +(* Note that if we unfold lt along with eq_fun above, then "apply" signals +as error "Impossible to unify", not just, e.g., "Cannot solve second-order +unification problem". Something is probably wrong. *) + +Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +Proof. +intros x1 x2 H1 x3 x4 H2; unfold le; rewrite H1; now rewrite H2. +Qed. + +Theorem lt_base_eq : forall n, lt 0 n = if_zero false true n. +Proof. +intro n; unfold lt; now rewrite recursion_0. +Qed. + +Theorem lt_step_eq : forall m n, lt (S m) n = recursion false (fun n' _ => lt m n') n. +Proof. +intros m n; unfold lt. +pose proof (recursion_succ (eq_fun E eq_bool) (if_zero false true) + (fun _ f => fun n => recursion false (fun n' _ => f n') n) + lt_base_wd lt_step_wd m n n) as H. +unfold eq_bool in H. +assert (H1 : n == n); [reflexivity | apply H in H1; now rewrite H1]. +Qed. + +Theorem lt_0 : forall n, ~ lt n 0. +Proof. +nondep_induct n. +rewrite lt_base_eq; rewrite if_zero_0; now intro. +intros n; rewrite lt_step_eq. rewrite recursion_0. now intro. +Qed. + +(* Above, we rewrite applications of function. Is it possible to rewrite +functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to +lt_step n (recursion lt_base lt_step n)? *) + +Lemma lt_0_1 : lt 0 1. +Proof. +rewrite lt_base_eq; now rewrite if_zero_succ. +Qed. + +Lemma lt_0_succn : forall n, lt 0 (S n). +Proof. +intro n; rewrite lt_base_eq; now rewrite if_zero_succ. +Qed. + +Lemma lt_succn_succm : forall n m, lt (S n) (S m) <-> lt n m. +Proof. +intros n m. +rewrite lt_step_eq. rewrite (recursion_succ eq_bool). +reflexivity. +now unfold eq_bool. +unfold fun2_wd; intros; now apply lt_wd. +Qed. + +Theorem lt_succ : forall m n, lt m (S n) <-> le m n. +Proof. +assert (A : forall m n, lt m (S n) <-> lt m n \/ m == n). +induct m. +nondep_induct n; +[split; intro; [now right | apply lt_0_1] | +intro n; split; intro; [left |]; apply lt_0_succn]. +intros n IH. nondep_induct n0. +split. +intro. assert (H1 : lt n 0); [now apply -> lt_succn_succm | false_hyp H1 lt_0]. +intro H; destruct H as [H | H]. +false_hyp H lt_0. false_hyp H succ_0. +intro m. pose proof (IH m) as H; clear IH. +assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_succn_succm |]. +assert (lt (S n) (S m) <-> lt n m); [apply lt_succn_succm |]. +assert (S n == S m <-> n == m); [split; [ apply succ_inj | apply succ_wd]|]. tauto. +intros; rewrite le_lt; apply A. +Qed. + +(*****************************************************) +(** Even *) + +Definition even (x : N) := recursion true (fun _ p => negb p) x. + +Lemma even_step_wd : fun2_wd E eq_bool eq_bool (fun x p => if p then false else true). +Proof. +unfold fun2_wd. +intros x x' Exx' b b' Ebb'. +unfold eq_bool; destruct b; destruct b'; now simpl. +Qed. + +Add Morphism even with signature E ==> eq_bool as even_wd. +Proof. +unfold even; intros. +apply recursion_wd with (A := bool) (EA := eq_bool). +now unfold eq_bool. +unfold eq_fun2. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl. +assumption. +Qed. + +Theorem even_0 : even 0 = true. +Proof. +unfold even. +now rewrite recursion_0. +Qed. + +Theorem even_succ : forall x : N, even (S x) = negb (even x). +Proof. +unfold even. +intro x; rewrite (recursion_succ (@eq bool)); try reflexivity. +unfold fun2_wd. +intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl. +Qed. + +(*****************************************************) +(** Division by 2 *) + +Definition half_aux (x : N) : N * N := + recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x. + +Definition half (x : N) := snd (half_aux x). + +Definition E2 := prod_rel E E. + +Add Relation (prod N N) E2 +reflexivity proved by (prod_rel_refl N N E E E_equiv E_equiv) +symmetry proved by (prod_rel_symm N N E E E_equiv E_equiv) +transitivity proved by (prod_rel_trans N N E E E_equiv E_equiv) +as E2_rel. + +Lemma half_step_wd: fun2_wd E E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))). +Proof. +unfold fun2_wd, E2, prod_rel. +intros _ _ _ p1 p2 [H1 H2]. +destruct p1; destruct p2; simpl in *. +now split; [rewrite H2 |]. +Qed. + +Add Morphism half with signature E ==> E as half_wd. +Proof. +unfold half. +assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)). +intros x y Exy; unfold half_aux; apply recursion_wd with (EA := E2); unfold E2. +unfold E2. +unfold prod_rel; simpl; now split. +unfold eq_fun2, prod_rel; simpl. +intros _ _ _ p1 p2; destruct p1; destruct p2; simpl. +intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption. +unfold E2, prod_rel in H. intros x y Exy; apply H in Exy. +exact (proj2 Exy). +Qed. + +(*****************************************************) +(** Logarithm for the base 2 *) + +Definition log (x : N) : N := +strong_rec 0 + (fun x g => + if (e x 0) then 0 + else if (e x 1) then 0 + else S (g (half x))) + x. + +Add Morphism log with signature E ==> E as log_wd. +Proof. +intros x x' Exx'. unfold log. +apply strong_rec_wd with (EA := E); try (reflexivity || assumption). +unfold eq_fun2. intros y y' Eyy' g g' Egg'. +assert (H : e y 0 = e y' 0); [now apply e_wd|]. +rewrite <- H; clear H. +assert (H : e y 1 = e y' 1); [now apply e_wd|]. +rewrite <- H; clear H. +assert (H : S (g (half y)) == S (g' (half y'))); +[apply succ_wd; apply Egg'; now apply half_wd|]. +now destruct (e y 0); destruct (e y 1). +Qed. + +(*********************************************************) +(** To get the properties of plus, times and lt defined *) +(** via recursion, we form the corresponding modules and *) +(** apply the properties functors to these modules *) + +Module NDefaultPlusModule <: NPlusSig. + +Module NBaseMod := NatMod. +(* If we used the name NBaseMod instead of NatMod then this would +produce many warnings like "Trying to mask the absolute name +NBaseMod", "Trying to mask the absolute name Nat.O" etc. *) + +Definition plus := plus. + +Add Morphism plus with signature E ==> E ==> E as plus_wd. +Proof. +exact plus_wd. +Qed. + +Theorem plus_0_l : forall n, plus 0 n == n. +Proof. +exact plus_0. +Qed. + +Theorem plus_succ_l : forall n m, plus (S n) m == S (plus n m). +Proof. +exact plus_succ. +Qed. + +End NDefaultPlusModule. + +Module NDefaultTimesModule <: NTimesSig. +Module NPlusMod := NDefaultPlusModule. + +Definition times := times. + +Add Morphism times with signature E ==> E ==> E as times_wd. +Proof. +exact times_wd. +Qed. + +Definition times_0_r := times_0_r. +Definition times_succ_r := times_succ_r. + +End NDefaultTimesModule. + +Module NDefaultOrderModule <: NOrderSig. +Module NBaseMod := NatMod. + +Definition lt := lt. +Definition le := le. + +Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. +Proof. +exact lt_wd. +Qed. + +Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +Proof. +exact le_wd. +Qed. + +(* This produces a warning about a morphism redeclaration. Why is not +there a warning after declaring lt? *) + +Theorem le_lt : forall x y, le x y <-> lt x y \/ x == y. +Proof. +exact le_lt. +Qed. + +Theorem lt_0 : forall x, ~ (lt x 0). +Proof. +exact lt_0. +Qed. + +Theorem lt_succ : forall x y, lt x (S y) <-> le x y. +Proof. +exact lt_succ. +Qed. + +End NDefaultOrderModule. + +Module Export DefaultTimesOrderProperties := + NTimesOrderProperties NDefaultTimesModule NDefaultOrderModule. + +End MiscFunctFunctor. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) |