diff options
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZAxioms.v | 120 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZDomain.v | 42 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZOrder.v | 447 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZPlus.v | 222 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZPlusOrder.v | 160 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZTimes.v | 135 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZTimesOrder.v | 92 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/CommRefl.v | 185 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 45 |
9 files changed, 1448 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v new file mode 100644 index 0000000000..4f0eab8e35 --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZAxioms.v @@ -0,0 +1,120 @@ +Require Import NumPrelude. +Require Import ZDomain. + +Module Type IntSignature. +Declare Module Export DomainModule : DomainSignature. + +Parameter Inline O : Z. +Parameter Inline S : Z -> Z. +Parameter Inline P : Z -> Z. + +Notation "0" := O. + +Add Morphism S with signature E ==> E as S_wd. +Add Morphism P with signature E ==> E as P_wd. + +Axiom S_inj : forall x y : Z, S x == S y -> x == y. +Axiom S_P : forall x : Z, S (P x) == x. + +Axiom induction : + forall Q : Z -> Prop, + pred_wd E Q -> Q 0 -> + (forall x, Q x -> Q (S x)) -> + (forall x, Q x -> Q (P x)) -> forall x, Q x. + +End IntSignature. + + +Module IntProperties (Export IntModule : IntSignature). + +Module Export DomainPropertiesModule := DomainProperties DomainModule. + +Ltac induct n := + try intros until n; + pattern n; apply induction; clear n; + [unfold NumPrelude.pred_wd; + let n := fresh "n" in + let m := fresh "m" in + let H := fresh "H" in intros n m H; qmorphism n m | | |]. + +Theorem P_inj : forall x y, P x == P y -> x == y. +Proof. +intros x y H. +setoid_replace x with (S (P x)); [| symmetry; apply S_P]. +setoid_replace y with (S (P y)); [| symmetry; apply S_P]. +now rewrite H. +Qed. + +Theorem P_S : forall x, P (S x) == x. +Proof. +intro x. +apply S_inj. +now rewrite S_P. +Qed. + +(* The following tactics are intended for replacing a certain +occurrence of a term t in the goal by (S (P t)) or by (P (S t)). +Unfortunately, this cannot be done by setoid_replace tactic for two +reasons. First, it seems impossible to do rewriting when one side of +the equation in question (S_P or P_S) is a variable, due to bug 1604. +This does not work even when the predicate is an identifier (e.g., +when one tries to rewrite (Q x) into (Q (S (P x)))). Second, the +setoid_rewrite tactic, like the ordinary rewrite tactic, does not +allow specifying the exact occurrence of the term to be rewritten. Now +while not in the setoid context, this occurrence can be specified +using the pattern tactic, it does not work with setoids, since pattern +creates a lambda abstractuion, and setoid_rewrite does not work with +them. *) + +Ltac rewrite_SP t set_tac repl thm := +let x := fresh "x" in +set_tac x t; +setoid_replace x with (repl x); [| symmetry; apply thm]; +unfold x; clear x. + +Tactic Notation "rewrite_S_P" constr(t) := +rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) S_P. + +Tactic Notation "rewrite_S_P" constr(t) "at" integer(k) := +rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) S_P. + +Tactic Notation "rewrite_P_S" constr(t) := +rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) P_S. + +Tactic Notation "rewrite_P_S" constr(t) "at" integer(k) := +rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) P_S. + +(* One can add tactic notations for replacements in assumptions rather +than in the goal. For the reason of many possible variants, the core +of the tactic is factored out. *) + +Section Induction. + +Variable Q : Z -> Prop. +Hypothesis Q_wd : pred_wd E Q. + +Add Morphism Q with signature E ==> iff as Q_morph. +Proof Q_wd. + +Theorem induction_n : + forall n, Q n -> + (forall m, Q m -> Q (S m)) -> + (forall m, Q m -> Q (P m)) -> forall m, Q m. +Proof. +induct n. +intros; now apply induction. +intros n IH H1 H2 H3; apply IH; try assumption. apply H3 in H1; now rewrite P_S in H1. +intros n IH H1 H2 H3; apply IH; try assumption. apply H2 in H1; now rewrite S_P in H1. +Qed. + +End Induction. + +Ltac induct_n k n := + try intros until k; + pattern k; apply induction_n with (n := n); clear k; + [unfold NumPrelude.pred_wd; + let n := fresh "n" in + let m := fresh "m" in + let H := fresh "H" in intros n m H; qmorphism n m | | |]. + +End IntProperties. diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v new file mode 100644 index 0000000000..00eab8842f --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZDomain.v @@ -0,0 +1,42 @@ +Require Import NumPrelude. + +Module Type DomainSignature. + +Parameter Z : Set. +Parameter E : relation Z. +Parameter e : Z -> Z -> bool. + +Axiom E_equiv_e : forall x y : Z, E x y <-> e x y. +Axiom E_equiv : equiv Z E. + +Add Relation Z E + reflexivity proved by (proj1 E_equiv) + symmetry proved by (proj2 (proj2 E_equiv)) + transitivity proved by (proj1 (proj2 E_equiv)) +as E_rel. + +Notation "x == y" := (E x y) (at level 70). +Notation "x # y" := (~ E x y) (at level 70). + +End DomainSignature. + +Module DomainProperties (Export DomainModule : DomainSignature). + +Add Morphism e with signature E ==> E ==> eq_bool as e_wd. +Proof. +intros x x' Exx' y y' Eyy'. +case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial. +assert (x == y); [apply <- E_equiv_e; now rewrite H2 | +assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' | +rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]]. +assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 | +assert (x == y); [rewrite Exx'; now rewrite Eyy' | +rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]]. +Qed. + +Theorem neq_symm : forall n m, n # m -> m # n. +Proof. +intros n m H1 H2; symmetry in H2; false_hyp H2 H1. +Qed. + +End DomainProperties. diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v new file mode 100644 index 0000000000..b1983d6f7f --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZOrder.v @@ -0,0 +1,447 @@ +Require Import NumPrelude. +Require Import ZDomain. +Require Import ZAxioms. +Require Import Coq.ZArith.Zmisc. (* for iter_nat *) + +Module Type OrderSignature. +Declare Module Export IntModule : IntSignature. + +Parameter Inline lt : Z -> Z -> bool. +Parameter Inline le : Z -> Z -> bool. +Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. +Add Morphism le with signature E ==> E ==> eq_bool as le_wd. + +Notation "n < m" := (lt n m). +Notation "n <= m" := (le n m). + +Axiom le_lt : forall n m, n <= m <-> n < m \/ n == m. +Axiom lt_irr : forall n, ~ (n < n). +Axiom lt_S : forall n m, n < (S m) <-> n <= m. + +End OrderSignature. + + +Module OrderProperties (Export OrderModule : OrderSignature). +Module Export IntPropertiesModule := IntProperties IntModule. + +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]. + +Theorem le_refl : forall n, n <= n. +Proof. +intro n; now le_intro2. +Qed. + +Theorem lt_n_Sn : forall n, n < S n. +Proof. +intro n. rewrite lt_S. now le_intro2. +Qed. + +Theorem le_n_Sn : forall n, n <= S n. +Proof. +intro; le_intro1; apply lt_n_Sn. +Qed. + +Theorem lt_Pn_n : forall n, P n < n. +Proof. +intro n; rewrite_S_P n at 2; apply lt_n_Sn. +Qed. + +Theorem le_Pn_n : forall n, P n <= n. +Proof. +intro; le_intro1; apply lt_Pn_n. +Qed. + +Theorem lt_n_Sm : forall n m, n < m -> n < S m. +Proof. +intros. rewrite lt_S. now le_intro1. +Qed. + +Theorem le_n_Sm : forall n m, n <= m -> n <= S m. +Proof. +intros n m H; rewrite <- lt_S in H; now le_intro1. +Qed. + +Theorem lt_n_m_P : forall n m, n < m <-> n <= P m. +Proof. +intros n m; rewrite_S_P m; rewrite P_S; apply lt_S. +Qed. + +Theorem not_le_n_Pn : forall n, ~ n <= P n. +Proof. +intros n H; le_elim H. +apply lt_n_Sm in H; rewrite S_P in H; false_hyp H lt_irr. +pose proof (lt_Pn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr. +Qed. + +Theorem le_S : forall n m, n <= S m <-> n <= m \/ n == S m. +Proof. +intros n m; rewrite le_lt. now rewrite lt_S. +Qed. + +Theorem lt_P : forall n m, (P n) < m <-> n <= m. +Proof. +intro n; induct_n m (P n). +split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_Pn. +intros m IH; split; intro H. +apply -> lt_S in H; le_elim H. +apply -> IH in H; now apply le_n_Sm. +rewrite <- H; rewrite S_P; now le_intro2. +apply -> le_S in H; destruct H as [H | H]. +apply <- IH in H. now apply lt_n_Sm. rewrite H; rewrite P_S; apply lt_n_Sn. +intros m IH; split; intro H. +pose proof H as H1. apply lt_n_Sm in H; rewrite S_P in H. +apply -> IH in H; le_elim H. now apply -> lt_n_m_P. +rewrite H in H1; false_hyp H1 lt_irr. +pose proof H as H1. apply le_n_Sm in H. rewrite S_P in H. +apply <- IH in H. apply -> lt_n_m_P in H. le_elim H. +assumption. apply P_inj in H; rewrite H in H1; false_hyp H1 not_le_n_Pn. +Qed. + +Theorem lt_Pn_m : forall n m, n < m -> P n < m. +Proof. +intros; rewrite lt_P; now le_intro1. +Qed. + +Theorem le_Pn_m : forall n m, n <= m -> P n <= m. +Proof. +intros n m H; rewrite <- lt_P in H; now le_intro1. +Qed. + +Theorem lt_n_m_S : forall n m, n < m <-> S n <= m. +Proof. +intros n m; rewrite_P_S n; rewrite S_P; apply lt_P. +Qed. + +Theorem lt_Sn_m : forall n m, S n < m -> n < m. +Proof. +intros n m H; rewrite_P_S n; now apply lt_Pn_m. +Qed. + +Theorem le_Sn_m : forall n m, S n <= m -> n <= m. +Proof. +intros n m H; rewrite <- lt_n_m_S in H; now le_intro1. +Qed. + +Theorem lt_n_Pm : forall n m, n < P m -> n < m. +Proof. +intros n m H; rewrite_S_P m; now apply lt_n_Sm. +Qed. + +Theorem le_n_Pm : forall n m, n <= P m -> n <= m. +Proof. +intros n m H; rewrite <- lt_n_m_P in H; now le_intro1. +Qed. + +Theorem lt_respects_S : forall n m, n < m <-> S n < S m. +Proof. +intros n m. rewrite lt_n_m_S. symmetry. apply lt_S. +Qed. + +Theorem le_respects_S : forall n m, n <= m <-> S n <= S m. +Proof. +intros n m. do 2 rewrite le_lt. +firstorder using lt_respects_S S_wd S_inj. +Qed. + +Theorem lt_respects_P : forall n m, n < m <-> P n < P m. +Proof. +intros n m. rewrite lt_n_m_P. symmetry; apply lt_P. +Qed. + +Theorem le_respects_P : forall n m, n <= m <-> P n <= P m. +Proof. +intros n m. do 2 rewrite le_lt. +firstorder using lt_respects_P P_wd P_inj. +Qed. + +Theorem lt_S_P : forall n m, S n < m <-> n < P m. +Proof. +intros n m; rewrite_P_S n at 2; apply lt_respects_P. +Qed. + +Theorem le_S_P : forall n m, S n <= m <-> n <= P m. +Proof. +intros n m; rewrite_P_S n at 2; apply le_respects_P. +Qed. + +Theorem lt_P_S : forall n m, P n < m <-> n < S m. +Proof. +intros n m; rewrite_S_P n at 2; apply lt_respects_S. +Qed. + +Theorem le_P_S : forall n m, P n <= m <-> n <= S m. +Proof. +intros n m; rewrite_S_P n at 2; apply le_respects_S. +Qed. + +Theorem lt_neq : forall n m, n < m -> n # m. +Proof. +intros n m H1 H2; rewrite H2 in H1; false_hyp H1 lt_irr. +Qed. + +Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. +Proof. +intros n m; induct_n n m. +intros p H _; false_hyp H lt_irr. +intros n IH p H1 H2. apply lt_Sn_m in H1. pose proof (IH p H1 H2) as H3. +rewrite lt_n_m_S in H3; le_elim H3. +assumption. rewrite <- H3 in H2. rewrite lt_S in H2; le_elim H2. +elimtype False; apply lt_irr with (n := n); now apply IH. +rewrite H2 in H1; false_hyp H1 lt_irr. +intros n IH p H1 H2. apply lt_Pn_m. rewrite lt_P in H1; le_elim H1. +now apply IH. now rewrite H1. +Qed. + +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_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_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 lt_asymm : forall n m, n < m -> ~ m < n. +Proof. +intros n m H1 H2; apply lt_irr with (n := n); now apply lt_trans with (m := m). +Qed. + +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 not_lt_Sn_n : forall n, ~ S n < n. +Proof. +intros n H; apply (lt_asymm n (S n)). apply lt_n_Sn. assumption. +Qed. + +Theorem not_le_Sn_n : forall n, ~ S n <= n. +Proof. +intros n H; le_elim H. false_hyp H not_lt_Sn_n. +pose proof (lt_n_Sn n) as H1. rewrite H in H1; false_hyp H1 lt_irr. +Qed. + +Theorem lt_gt : forall n m, n < m -> m < n -> False. +Proof. +intros n m H1 H2; apply lt_irr with (n := n); now apply lt_trans with (m := m). +Qed. + +Theorem lt_total : forall n m, n < m \/ n == m \/ m < n. +Proof. +intros n m; induct_n n m. +right; now left. +intros n IH; destruct IH as [H | [H | H]]. +rewrite lt_n_m_S in H. rewrite le_lt in H; tauto. +right; right; rewrite H; apply lt_n_Sn. +right; right; now apply lt_n_Sm. +intros n IH; destruct IH as [H | [H | H]]. +left; now apply lt_Pn_m. +left; rewrite H; apply lt_Pn_n. +rewrite lt_n_m_P in H. rewrite le_lt in H. +setoid_replace (m == P n) with (P n == m) in H using relation iff. tauto. +split; intro; now symmetry. +Qed. + +Theorem le_gt : forall n m, n <= m <-> ~ m < n. +Proof. +intros n m. rewrite -> le_lt. +pose proof (lt_total n m). pose proof (lt_gt n m). +assert (n == m -> ~ m < n); [intro A; rewrite A; apply lt_irr |]. +tauto. +Qed. + +Theorem lt_ge : forall n m, n < m <-> ~ m <= n. +Proof. +intros n m. rewrite -> le_lt. +pose proof (lt_total m n). pose proof (lt_gt n m). +assert (n < m -> m # n); [intros A B; rewrite B in A; false_hyp A lt_irr |]. +tauto. +Qed. + +Theorem lt_discrete : forall n m, n < m -> m < S n -> False. +Proof. +intros n m H1 H2; apply -> lt_S in H2; apply -> lt_ge in H1; false_hyp H2 H1. +Qed. + +(* Decidability of order can be proved either from totality or from the fact +that < and <= are boolean functions *) + +(** A corollary of having an order is that Z is infinite in both +directions *) + +Theorem neq_Sn_n : forall n, S n # n. +Proof. +intros n H. pose proof (lt_n_Sn n) as H1. rewrite H in H1. false_hyp H1 lt_irr. +Qed. + +Theorem neq_Pn_n : forall n, P n # n. +Proof. +intros n H. apply S_wd in H. rewrite S_P in H. now apply neq_Sn_n with (n := n). +Qed. + +Lemma lt_n_Skn : + forall (n : Z) (k : nat), n < iter_nat (Datatypes.S k) Z S n. +Proof. +intro n; induction k as [| k IH]; simpl in *. +apply lt_n_Sn. now apply lt_n_Sm. +Qed. + +Lemma lt_Pkn_n : + forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z P n < n. +Proof. +intro n; induction k as [| k IH]; simpl in *. +apply lt_Pn_n. now apply lt_Pn_m. +Qed. + +Theorem neq_n_Skn : + forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z S n # n. +Proof. +intros n k H. pose proof (lt_n_Skn n k) as H1. rewrite H in H1. +false_hyp H1 lt_irr. +Qed. + +Theorem neq_Pkn_n : + forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z P n # n. +Proof. +intros n k H. pose proof (lt_Pkn_n n k) as H1. rewrite H in H1. +false_hyp H1 lt_irr. +Qed. + +(** Stronger variant of induction with assumptions n >= 0 (n <= 0) +in the induction step *) + +Section Induction. + +Variable Q : Z -> Prop. +Hypothesis Q_wd : pred_wd E Q. + +Add Morphism Q with signature E ==> iff as Q_morph. +Proof Q_wd. + +Section Center. + +Variable z : Z. (* Q z is the basis of induction *) + +Section RightInduction. + +Let Q' := fun n : Z => forall m, z <= m -> m < n -> Q m. + +Add Morphism Q' with signature E ==> iff as Q'_pos_wd. +Proof. +intros x1 x2 H; unfold Q'; qmorphism x1 x2. +Qed. + +Theorem right_induction : + Q z -> (forall n, z <= n -> Q n -> Q (S n)) -> forall n, z <= n -> Q n. +Proof. +intros Qz QS k k_ge_z. +assert (H : forall n, Q' n). induct_n n z; unfold Q'. +intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1. +intros n IH m H2 H3. +rewrite lt_S in H3; le_elim H3. now apply IH. +le_elim H2. rewrite_S_P m. +apply QS. now apply -> lt_n_m_P. apply IH. now apply -> lt_n_m_P. +rewrite H3; apply lt_Pn_n. now rewrite <- H2. +intros n IH m H2 H3. apply IH. assumption. now apply lt_n_Pm. +pose proof (H (S k)) as H1; unfold Q' in H1. apply H1. +apply k_ge_z. apply lt_n_Sn. +Qed. + +End RightInduction. + +Section LeftInduction. + +Let Q' := fun n : Z => forall m, m <= z -> n < m -> Q m. + +Add Morphism Q' with signature E ==> iff as Q'_neg_wd. +Proof. +intros x1 x2 H; unfold Q'; qmorphism x1 x2. +Qed. + +Theorem left_induction : + Q z -> (forall n, n <= z -> Q n -> Q (P n)) -> forall n, n <= z -> Q n. +Proof. +intros Qz QP k k_le_z. +assert (H : forall n, Q' n). induct_n n z; unfold Q'. +intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1. +intros n IH m H2 H3. apply IH. assumption. now apply lt_Sn_m. +intros n IH m H2 H3. +rewrite lt_P in H3; le_elim H3. now apply IH. +le_elim H2. rewrite_P_S m. +apply QP. now apply -> lt_n_m_S. apply IH. now apply -> lt_n_m_S. +rewrite H3; apply lt_n_Sn. now rewrite H2. +pose proof (H (P k)) as H1; unfold Q' in H1. apply H1. +apply k_le_z. apply lt_Pn_n. +Qed. + +End LeftInduction. + +Theorem induction_ord_n : + Q z -> + (forall n, z <= n -> Q n -> Q (S n)) -> + (forall n, n <= z -> Q n -> Q (P n)) -> + forall n, Q n. +Proof. +intros Qz QS QP n. +destruct (lt_total n z) as [H | [H | H]]. +now apply left_induction; [| | le_intro1]. +now rewrite H. +now apply right_induction; [| | le_intro1]. +Qed. + +End Center. + +Theorem induction_ord : + Q 0 -> + (forall n, 0 <= n -> Q n -> Q (S n)) -> + (forall n, n <= 0 -> Q n -> Q (P n)) -> + forall n, Q n. +Proof (induction_ord_n 0). + +Theorem lt_ind : forall (n : Z), + Q (S n) -> + (forall m : Z, n < m -> Q m -> Q (S m)) -> + forall m : Z, n < m -> Q m. +Proof. +intros n H1 H2 m H3. +apply right_induction with (S n). assumption. +intros; apply H2; try assumption. now apply <- lt_n_m_S. +now apply -> lt_n_m_S. +Qed. + +Theorem le_ind : forall (n : Z), + Q n -> + (forall m : Z, n <= m -> Q m -> Q (S m)) -> + forall m : Z, n <= m -> Q m. +Proof. +intros n H1 H2 m H3. +now apply right_induction with n. +Qed. + +End Induction. + +Ltac induct_ord n := + try intros until n; + pattern n; apply induction_ord; clear n; + [unfold NumPrelude.pred_wd; + let n := fresh "n" in + let m := fresh "m" in + let H := fresh "H" in intros n m H; qmorphism n m | | |]. + +End OrderProperties. + diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v new file mode 100644 index 0000000000..1b5aa73fb2 --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZPlus.v @@ -0,0 +1,222 @@ +Require Import NumPrelude. +Require Import ZDomain. +Require Import ZAxioms. + +Module Type PlusSignature. +Declare Module Export IntModule : IntSignature. + +Parameter Inline plus : Z -> Z -> Z. +Parameter Inline minus : Z -> Z -> Z. +Parameter Inline uminus : Z -> Z. + +Notation "x + y" := (plus x y). +Notation "x - y" := (minus x y). +Notation "- x" := (uminus x). + +Add Morphism plus with signature E ==> E ==> E as plus_wd. +Add Morphism minus with signature E ==> E ==> E as minus_wd. +Add Morphism uminus with signature E ==> E as uminus_wd. + +Axiom plus_0 : forall n, 0 + n == n. +Axiom plus_S : forall n m, (S n) + m == S (n + m). + +Axiom minus_0 : forall n, n - 0 == n. +Axiom minus_S : forall n m, n - (S m) == P (n - m). + +Axiom uminus_0 : - 0 == 0. +Axiom uminus_S : forall n, - (S n) == P (- n). + +End PlusSignature. + +Module PlusProperties (Export PlusModule : PlusSignature). + +Module Export IntPropertiesModule := IntProperties IntModule. + +Theorem plus_P : forall n m, P n + m == P (n + m). +Proof. +intros n m. rewrite_S_P n at 2. rewrite plus_S. now rewrite P_S. +Qed. + +Theorem minus_P : forall n m, n - (P m) == S (n - m). +Proof. +intros n m. rewrite_S_P m at 2. rewrite minus_S. now rewrite S_P. +Qed. + +Theorem uminus_P : forall n, - (P n) == S (- n). +Proof. +intro n. rewrite_S_P n at 2. rewrite uminus_S. now rewrite S_P. +Qed. + +Theorem plus_n_0 : forall n, n + 0 == n. +Proof. +induct n. +now rewrite plus_0. +intros n IH. rewrite plus_S. now rewrite IH. +intros n IH. rewrite plus_P. now rewrite IH. +Qed. + +Theorem plus_n_Sm : forall n m, n + S m == S (n + m). +Proof. +intros n m; induct n. +now do 2 rewrite plus_0. +intros n IH. do 2 rewrite plus_S. now rewrite IH. +intros n IH. do 2 rewrite plus_P. rewrite IH. rewrite P_S; now rewrite S_P. +Qed. + +Theorem plus_n_Pm : forall n m, n + P m == P (n + m). +Proof. +intros n m; rewrite_S_P m at 2. rewrite plus_n_Sm; now rewrite P_S. +Qed. + +Theorem plus_opp_minus : forall n m, n + (- m) == n - m. +Proof. +induct m. +rewrite uminus_0; rewrite minus_0; now rewrite plus_n_0. +intros m IH. rewrite uminus_S; rewrite minus_S. rewrite plus_n_Pm; now rewrite IH. +intros m IH. rewrite uminus_P; rewrite minus_P. rewrite plus_n_Sm; now rewrite IH. +Qed. + +Theorem minus_0_n : forall n, 0 - n == - n. +Proof. +intro n; rewrite <- plus_opp_minus; now rewrite plus_0. +Qed. + +Theorem minus_Sn_m : forall n m, S n - m == S (n - m). +Proof. +intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_S. +Qed. + +Theorem minus_Pn_m : forall n m, P n - m == P (n - m). +Proof. +intros n m. rewrite_S_P n at 2; rewrite minus_Sn_m; now rewrite P_S. +Qed. + +Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p. +Proof. +intros n m p; induct n. +now do 2 rewrite plus_0. +intros n IH. do 3 rewrite plus_S. now rewrite IH. +intros n IH. do 3 rewrite plus_P. now rewrite IH. +Qed. + +Theorem plus_comm : forall n m, n + m == m + n. +Proof. +intros n m; induct n. +rewrite plus_0; now rewrite plus_n_0. +intros n IH; rewrite plus_S; rewrite plus_n_Sm; now rewrite IH. +intros n IH; rewrite plus_P; rewrite plus_n_Pm; now rewrite IH. +Qed. + +Theorem minus_diag : forall n, n - n == 0. +Proof. +induct n. +now rewrite minus_0. +intros n IH. rewrite minus_S; rewrite minus_Sn_m; rewrite P_S; now rewrite IH. +intros n IH. rewrite minus_P; rewrite minus_Pn_m; rewrite S_P; now rewrite IH. +Qed. + +Theorem plus_opp_r : forall n, n + (- n) == 0. +Proof. +intro n; rewrite plus_opp_minus; now rewrite minus_diag. +Qed. + +Theorem plus_opp_l : forall n, - n + n == 0. +Proof. +intro n; rewrite plus_comm; apply plus_opp_r. +Qed. + +Theorem minus_swap : forall n m, - m + n == n - m. +Proof. +intros n m; rewrite <- plus_opp_minus; now rewrite plus_comm. +Qed. + +Theorem plus_minus_inverse : forall n m, n + (m - n) == m. +Proof. +intros n m; rewrite <- minus_swap. rewrite plus_assoc; +rewrite plus_opp_r; now rewrite plus_0. +Qed. + +Theorem plus_minus_distr : forall n m p, n + (m - p) == (n + m) - p. +Proof. +intros n m p; do 2 rewrite <- plus_opp_minus; now rewrite plus_assoc. +Qed. + +Theorem double_opp : forall n, - (- n) == n. +Proof. +induct n. +now do 2 rewrite uminus_0. +intros n IH. rewrite uminus_S; rewrite uminus_P; now rewrite IH. +intros n IH. rewrite uminus_P; rewrite uminus_S; now rewrite IH. +Qed. + +Theorem opp_plus_distr : forall n m, - (n + m) == - n + (- m). +Proof. +intros n m; induct n. +rewrite uminus_0; now do 2 rewrite plus_0. +intros n IH. rewrite plus_S; do 2 rewrite uminus_S. rewrite IH. now rewrite plus_P. +intros n IH. rewrite plus_P; do 2 rewrite uminus_P. rewrite IH. now rewrite plus_S. +Qed. + +Theorem opp_minus_distr : forall n m, - (n - m) == - n + m. +Proof. +intros n m; rewrite <- plus_opp_minus; rewrite opp_plus_distr. +now rewrite double_opp. +Qed. + +Theorem opp_inj : forall n m, - n == - m -> n == m. +Proof. +intros n m H. apply uminus_wd in H. now do 2 rewrite double_opp in H. +Qed. + +Theorem minus_plus_distr : forall n m p, n - (m + p) == (n - m) - p. +Proof. +intros n m p; rewrite <- plus_opp_minus. rewrite opp_plus_distr. rewrite plus_assoc. +now do 2 rewrite plus_opp_minus. +Qed. + +Theorem minus_minus_distr : forall n m p, n - (m - p) == (n - m) + p. +Proof. +intros n m p; rewrite <- plus_opp_minus. rewrite opp_minus_distr. rewrite plus_assoc. +now rewrite plus_opp_minus. +Qed. + +Theorem plus_minus_swap : forall n m p, n + m - p == n - p + m. +Proof. +intros n m p. rewrite <- plus_minus_distr. +rewrite <- (plus_opp_minus n p). rewrite <- plus_assoc. now rewrite minus_swap. +Qed. + +Theorem plus_cancel_l : forall n m p, n + m == n + p -> m == p. +Proof. +intros n m p H. +assert (H1 : - n + n + m == -n + n + p). +do 2 rewrite <- plus_assoc; now rewrite H. +rewrite plus_opp_l in H1; now do 2 rewrite plus_0 in H1. +Qed. + +Theorem plus_cancel_r : forall n m p, n + m == p + m -> n == p. +Proof. +intros n m p H. +rewrite plus_comm in H. set (k := m + n) in H. rewrite plus_comm in H. +unfold k in H; clear k. now apply plus_cancel_l with m. +Qed. + +Theorem plus_minus_l : forall n m p, m + p == n -> p == n - m. +Proof. +intros n m p H. +assert (H1 : - m + m + p == - m + n). +rewrite <- plus_assoc; now rewrite H. +rewrite plus_opp_l in H1. rewrite plus_0 in H1. now rewrite minus_swap in H1. +Qed. + +Theorem plus_minus_r : forall n m p, m + p == n -> m == n - p. +Proof. +intros n m p H; rewrite plus_comm in H; now apply plus_minus_l in H. +Qed. + +Lemma minus_eq : forall n m, n - m == 0 -> n == m. +Proof. +intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0. +Qed. + +End PlusProperties. diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v new file mode 100644 index 0000000000..abaaa664f7 --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v @@ -0,0 +1,160 @@ +Require Import ZOrder. +Require Import ZPlus. +(* Warning: Trying to mask the absolute name "Plus"!!! *) + +Module PlusOrderProperties (Export PlusModule : PlusSignature) + (Export OrderModule : OrderSignature with + Module IntModule := PlusModule.IntModule). + +Module Export PlusPropertiesModule := PlusProperties PlusModule. +Module Export OrderPropertiesModule := OrderProperties OrderModule. + +Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m. +Proof. +intros n m p; induct p. +now do 2 rewrite plus_0. +intros p IH. do 2 rewrite plus_S. now rewrite <- lt_respects_S. +intros p IH. do 2 rewrite plus_P. now rewrite <- lt_respects_P. +Qed. + +Theorem plus_lt_compat_r : forall n m p, n < m <-> n + p < m + p. +Proof. +intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p); +apply plus_lt_compat_l. +Qed. + +Theorem plus_le_compat_l : forall n m p, n <= m <-> p + n <= p + m. +Proof. +intros n m p; do 2 rewrite <- lt_S. rewrite <- plus_n_Sm; +apply plus_lt_compat_l. +Qed. + +Theorem plus_le_compat_r : forall n m p, n <= m <-> n + p <= m + p. +Proof. +intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p); +apply plus_le_compat_l. +Qed. + +Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. +Proof. +intros n m p q H1 H2. apply lt_trans with (m := m + p). +now apply -> plus_lt_compat_r. now apply -> plus_lt_compat_l. +Qed. + +Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q. +Proof. +intros n m p q H1 H2. le_elim H2. now apply plus_lt_compat. +rewrite H2. now apply -> plus_lt_compat_r. +Qed. + +Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. +Proof. +intros n m p q H1 H2. le_elim H1. now apply plus_lt_compat. +rewrite H1. now apply -> plus_lt_compat_l. +Qed. + +Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q. +Proof. +intros n m p q H1 H2. le_elim H1. le_intro1; now apply plus_lt_le_compat. +rewrite H1. now apply -> plus_le_compat_l. +Qed. + +Theorem plus_pos : forall n m, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof. +intros; rewrite <- (plus_0 0); now apply plus_le_compat. +Qed. + +Lemma lt_opp_forward : forall n m, n < m -> - m < - n. +Proof. +induct n. +induct_ord m. +intro H; false_hyp H lt_irr. +intros m H1 IH H2. rewrite uminus_S. rewrite uminus_0 in *. +le_elim H1. apply IH in H1. now apply lt_Pn_m. +rewrite <- H1; rewrite uminus_0; apply lt_Pn_n. +intros m H1 IH H2. apply lt_n_Pm in H2. apply -> le_gt in H1. false_hyp H2 H1. +intros n IH m H. rewrite uminus_S. +apply -> lt_S_P in H. apply IH in H. rewrite uminus_P in H. now apply -> lt_S_P. +intros n IH m H. rewrite uminus_P. +apply -> lt_P_S in H. apply IH in H. rewrite uminus_S in H. now apply -> lt_P_S. +Qed. + +Theorem lt_opp : forall n m, n < m <-> - m < - n. +Proof. +intros n m; split. +apply lt_opp_forward. +intro; rewrite <- (double_opp n); rewrite <- (double_opp m); +now apply lt_opp_forward. +Qed. + +Theorem le_opp : forall n m, n <= m <-> - m <= - n. +Proof. +intros n m; do 2 rewrite -> le_lt; rewrite <- lt_opp. +assert (n == m <-> - m == - n). +split; intro; [now apply uminus_wd | now apply opp_inj]. +tauto. +Qed. + +Theorem lt_opp_neg : forall n, n < 0 <-> 0 < - n. +Proof. +intro n. set (k := 0) in |-* at 2. +setoid_replace k with (- k); unfold k; clear k. +apply lt_opp. now rewrite uminus_0. +Qed. + +Theorem le_opp_neg : forall n, n <= 0 <-> 0 <= - n. +Proof. +intro n. set (k := 0) in |-* at 2. +setoid_replace k with (- k); unfold k; clear k. +apply le_opp. now rewrite uminus_0. +Qed. + +Theorem lt_opp_pos : forall n, 0 < n <-> - n < 0. +Proof. +intro n. set (k := 0) in |-* at 2. +setoid_replace k with (- k); unfold k; clear k. +apply lt_opp. now rewrite uminus_0. +Qed. + +Theorem le_opp_pos : forall n, 0 <= n <-> - n <= 0. +Proof. +intro n. set (k := 0) in |-* at 2. +setoid_replace k with (- k); unfold k; clear k. +apply le_opp. now rewrite uminus_0. +Qed. + +Theorem minus_lt_decr_r : forall n m p, n < m <-> p - m < p - n. +Proof. +intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_lt_compat_l. +apply lt_opp. +Qed. + +Theorem minus_le_nonincr_r : forall n m p, n <= m <-> p - m <= p - n. +Proof. +intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_le_compat_l. +apply le_opp. +Qed. + +Theorem minus_lt_incr_l : forall n m p, n < m <-> n - p < m - p. +Proof. +intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_lt_compat_r. +Qed. + +Theorem minus_le_nondecr_l : forall n m p, n <= m <-> n - p <= m - p. +Proof. +intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_le_compat_r. +Qed. + +Theorem lt_plus_swap : forall n m p, n + p < m <-> n < m - p. +Proof. +intros n m p. rewrite (minus_lt_incr_l (n + p) m p). +rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. +Qed. + +Theorem le_plus_swap : forall n m p, n + p <= m <-> n <= m - p. +Proof. +intros n m p. rewrite (minus_le_nondecr_l (n + p) m p). +rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. +Qed. + +End PlusOrderProperties. diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v new file mode 100644 index 0000000000..3f9c7c4ce6 --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZTimes.v @@ -0,0 +1,135 @@ +Require Import NumPrelude. +Require Import ZDomain. +Require Import ZAxioms. +Require Import ZPlus. + +Module Type TimesSignature. +Declare Module Export PlusModule : PlusSignature. + +Parameter Inline times : Z -> Z -> Z. + +Notation "x * y" := (times x y). + +Add Morphism times with signature E ==> E ==> E as times_wd. + +Axiom times_0 : forall n, n * 0 == 0. +Axiom times_S : forall n m, n * (S m) == n * m + n. + +(* Here recursion is done on the second argument to conform to the +usual definition of ordinal multiplication in set theory, which is not +commutative. It seems, however, that this definition in set theory is +unfortunate for two reasons. First, multiplication of two ordinals A +and B can be defined as (an order type of) the cartesian product B x A +(not A x B) ordered lexicographically. For example, omega * 2 = +2 x omega = {(0,0) < (0,1) < (0,2) < ... < (1,0) < (1,1) < (1,2) < ...}, +while 2 * omega = omega x 2 = {(0,0) < (0,1) < (1,0) < (1,1) < (2,0) < +(2,1) < ...} = omega. Secondly, the way the product 2 * 3 is said in +French (deux fois trois) and Russian (dvazhdy tri) implies 3 + 3, not +2 + 2 + 2. So it would possibly be more reasonable to define multiplication +(here as well as in set theory) by recursion on the first argument. *) + +End TimesSignature. + +Module TimesProperties (Export TimesModule : TimesSignature). + +Module Export PlusPropertiesModule := PlusProperties PlusModule. + +Theorem times_P : forall n m, n * (P m) == n * m - n. +Proof. +intros n m. rewrite_S_P m at 2. rewrite times_S. rewrite <- plus_minus_distr. +rewrite minus_diag. now rewrite plus_n_0. +Qed. + +Theorem times_0_n : forall n, 0 * n == 0. +Proof. +induct n. +now rewrite times_0. +intros n IH. rewrite times_S. rewrite IH; now rewrite plus_0. +intros n IH. rewrite times_P. rewrite IH; now rewrite minus_0. +Qed. + +Theorem times_Sn_m : forall n m, (S n) * m == n * m + m. +Proof. +induct m. +do 2 rewrite times_0. now rewrite plus_0. +intros m IH. do 2 rewrite times_S. rewrite IH. +do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity. +do 2 rewrite plus_n_Sm; now rewrite plus_comm. +intros m IH. do 2 rewrite times_P. rewrite IH. +rewrite <- plus_minus_swap. do 2 rewrite <- plus_minus_distr. +apply plus_wd. reflexivity. +rewrite minus_S. now rewrite minus_Pn_m. +Qed. + +Theorem times_Pn_m : forall n m, (P n) * m == n * m - m. +Proof. +intros n m. rewrite_S_P n at 2. rewrite times_Sn_m. +rewrite <- plus_minus_distr. rewrite minus_diag; now rewrite plus_n_0. +Qed. + +Theorem times_comm : forall n m, n * m == m * n. +Proof. +intros n m; induct n. +rewrite times_0_n; now rewrite times_0. +intros n IH. rewrite times_Sn_m; rewrite times_S; now rewrite IH. +intros n IH. rewrite times_Pn_m; rewrite times_P; now rewrite IH. +Qed. + +Theorem times_opp_r : forall n m, n * (- m) == - (n * m). +Proof. +intros n m; induct m. +rewrite uminus_0; rewrite times_0; now rewrite uminus_0. +intros m IH. rewrite uminus_S. rewrite times_P; rewrite times_S. rewrite IH. +rewrite <- plus_opp_minus; now rewrite opp_plus_distr. +intros m IH. rewrite uminus_P. rewrite times_P; rewrite times_S. rewrite IH. +now rewrite opp_minus_distr. +Qed. + +Theorem times_opp_l : forall n m, (- n) * m == - (n * m). +Proof. +intros n m; rewrite (times_comm (- n) m); rewrite (times_comm n m); +now rewrite times_opp_r. +Qed. + +Theorem times_opp_opp : forall n m, (- n) * (- m) == n * m. +Proof. +intros n m. rewrite times_opp_l. rewrite times_opp_r. now rewrite double_opp. +Qed. + +Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p. +Proof. +intros n m p; induct m. +rewrite times_0; now do 2 rewrite plus_0. +intros m IH. rewrite plus_S. do 2 rewrite times_S. rewrite IH. +do 2 rewrite <- plus_assoc; apply plus_wd; [reflexivity | apply plus_comm]. +intros m IH. rewrite plus_P. do 2 rewrite times_P. rewrite IH. +apply plus_minus_swap. +Qed. + +Theorem times_plus_distr_l : forall n m p, (n + m) * p == n * p + m * p. +Proof. +intros n m p; rewrite (times_comm (n + m) p); rewrite times_plus_distr_r; +rewrite (times_comm p n); now rewrite (times_comm p m). +Qed. + +Theorem times_minus_distr_r : forall n m p, n * (m - p) == n * m - n * p. +Proof. +intros n m p. +do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_r. now rewrite times_opp_r. +Qed. + +Theorem times_minus_distr_l : forall n m p, (n - m) * p == n * p - m * p. +Proof. +intros n m p. +do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_l. now rewrite times_opp_l. +Qed. + +Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p. +Proof. +intros n m p; induct p. +now do 3 rewrite times_0. +intros p IH. do 2 rewrite times_S. rewrite times_plus_distr_r. now rewrite IH. +intros p IH. do 2 rewrite times_P. rewrite times_minus_distr_r. now rewrite IH. +Qed. + +End TimesProperties. diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v new file mode 100644 index 0000000000..1f8b0a9478 --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v @@ -0,0 +1,92 @@ +Require Import ZPlus. +Require Import ZTimes. +Require Import ZOrder. +(* Warning: Trying to mask the absolute name "Plus"!!! *) +Require Import ZPlusOrder. + +Module TimesOrderProperties (Export TimesModule : TimesSignature) + (Export OrderModule : OrderSignature with + Module IntModule := TimesModule.PlusModule.IntModule). + +Module Export TimesPropertiesModule := TimesProperties TimesModule. +Module Export PlusOrderPropertiesModule := + PlusOrderProperties TimesModule.PlusModule OrderModule. + +Theorem mult_lt_compat_r : forall n m p, 0 < p -> n < m -> n * p < m * p. +Proof. +intros n m p; induct_ord p. +intros H _; false_hyp H lt_irr. +intros p H IH H1 H2. do 2 rewrite times_S. +apply -> lt_S in H1; le_elim H1. +apply plus_lt_compat. now apply IH. assumption. +rewrite <- H1. do 2 rewrite times_0; now do 2 rewrite plus_0. +intros p H IH H1 H2. apply lt_n_Pm in H1. apply -> le_gt in H. +false_hyp H1 H. +Qed. + +Theorem mult_lt_compat_l : forall n m p, 0 < p -> n < m -> p * n < p * m. +Proof. +intros n m p. rewrite (times_comm p n); rewrite (times_comm p m). +apply mult_lt_compat_r. +Qed. + +Theorem mult_lt_le_compat_r : forall n m p, 0 < p -> n <= m -> n * p <= m * p. +Proof. +intros n m p H1 H2; le_elim H2. +le_intro1; now apply mult_lt_compat_r. +rewrite H2. now le_intro2. +Qed. + +Theorem mult_lt_le_compat_l : forall n m p, 0 < p -> n <= m -> p * n <= p * m. +Proof. +intros n m p. rewrite (times_comm p n); rewrite (times_comm p m). +apply mult_lt_le_compat_r. +Qed. + +(* And so on *) + +Theorem mult_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m. +Proof. +intros n m; set (k := 0) in |-* at 3; +setoid_replace k with (n * 0); unfold k; clear k. +apply mult_lt_compat_l. now rewrite times_0. +Qed. + +Theorem mult_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0. +Proof. +intros n m; set (k := 0) in |-* at 3; +setoid_replace k with (n * 0); unfold k; clear k. +apply mult_lt_compat_l. now rewrite times_0. +Qed. +(* The same proof script as for mult_pos_pos! *) + +Theorem mult_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0. +Proof. +intros n m H1 H2; rewrite times_comm; now apply mult_pos_neg. +Qed. + +Theorem mult_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m. +Proof. +intros n m H1 H2. setoid_replace (n * m) with (- - (n * m)); +[| symmetry; apply double_opp]. +rewrite <- times_opp_l. rewrite <- times_opp_r. +apply -> lt_opp_neg in H1. apply -> lt_opp_neg in H2. +now apply mult_pos_pos. +Qed. + +(** With order, Z is an integral domain *) +Theorem mult_neq_0 : forall n m, n # 0 -> m # 0 -> n * m # 0. +Proof. +intros n m H1 H2. +destruct (lt_total n 0) as [H3 | [H3 | H3]]; +destruct (lt_total m 0) as [H4 | [H4 | H4]]. +apply neq_symm. apply lt_neq. now apply mult_neg_neg. +false_hyp H4 H2. +apply lt_neq; now apply mult_neg_pos. +false_hyp H3 H1. false_hyp H3 H1. false_hyp H3 H1. +apply lt_neq; now apply mult_pos_neg. +false_hyp H4 H2. +apply neq_symm. apply lt_neq. now apply mult_pos_pos. +Qed. + +End TimesOrderProperties. diff --git a/theories/Numbers/Integer/NatPairs/CommRefl.v b/theories/Numbers/Integer/NatPairs/CommRefl.v new file mode 100644 index 0000000000..673a1fe50d --- /dev/null +++ b/theories/Numbers/Integer/NatPairs/CommRefl.v @@ -0,0 +1,185 @@ +Require Import Arith. +Require Import List. +Require Import Setoid. + +Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin. + +Fixpoint flatten_aux (t fin:bin){struct t} : bin := + match t with + | node t1 t2 => flatten_aux t1 (flatten_aux t2 fin) + | x => node x fin + end. + +Fixpoint flatten (t:bin) : bin := + match t with + | node t1 t2 => flatten_aux t1 (flatten t2) + | x => x + end. + +Fixpoint nat_le_bool (n m:nat){struct m} : bool := + match n, m with + | O, _ => true + | S _, O => false + | S n, S m => nat_le_bool n m + end. + +Fixpoint insert_bin (n:nat)(t:bin){struct t} : bin := + match t with + | leaf m => match nat_le_bool n m with + | true => node (leaf n)(leaf m) + | false => node (leaf m)(leaf n) + end + | node (leaf m) t' => match nat_le_bool n m with + | true => node (leaf n) t + | false => + node (leaf m)(insert_bin n t') + end + | t => node (leaf n) t + end. + +Fixpoint sort_bin (t:bin) : bin := + match t with + | node (leaf n) t' => insert_bin n (sort_bin t') + | t => t + end. + +Section commut_eq. +Variable A : Set. +Variable E : relation A. +Variable f : A -> A -> A. + +Hypothesis E_equiv : equiv A E. +Hypothesis comm : forall x y : A, f x y = f y x. +Hypothesis assoc : forall x y z : A, f x (f y z) = f (f x y) z. + +Notation "x == y" := (E x y) (at level 70). + +Add Relation A E + reflexivity proved by (proj1 E_equiv) + symmetry proved by (proj2 (proj2 E_equiv)) + transitivity proved by (proj1 (proj2 E_equiv)) +as E_rel. + +Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A := + match t with + | node t1 t2 => f (bin_A l def t1)(bin_A l def t2) + | leaf n => nth n l def + end. + Theorem flatten_aux_valid_A : + forall (l:list A)(def:A)(t t':bin), + f (bin_A l def t)(bin_A l def t') == bin_A l def (flatten_aux t t'). +Proof. + intros l def t; elim t; simpl; auto. + intros t1 IHt1 t2 IHt2 t'. rewrite <- IHt1; rewrite <- IHt2. + symmetry; apply assoc. +Qed. + Theorem flatten_valid_A : + forall (l:list A)(def:A)(t:bin), + bin_A l def t == bin_A l def (flatten t). +Proof. + intros l def t; elim t; simpl; trivial. + intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid_A; rewrite <- IHt2. + trivial. +Qed. + +Theorem flatten_valid_A_2 : + forall (t t':bin)(l:list A)(def:A), + bin_A l def (flatten t) == bin_A l def (flatten t')-> + bin_A l def t == bin_A l def t'. +Proof. + intros t t' l def Heq. + rewrite (flatten_valid_A l def t); rewrite (flatten_valid_A l def t'). + trivial. +Qed. + +Theorem insert_is_f : forall (l:list A)(def:A)(n:nat)(t:bin), + bin_A l def (insert_bin n t) == + f (nth n l def) (bin_A l def t). +Proof. + intros l def n t; elim t. + intros t1; case t1. + intros t1' t1'' IHt1 t2 IHt2. + simpl. + auto. + intros n0 IHt1 t2 IHt2. + simpl. + case (nat_le_bool n n0). + simpl. + auto. + simpl. + rewrite IHt2. + repeat rewrite assoc; rewrite (comm (nth n l def)); auto. + simpl. + intros n0; case (nat_le_bool n n0); auto. + rewrite comm; auto. +Qed. + +Theorem sort_eq : forall (l:list A)(def:A)(t:bin), + bin_A l def (sort_bin t) == bin_A l def t. +Proof. + intros l def t; elim t. + intros t1 IHt1; case t1. + auto. + intros n t2 IHt2; simpl; rewrite insert_is_f. + rewrite IHt2; auto. + auto. +Qed. + + +Theorem sort_eq_2 : + forall (l:list A)(def:A)(t1 t2:bin), + bin_A l def (sort_bin t1) == bin_A l def (sort_bin t2)-> + bin_A l def t1 == bin_A l def t2. +Proof. + intros l def t1 t2. + rewrite <- (sort_eq l def t1); rewrite <- (sort_eq l def t2). + trivial. +Qed. + +End commut_eq. + + +Ltac term_list f l v := + match v with + | (f ?X1 ?X2) => + let l1 := term_list f l X2 in term_list f l1 X1 + | ?X1 => constr:(cons X1 l) + end. + +Ltac compute_rank l n v := + match l with + | (cons ?X1 ?X2) => + let tl := constr:X2 in + match constr:(X1 == v) with + | (?X1 == ?X1) => n + | _ => compute_rank tl (S n) v + end + end. + +Ltac model_aux l f v := + match v with + | (f ?X1 ?X2) => + let r1 := model_aux l f X1 with r2 := model_aux l f X2 in + constr:(node r1 r2) + | ?X1 => let n := compute_rank l 0 X1 in constr:(leaf n) + | _ => constr:(leaf 0) + end. + +Ltac comm_eq A f assoc_thm comm_thm := + match goal with + | [ |- (?X1 == ?X2 :>A) ] => + let l := term_list f (nil (A:=A)) X1 in + let term1 := model_aux l f X1 + with term2 := model_aux l f X2 in + (change (bin_A A f l X1 term1 == bin_A A f l X1 term2); + apply flatten_valid_A_2 with (1 := assoc_thm); + apply sort_eq_2 with (1 := comm_thm)(2 := assoc_thm); + auto) + end. + +(* +Theorem reflection_test4 : forall x y z:nat, x+(y+z) = (z+x)+y. +Proof. + intros x y z. comm_eq nat plus plus_assoc plus_comm. +Qed. +*)
\ No newline at end of file diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v new file mode 100644 index 0000000000..d2634970db --- /dev/null +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -0,0 +1,45 @@ +Require Import NDomain. +Require Import NAxioms. +Require Import NPlus. +Require Import NTimes. +Require Import NLt. +Require Import NPlusLt. +Require Import NTimesLt. + +Require Import ZDomain. +Require Import ZAxioms. +Require Import ZPlus. +Require Import ZTimes. +Require Import ZOrder. +Require Import ZPlusOrder. +Require Import ZTimesOrder. + +Module NatPairsDomain (Export PlusModule : NPlus.PlusSignature) <: + ZDomain.DomainSignature. + +Module Export PlusPropertiesModule := NPlus.PlusProperties PlusModule. + +Definition Z : Set := (N * N)%type. +Definition E (p1 p2 : Z) := (fst p1) + (snd p2) == (fst p2) + (snd p1). +Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)). + +Theorem E_equiv_e : forall x y : Z, E x y <-> e x y. +Proof. +intros x y; unfold E, e; apply E_equiv_e. +Qed. + +Theorem E_equiv : equiv Z E. +Proof. +split; [| split]; unfold reflexive, symmetric, transitive, E. +now intro x. +intros x y z H1 H2. +comm_eq N + + + +assert (H : ((fst x) + (snd y)) + ((fst y) + (snd z)) == + ((fst y) + (snd x)) + ((fst z) + (snd y))); [now apply plus_wd |]. +assert (H : (fst y) + (snd y) + (fst x) + (snd z) == + (fst y) + (snd y) + (snd x) + (fst z)). + + |