diff options
Diffstat (limited to 'theories/Numbers/Natural/Axioms/NOrder.v')
| -rw-r--r-- | theories/Numbers/Natural/Axioms/NOrder.v | 497 |
1 files changed, 253 insertions, 244 deletions
diff --git a/theories/Numbers/Natural/Axioms/NOrder.v b/theories/Numbers/Natural/Axioms/NOrder.v index 1b631ce646..b4f363901a 100644 --- a/theories/Numbers/Natural/Axioms/NOrder.v +++ b/theories/Numbers/Natural/Axioms/NOrder.v @@ -1,330 +1,339 @@ -Require Export NAxioms. +Require Export NBase. +Require Import NZOrder. -Module Type NOrderSignature. -Declare Module Export NatModule : NatSignature. +Module Type NOrderSig. +Declare Module Export NBaseMod : NBaseSig. Open Local Scope NatScope. -Parameter Inline lt : N -> N -> bool. -Parameter Inline le : N -> N -> bool. +Parameter Inline lt : N -> N -> Prop. +Parameter Inline le : N -> N -> Prop. Notation "x < y" := (lt x y) : NatScope. Notation "x <= y" := (le x y) : NatScope. Notation "x > y" := (lt y x) (only parsing) : NatScope. Notation "x >= y" := (le y x) (only parsing) : NatScope. -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +Add Morphism lt with signature E ==> E ==> iff as lt_wd. +Add Morphism le with signature E ==> E ==> iff as le_wd. -Axiom le_lt : forall x y, x <= y <-> x < y \/ x == y. -Axiom lt_0 : forall x, ~ (x < 0). -Axiom lt_S : forall x y, x < S y <-> x <= y. -End NOrderSignature. +Axiom le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y. +Axiom nlt_0_r : forall x, ~ (x < 0). +Axiom lt_succ_le : forall x y, x < S y <-> x <= y. -Module NOrderProperties (Import NOrderModule : NOrderSignature). -Module Export NatPropertiesModule := NatProperties NatModule. +End NOrderSig. + +Module NOrderPropFunct (Import NOrderModule : NOrderSig). +Module Export NBasePropMod := NBasePropFunct NBaseMod. Open Local Scope NatScope. -Ltac le_intro1 := rewrite le_lt; left. -Ltac le_intro2 := rewrite le_lt; right. -Ltac le_elim H := rewrite le_lt in H; destruct H as [H | H]. +Ltac le_intro1 := rewrite le_lt_or_eq; left. +Ltac le_intro2 := rewrite le_lt_or_eq; right. +Ltac le_elim H := rewrite le_lt_or_eq in H; destruct H as [H | H]. -Lemma lt_stepl : forall x y z, x < y -> x == z -> z < y. +Theorem lt_succ_lt : forall n m : N, S n < m -> n < m. Proof. -intros x y z H1 H2; now rewrite <- H2. +intro n; induct m. +intro H; false_hyp H nlt_0_r. +intros m IH H. apply <- lt_succ_le. apply -> lt_succ_le in H. le_elim H. +le_intro1; now apply IH. +rewrite <- H; le_intro1. apply <- lt_succ_le; now le_intro2. Qed. -Lemma lt_stepr : forall x y z, x < y -> y == z -> x < z. +Theorem lt_irrefl : forall n : N, ~ (n < n). Proof. -intros x y z H1 H2; now rewrite <- H2. +induct n. +apply nlt_0_r. +intros n IH H. apply -> lt_succ_le in H; le_elim H. +apply lt_succ_lt in H; now apply IH. +assert (n < S n) by (apply <- lt_succ_le; now le_intro2). +rewrite H in *; now apply IH. Qed. -Lemma le_stepl : forall x y z, x <= y -> x == z -> z <= y. -Proof. -intros x y z H1 H2; now rewrite <- H2. -Qed. +Module NZOrderMod <: NZOrderSig. +Module NZBaseMod := NZBaseMod. -Lemma le_stepr : forall x y z, x <= y -> y == z -> x <= z. -Proof. -intros x y z H1 H2; now rewrite <- H2. -Qed. +Definition NZlt := lt. +Definition NZle := le. -Declare Left Step lt_stepl. -Declare Right Step lt_stepr. -Declare Left Step le_stepl. -Declare Right Step le_stepr. +Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd. +Proof lt_wd. -Theorem le_refl : forall n, n <= n. -Proof. -intro; now le_intro2. -Qed. +Add Morphism NZle with signature E ==> E ==> iff as NZle_wd. +Proof le_wd. -Theorem le_0_r : forall n, n <= 0 -> n == 0. -Proof. -intros n H; le_elim H; [false_hyp H lt_0 | assumption]. -Qed. +Definition NZle_lt_or_eq := le_lt_or_eq. +Definition NZlt_succ_le := lt_succ_le. +Definition NZlt_succ_lt := lt_succ_lt. +Definition NZlt_irrefl := lt_irrefl. -Theorem lt_n_Sn : forall n, n < S n. -Proof. -intro n. apply <- lt_S. now le_intro2. -Qed. +End NZOrderMod. -Theorem lt_closed_S : forall n m, n < m -> n < S m. -Proof. -intros. apply <- lt_S. now le_intro1. -Qed. +Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod. -Theorem lt_S_lt : forall n m, S n < m -> n < m. -Proof. -intro n; induct m. -intro H; absurd_hyp H; [apply lt_0 | assumption]. -intros x IH H. -apply -> lt_S in H. le_elim H. -apply IH in H; now apply lt_closed_S. -rewrite <- H. -apply lt_closed_S; apply lt_n_Sn. -Qed. +(* Renaming theorems from NZOrder.v *) -Theorem lt_0_Sn : forall n, 0 < S n. -Proof. -induct n; [apply lt_n_Sn | intros x H; now apply lt_closed_S]. -Qed. +Theorem lt_le_incl : forall n m : N, n < m -> n <= m. +Proof NZlt_le_incl. -Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. -Proof. -intros n m p; induct m. -intros H1 H2; absurd_hyp H1; [ apply lt_0 | assumption]. -intros x IH H1 H2. -apply -> lt_S in H1. le_elim H1. -apply IH; [assumption | apply lt_S_lt; assumption]. -rewrite H1; apply lt_S_lt; assumption. -Qed. +Theorem lt_neq : forall n m : N, n < m -> n ~= m. +Proof NZlt_neq. -Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. -Proof. -intros n m p H1 H2; le_elim H1. -le_elim H2. le_intro1; now apply lt_trans with (m := m). -le_intro1; now rewrite <- H2. now rewrite H1. -Qed. +Theorem le_refl : forall n : N, n <= n. +Proof NZle_refl. -Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. -Proof. -intros n m p H1 H2; le_elim H1. -now apply lt_trans with (m := m). now rewrite H1. -Qed. +Theorem lt_succ_r : forall n : N, n < S n. +Proof NZlt_succ_r. -Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. -Proof. -intros n m p H1 H2; le_elim H2. -now apply lt_trans with (m := m). now rewrite <- H2. -Qed. +Theorem le_succ_r : forall n : N, n <= S n. +Proof NZle_succ_r. -Theorem lt_positive : forall n m, n < m -> 0 < m. -Proof. -intros n m; induct n. -trivial. -intros x IH H. -apply lt_trans with (m := S x); [apply lt_0_Sn | apply H]. -Qed. +Theorem lt_lt_succ : forall n m : N, n < m -> n < S m. +Proof NZlt_lt_succ. -Theorem lt_resp_S : forall n m, S n < S m <-> n < m. -Proof. -intros n m; split. -intro H; apply -> lt_S in H; le_elim H. -intros; apply lt_S_lt; assumption. -rewrite <- H; apply lt_n_Sn. -induct m. -intro H; false_hyp H lt_0. -intros x IH H. -apply -> lt_S in H; le_elim H. -apply lt_trans with (m := S x). -apply IH; assumption. -apply lt_n_Sn. -rewrite H; apply lt_n_Sn. -Qed. +Theorem le_le_succ : forall n m : N, n <= m -> n <= S m. +Proof NZle_le_succ. -Theorem le_resp_S : forall n m, S n <= S m <-> n <= m. -Proof. -intros n m; do 2 rewrite le_lt. -pose proof (S_wd n m); pose proof (S_inj n m); pose proof (lt_resp_S n m); tauto. -Qed. +Theorem le_succ_le_or_eq_succ : forall n m : N, n <= S m <-> n <= m \/ n == S m. +Proof NZle_succ_le_or_eq_succ. -Theorem lt_le_S_l : forall n m, n < m <-> S n <= m. -Proof. -intros n m; nondep_induct m. -split; intro H; [false_hyp H lt_0 | -le_elim H; [false_hyp H lt_0 | false_hyp H S_0]]. -intros m; split; intro H. -apply -> lt_S in H. le_elim H; [le_intro1; now apply <- lt_resp_S | le_intro2; now apply S_wd]. -le_elim H; [apply lt_trans with (m := S n); [apply lt_n_Sn | assumption] | -apply S_inj in H; rewrite H; apply lt_n_Sn]. -Qed. +Theorem neq_succ_l : forall n : N, S n ~= n. +Proof NZneq_succ_l. -Theorem le_S_0 : forall n, ~ (S n <= 0). -Proof. -intros n H; apply <- lt_le_S_l in H; false_hyp H lt_0. -Qed. +Theorem nlt_succ_l : forall n : N, ~ S n < n. +Proof NZnlt_succ_l. -Theorem le_S_l_le : forall n m, S n <= m -> n <= m. -Proof. -intros; le_intro1; now apply <- lt_le_S_l. -Qed. +Theorem nle_succ_l : forall n : N, ~ S n <= n. +Proof NZnle_succ_l. -Theorem lt_irr : forall n, ~ (n < n). -Proof. -induct n. -apply lt_0. -intro x; unfold not; intros H1 H2; apply H1; now apply -> lt_resp_S. -Qed. +Theorem lt_le_succ : forall n m : N, n < m <-> S n <= m. +Proof NZlt_le_succ. -Theorem le_antisym : forall n m, n <= m -> m <= n -> n == m. -Proof. -intros n m H1 H2; le_elim H1; le_elim H2. -elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m). -now symmetry. assumption. assumption. -Qed. +Theorem le_succ_le : forall n m : N, S n <= m -> n <= m. +Proof NZle_succ_le. -Theorem neq_0_lt : forall n, 0 # n -> 0 < n. -Proof. -induct n. -intro H; now elim H. -intros; apply lt_0_Sn. -Qed. +Theorem succ_lt_mono : forall n m : N, n < m <-> S n < S m. +Proof NZsucc_lt_mono. -Theorem lt_0_neq : forall n, 0 < n -> 0 # n. -Proof. -induct n. -intro H; absurd_hyp H; [apply lt_0 | assumption]. -unfold not; intros; now apply S_0 with (n := n). -Qed. +Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m. +Proof NZsucc_le_mono. -Theorem lt_asymm : forall n m, ~ (n < m /\ m < n). -Proof. -unfold not; intros n m [H1 H2]. -now apply (lt_trans n m n) in H1; [false_hyp H1 lt_irr|]. -Qed. +Theorem lt_lt_false : forall n m, n < m -> m < n -> False. +Proof NZlt_lt_false. -Theorem le_0_l: forall n, 0 <= n. -Proof. -induct n; [now le_intro2 | intros; le_intro1; apply lt_0_Sn]. -Qed. +Theorem lt_asymm : forall n m, n < m -> ~ m < n. +Proof NZlt_asymm. + +Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p. +Proof NZlt_trans. + +Theorem le_trans : forall n m p : N, n <= m -> m <= p -> n <= p. +Proof NZle_trans. + +Theorem le_lt_trans : forall n m p : N, n <= m -> m < p -> n < p. +Proof NZle_lt_trans. + +Theorem lt_le_trans : forall n m p : N, n < m -> m <= p -> n < p. +Proof NZlt_le_trans. + +Theorem le_antisymm : forall n m : N, n <= m -> m <= n -> n == m. +Proof NZle_antisymm. + +(** Trichotomy, decidability, and double negation elimination *) + +Theorem lt_trichotomy : forall n m : N, n < m \/ n == m \/ m < n. +Proof NZlt_trichotomy. + +Theorem le_lt_dec : forall n m : N, n <= m \/ m < n. +Proof NZle_lt_dec. + +Theorem le_nlt : forall n m : N, n <= m <-> ~ m < n. +Proof NZle_nlt. + +Theorem lt_dec : forall n m : N, n < m \/ ~ n < m. +Proof NZlt_dec. + +Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m. +Proof NZlt_dne. + +Theorem nle_lt : forall n m : N, ~ n <= m <-> m < n. +Proof NZnle_lt. + +Theorem le_dec : forall n m : N, n <= m \/ ~ n <= m. +Proof NZle_dec. + +Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m. +Proof NZle_dne. + +Theorem lt_nlt_succ : forall n m : N, n < m <-> ~ m < S n. +Proof NZlt_nlt_succ. + +Theorem lt_exists_pred : + forall z n : N, z < n -> exists k : N, n == S k /\ z <= k. +Proof NZlt_exists_pred. + +Theorem lt_succ_iter_r : + forall (n : nat) (m : N), m < NZsucc_iter (Datatypes.S n) m. +Proof NZlt_succ_iter_r. + +Theorem neq_succ_iter_l : + forall (n : nat) (m : N), NZsucc_iter (Datatypes.S n) m ~= m. +Proof NZneq_succ_iter_l. + +(** Stronger variant of induction with assumptions n >= 0 (n < 0) +in the induction step *) -Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n. +Theorem right_induction : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + forall n : N, z <= n -> A n. +Proof NZright_induction. + +Theorem left_induction : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, A z -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : N, n <= z -> A n. +Proof NZleft_induction. + +Theorem central_induction : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : N, A n. +Proof NZcentral_induction. + +Theorem right_induction' : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, + (forall n : N, n <= z -> A n) -> + (forall n : N, z <= n -> A n -> A (S n)) -> + forall n : N, A n. +Proof NZright_induction'. + +Theorem strong_right_induction' : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, + (forall n : N, n <= z -> A n) -> + (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) -> + forall n : N, A n. +Proof NZstrong_right_induction'. + +(** Elimintation principle for < *) + +Theorem lt_ind : + forall A : N -> Prop, predicate_wd E A -> + forall n : N, + A (S n) -> + (forall m : N, n < m -> A m -> A (S m)) -> + forall m : N, n < m -> A m. +Proof NZlt_ind. + +(** Elimintation principle for <= *) + +Theorem le_ind : + forall A : N -> Prop, predicate_wd E A -> + forall n : N, + A n -> + (forall m : N, n <= m -> A m -> A (S m)) -> + forall m : N, n <= m -> A m. +Proof NZle_ind. + +(** Theorems that are true for natural numbers but not for integers *) + +Theorem le_0_l : forall n : N, 0 <= n. Proof. -intros n m; induct n. -assert (H : 0 <= m); [apply le_0_l | apply -> le_lt in H; tauto]. -intros n IH. destruct IH as [H | H]. -assert (H1 : S n <= m); [now apply -> lt_le_S_l | apply -> le_lt in H1; tauto]. -destruct H as [H | H]. -right; right; rewrite H; apply lt_n_Sn. -right; right; apply lt_trans with (m := n); [assumption | apply lt_n_Sn]. +induct n. +now le_intro2. +intros; now apply le_le_succ. Qed. -(** The law of excluded middle for < *) -Theorem lt_em : forall n m, n < m \/ ~ n < m. +Theorem nle_succ_0 : forall n, ~ (S n <= 0). Proof. -intros n m; pose proof (lt_trichotomy n m) as H. -destruct H as [H1 | H1]; [now left |]. -destruct H1 as [H2 | H2]. -right; rewrite H2; apply lt_irr. -right; intro; apply (lt_asymm n m); split; assumption. +intros n H; apply <- lt_le_succ in H; false_hyp H nlt_0_r. Qed. -Theorem not_lt : forall n m, ~ (n < m) <-> n >= m. +Theorem le_0_eq_0 : forall n, n <= 0 -> n == 0. Proof. -intros n m; split; intro H. -destruct (lt_trichotomy n m) as [H1 | [H1 | H1]]. -false_hyp H1 H. rewrite H1; apply le_refl. now le_intro1. -intro; now apply (le_lt_trans m n m) in H; [false_hyp H lt_irr |]. +intros n H; le_elim H; [false_hyp H nlt_0_r | assumption]. Qed. -Theorem lt_or_ge : forall n m, n < m \/ n >= m. +Theorem lt_0_succ : forall n, 0 < S n. Proof. -intros n m; rewrite <- not_lt; apply lt_em. +induct n; [apply lt_succ_r | intros n H; now apply lt_lt_succ]. Qed. -Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n. +Theorem lt_lt_0 : forall n m, n < m -> 0 < m. Proof. -intros n m H; destruct (lt_trichotomy n m) as [A | A]; [now left |]. -now destruct A as [A | A]; [elim H | right]. +intros n m; induct n. +trivial. +intros n IH H. apply IH; now apply lt_succ_lt. Qed. -Theorem lt_exists_pred : forall n m, m < n -> exists p, n == S p. +Theorem neq_0_lt_0 : forall n, 0 ~= n -> 0 < n. Proof. -nondep_induct n. -intros m H; false_hyp H lt_0. -intros n _ _; now exists n. +nondep_induct n. intro H; now elim H. intros; apply lt_0_succ. Qed. -(** Elimination principles for < and <= *) - -Section Induction1. - -Variable Q : N -> Prop. -Hypothesis Q_wd : pred_wd E Q. -Variable n : N. - -Add Morphism Q with signature E ==> iff as Q_morph1. -Proof Q_wd. - -Theorem le_ind : - Q n -> - (forall m, n <= m -> Q m -> Q (S m)) -> - forall m, n <= m -> Q m. +Lemma Acc_nonneg_lt : forall n : N, + Acc (fun n m => 0 <= n /\ n < m) n -> Acc lt n. Proof. -intros Base Step. induct m. -intro H. apply le_0_r in H. now rewrite <- H. -intros m IH H. le_elim H. -apply -> lt_S in H. now apply Step; [| apply IH]. -now rewrite <- H. +intros n H; induction H as [n _ H2]; +constructor; intros y H; apply H2; split; [apply le_0_l | assumption]. Qed. -Theorem lt_ind : - Q (S n) -> - (forall m, n < m -> Q m -> Q (S m)) -> - forall m, n < m -> Q m. +Theorem lt_wf : well_founded lt. Proof. -intros Base Step. induct m. -intro H; false_hyp H lt_0. -intros m IH H. apply -> lt_S in H. le_elim H. -now apply Step; [| apply IH]. now rewrite <- H. +unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf. Qed. -End Induction1. +(** Elimination principlies for < and <= for relations *) -Section Induction2. +Section RelElim. -(* Variable Q : relation N. -- does not work !!! *) -Variable Q : N -> N -> Prop. -Hypothesis Q_wd : rel_wd E Q. +(* FIXME: Variable R : relation N. -- does not work *) -Add Morphism Q with signature E ==> E ==> iff as Q_morph2. -Proof Q_wd. +Variable R : N -> N -> Prop. +Hypothesis R_wd : rel_wd E E R. + +Add Morphism R with signature E ==> E ==> iff as R_morph2. +Proof R_wd. Theorem le_ind_rel : - (forall m, Q 0 m) -> - (forall n m, n <= m -> Q n m -> Q (S n) (S m)) -> - forall n m, n <= m -> Q n m. + (forall m, R 0 m) -> + (forall n m, n <= m -> R n m -> R (S n) (S m)) -> + forall n m, n <= m -> R n m. Proof. intros Base Step; induct n. intros; apply Base. -intros n IH m; nondep_induct m. -intro H; false_hyp H le_S_0. -intros m H. apply -> le_resp_S in H. now apply Step; [| apply IH]. +intros n IH m H. elim H using le_ind. +solve_predicate_wd. +apply Step; [| apply IH]; now le_intro2. +intros k H1 H2. apply le_succ_le in H1. auto. Qed. Theorem lt_ind_rel : - (forall m, Q 0 (S m)) -> - (forall n m, n < m -> Q n m -> Q (S n) (S m)) -> - forall n m, n < m -> Q n m. + (forall m, R 0 (S m)) -> + (forall n m, n < m -> R n m -> R (S n) (S m)) -> + forall n m, n < m -> R n m. Proof. intros Base Step; induct n. -intros m H. apply lt_exists_pred in H; destruct H as [m' H]. +intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. rewrite H; apply Base. -intros n IH m; nondep_induct m. -intro H; false_hyp H lt_0. -intros m H. apply -> lt_resp_S in H. now apply Step; [| apply IH]. +intros n IH m H. elim H using lt_ind. +solve_predicate_wd. +apply Step; [| apply IH]; now apply lt_succ_r. +intros k H1 H2. apply lt_succ_lt in H1. auto. Qed. -End Induction2. +End RelElim. + +End NOrderPropFunct. + -End NOrderProperties. +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) |