diff options
25 files changed, 4071 insertions, 1 deletions
@@ -875,7 +875,7 @@ SORTINGVO=\ theories/Sorting/Heap.vo theories/Sorting/Permutation.vo \ theories/Sorting/Sorting.vo theories/Sorting/PermutSetoid.vo \ theories/Sorting/PermutEq.vo - + BOOLVO=\ theories/Bool/Bool.vo theories/Bool/IfProp.vo \ theories/Bool/Zerob.vo theories/Bool/DecBool.vo \ @@ -1046,6 +1046,34 @@ REALSVO=$(REALSBASEVO) $(REALS_$(REALS)) ALLREALS=$(REALSBASEVO) $(REALS_all) +NUMBERSDIR=theories/Numbers +NATURALDIR=$(NUMBERSDIR)/Natural +NATAXIOMSDIR=$(NATURALDIR)/Axioms +NATURALAXIOMSVO=\ + $(NATAXIOMSDIR)/NAxioms.vo $(NATAXIOMSDIR)/NDepRec.vo\ + $(NATAXIOMSDIR)/NDomain.vo $(NATAXIOMSDIR)/NLt.vo\ + $(NATAXIOMSDIR)/NMiscFunct.vo $(NATAXIOMSDIR)/NIso.vo\ + $(NATAXIOMSDIR)/NOtherInd.vo $(NATAXIOMSDIR)/NPlusLt.vo\ + $(NATAXIOMSDIR)/NPlus.vo $(NATAXIOMSDIR)/NStrongRec.vo\ + $(NATAXIOMSDIR)/NTimesLt.vo $(NATAXIOMSDIR)/NTimes.vo + +NATURALPEANOVO=$(NATURALDIR)/Peano/NPeano.vo +NATURALBINARYVO=$(NATURALDIR)/Binary/NBinary.vo +NATURALVO=$(NATURALAXIOMSVO) $(NATURALPEANOVO) $(NATURALBINARYVO) + +INTEGERDIR=$(NUMBERSDIR)/Integer +INTAXIOMSDIR=$(INTEGERDIR)/Axioms +INTEGERAXIOMSVO=\ + $(INTAXIOMSDIR)/ZAxioms.vo $(INTAXIOMSDIR)/ZDomain.vo\ + $(INTAXIOMSDIR)/ZOrder.vo $(INTAXIOMSDIR)/ZPlusOrder.vo\ + $(INTAXIOMSDIR)/ZPlus.vo $(INTAXIOMSDIR)/ZTimesOrder.vo\ + $(INTAXIOMSDIR)/ZTimes.vo + +INTEGERNATPAIRSVO=$(INTEGERDIR)/NatPairs/ZNatPairs.vo +INTEGERVO=$(INTEGERAXIOMSVO) $(INTEGERNATPAIRSVO) + +NUMBERSVO=$(NATURALVO) $(INTEGERVO) + SETOIDSVO=theories/Setoids/Setoid.vo THEORIESVO =\ @@ -1079,6 +1107,11 @@ reals: $(REALSVO) allreals: $(ALLREALS) setoids: $(SETOIDSVO) sorting: $(SORTINGVO) +# numbers +natural: $(NATURALVO) +integer: $(INTEGERVO) +rational: $(RATIONALVO) +numbers: $(NUMBERSVO) noreal: logic arith bool zarith qarith lists sets fsets intmap relations \ wellfounded setoids sorting diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v new file mode 100644 index 000000000..4f0eab8e3 --- /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 000000000..00eab8842 --- /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 000000000..b1983d6f7 --- /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 000000000..1b5aa73fb --- /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 000000000..abaaa664f --- /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 000000000..3f9c7c4ce --- /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 000000000..1f8b0a947 --- /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 000000000..673a1fe50 --- /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 000000000..d2634970d --- /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)). + + diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v new file mode 100644 index 000000000..55f07eb89 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NAxioms.v @@ -0,0 +1,333 @@ +Require Export NDomain. + +(********************************************************************* +* Peano Axioms * +*********************************************************************) + +Module Type NatSignature. +Declare Module Export DomainModule : DomainSignature. + +Parameter Inline O : N. +Parameter Inline S : N -> N. + +Notation "0" := O. +Notation "1" := (S O). + +Add Morphism S with signature E ==> E as S_wd. + +(* It is natural to formulate induction for well-defined predicates +only because standard induction +forall P, P 0 -> (forall n, P n -> P (S n)) -> forall n, P n +does not hold in the setoid context (for example, there is no reason +for (P x) hold when x == 0 but x <> 0). However, it is possible to +formulate induction without mentioning well-defidedness (see OtherInd.v); +this formulation is equivalent. *) +Axiom induction : + forall P : N -> Prop, pred_wd E P -> + P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n. + +(* Why do we separate induction and recursion? + +(1) When induction and recursion are the same, they are dependent +(nondependent induction does not make sense). However, one must impose +conditions on the predicate, or codomain, that it respects the setoid +equality. For induction this means considering predicates P for which +forall n n', n == n' -> (P n <-> P n') holds. For recursion, where P : +nat -> Set, we cannot say (P n <-> P n'). It may make sense to require +forall n n', n == n' -> (P n = P n'). + +(2) Unlike induction, recursion requires that two equalities hold: +[recursion a f 0 == a] and [recursion a f (S n) == f n (recursion a f n)] +(or something like this). It may be difficult to state, let alone prove, +these equalities because the left- and the right-hand sides may have +different types (P t1) and (P t2) where t1 == t2 is provable but t1 and t2 +are not convertible into each other. Nevertheless, these equalities may +be proved using dependent equality (EqdepFacts) or JM equality (JMeq). +However, requiring this for any implementation of natural numbers seems +a little complex. It may make sense to devote a separate module to dependent +recursion (see DepRec.v). *) + +Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A. + +Implicit Arguments recursion [A]. + +(* Suppose the codomain A has a setoid equality relation EA. If A is a +function space C -> D, it makes sense to consider extensional +functional equality as EA. Indeed, suppose, for example, that we say +[Definition g (x : N) : C -> D := (recursion ... x ...)]. We would +like to show that the function g of two arguments is well-defined. +This requirement is the same as the requirement that the functions of +one argument (g x) and (g x') are extensionally equal whenever x == +x', i.e., + +forall x x' : N, x == x' -> eq_fun (g x) (g x'), + +which is the same as + +forall x x' : N, x == x' -> forall y y' : C, EC y y' -> ED (g x y) (g x' y') + +where EC and ED are setoid equalities on C and D, respectively. + +Now, if we consider EA to be extensional equality on the function +space, we cannot require that EA is reflexive. Indeed, reflexivity of +EA: + +forall f : C -> D, eq_fun f f + +or + +forall f : C -> D, forall x x', EC x x' -> ED (f x) (f x') + +means that every function f ; C -> D is well-defined, which is in +general false. We can expect that EA is symmetric and transitive, +i.e., that EA is a partial equivalence relation (PER). However, there +seems to be no need to require this in the following axioms. + +When we defined a function by recursion, the arguments of this +function may occur in the recursion's base case a, the counter x, or +the step function f. For example, in the following definition: + +Definition plus (x y : N) := recursion y (fun _ p => S p) x. + +one argument becomes the base case and the other becomes the counter. + +In the definitions of times: + +Definition times (x y : N) := recursion 0 (fun x p => plus y p) x. + +the argument y occurs in the step function. Thus it makes sense to +formulate an axiom saying that (recursion a f x) is equal to +(recursion a' f' x') whenever (EA a a'), x == x', and eq_fun2 f f'. We +need to vary all three arguments; for example, claiming that +(recursion a f x) equals (recursion a' f x') with the same f whenever +(EA a a') and x == x' is not enough to prove well-defidedness of +multiplication defined above. + +This leads to the axioms given below. There is a question if it is +possible to formulate simpler axioms that would imply this statement +for any implementation. Indeed, the proof seems to have to proceed by +straighforward induction on x. The difficulty is that we cannot prove +(EA (recursion a f x) (recursion a' f' x')) using the induction axioms +above because recursion is not declared to be a setoid morphism: +that's what we are proving! Therefore, this has to be proved by +induction inside each particular implementation. *) + +Axiom recursion_wd : forall (A : Set) (EA : relation A), + forall a a' : A, EA a a' -> + forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> + forall x x' : N, x == x' -> + EA (recursion a f x) (recursion a' f' x'). + +(* Can we instead declare recursion as a morphism? It does not seem +so. For this, we need to register the relation EA, and for this we +need to declare it as a variable in a section. But information about +morhisms is lost when sections are closed. *) + +(* When the function recursion is polymorphic on the codomain A, there +seems no other option than to return the given base case a when the +counter is 0. Therefore, we can formulate the following axioms with +Leibniz equality. *) + +Axiom recursion_0 : + forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a. + +Axiom recursion_S : + forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). + +(* It may be possible to formulate recursion_0 and recursion_S as follows: +Axiom recursion_0 : + forall (a : A) (f : N -> A -> A), + EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a. + +Axiom recursion_S : + forall (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). + +Then it is possible to prove recursion_wd (see IotherInd.v). This +raises some questions: + +(1) Can the axioms recursion_wd, recursion_0 and recursion_S (both +variants) proved for all reasonable implementations? + +(2) Can these axioms be proved without assuming that EA is symmetric +and transitive? In OtherInd.v, recursion_wd can be proved from +recursion_0 and recursion_S by assuming symmetry and transitivity. + +(2) Which variant requires proving less for each implementation? Can +it be that proving all three axioms about recursion has some common +parts which have to be repeated? *) + +Implicit Arguments recursion_wd [A]. +Implicit Arguments recursion_0 [A]. +Implicit Arguments recursion_S [A]. + +End NatSignature. + +Module NatProperties (Export NatModule : NatSignature). + +Module Export DomainPropertiesModule := DomainProperties DomainModule. + +(* This tactic applies the induction axioms and solves the resulting +goal "pred_wd E P" *) +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 | |]. + +Definition if_zero (A : Set) (a b : A) (n : N) : A := + recursion a (fun _ _ => b) n. + +Add Morphism if_zero with signature LE_Set ==> LE_Set ==> E ==> LE_Set as if_zero_wd. +Proof. +unfold LE_Set. +intros; unfold if_zero; now apply recursion_wd with (EA := (@eq A)); +[| unfold eq_fun2; now intros |]. +Qed. + +Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a. +Proof. +unfold if_zero; intros; now rewrite recursion_0. +Qed. + +Theorem if_zero_S : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b. +Proof. +intros; unfold if_zero. +now rewrite (recursion_S (@eq A)); [| | unfold fun2_wd; now intros]. +Qed. + +Implicit Arguments if_zero [A]. + +(* To prove this statement, we need to provably different terms, +e.g., true and false *) +Theorem S_0 : forall n, ~ S n == 0. +Proof. +intros n H. +assert (true = false); [| discriminate]. +replace true with (if_zero false true (S n)) by apply if_zero_S. +pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0. +change (LE_Set bool (if_zero false true (S n)) (if_zero false true 0)). +rewrite H. unfold LE_Set. reflexivity. +Qed. + +Definition pred (n : N) : N := recursion 0 (fun m _ => m) n. + +Add Morphism pred with signature E ==> E as pred_wd. +Proof. +intros; unfold pred. +now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |]. +Qed. + +Theorem pred_0 : pred 0 == 0. +Proof. +unfold pred; now rewrite recursion_0. +Qed. + +Theorem pred_S : forall n, pred (S n) == n. +Proof. +intro n; unfold pred; now rewrite (recursion_S E); [| unfold fun2_wd; now intros |]. +Qed. + +Theorem S_inj : forall m n, S m == S n -> m == n. +Proof. +intros m n H. +setoid_replace m with (pred (S m)) by (symmetry; apply pred_S). +setoid_replace n with (pred (S n)) by (symmetry; apply pred_S). +now apply pred_wd. +Qed. + +Theorem not_eq_S : forall n m, n # m -> S n # S m. +Proof. +intros n m H1 H2. apply S_inj in H2. now apply H1. +Qed. + +Theorem not_eq_Sn_n : forall n, S n # n. +Proof. +induct n. +apply S_0. +intros n IH H. apply S_inj in H. now apply IH. +Qed. + +Theorem not_all_eq_0 : ~ forall n, n == 0. +Proof. +intro H; apply (S_0 0). apply H. +Qed. + +Theorem not_0_implies_S : forall n, n # 0 <-> exists m, n == S m. +Proof. +intro n; split. +induct n; [intro H; now elim H | intros n _ _; now exists n]. +intro H; destruct H as [m H]; rewrite H; apply S_0. +Qed. + +Theorem nondep_induction : + forall P : N -> Prop, NumPrelude.pred_wd E P -> + P 0 -> (forall n, P (S n)) -> forall n, P n. +Proof. +intros; apply induction; auto. +Qed. + +Ltac nondep_induct n := + try intros until n; + pattern n; apply nondep_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 O_or_S : forall n, n == 0 \/ exists m, n == S m. +Proof. +nondep_induct n; [now left | intros n; right; now exists n]. +Qed. + +(* The following is useful for reasoning about, e.g., Fibonacci numbers *) +Section DoubleInduction. +Variable P : N -> Prop. +Hypothesis P_correct : NumPrelude.pred_wd E P. + +Add Morphism P with signature E ==> iff as P_morphism. +Proof. +exact P_correct. +Qed. + +Theorem double_induction : + P 0 -> P 1 -> + (forall n, P n -> P (S n) -> P (S (S n))) -> forall n, P n. +Proof. +intros until 3. +assert (D : forall n, P n /\ P (S n)); [ |intro n; exact (proj1 (D n))]. +induct n; [ | intros n [IH1 IH2]]; auto. +Qed. + +End DoubleInduction. + +(* The following is useful for reasoning about, e.g., Ackermann function *) +Section TwoDimensionalInduction. +Variable R : N -> N -> Prop. +Hypothesis R_correct : rel_wd E R. + +Add Morphism R with signature E ==> E ==> iff as R_morphism. +Proof. +exact R_correct. +Qed. + +Theorem two_dim_induction : + R 0 0 -> + (forall n m, R n m -> R n (S m)) -> + (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m. +Proof. +intros H1 H2 H3. induct n. +induct m. +exact H1. exact (H2 0). +intros n IH. induct m. +now apply H3. exact (H2 (S n)). +Qed. + +End TwoDimensionalInduction. + +End NatProperties. diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v new file mode 100644 index 000000000..7da105f5b --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NDepRec.v @@ -0,0 +1,71 @@ +Require Import NAxioms. +Require Import NPlus. +Require Import NTimes. + +(* Here we allow dependent recursion only for domains with Libniz +equality. The reason is that, if the domain is A : nat -> Set, then (A +n) must coincide with (A n') whenever n == n'. However, it is possible +to try to use arbitrary domain and require that n == n' -> A n = A n'. *) + +Module Type DepRecSignature. +Declare Module DomainModule : DomainEqSignature. +Declare Module Export NatModule : NatSignature with + Module DomainModule := DomainModule. +(* Instead of these two lines, I would like to say +Declare Module Export Nat : NatSignature with Module Domain : NatDomainEq. *) + +Parameter Inline dep_recursion : + forall A : N -> Set, A 0 -> (forall n, A n -> A (S n)) -> forall n, A n. + +Axiom dep_recursion_0 : + forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)), + dep_recursion A a f 0 = a. + +Axiom dep_recursion_S : + forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)) (n : N), + dep_recursion A a f (S n) = f n (dep_recursion A a f n). + +End DepRecSignature. + +Module DepRecTimesProperties (Export DepRecModule : DepRecSignature) + (Export TimesModule : TimesSignature + with Module PlusModule.NatModule := DepRecModule.NatModule). + +Module Export TimesPropertiesModule := TimesProperties TimesModule. + +Theorem not_0_implies_S_dep : forall n, n # O -> {m : N | n == S m}. +Proof. +intro n; pattern n; apply dep_recursion; clear n; +[intro H; now elim H | intros n _ _; now exists n]. +Qed. + +Theorem plus_eq_1_dep : + forall m n : N, m + n == 1 -> {m == 0 /\ n == 1} + {m == 1 /\ n == 0}. +(* Why do we write == here instead of just = ? "x == y" is a notation +for (E x y) declared (along with E := (@eq N)) in NatDomainEq signature. If we +want to rewrite, e.g., plus_comm, which contains E, in a formula with +=, setoid rewrite signals an error, because E is not declared a +morphism w.r.t. = even though E is defined to be =. Thus, we need to +use E instead of = in our formulas. *) +Proof. +intros m n; pattern m; apply dep_recursion; clear m. +intro H. +rewrite plus_0_n in H. left; now split. +intros m IH H. rewrite plus_Sn_m in H. apply S_inj in H. +apply plus_eq_0 in H. destruct H as [H1 H2]. +right; now split; [rewrite H1 |]. +Qed. + +Theorem times_eq_0_dep : + forall n m, n * m == 0 -> {n == 0} + {m == 0}. +Proof. +intros n m; pattern n; apply dep_recursion; pattern m; apply dep_recursion; +clear n m. +intros; left; reflexivity. +intros; left; reflexivity. +intros; right; reflexivity. +intros n _ m _ H. +rewrite times_Sn_m in H; rewrite plus_Sn_m in H; now apply S_0 in H. +Qed. + +End DepRecTimesProperties. diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v new file mode 100644 index 000000000..ebc692d5b --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NDomain.v @@ -0,0 +1,77 @@ +Require Export NumPrelude. + +Module Type DomainSignature. + +Parameter Inline N : Set. +Parameter Inline E : relation N. +Parameter Inline e : N -> N -> bool. + +(* Theoretically, we it is enough to have decidable equality e only. +If necessary, E could be defined using a coercion. However, after we +prove properties of natural numbers, we would like them to eventually +use ordinary Leibniz equality. E.g., we would like the commutativity +theorem, instantiated to nat, to say forall x y : nat, x + y = y + x, +and not forall x y : nat, eq_true (e (x + y) (y + x)) + +In fact, if we wanted to have decidable equality e only, we would have +some trouble doing rewriting. If there is a hypothesis H : e x y, this +means more precisely that H : eq_true (e x y). Such hypothesis is not +recognized as equality by setoid rewrite because it does not have the +form R x y where R is an identifier. *) + +Axiom E_equiv_e : forall x y : N, E x y <-> e x y. +Axiom E_equiv : equiv N E. + +Add Relation N 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. + +(* Now we give DomainSignature, but with E being Leibniz equality. If +an implementation uses this signature, then more facts may be proved +about it. *) +Module Type DomainEqSignature. + +Parameter Inline N : Set. +Definition E := (@eq N). +Parameter Inline e : N -> N -> bool. + +Axiom E_equiv_e : forall x y : N, E x y <-> e x y. +Definition E_equiv : equiv N E := eq_equiv N. + +Add Relation N 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) -> False) (at level 70). +(* Why do we need a new notation for Leibniz equality? See DepRec.v *) + +End DomainEqSignature. + +Module DomainProperties (Export DomainModule : DomainSignature). +(* It also accepts module of type NatDomainEq *) + +(* The following easily follows from transitivity of e and E, but +we need to deal with the coercion *) +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. + +End DomainProperties. diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v new file mode 100644 index 000000000..41d7d6145 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NIso.v @@ -0,0 +1,115 @@ +Require Import NAxioms. + +Module Homomorphism (Nat1 Nat2 : NatSignature). + +Module Import DomainProperties1 := DomainProperties Nat1.DomainModule. +Module Import DomainProperties2 := DomainProperties Nat2.DomainModule. +(* This registers Nat1.Domain.E and Nat2.Domain.E as setoid relations *) + +Notation Local N1 := Nat1.DomainModule.N. +Notation Local N2 := Nat2.DomainModule.N. +Notation Local E1 := Nat1.DomainModule.E. +Notation Local E2 := Nat2.DomainModule.E. +Notation Local O1 := Nat1.O. +Notation Local O2 := Nat2.O. +Notation Local S1 := Nat1.S. +Notation Local S2 := Nat2.S. +Notation Local "x == y" := (Nat2.DomainModule.E x y) (at level 70). + +Definition homomorphism (f : N1 -> N2) : Prop := + f O1 == O2 /\ forall x : N1, f (S1 x) == S2 (f x). + +Definition natural_isomorphism : N1 -> N2 := + Nat1.recursion O2 (fun (x : N1) (p : N2) => S2 p). + +Add Morphism natural_isomorphism +with signature E1 ==> E2 +as natural_isomorphism_wd. +Proof. +unfold natural_isomorphism. +intros x y Exy. +apply Nat1.recursion_wd with (EA := E2). +reflexivity. +unfold eq_fun2. intros _ _ _ y' y'' H. now apply Nat2.S_wd. +assumption. +Qed. + +Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2. +Proof. +unfold natural_isomorphism; now rewrite Nat1.recursion_0. +Qed. + +Theorem natural_isomorphism_S : + forall x : N1, natural_isomorphism (S1 x) == S2 (natural_isomorphism x). +Proof. +unfold natural_isomorphism; +intro x; now rewrite (Nat1.recursion_S Nat2.DomainModule.E); +[| unfold fun2_wd; intros; apply Nat2.S_wd |]. +Qed. + +Theorem iso_hom : homomorphism natural_isomorphism. +Proof. +unfold homomorphism, natural_isomorphism; split; +[exact natural_isomorphism_0 | exact natural_isomorphism_S]. +Qed. + +End Homomorphism. + +Module Inverse (Nat1 Nat2 : NatSignature). + +Module Import NatProperties1 := NatProperties Nat1. +(* This makes the tactic induct available. Since it is taken from +NatProperties Nat1, it refers to Nat1.induction. *) + +Module Hom12 := Homomorphism Nat1 Nat2. +Module Hom21 := Homomorphism Nat2 Nat1. + +Notation Local N1 := Nat1.DomainModule.N. +Notation Local N2 := Nat2.DomainModule.N. +Notation Local h12 := Hom12.natural_isomorphism. +Notation Local h21 := Hom21.natural_isomorphism. + +Notation Local "x == y" := (Nat1.DomainModule.E x y) (at level 70). + +Lemma iso_inverse : + forall x : N1, h21 (h12 x) == x. +Proof. +induct x. +now rewrite Hom12.natural_isomorphism_0; rewrite Hom21.natural_isomorphism_0. +intros x IH. +rewrite Hom12.natural_isomorphism_S; rewrite Hom21.natural_isomorphism_S; +now rewrite IH. +Qed. + +End Inverse. + +Module Isomorphism (Nat1 Nat2 : NatSignature). + +Module Hom12 := Homomorphism Nat1 Nat2. +Module Hom21 := Homomorphism Nat2 Nat1. + +Module Inverse121 := Inverse Nat1 Nat2. +Module Inverse212 := Inverse Nat2 Nat1. + +Notation Local N1 := Nat1.DomainModule.N. +Notation Local N2 := Nat2.DomainModule.N. +Notation Local E1 := Nat1.DomainModule.E. +Notation Local E2 := Nat2.DomainModule.E. +Notation Local h12 := Hom12.natural_isomorphism. +Notation Local h21 := Hom21.natural_isomorphism. + +Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop := + Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\ + forall x : N1, E1 (f2 (f1 x)) x /\ + forall y : N2, E2 (f1 (f2 y)) y. + +Theorem iso_iso : isomorphism h12 h21. +Proof. +unfold isomorphism. +split. apply Hom12.iso_hom. +split. apply Hom21.iso_hom. +split. apply Inverse121.iso_inverse. +apply Inverse212.iso_inverse. +Qed. + +End Isomorphism. diff --git a/theories/Numbers/Natural/Axioms/NLt.v b/theories/Numbers/Natural/Axioms/NLt.v new file mode 100644 index 000000000..210786bba --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NLt.v @@ -0,0 +1,168 @@ +Require Export NAxioms. + +Module Type LtSignature. +Declare Module Export NatModule : NatSignature. + +Parameter Inline lt : N -> N -> bool. + +Notation "x < y" := (lt x y). + +Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. + +Axiom lt_0 : forall x, ~ (x < 0). +Axiom lt_S : forall x y, x < S y <-> x < y \/ x == y. +End LtSignature. + +Module LtProperties (Export LtModule : LtSignature). + +Module Export NatPropertiesModule := NatProperties NatModule. + +Theorem lt_n_Sn : forall n, n < S n. +Proof. +intro n. apply <- lt_S. now right. +Qed. + +Theorem lt_closed_S : forall n m, n < m -> n < S m. +Proof. +intros. apply <- lt_S. now left. +Qed. + +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; elim H. +intro H1; apply IH in H1; now apply lt_closed_S. +intro H1; rewrite <- H1. +apply lt_closed_S; apply lt_n_Sn. +Qed. + +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_transitive : 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; elim H1. +intro H; apply IH; [assumption | apply lt_S_lt; assumption]. +intro H; rewrite H; apply lt_S_lt; assumption. +Qed. + +Theorem lt_positive : forall n m, n < m -> 0 < m. +Proof. +intros n m; induct n. +trivial. +intros x IH H. +apply lt_transitive with (m := S x); [apply lt_0_Sn | apply H]. +Qed. + +Theorem S_respects_lt : forall n m, S n < S m <-> n < m. +Proof. +intros n m; split. +intro H; apply -> lt_S in H; elim H. +intros; apply lt_S_lt; assumption. +intro H1; rewrite <- H1; apply lt_n_Sn. +induct m. +intro H; absurd_hyp H; [ apply lt_0 | assumption]. +intros x IH H. +apply -> lt_S in H; elim H; intro H1. +apply lt_transitive with (m := S x). +apply IH; assumption. +apply lt_n_Sn. +rewrite H1; apply lt_n_Sn. +Qed. + +Theorem lt_n_m : forall n m, n < m <-> S n < m \/ S n == m. +Proof. +intros n m; nondep_induct m. +split; intro H; [false_hyp H lt_0 | +destruct H as [H | H]; [false_hyp H lt_0 | false_hyp H S_0]]. +intros m; split; intro H. +apply -> lt_S in H. destruct H; [left; now apply <- S_respects_lt | right; now apply S_wd]. +destruct H; [apply lt_transitive with (m := S n); [apply lt_n_Sn | assumption] | +apply S_inj in H; rewrite H; apply lt_n_Sn]. +Qed. + +Theorem lt_irreflexive : forall n, ~ (n < n). +Proof. +induct n. +apply lt_0. +intro x; unfold not; intros H1 H2; apply H1; now apply -> S_respects_lt. +Qed. + +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 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 lt_asymmetric : forall n m, ~ (n < m /\ m < n). +Proof. +unfold not; intros n m [H1 H2]. +now apply (lt_transitive n m n) in H1; [false_hyp H1 lt_irreflexive|]. +Qed. + +Theorem eq_0_or_lt_0: forall n, 0 == n \/ 0 < n. +Proof. +induct n; [now left | intros x; right; apply lt_0_Sn]. +Qed. + +Theorem lt_options : forall n m, n < m -> S n < m \/ S n == m. +Proof. +intros n m; induct m. +intro H; false_hyp H lt_0. +intros x IH H. +apply -> lt_S in H; elim H; intro H1. +apply IH in H1; elim H1; intro H2. +left; apply lt_transitive with (m := x); [assumption | apply lt_n_Sn]. +rewrite H2; left; apply lt_n_Sn. +right; rewrite H1; reflexivity. +Qed. + +Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n. +Proof. +intros n m; induct n. +assert (H : 0 == m \/ 0 < m); [apply eq_0_or_lt_0 | tauto]. +intros n IH. destruct IH as [H | H]. +assert (S n < m \/ S n == m); [now apply lt_options | tauto]. +destruct H as [H1 | H1]. +right; right; rewrite H1; apply lt_n_Sn. +right; right; apply lt_transitive with (m := n); [assumption | apply lt_n_Sn]. +Qed. + +Theorem lt_dichotomy : forall n m, n < m \/ ~ n < m. +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_irreflexive. +right; intro; apply (lt_asymmetric n m); split; assumption. +Qed. + +Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n. +Proof. +intros n m H; destruct (lt_trichotomy n m) as [A | A]; [now left |]. +now destruct A as [A | A]; [elim H | right]. +Qed. + +Theorem lt_exists_pred : forall n, 0 < n -> exists m, n == S m. +Proof. +induct n. +intro H; false_hyp H lt_0. +intros n IH H; now exists n. +Qed. + +End LtProperties. diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v new file mode 100644 index 000000000..5f9b7b1d1 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v @@ -0,0 +1,373 @@ +Require Import Bool. (* To get the negb function *) +Require Import NAxioms. +Require Import NStrongRec. +Require Import NPlus. +Require Import NTimes. +Require Import NLt. +Require Import NPlusLt. +Require Import NTimesLt. + +Module MiscFunctFunctor (NatMod : NatSignature). +Module Export NatPropertiesModule := NatProperties NatMod. +Module Export StrongRecPropertiesModule := StrongRecProperties NatMod. + +(*****************************************************) +(** 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_S : forall x y, plus (S x) y == S (plus x y). +Proof. +intros x y; unfold plus. +now rewrite (recursion_S E); [|apply plus_step_wd|]. +Qed. + +(*****************************************************) +(** Multiplication *) + +Definition times (x y : N) := recursion 0 (fun x p => plus y p) x. + +Lemma times_step_wd : forall y, fun2_wd E E E (fun x p => plus y p). +Proof. +unfold fun2_wd. intros y _ _ _ p p' Ezz'. +now apply plus_wd. +Qed. + +Lemma times_step_equal : + forall y y', y == y' -> eq_fun2 E E E (fun x p => plus y p) (fun x p => plus y' p). +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 : forall y, times 0 y == 0. +Proof. +intro y. unfold times. now rewrite recursion_0. +Qed. + +Theorem times_S : forall x y, times (S x) y == plus y (times x y). +Proof. +intros x y; unfold times. +now rewrite (recursion_S 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. + +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_Set. +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. *) + +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_S (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_S. +Qed. + +Lemma lt_0_Sn : forall n, lt 0 (S n). +Proof. +intro n; rewrite lt_base_eq; now rewrite if_zero_S. +Qed. + +Lemma lt_Sn_Sm : forall n m, lt (S n) (S m) <-> lt n m. +Proof. +intros n m. +rewrite lt_step_eq. rewrite (recursion_S eq_bool). +reflexivity. +now unfold eq_bool. +unfold fun2_wd; intros; now apply lt_wd. +Qed. + +Theorem lt_S : forall m n, lt m (S n) <-> lt m n \/ m == n. +Proof. +induct m. +nondep_induct n; +[split; intro; [now right | apply lt_0_1] | +intro n; split; intro; [left |]; apply lt_0_Sn]. +intros n IH. nondep_induct n0. +split. +intro. assert (H1 : lt n 0); [now apply -> lt_Sn_Sm | false_hyp H1 lt_0]. +intro H; destruct H as [H | H]. +false_hyp H lt_0. false_hyp H S_0. +intro m. pose proof (IH m) as H; clear IH. +assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_Sn_Sm |]. +assert (lt (S n) (S m) <-> lt n m); [apply lt_Sn_Sm |]. +assert (S n == S m <-> n == m); [split; [ apply S_inj | apply S_wd]|]. +tauto. +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_S : forall x : N, even (S x) = negb (even x). +Proof. +unfold even. +intro x; rewrite (recursion_S (@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 S_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 DefaultPlusModule <: PlusSignature. + +Module NatModule := NatMod. +(* If we used the name NatModule instead of NatMod then this would +produce many warnings like "Trying to mask the absolute name +NatModule", "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_n : forall n, plus 0 n == n. +Proof. +exact plus_0. +Qed. + +Theorem plus_Sn_m : forall n m, plus (S n) m == S (plus n m). +Proof. +exact plus_S. +Qed. + +End DefaultPlusModule. + +Module DefaultTimesModule <: TimesSignature. +Module Export PlusModule := DefaultPlusModule. + +Definition times := times. + +Add Morphism times with signature E ==> E ==> E as times_wd. +Proof. +exact times_wd. +Qed. + +Theorem times_0_n : forall n, times 0 n == 0. +Proof. +exact times_0. +Qed. + +Theorem times_Sn_m : forall n m, times (S n) m == plus m (times n m). +Proof. +exact times_S. +Qed. + +End DefaultTimesModule. + +Module DefaultLtModule <: LtSignature. +Module NatModule := NatMod. + +Definition lt := lt. + +Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. +Proof. +exact lt_wd. +Qed. + +Theorem lt_0 : forall x, ~ (lt x 0). +Proof. +exact lt_0. +Qed. + +Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x == y. +Proof. +exact lt_S. +Qed. + +End DefaultLtModule. + +Module Export DefaultPlusProperties := PlusProperties DefaultPlusModule. +Module Export DefaultTimesProperties := TimesProperties DefaultTimesModule. +Module Export DefaultLtProperties := LtProperties DefaultLtModule. +Module Export DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule. +Module Export DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule. + +(*Opaque MiscFunctFunctor.plus. +Check plus_comm. (* This produces the following *) +Eval compute in (forall n m : PlusModule.NatModule.DomainModule.N, plus n m == plus m n).*) + +End MiscFunctFunctor. diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Axioms/NOtherInd.v new file mode 100644 index 000000000..e37669bad --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NOtherInd.v @@ -0,0 +1,159 @@ +Require Export NDomain. +Declare Module Export DomainModule : DomainSignature. + +Parameter O : N. +Parameter S : N -> N. + +Notation "0" := O. + +Definition induction := +forall P : N -> Prop, pred_wd E P -> + P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n. + +Definition other_induction := +forall P : N -> Prop, + (forall n : N, n == 0 -> P n) -> + (forall n : N, P n -> forall m : N, m == S n -> P m) -> + forall n : N, P n. + +Theorem other_ind_implies_ind : other_induction -> induction. +Proof. +unfold induction, other_induction; intros OI P P_wd Base Step. +apply OI; unfold pred_wd in P_wd. +intros; now apply -> (P_wd 0). +intros n Pn m EmSn; now apply -> (P_wd (S n)); [apply Step|]. +Qed. + +Theorem ind_implies_other_ind : induction -> other_induction. +Proof. +intros I P Base Step. +set (Q := fun n => forall m, m == n -> P m). +cut (forall n, Q n). +unfold Q; intros H n; now apply (H n). +apply I. +unfold pred_wd, Q. intros x y Exy. +split; intros H m Em; apply H; [now rewrite Exy | now rewrite <- Exy]. +exact Base. +intros n Qn m EmSn; now apply Step with (n := n); [apply Qn |]. +Qed. + +(* This theorem is not really needed. It shows that if we have +other_induction and we proved the base case and the induction step, we +can in fact show that the predicate in question is well-defined, and +therefore we can turn this other induction into the standard one. *) +Theorem other_ind_implies_pred_wd : +other_induction -> + forall P : N -> Prop, + (forall n : N, n == 0 -> P n) -> + (forall n : N, P n -> forall m : N, m == S n -> P m) -> + pred_wd E P. +Proof. +intros OI P Base Step; unfold pred_wd. +intros x; pattern x; apply OI; clear x. +(* Base case *) +intros x H1 y H2. +assert (y == 0); [rewrite <- H2; now rewrite H1|]. +assert (P x); [now apply Base|]. +assert (P y); [now apply Base|]. +split; now intro. +(* Step *) +intros x IH z H y H1. +rewrite H in H1. symmetry in H1. +split; (intro H2; eapply Step; [|apply H || apply H1]); now apply OI. +Qed. + +Section Recursion. + +Variable A : Set. +Variable EA : relation A. +Hypothesis EA_symm : symmetric A EA. +Hypothesis EA_trans : transitive A EA. + +Add Relation A EA + symmetry proved by EA_symm + transitivity proved by EA_trans +as EA_rel. + +Lemma EA_neighbor : forall a a' : A, EA a a' -> EA a a. +Proof. +intros a a' EAaa'. +apply EA_trans with (y := a'); [assumption | apply EA_symm; assumption]. +Qed. + +Parameter recursion : A -> (N -> A -> A) -> N -> A. + +Axiom recursion_0 : + forall (a : A) (f : N -> A -> A), + EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a. + +Axiom recursion_S : + forall (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). + +Theorem recursion_wd : induction -> + forall a a' : A, EA a a' -> + forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' -> + forall x x' : N, x == x' -> + EA (recursion a f x) (recursion a' f' x'). +Proof. +intros I a a' Eaa' f f' f_wd f'_wd Eff'. +apply ind_implies_other_ind in I. +intro x; pattern x; apply I; clear x. +intros x Ex0 x' Exx'. +rewrite Ex0 in Exx'; symmetry in Exx'. +(* apply recursion_0 in Ex0. produces +Anomaly: type_of: this is not a well-typed term. Please report. *) +assert (EA (recursion a f x) a). +apply recursion_0. now apply EA_neighbor with (a' := a'). assumption. +assert (EA a' (recursion a' f' x')). +apply EA_symm. apply recursion_0. now apply EA_neighbor with (a' := a). assumption. +apply EA_trans with (y := a). assumption. +now apply EA_trans with (y := a'). +intros x IH y H y' H1. +rewrite H in H1; symmetry in H1. +assert (EA (recursion a f y) (f x (recursion a f x))). +apply recursion_S. now apply EA_neighbor with (a' := a'). +assumption. now symmetry. +assert (EA (f' x (recursion a' f' x)) (recursion a' f' y')). +symmetry; apply recursion_S. now apply EA_neighbor with (a' := a). assumption. +now symmetry. +assert (EA (f x (recursion a f x)) (f' x (recursion a' f' x))). +apply Eff'. reflexivity. apply IH. reflexivity. +apply EA_trans with (y := (f x (recursion a f x))). assumption. +apply EA_trans with (y := (f' x (recursion a' f' x))). assumption. +assumption. +Qed. + +Axiom recursion_0' : + forall (a : A) (f : N -> A -> A), + forall x : N, x == 0 -> recursion a f x = a. + +Axiom recursion_S' : + forall (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). + +Theorem recursion_wd' : other_induction -> + forall a a' : A, EA a a -> EA a' a' -> EA a a' -> + forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' -> + forall x x' : N, x == x' -> + EA (recursion a f x) (recursion a' f' x'). +Proof. +intros I a a' a_wd a'_wd Eaa' f f' f_wd f'_wd Eff'. +intro x; pattern x; apply I; clear x. +intros x Ex0 x' Exx'. rewrite Ex0 in Exx'. symmetry in Exx'. +replace (recursion a f x) with a. replace (recursion a' f' x') with a'. +assumption. symmetry; now apply recursion_0'. symmetry; now apply recursion_0'. +intros x IH y EySx y' Eyy'. rewrite EySx in Eyy'. symmetry in Eyy'. +apply EA_trans with (y := (f x (recursion a f x))). now apply recursion_S'. +apply EA_trans with (y := (f' x (recursion a' f' x))). +apply Eff'. reflexivity. now apply IH. +symmetry; now apply recursion_S'. +Qed. + + + +End Recursion. + +Implicit Arguments recursion [A]. diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v new file mode 100644 index 000000000..29b65e3f4 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NPlus.v @@ -0,0 +1,184 @@ +Require Export NAxioms. + +Module Type PlusSignature. +Declare Module Export NatModule : NatSignature. + +Parameter Inline plus : N -> N -> N. + +Notation "x + y" := (plus x y). + +Add Morphism plus with signature E ==> E ==> E as plus_wd. + +Axiom plus_0_n : forall n, 0 + n == n. +Axiom plus_Sn_m : forall n m, (S n) + m == S (n + m). + +End PlusSignature. + +Module PlusProperties (Export PlusModule : PlusSignature). + +Module Export NatPropertiesModule := NatProperties NatModule. + +Lemma plus_0_r : forall n, n + 0 == n. +Proof. +induct n. +now rewrite plus_0_n. +intros x IH. +rewrite plus_Sn_m. +now rewrite IH. +Qed. + +Lemma plus_0_l : forall n, 0 + n == n. +Proof. +intro n. +now rewrite plus_0_n. +Qed. + +Lemma plus_n_Sm : forall n m, n + S m == S (n + m). +Proof. +intros n m; generalize n; clear n. induct n. +now repeat rewrite plus_0_n. +intros x IH. +repeat rewrite plus_Sn_m; now rewrite IH. +Qed. + +Lemma plus_Sn_m : forall n m, S n + m == S (n + m). +Proof. +intros. +now rewrite plus_Sn_m. +Qed. + +Lemma plus_comm : forall n m, n + m == m + n. +Proof. +intros n m; generalize n; clear n. induct n. +rewrite plus_0_l; now rewrite plus_0_r. +intros x IH. +rewrite plus_Sn_m; rewrite plus_n_Sm; now rewrite IH. +Qed. + +Lemma plus_assoc : forall n m p, n + (m + p) == (n + m) + p. +Proof. +intros n m p; generalize n; clear n. induct n. +now repeat rewrite plus_0_l. +intros x IH. +repeat rewrite plus_Sn_m; now rewrite IH. +Qed. + +Lemma plus_1_l : forall n, 1 + n == S n. +Proof. +intro n; rewrite plus_Sn_m; now rewrite plus_0_n. +Qed. + +Lemma plus_1_r : forall n, n + 1 == S n. +Proof. +intro n; rewrite plus_comm; apply plus_1_l. +Qed. + +Lemma plus_cancel_l : forall n m p, p + n == p + m -> n == m. +Proof. +induct p. +do 2 rewrite plus_0_n; trivial. +intros p IH H. do 2 rewrite plus_Sn_m in H. apply S_inj in H. now apply IH. +Qed. + +Lemma plus_cancel_r : forall n m p, n + p == m + p -> n == m. +Proof. +intros n m p. +rewrite plus_comm. +set (k := p + n); rewrite plus_comm; unfold k. +apply plus_cancel_l. +Qed. + +Lemma plus_eq_0 : forall n m, n + m == 0 -> n == 0 /\ m == 0. +Proof. +intros n m; induct n. +rewrite plus_0_n; now split. +intros n IH H. rewrite plus_Sn_m in H. +absurd_hyp H; [|assumption]. unfold not; apply S_0. +Qed. + +Lemma succ_plus_discr : forall n m, m # S (n + m). +Proof. +intro n; induct m. +intro H. apply S_0 with (n := (n + 0)). now apply (proj2 (proj2 E_equiv)). (* symmetry *) +intros m IH H. apply S_inj in H. rewrite plus_n_Sm in H. +unfold not in IH; now apply IH. +Qed. + +Lemma n_SSn : forall n, n # S (S n). +Proof. +intro n. pose proof (succ_plus_discr 1 n) as H. +rewrite plus_Sn_m in H; now rewrite plus_0_n in H. +Qed. + +Lemma n_SSSn : forall n, n # S (S (S n)). +Proof. +intro n. pose proof (succ_plus_discr (S (S 0)) n) as H. +do 2 rewrite plus_Sn_m in H. now rewrite plus_0_n in H. +Qed. + +Lemma n_SSSSn : forall n, n # S (S (S (S n))). +Proof. +intro n. pose proof (succ_plus_discr (S (S (S 0))) n) as H. +do 3 rewrite plus_Sn_m in H. now rewrite plus_0_n in H. +Qed. + +(* The following section is devoted to defining a function that, given +two numbers whose some equals 1, decides which number equals 1. The +main property of the function is also proved .*) + +(* First prove a theorem with ordinary disjunction *) +Theorem plus_eq_1 : + forall m n, m + n == 1 -> (m == 0 /\ n == 1) \/ (m == 1 /\ n == 0). +induct m. +intros n H; rewrite plus_0_n in H; left; now split. +intros n IH m H; rewrite plus_Sn_m in H; apply S_inj in H; +apply plus_eq_0 in H; destruct H as [H1 H2]; +now right; split; [apply S_wd |]. +Qed. + +Definition plus_eq_1_dec (m n : N) : bool := recursion true (fun _ _ => false) m. + +Lemma plus_eq_1_dec_step_wd : fun2_wd E eq_bool eq_bool (fun _ _ => false). +Proof. +unfold fun2_wd; intros. unfold eq_bool. reflexivity. +Qed. + +Add Morphism plus_eq_1_dec with signature E ==> E ==> eq_bool as plus_eq_1_dec_wd. +Proof. +unfold fun2_wd, plus_eq_1_dec. +intros x x' Exx' y y' Eyy'. +apply recursion_wd with (EA := eq_bool). +unfold eq_bool; reflexivity. +unfold eq_fun2; unfold eq_bool; reflexivity. +assumption. +Qed. + +Lemma plus_eq_1_dec_0 : forall n, plus_eq_1_dec 0 n = true. +Proof. +intro n. unfold plus_eq_1_dec. +now apply recursion_0. +Qed. + +Lemma plus_eq_1_dec_S : forall m n, plus_eq_1_dec (S n) m = false. +Proof. +intros n m. unfold plus_eq_1_dec. +now rewrite (recursion_S eq_bool); +[| unfold eq_bool | apply plus_eq_1_dec_step_wd]. +Qed. + +Theorem plus_eq_1_dec_correct : + forall m n, m + n == 1 -> + (plus_eq_1_dec m n = true -> m == 0 /\ n == 1) /\ + (plus_eq_1_dec m n = false -> m == 1 /\ n == 0). +Proof. +intros m n; induct m. +intro H. rewrite plus_0_l in H. +rewrite plus_eq_1_dec_0. +split; [intros; now split | intro H1; discriminate H1]. +intros m _ H. rewrite plus_eq_1_dec_S. +split; [intro H1; discriminate | intros _ ]. +rewrite plus_Sn_m in H. apply S_inj in H. +apply plus_eq_0 in H; split; [apply S_wd | ]; tauto. +Qed. + +End PlusProperties. diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusLt.v new file mode 100644 index 000000000..ac322a8f2 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NPlusLt.v @@ -0,0 +1,50 @@ +Require Export NPlus. +Require Export NLt. + +Module PlusLtProperties (Export PlusModule : PlusSignature) + (Export LtModule : LtSignature with + Module NatModule := PlusModule.NatModule). + +Module Export PlusPropertiesModule := PlusProperties PlusModule. +Module Export LtPropertiesModule := LtProperties LtModule. + +(* Print All locks up here !!! *) +Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. +Proof. +intros n m p; induct p. +now rewrite plus_0_r. +intros x IH H. +rewrite plus_n_Sm. apply lt_closed_S. apply IH; apply H. +Qed. + +Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m. +Proof. +intros n m p H; induct p. +do 2 rewrite plus_0_n; assumption. +intros x IH. do 2 rewrite plus_Sn_m. now apply <- S_respects_lt. +Qed. + +Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. +Proof. +intros n m p H; rewrite plus_comm. +set (k := p + n); rewrite plus_comm; unfold k; clear k. +now apply plus_lt_compat_l. +Qed. + +Lemma 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_transitive with (m := m + p); +[now apply plus_lt_compat_r | now apply plus_lt_compat_l]. +Qed. + +Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m. +Proof. +intros n m p; induct p. +now do 2 rewrite plus_0_n. +intros x IH H. +do 2 rewrite plus_Sn_m in H. +apply IH; now apply -> S_respects_lt. +Qed. + +End PlusLtProperties. diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v new file mode 100644 index 000000000..a97dca9a5 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NStrongRec.v @@ -0,0 +1,67 @@ +Require Import NAxioms. + +Module StrongRecProperties (Export NatModule : NatSignature). +Module Export DomainPropertiesModule := DomainProperties NatModule.DomainModule. + +Section StrongRecursion. + +Variable A : Set. +Variable EA : relation A. + +Hypothesis EA_equiv : equiv A EA. + +Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (x : N) : A := +(recursion (fun _ : N => a) + (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)) + (S x)) x. + +Lemma strong_rec_step_wd : forall f : N -> (N -> A) -> A, +fun2_wd E (eq_fun E EA) EA f -> + fun2_wd E (eq_fun E EA) (eq_fun E EA) + (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)). +Proof. +unfold fun2_wd; intros f f_wd. +intros x x' Exx'. unfold eq_fun. intros g g' Egg' y y' Eyy'. +assert (H : e y x = e y' x'). now apply e_wd. rewrite H. +destruct (e y' x'); simpl. +now apply f_wd. now apply Egg'. +Qed. + +Theorem strong_rec_wd : +forall a a', EA a a' -> + forall f f', eq_fun2 E (eq_fun E EA) EA f f' -> + forall x x', x == x' -> + EA (strong_rec a f x) (strong_rec a' f' x'). +Proof. +intros a a' Eaa' f f' Eff' x x' Exx'. +assert (H : eq_fun E EA + (recursion (fun _ : N => a) + (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)) + (S x)) + (recursion (fun _ : N => a') + (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f' x p) else (p y)) + (S x'))). +apply recursion_wd with (EA := eq_fun E EA). +unfold eq_fun; now intros. +unfold eq_fun2. intros y y' Eyy' p p' Epp'. unfold eq_fun. intros z z' Ezz'. +assert (H: e z y = e z' y'); [now apply e_wd|]. +rewrite <- H. destruct (e z y); [now apply Eff' | now apply Epp']. +now rewrite Exx'. +unfold strong_rec. +now apply H. +Qed. + +(* To do: +Definition step_good (g : N -> (N -> A) -> A) := + forall (x : N) (h1 h2 : N -> A), + (forall y : N, y < x -> EA (h1 y) (h2 y)) -> EA (g x h1) (g x h2). + +Theorem strong_recursion_fixpoint : forall a g, step_good g -> + let f x := (strong_rec a g x) in forall x, EA (f x) (g x f). +*) + +End StrongRecursion. + +Implicit Arguments strong_rec [A]. + +End StrongRecProperties. diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v new file mode 100644 index 000000000..a47070083 --- /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. diff --git a/theories/Numbers/Natural/Axioms/NTimesLt.v b/theories/Numbers/Natural/Axioms/NTimesLt.v new file mode 100644 index 000000000..e67b5bb2a --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NTimesLt.v @@ -0,0 +1,64 @@ +Require Export NLt. +Require Export NTimes. +Require Export NPlusLt. + +Module TimesLtProperties (Export TimesModule : TimesSignature) + (Export LtModule : LtSignature with + Module NatModule := TimesModule.PlusModule.NatModule). + +Module Export TimesPropertiesModule := TimesProperties TimesModule. +Module Export LtPropertiesModule := LtProperties LtModule. +Module Export PlusLtPropertiesModule := PlusLtProperties TimesModule.PlusModule LtModule. + +Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. +Proof. +intros n m p; induct n. +now do 2 rewrite mult_1_l. +intros x IH H. +rewrite times_Sn_m. +set (k := S x * m); rewrite times_Sn_m; unfold k; clear k. +apply plus_lt_compat; [assumption | apply IH; assumption]. +Qed. + +Lemma mult_S_lt_compat_r : forall n m p, m < p -> m * (S n) < p * (S n). +Proof. +intros n m p H. +set (k := (p * (S n))); rewrite mult_comm; unfold k; clear k. +set (k := ((S n) * m)); rewrite mult_comm; unfold k; clear k. +now apply mult_S_lt_compat_l. +Qed. + +Lemma mult_lt_compat_l : forall m n p, n < m -> 0 < p -> p * n < p * m. +Proof. +intros n m p H1 H2. +apply (lt_exists_pred p) in H2. +destruct H2 as [q H]. repeat rewrite H. +now apply mult_S_lt_compat_l. +Qed. + +Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. +Proof. +intros n m p H1 H2. +apply (lt_exists_pred p) in H2. +destruct H2 as [q H]. repeat rewrite H. +now apply mult_S_lt_compat_r. +Qed. + +Lemma mult_positive : forall n m, 0 < n -> 0 < m -> 0 < n * m. +Proof. +intros n m H1 H2. +rewrite <- (times_0_n m); now apply mult_lt_compat_r. +Qed. + +Lemma mult_lt_compat : forall n m p q, n < m -> p < q -> n * p < m * q. +Proof. +intros n m p q; induct n. +intros; rewrite times_0_n; apply mult_positive; +[assumption | apply lt_positive with (n := p); assumption]. +intros x IH H1 H2. +apply lt_transitive with (m := ((S x) * q)). +now apply mult_S_lt_compat_l; assumption. +now apply mult_lt_compat_r; [| apply lt_positive with (n := p)]. +Qed. + +End TimesLtProperties. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v new file mode 100644 index 000000000..47b39bfeb --- /dev/null +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -0,0 +1,221 @@ +Require Import NArith. +Require Import Ndec. + +Require Import NDepRec. +Require Import NAxioms. +Require Import NPlus. +Require Import NTimes. +Require Import NLt. +Require Import NPlusLt. +Require Import NTimesLt. +Require Import NMiscFunct. + +Open Scope N_scope. + +Module BinaryDomain <: DomainEqSignature. + +Definition N := N. +Definition E := (@eq N). +Definition e := Neqb. + +Theorem E_equiv_e : forall x y : N, E x y <-> e x y. +Proof. +unfold E, e; intros x y; split; intro H; +[rewrite H; now rewrite Neqb_correct | +apply Neqb_complete; now inversion H]. +Qed. + +Definition E_equiv : equiv N E := eq_equiv N. + +Add Relation N E + reflexivity proved by (proj1 E_equiv) + symmetry proved by (proj2 (proj2 E_equiv)) + transitivity proved by (proj1 (proj2 E_equiv)) +as E_rel. + +End BinaryDomain. + +Module BinaryNat <: NatSignature. + +Module Export DomainModule := BinaryDomain. + +Definition O := N0. +Definition S := Nsucc. + +Add Morphism S with signature E ==> E as S_wd. +Proof. +congruence. +Qed. + +Theorem induction : + forall P : N -> Prop, pred_wd E P -> + P 0 -> (forall n, P n -> P (S n)) -> forall n, P n. +Proof. +intros P P_wd; apply Nind. +Qed. + +Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) := + Nrec (fun _ => A) a f n. +Implicit Arguments recursion [A]. + +Theorem recursion_wd : +forall (A : Set) (EA : relation A), + forall a a' : A, EA a a' -> + forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> + forall x x' : N, x = x' -> + EA (recursion a f x) (recursion a' f' x'). +Proof. +unfold fun2_wd, E, eq_fun2. +intros A EA a a' Eaa' f f' Eff'. +intro x; pattern x; apply Nind. +intros x' H; now rewrite <- H. +clear x. +intros x IH x' H; rewrite <- H. +unfold recursion, Nrec in *; do 2 rewrite Nrect_step. +now apply Eff'; [| apply IH]. +Qed. + +Theorem recursion_0 : + forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a. +Proof. +intros A a f; unfold recursion; unfold Nrec; now rewrite Nrect_base. +Qed. + +Theorem recursion_S : + forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). +Proof. +unfold E, recursion, Nrec, fun2_wd; intros A EA a f EAaa f_wd n; pattern n; apply Nind. +rewrite Nrect_step; rewrite Nrect_base; now apply f_wd. +clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|]. +now rewrite Nrect_step. +Qed. + +End BinaryNat. + +Module BinaryDepRec <: DepRecSignature. +Module Export DomainModule := BinaryDomain. +Module Export NatModule := BinaryNat. + +Definition dep_recursion := Nrec. + +Theorem dep_recursion_0 : + forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)), + dep_recursion A a f 0 = a. +Proof. +intros A a f; unfold dep_recursion; unfold Nrec; now rewrite Nrect_base. +Qed. + +Theorem dep_recursion_S : + forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)) (n : N), + dep_recursion A a f (S n) = f n (dep_recursion A a f n). +Proof. +intros A a f n; unfold dep_recursion; unfold Nrec; now rewrite Nrect_step. +Qed. + +End BinaryDepRec. + +Module BinaryPlus <: PlusSignature. + +Module Export NatModule := BinaryNat. + +Definition plus := Nplus. + +Add Morphism plus with signature E ==> E ==> E as plus_wd. +Proof. +unfold E; congruence. +Qed. + +Theorem plus_0_n : forall n, 0 + n = n. +Proof. +exact Nplus_0_l. +Qed. + +Theorem plus_Sn_m : forall n m, (S n) + m = S (n + m). +Proof. +exact Nplus_succ. +Qed. + +End BinaryPlus. + +Module BinaryTimes <: TimesSignature. +Module Export PlusModule := BinaryPlus. + +Definition times := Nmult. + +Add Morphism times with signature E ==> E ==> E as times_wd. +Proof. +unfold E; congruence. +Qed. + +Theorem times_0_n : forall n, 0 * n = 0. +Proof. +exact Nmult_0_l. +Qed. + +Theorem times_Sn_m : forall n m, (S n) * m = m + n * m. +Proof. +exact Nmult_Sn_m. +Qed. + +End BinaryTimes. + +Module BinaryLt <: LtSignature. +Module Export NatModule := BinaryNat. + +Definition lt (m n : N) := less_than (Ncompare m n). + +Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. +Proof. +unfold E; congruence. +Qed. + +Theorem lt_0 : forall x, ~ (lt x 0). +Proof. +unfold lt; destruct x as [|x]; simpl; now intro. +Qed. + +Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x = y. +Proof. +intros x y. +assert (H1 : lt x (S y) <-> Ncompare x (S y) = Lt); +[unfold lt, less_than; destruct (x ?= S y); simpl; split; now intro |]. +assert (H2 : lt x y <-> Ncompare x y = Lt); +[unfold lt, less_than; destruct (x ?= y); simpl; split; now intro |]. +pose proof (Ncompare_n_Sm x y) as H. tauto. +Qed. + +End BinaryLt. + +Module Export BinaryPlusProperties := PlusProperties BinaryPlus. +Module Export BinaryTimesProperties := TimesProperties BinaryTimes. +Module Export BinaryDepRecTimesProperties := + DepRecTimesProperties BinaryDepRec BinaryTimes. +Module Export BinaryLtProperties := LtProperties BinaryLt. +Module Export BinaryPlusLtProperties := PlusLtProperties BinaryPlus BinaryLt. +Module Export BinaryTimesLtProperties := TimesLtProperties BinaryTimes BinaryLt. + +Module Export BinaryRecEx := MiscFunctFunctor BinaryNat. +(* Time Eval compute in (log 100000). *) (* 98 sec *) + +Fixpoint binposlog (p : positive) : N := +match p with +| xH => 0 +| xO p' => Nsucc (binposlog p') +| xI p' => Nsucc (binposlog p') +end. + +Definition binlog (n : N) : N := +match n with +| 0 => 0 +| Npos p => binposlog p +end. + +(* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *) + + +(*Check nat_total_order : forall n m : N, (n = m -> False) -> lt n m \/ lt m n. +Check mult_positive : forall n m : N, lt 0 n -> lt 0 m -> lt 0 (n * m).*) + +Close Scope N_scope. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v new file mode 100644 index 000000000..403521e7c --- /dev/null +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -0,0 +1,221 @@ +Require Import NDepRec. +Require Import NPlus. +Require Import NTimes. +Require Import NLt. +Require Import NPlusLt. +Require Import NTimesLt. +Require Import NMiscFunct. + +Module PeanoDomain <: DomainEqSignature. + +Definition N := nat. +Definition E := (@eq nat). +Definition e := eq_nat_bool. + +Theorem E_equiv_e : forall x y : N, E x y <-> e x y. +Proof. +unfold E, e; intros x y; split; intro H; +[rewrite H; apply eq_nat_bool_refl | +now apply eq_nat_bool_implies_eq]. +Qed. + +Definition E_equiv : equiv N E := eq_equiv N. + +Add Relation N E + reflexivity proved by (proj1 E_equiv) + symmetry proved by (proj2 (proj2 E_equiv)) + transitivity proved by (proj1 (proj2 E_equiv)) +as E_rel. + +End PeanoDomain. + +Module PeanoNat <: NatSignature. + +Module Export DomainModule := PeanoDomain. + +Definition O := 0. +Definition S := S. + +Add Morphism S with signature E ==> E as S_wd. +Proof. +congruence. +Qed. + +Theorem induction : + forall P : nat -> Prop, pred_wd (@eq nat) P -> + P 0 -> (forall n, P n -> P (S n)) -> forall n, P n. +Proof. +intros P W Base Step n; elim n; assumption. +Qed. + +Definition recursion := fun A : Set => nat_rec (fun _ => A). +Implicit Arguments recursion [A]. + +Theorem recursion_wd : +forall (A : Set) (EA : relation A), + forall a a' : A, EA a a' -> + forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> + forall x x' : N, x = x' -> + EA (recursion a f x) (recursion a' f' x'). +Proof. +unfold fun2_wd, E. +intros A EA a a' Eaa' f f' Eff'. +induction x as [| n IH]; intros x' H; rewrite <- H; simpl. +assumption. +apply Eff'; [reflexivity | now apply IH]. +Qed. + +Theorem recursion_0 : + forall (A : Set) (a : A) (f : N -> A -> A), recursion a f O = a. +Proof. +reflexivity. +Qed. + +Theorem recursion_S : +forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). +Proof. +intros A EA a f EAaa f_wd. unfold fun2_wd, E in *. +induction n; simpl; now apply f_wd. +Qed. + +End PeanoNat. + +Module PeanoDepRec <: DepRecSignature. + +Module Export DomainModule := PeanoDomain. +Module Export NatModule <: NatSignature := PeanoNat. + +Definition dep_recursion := nat_rec. + +Theorem dep_recursion_0 : + forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)), + dep_recursion A a f 0 = a. +Proof. +reflexivity. +Qed. + +Theorem dep_recursion_S : + forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)) (n : N), + dep_recursion A a f (S n) = f n (dep_recursion A a f n). +Proof. +reflexivity. +Qed. + +End PeanoDepRec. + +Module PeanoPlus <: PlusSignature. + +Module Export NatModule := PeanoNat. + +Definition plus := plus. + +Add Morphism plus with signature E ==> E ==> E as plus_wd. +Proof. +unfold E; congruence. +Qed. + +Theorem plus_0_n : forall n, 0 + n = n. +Proof. +reflexivity. +Qed. + +Theorem plus_Sn_m : forall n m, (S n) + m = S (n + m). +Proof. +reflexivity. +Qed. + +End PeanoPlus. + +Module PeanoTimes <: TimesSignature. +Module Export PlusModule := PeanoPlus. + +Definition times := mult. + +Add Morphism times with signature E ==> E ==> E as times_wd. +Proof. +unfold E; congruence. +Qed. + +Theorem times_0_n : forall n, 0 * n = 0. +Proof. +auto. +Qed. + +Theorem times_Sn_m : forall n m, (S n) * m = m + n * m. +Proof. +auto. +Qed. + +End PeanoTimes. + +(* Some checks: +Check times_eq_1 : forall n m, n * m = 1 -> n = 1 /\ m = 1. +Eval compute in times_eq_0_dec 0 5. +Eval compute in times_eq_0_dec 5 0. *) + +Module PeanoLt <: LtSignature. +Module Export NatModule := PeanoNat. + +Definition lt := lt_bool. + +Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. +Proof. +unfold E, eq_bool; congruence. +Qed. + +Theorem lt_0 : forall x, ~ (lt x 0). +Proof. +exact lt_bool_0. +Qed. + +Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x = y. +Proof. +exact lt_bool_S. +Qed. + +End PeanoLt. + +(* Obtaining properties for +, *, <, and their combinations *) + +Module Export PeanoPlusProperties := PlusProperties PeanoPlus. +Module Export PeanoTimesProperties := TimesProperties PeanoTimes. +Module Export PeanoLtProperties := LtProperties PeanoLt. +Module Export PeanoPlusLtProperties := PlusLtProperties PeanoPlus PeanoLt. +Module Export PeanoTimesLtProperties := TimesLtProperties PeanoTimes PeanoLt. +Module Export PeanoDepRecTimesProperties := + DepRecTimesProperties PeanoDepRec PeanoTimes. + +Module MiscFunctModule := MiscFunctFunctor PeanoNat. + +(*Eval compute in MiscFunctModule.lt 6 5.*) + +(*Set Printing All.*) +(*Check plus_comm. +Goal forall x y : nat, x + y = y + x. +intros x y. +rewrite plus_comm. reflexivity. (* does now work -- but the next line does *) +apply plus_comm.*) + +(*Opaque plus. +Eval compute in (forall n m : N, E m (PeanoPlus.Nat.S (PeanoPlus.plus n m)) -> False). + +Eval compute in (plus_eq_1_dec 1 1). +Opaque plus_eq_1_dec. +Check plus_eq_1. +Eval compute in (forall m n : N, + E (PeanoPlus.plus m n) (PeanoPlus.Nat.S PeanoPlus.Nat.O) -> + (plus_eq_1_dec m n = true -> + E m PeanoPlus.Nat.O /\ E n (PeanoPlus.Nat.S PeanoPlus.Nat.O)) /\ + (plus_eq_1_dec m n = false -> + E m (PeanoPlus.Nat.S PeanoPlus.Nat.O) /\ E n PeanoPlus.Nat.O)).*) + +(*Require Import rec_ex. + +Module Import PeanoRecursionExamples := RecursionExamples PeanoNat. + +Eval compute in mult 3 15. +Eval compute in e 100 100. +Eval compute in log 8. +Eval compute in half 0.*) diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v new file mode 100644 index 000000000..2fe547681 --- /dev/null +++ b/theories/Numbers/NumPrelude.v @@ -0,0 +1,324 @@ +Require Export Setoid. + +(* +Contents: +- Coercion from bool to Prop +- An attempt to extend setoid rewrite to formulas with quantifiers +- Extentional properties of predicates, relations and functions + (well-definedness and equality) +- Relations on cartesian product +- Some boolean functions on nat +- Miscellaneous +*) + +(** Coercion from bool to Prop *) + +Definition eq_bool := (@eq bool). + +Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. +Coercion eq_true : bool >-> Sortclass. + +Theorem neg_eq_true : forall x : bool, ~ x -> x = false. +Proof. +intros x H; destruct x; [elim (H is_eq_true) | reflexivity]. +Qed. + +(** An attempt to extend setoid rewrite to formulas with quantifiers *) + +(* The following algorithm was explained to me by Bruno Barras. + +In the future, we need to prove that some predicates are +well-defined w.r.t. a setoid relation, i.e., we need to prove theorems +of the form "forall x y, x == y -> (P x <-> P y)". The reason is that it +makes sense to do induction only on predicates that satisfy this +property. Ideally, such goal should be proved by saying "intros x y H; +rewrite H; reflexivity". + +Now, such predicates P may contain quantifiers besides setoid +morphisms. However, the tactic "rewrite" (which in this case stands +for "setoid_rewrite") currently cannot handle universal quantifiers as +well as lambda abstractions, which are part of the existential +quantifier notation (recall that "exists x, P" stands for "ex (fun x +=> p)"). + +Therefore, to prove that P x <-> P y, we proceed as follows. Suppose +that P x is C[forall z, Q[x,z]] where C is a context, i.e., a term +with a hole. We assume that the hole of C does not occur inside +another quantifier, i.e., that forall z, Q[x,z] is a top-level +quantifier in P. The notation Q[x,z] means that the term Q contains +free occurrences of variables x and z. We prove that forall z, Q[x,z] +<-> forall z, Q[y,z]. To do this, we show that forall z, Q[x,z] <-> +Q[y,z]. After performing "intro z", this goal is handled recursively, +until no more quantifiers are left in Q. + +After we obtain the goal + +H : x == y +H1 : forall z, Q[x,z] <-> forall z, Q[y,z] +================================= +C[forall z, Q[x,z]] <-> C[forall z, Q[y,z]] + +we say "rewrite H1". Repeating this for other quantifier subformulas +in P, we make them all identical in P x and P y. After that, saying +"rewrite H" solves the goal. + +To implement this algorithm, we need the following theorems: + +Theorem forall_morphism : + forall (A : Set) (P Q : A -> Prop), + (forall x : A, P x <-> Q x) -> ((forall x : A, P x) <-> (forall x : A, Q x)). + +Theorem exists_morphism : + forall (A : Set) (P Q : A -> Prop), + (forall x : A, P x <-> Q x) -> (ex P <-> ex Q) + +Below, we obtain them by registering the universal and existential +quantifiers as setoid morphisms, though they can be proved without any +reference to setoids. Ideally, registering quantifiers as morphisms +should take care of setoid rewriting in the presence of quantifiers, +but as described above, this is currently not so, and we have to +handle quantifiers manually. + +The job of deriving P x <-> P y from x == y is done by the tactic +qmorphism x y below. *) + +Section Quantifiers. + +Variable A : Set. + +Definition predicate := A -> Prop. + +Definition equiv_predicate : relation predicate := + fun (P1 P2 : predicate) => forall x : A, P1 x <-> P2 x. + +Theorem equiv_predicate_refl : reflexive predicate equiv_predicate. +Proof. +unfold reflexive, equiv_predicate. reflexivity. +Qed. + +Theorem equiv_predicate_symm : symmetric predicate equiv_predicate. +Proof. +firstorder. +Qed. + +Theorem equiv_predicate_trans : transitive predicate equiv_predicate. +Proof. +firstorder. +Qed. + +Add Relation predicate equiv_predicate + reflexivity proved by equiv_predicate_refl + symmetry proved by equiv_predicate_symm + transitivity proved by equiv_predicate_trans +as equiv_predicate_rel. + +Add Morphism (@ex A) + with signature equiv_predicate ==> iff + as exists_morphism. +Proof. +firstorder. +Qed. + +Add Morphism (fun P : predicate => forall x : A, P x) + with signature equiv_predicate ==> iff + as forall_morphism. +Proof. +firstorder. +Qed. + +End Quantifiers. + +(* replace x by y in t *) +Ltac repl x y t := +match t with +| context C [x] => let t' := (context C [y]) in repl x y t' +| _ => t +end. + +Ltac qmorphism x y := +lazymatch goal with +| |- ?P <-> ?P => reflexivity +| |- context [ex ?P] => + match P with + | context [x] => + let P' := repl x y P in + setoid_replace (ex P) with (ex P') using relation iff; + [qmorphism x y | + apply exists_morphism; unfold equiv_predicate; intros; qmorphism x y] + end +| |- context [forall z, @?P z] => + match P with + | context [x] => + let P' := repl x y P in + setoid_replace (forall z, P z) with (forall z, P' z) using relation iff; + [qmorphism x y | + apply forall_morphism; unfold equiv_predicate; intros; qmorphism x y] + end +| _ => setoid_replace x with y; [reflexivity | assumption] +end. + +(** Extentional properties of predicates, relations and functions *) + +Section ExtensionalProperties. + +Variables A B C : Set. +Variable EA : relation A. +Variable EB : relation B. +Variable EC : relation C. + +(* "wd" stands for "well-defined" *) + +Definition fun_wd (f : A -> B) := forall x y : A, EA x y -> EB (f x) (f y). + +Definition fun2_wd (f : A -> B -> C) := + forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f x' y'). + +Definition pred_wd (P : predicate A) := + forall x y, EA x y -> (P x <-> P y). + +Definition rel_wd (R : relation A) := + forall x x', EA x x' -> forall y y', EA y y' -> (R x y <-> R x' y'). + +Definition eq_fun : relation (A -> B) := + fun f f' => forall x x' : A, EA x x' -> EB (f x) (f' x'). + +(* Note that reflexivity of eq_fun means that every function +is well-defined w.r.t. EA and EB, i.e., +forall x x' : A, EA x x' -> EB (f x) (f x') *) + +Definition eq_fun2 (f f' : A -> B -> C) := + forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f' x' y'). + +End ExtensionalProperties. + +Implicit Arguments fun_wd [A B]. +Implicit Arguments fun2_wd [A B C]. +Implicit Arguments eq_fun [A B]. +Implicit Arguments eq_fun2 [A B C]. +Implicit Arguments pred_wd [A]. +Implicit Arguments rel_wd [A]. + +(** Relations on cartesian product. Used in MiscFunct for defining +functions whose domain is a product of sets by primitive recursion *) + +Section RelationOnProduct. + +Variables A B : Set. +Variable EA : relation A. +Variable EB : relation B. + +Hypothesis EA_equiv : equiv A EA. +Hypothesis EB_equiv : equiv B EB. + +Definition prod_rel : relation (A * B) := + fun p1 p2 => EA (fst p1) (fst p2) /\ EB (snd p1) (snd p2). + +Lemma prod_rel_refl : reflexive (A * B) prod_rel. +Proof. +unfold reflexive, prod_rel. +destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl. +Qed. + +Lemma prod_rel_symm : symmetric (A * B) prod_rel. +Proof. +unfold symmetric, prod_rel. +destruct x; destruct y; +split; [apply (proj2 (proj2 EA_equiv)) | apply (proj2 (proj2 EB_equiv))]; simpl in *; tauto. +Qed. + +Lemma prod_rel_trans : transitive (A * B) prod_rel. +Proof. +unfold transitive, prod_rel. +destruct x; destruct y; destruct z; simpl. +intros; split; [apply (proj1 (proj2 EA_equiv)) with (y := a0) | +apply (proj1 (proj2 EB_equiv)) with (y := b0)]; tauto. +Qed. + +Theorem prod_rel_equiv : equiv (A * B) prod_rel. +Proof. +unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_symm]]. +Qed. + +End RelationOnProduct. + +Implicit Arguments prod_rel [A B]. +Implicit Arguments prod_rel_equiv [A B]. + +(** Some boolean functions on nat. Their analogs are available in the +standard library; however, we provide simpler definitions. Used in +defining implementations of natural numbers. *) + +Fixpoint eq_nat_bool (x y : nat) {struct x} : bool := +match x, y with +| 0, 0 => true +| S x', S y' => eq_nat_bool x' y' +| _, _ => false +end. + +Theorem eq_nat_bool_implies_eq : forall x y, eq_nat_bool x y -> x = y. +Proof. +induction x; destruct y; simpl; intro H; try (reflexivity || inversion H). +apply IHx in H; now rewrite H. +Qed. + +Theorem eq_nat_bool_refl : forall x, eq_nat_bool x x. +Proof. +induction x; now simpl. +Qed. + +(* The boolean less function can be defined as +fun n m => proj1_sig (nat_lt_ge_bool n m) +using the standard library. +However, this definitionseems too complex. First, there are many +functions involved: nat_lt_ge_bool is defined (in Coq.Arith.Bool_nat) +using bool_of_sumbool and +lt_ge_dec : forall x y : nat, {x < y} + {x >= y}, +where the latter function is defined using sumbool_not and +le_lt_dec : forall n m : nat, {n <= m} + {m < n}. +Second, this definition is not the most efficient, especially since +le_lt_dec is proved using tactics, not by giving the explicit proof term. *) + +Fixpoint lt_bool (n m : nat) {struct n} : bool := +match n, m with +| 0, S _ => true +| S n', S m' => lt_bool n' m' +| _, 0 => false +end. + +(* The following properties are used both in Peano.v and in MPeano.v *) + +Theorem lt_bool_0 : forall x, ~ (lt_bool x 0). +Proof. +destruct x as [|x]; simpl; now intro. +Qed. + +Theorem lt_bool_S : forall x y, lt_bool x (S y) <-> lt_bool x y \/ x = y. +Proof. +induction x as [| x IH]; destruct y as [| y]; simpl. +split; [now right | now intro]. +split; [now left | now intro]. +split; [intro H; false_hyp H lt_bool_0 | +intro H; destruct H as [H | H]; now auto]. +assert (H : x = y <-> S x = S y); [split; auto|]. +rewrite <- H; apply IH. +Qed. + +(** Miscellaneous *) + +Definition less_than (x : comparison) : bool := +match x with Lt => true | _ => false end. + +Definition LE_Set : forall A : Set, relation A := (@eq). + +Lemma eq_equiv : forall A : Set, equiv A (LE_Set A). +Proof. +intro A; unfold equiv, LE_Set, reflexive, symmetric, transitive. +repeat split; [exact (@trans_eq A) | exact (@sym_eq A)]. +(* It is interesting how the tactic split proves reflexivity *) +Qed. + +Add Relation (fun A : Set => A) LE_Set + reflexivity proved by (fun A : Set => (proj1 (eq_equiv A))) + symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A)))) + transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A)))) +as EA_rel. |