math-classes/math-classes

Move theory on int_to_nat to a separate file. Perform some clean up.

1 parent 7a0f939 commit 926a2ca685dc05a9cb1e28fd8f6f6e251dbed74a robbertkrebbers committed Oct 10, 2011
Showing with 286 additions and 167 deletions.
1. +11 −16 src/implementations/nonneg_integers_naturals.v
2. +15 −0 src/orders/semirings.v
3. +2 −119 src/theory/int_abs.v
4. +211 −0 src/theory/int_to_nat.v
5. +47 −32 src/theory/integers.v
27 src/implementations/nonneg_integers_naturals.v
 @@ -1,5 +1,5 @@ Require - peano_naturals orders.integers theory.integers. + peano_naturals. Require Import Ring abstract_algebra interfaces.integers interfaces.naturals interfaces.orders interfaces.additional_operations int_abs. @@ -12,38 +12,31 @@ Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Z Add Ring Z: (rings.stdlib_ring_theory Z). (* We show that [Z⁺] is an instance of the naturals by constructing a retract to [nat] *) -Program Definition of_nat (x : nat) : Z⁺ := (naturals_to_semiring nat Z x)↾_. +Program Let of_nat (x : nat) : Z⁺ := (naturals_to_semiring nat Z x)↾_. Next Obligation. apply nat_int.to_semiring_nonneg. Qed. Local Ltac unfold_equivs := unfold equiv, sig_equiv in *; simpl in *. Instance: Proper ((=) ==> (=)) of_nat. -Proof. - intros x y E. unfold_equivs. - now rewrite E. -Qed. +Proof. intros ?? E. unfold_equivs. now rewrite E. Qed. Instance: SemiRing_Morphism of_nat. Proof. - pose proof (_ : SemiRing (Z⁺)). repeat (split; try apply _); repeat intro; unfold_equivs. now apply rings.preserves_plus. unfold mon_unit, zero_is_mon_unit. now apply rings.preserves_0. now apply rings.preserves_mult. unfold mon_unit, one_is_mon_unit. now apply rings.preserves_1. Qed. -Program Instance to_nat: Inverse of_nat := λ x, int_abs Z nat (`x). +Program Let to_nat: Inverse of_nat := λ x, int_abs Z nat (`x). +Existing Instance to_nat. Instance: Proper ((=) ==> (=)) to_nat. -Proof. - intros [x Ex] [y Ey] E. unfold to_nat. unfold_equivs. - now rewrite E. -Qed. +Proof. intros [??] [??] E. unfold to_nat. unfold_equivs. now rewrite E. Qed. -Instance ZPos_to_nat_sr_morphism: SemiRing_Morphism to_nat. +Instance: SemiRing_Morphism to_nat. Proof. - pose proof (_ : SemiRing (Z⁺)). repeat (split; try apply _). intros [x Ex] [y Ey]. unfold to_nat; unfold_equivs. simpl. now apply int_abs_nonneg_plus. @@ -64,8 +57,10 @@ Qed. Global Instance: NaturalsToSemiRing (Z⁺) := naturals.retract_is_nat_to_sr of_nat. Global Instance: Naturals (Z⁺) := naturals.retract_is_nat of_nat. -Global Program Instance ZPos_cut_minus `{∀ x y : Z, Decision (x ≤ y)} : CutMinus (Z⁺) - := λ x y, if decide_rel (≤) x y then 0 else ((x : Z) - (y : Z))↾_. +Context `{∀ x y : Z, Decision (x ≤ y)}. + +Global Program Instance ZPos_cut_minus: CutMinus (Z⁺) := λ x y, + if decide_rel (≤) x y then 0 else ((x : Z) - (y : Z))↾_. Next Obligation. apply <-rings.flip_nonneg_minus. now apply orders.le_flip.
15 src/orders/semirings.v
 @@ -665,6 +665,17 @@ Section another_semiring_strict. Context `{StrictSemiRingOrder R1} `{StrictSemiRingOrder R2} `{!SemiRing_Morphism (f : R1 → R2)}. + Lemma strictly_preserving_preserves_pos : (∀ x, 0 < x → 0 < f x) → StrictlyOrderPreserving f. + Proof. + intros E. + repeat (split; try apply _). + intros x y F. + destruct (decompose_lt F) as [z [Ez1 Ez2]]. + apply compose_lt with (f z). + now apply E. + now rewrite Ez2, preserves_plus. + Qed. + Instance preserves_pos `{!StrictlyOrderPreserving f} x : PropHolds (0 < x) → PropHolds (0 < f x). Proof. intros. rewrite <-(preserves_0 (f:=f)). now apply (strictly_order_preserving f). Qed. @@ -681,3 +692,7 @@ End another_semiring_strict. (* Due to bug #2528 *) Hint Extern 15 (PropHolds (_ ≤ _ _)) => eapply @preserves_nonneg : typeclass_instances. Hint Extern 15 (PropHolds (_ < _ _)) => eapply @preserves_pos : typeclass_instances. + +(* Oddly enough, the above hints do not work for goals of the following shape? *) +Hint Extern 15 (PropHolds (_ ≤ '_)) => eapply @preserves_nonneg : typeclass_instances. +Hint Extern 15 (PropHolds (_ < '_)) => eapply @preserves_pos : typeclass_instances.
121 src/theory/int_abs.v
 @@ -1,8 +1,6 @@ -Require - theory.nat_distance. Require Import - Ring interfaces.naturals abstract_algebra interfaces.orders natpair_integers - theory.integers theory.rings orders.naturals orders.rings. + Ring interfaces.naturals abstract_algebra interfaces.orders + orders.nat_int theory.integers theory.rings orders.rings. Section contents. Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt} `{Naturals N}. @@ -25,49 +23,11 @@ Lemma int_abs_unique (a b : IntAbs Z N) (z : Z) : int_abs Z N (ia:=a) z = int_abs Z N (ia:=a) z. Proof. now apply int_abs_unique_respectful. Qed. -Lemma int_to_nat_unique_respectful {a b : IntAbs Z N} : - ((=) ==> (=))%signature (int_to_nat Z N (ia:=a)) (int_to_nat Z N (ia:= b)). -Proof. - intros x y E. unfold int_to_nat, int_abs_sig. - apply (injective (naturals_to_semiring N Z)). - destruct a as [[z1 A]|[z1 A]], b as [[z2 B]|[z2 B]]. - now rewrite A, B. - destruct (naturals.to_ring_zero_sum z2 z1) as [? E2]. - now rewrite B, A, involutive. - now rewrite E2. - destruct (naturals.to_ring_zero_sum z1 z2) as [? E2]. - now rewrite B, A, involutive. - now rewrite E2. - reflexivity. -Qed. - -Lemma int_to_nat_unique (a b : IntAbs Z N) (z : Z) : - int_to_nat Z N (ia:=a) z = int_to_nat Z N (ia:=a) z. -Proof. now apply int_to_nat_unique_respectful. Qed. - -Global Program Instance slow_int_abs: IntAbs Z N | 10 := λ x, - match int_abs_sig (SRpair N) N (integers_to_ring Z (SRpair N) x) with - | inl (n↾E) => inl n - | inr (n↾E) => inr n - end. -Next Obligation. - apply (injective (integers_to_ring Z (SRpair N))). - rewrite <-E. apply (naturals.to_semiring_twice _ _ _). -Qed. -Next Obligation. - apply (injective (integers_to_ring Z (SRpair N))). - rewrite preserves_negate, <-E. - now apply (naturals.to_semiring_twice _ _ _). -Qed. - Context `{!IntAbs Z N}. Global Instance int_abs_proper: Setoid_Morphism (int_abs Z N) | 0. Proof. split; try apply _. now apply int_abs_unique_respectful. Qed. -Global Instance int_to_nat_proper: Setoid_Morphism (int_to_nat Z N) | 0. -Proof. split; try apply _. now apply int_to_nat_unique_respectful. Qed. - Context `{!SemiRing_Morphism (f : N → Z)}. Lemma int_abs_spec x : @@ -165,81 +125,4 @@ Proof. rewrite int_abs_nonpos. ring. now apply nonpos_nonneg_mult. rewrite int_abs_nonneg. ring. now apply nonpos_mult. Qed. - -Lemma int_to_nat_spec x : - { 0 ≤ x ∧ f (int_to_nat Z N x) = x } + { x ≤ 0 ∧ int_to_nat Z N x = 0 }. -Proof. - unfold int_to_nat. destruct int_abs_sig as [[n E]|[n E]]. - left. rewrite <-E. split. - now apply to_semiring_nonneg. - apply (naturals.to_semiring_unique_alt _ _). - right. intuition. apply flip_nonpos_negate. rewrite <-E. - now apply to_semiring_nonneg. -Qed. - -Lemma int_to_nat_nat n : - int_to_nat Z N (f n) = n. -Proof. - apply (injective f). destruct (int_to_nat_spec (f n)) as [[??]|[? E]]; intuition. - rewrite E, preserves_0. apply (antisymmetry (≤)); intuition. - now apply to_semiring_nonneg. -Qed. - -Lemma int_to_nat_negate_nat n : - int_to_nat Z N (-f n) = 0. -Proof. - apply (injective f). destruct (int_to_nat_spec (-f n)) as [[? E]|[? E]]. - rewrite E, preserves_0. apply (antisymmetry (≤)); intuition. - now apply negate_to_ring_nonpos. - now rewrite E. -Qed. - -Lemma int_to_nat_0 : int_to_nat Z N 0 = 0. -Proof. rewrite <-(preserves_0 (f:=f)) at 1. now apply int_to_nat_nat. Qed. - -Lemma int_to_nat_nonneg x : - 0 ≤ x → f (int_to_nat Z N x) = x. -Proof. - intros E1. destruct (int_to_nat_spec x) as [[? E2]|[? E2]]; intuition. - rewrite E2, preserves_0. now apply (antisymmetry (≤)). -Qed. - -Lemma int_to_nat_nonpos x : - x ≤ 0 → f (int_to_nat Z N x) = 0. -Proof. - intros E. destruct (int_to_nat_spec x) as [[? E2]|[? E2]]. - rewrite E2. now apply (antisymmetry (≤)). - now rewrite E2, preserves_0. -Qed. - -Lemma int_to_nat_nonneg_plus x y : - 0 ≤ x → 0 ≤ y → int_to_nat Z N (x + y) = int_to_nat Z N x + int_to_nat Z N y. -Proof. - intros. apply (injective f). - rewrite preserves_plus, !int_to_nat_nonneg; intuition. - now apply nonneg_plus_compat. -Qed. - -Lemma int_to_nat_mult_nonneg_l x y : - 0 ≤ x → int_to_nat Z N (x * y) = int_to_nat Z N x * int_to_nat Z N y. -Proof. - intros E. apply (injective f). rewrite preserves_mult. - rewrite (int_to_nat_nonneg x) by easy. - destruct (int_to_nat_spec y) as [[? Ey]|[? Ey]]; rewrite Ey, ?preserves_0. - rewrite int_to_nat_nonneg. easy. now apply nonneg_mult_compat. - rewrite int_to_nat_nonpos. ring. now apply nonneg_nonpos_mult. -Qed. - -Lemma int_to_nat_mult_nonneg_r x y : - 0 ≤ y → int_to_nat Z N (x * y) = int_to_nat Z N x * int_to_nat Z N y. -Proof. - rewrite (commutativity x), (commutativity (int_to_nat Z N x)). - now apply int_to_nat_mult_nonneg_l. -Qed. - -Lemma int_to_nat_1 : int_to_nat Z N 1 = 1. -Proof. - apply (injective f). rewrite preserves_1. - apply int_to_nat_nonneg; solve_propholds. -Qed. End contents.
211 src/theory/int_to_nat.v
 @@ -0,0 +1,211 @@ +Require Import + Ring interfaces.naturals abstract_algebra interfaces.orders + orders.nat_int theory.integers theory.rings orders.rings. + +Section contents. +Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt} `{Naturals N}. + +Add Ring Z : (rings.stdlib_ring_theory Z). + +Lemma int_to_nat_unique_respectful {a b : IntAbs Z N} : + ((=) ==> (=))%signature (int_to_nat Z N (ia:=a)) (int_to_nat Z N (ia:= b)). +Proof. + intros x y E. unfold int_to_nat, int_abs_sig. + apply (injective (naturals_to_semiring N Z)). + destruct a as [[z1 A]|[z1 A]], b as [[z2 B]|[z2 B]]. + now rewrite A, B. + destruct (naturals.to_ring_zero_sum z2 z1) as [? E2]. + now rewrite B, A, involutive. + now rewrite E2. + destruct (naturals.to_ring_zero_sum z1 z2) as [? E2]. + now rewrite B, A, involutive. + now rewrite E2. + reflexivity. +Qed. + +Lemma int_to_nat_unique (a b : IntAbs Z N) (z : Z) : + int_to_nat Z N (ia:=a) z = int_to_nat Z N (ia:=a) z. +Proof. now apply int_to_nat_unique_respectful. Qed. + +Context `{!IntAbs Z N}. + +Global Instance int_to_nat_proper: Setoid_Morphism (int_to_nat Z N) | 0. +Proof. split; try apply _. now apply int_to_nat_unique_respectful. Qed. + +Context `{!SemiRing_Morphism (f : N → Z)}. + +Lemma int_to_nat_spec x : + { 0 ≤ x ∧ f (int_to_nat Z N x) = x } + { x ≤ 0 ∧ int_to_nat Z N x = 0 }. +Proof. + unfold int_to_nat. destruct int_abs_sig as [[n E]|[n E]]. + left. rewrite <-E. split. + now apply to_semiring_nonneg. + apply (naturals.to_semiring_unique_alt _ _). + right. intuition. apply flip_nonpos_negate. rewrite <-E. + now apply to_semiring_nonneg. +Qed. + +Lemma int_to_nat_nat n : + int_to_nat Z N (f n) = n. +Proof. + apply (injective f). destruct (int_to_nat_spec (f n)) as [[??]|[? E]]; intuition. + rewrite E, preserves_0. apply (antisymmetry (≤)); intuition. + now apply to_semiring_nonneg. +Qed. + +Lemma int_to_nat_cancel_l x n : + x = f n → int_to_nat Z N x = n. +Proof. intros E. now rewrite E, int_to_nat_nat. Qed. + +Lemma int_to_nat_cancel_r x n : + f n = x → n = int_to_nat Z N x. +Proof. intros E. now rewrite <-E, int_to_nat_nat. Qed. + +Lemma int_to_nat_negate_nat n : + int_to_nat Z N (-f n) = 0. +Proof. + apply (injective f). destruct (int_to_nat_spec (-f n)) as [[? E]|[? E]]. + rewrite E, preserves_0. apply (antisymmetry (≤)); intuition. + apply rings.flip_nonneg_negate. now apply to_semiring_nonneg. + now rewrite E. +Qed. + +Lemma int_to_nat_0 : int_to_nat Z N 0 = 0. +Proof. apply int_to_nat_cancel_l. now rewrite preserves_0. Qed. + +Lemma int_to_nat_of_nonneg x : + 0 ≤ x → f (int_to_nat Z N x) = x. +Proof. + intros E1. destruct (int_to_nat_spec x) as [[? E2]|[? E2]]; intuition. + rewrite E2, preserves_0. now apply (antisymmetry (≤)). +Qed. + +Lemma int_to_nat_of_nonpos x : + x ≤ 0 → int_to_nat Z N x = 0. +Proof. + intros E. destruct (int_to_nat_spec x) as [[? E2]|]; intuition. + apply int_to_nat_cancel_l. rewrite preserves_0. + now apply (antisymmetry (≤)). +Qed. + +Lemma int_to_nat_nonneg_plus x y : + 0 ≤ x → 0 ≤ y → int_to_nat Z N (x + y) = int_to_nat Z N x + int_to_nat Z N y. +Proof. + intros. apply (injective f). + rewrite preserves_plus, !int_to_nat_of_nonneg; intuition. + now apply nonneg_plus_compat. +Qed. + +Lemma int_to_nat_mult_nonneg_l x y : + 0 ≤ x → int_to_nat Z N (x * y) = int_to_nat Z N x * int_to_nat Z N y. +Proof. + intros E. apply (injective f). rewrite preserves_mult. + rewrite (int_to_nat_of_nonneg x) by easy. + destruct (int_to_nat_spec y) as [[? Ey]|[? Ey]]; rewrite Ey, ?preserves_0. + rewrite int_to_nat_of_nonneg. easy. now apply nonneg_mult_compat. + rewrite int_to_nat_of_nonpos, preserves_0. ring. now apply nonneg_nonpos_mult. +Qed. + +Lemma int_to_nat_mult_nonneg_r x y : + 0 ≤ y → int_to_nat Z N (x * y) = int_to_nat Z N x * int_to_nat Z N y. +Proof. + rewrite (commutativity x), (commutativity (int_to_nat Z N x)). + now apply int_to_nat_mult_nonneg_l. +Qed. + +Lemma int_to_nat_1 : int_to_nat Z N 1 = 1. +Proof. apply int_to_nat_cancel_l. now rewrite preserves_1. Qed. + +Context `{Apart N} `{!TrivialApart N} `{!FullPseudoSemiRingOrder (A:=N) Nle Nlt}. + +Global Instance int_to_nat_nonneg x : + PropHolds (0 ≤ int_to_nat Z N x). +Proof. + destruct (int_to_nat_spec x) as [[? E]|[? E]]. + apply (order_reflecting f). now rewrite preserves_0, E. + rewrite E. solve_propholds. +Qed. + +Global Instance int_to_nat_pos x : + PropHolds (0 < x) → PropHolds (0 < int_to_nat Z N x). +Proof. + rewrite !lt_iff_le_ne. intros [??]. split. + solve_propholds. + apply (setoids.morphism_ne f). + now rewrite preserves_0, int_to_nat_of_nonneg. +Qed. + +Lemma int_to_nat_le_l x y : + 0 ≤ x → x ≤ y → f (int_to_nat Z N x) ≤ y. +Proof. intros. now rewrite int_to_nat_of_nonneg. Qed. + +Lemma int_to_nat_le_cancel_l x n : + 0 ≤ x → x ≤ f n → int_to_nat Z N x ≤ n. +Proof. intros. now apply (order_reflecting f), int_to_nat_le_l. Qed. + +Lemma int_to_nat_le_r x y : + x ≤ y → x ≤ f (int_to_nat Z N y). +Proof. + intros E1. destruct (int_to_nat_spec y) as [[? E2]|[? E2]]. + now rewrite E2. + rewrite E2, preserves_0. now transitivity y. +Qed. + +Lemma int_to_nat_le_cancel_r x n : + f n ≤ x → n ≤ int_to_nat Z N x. +Proof. intros. now apply (order_reflecting f), int_to_nat_le_r. Qed. + +Global Instance: OrderPreserving (int_to_nat Z N). +Proof. + repeat (split; try apply _). intros x y E. + destruct (total (≤) 0 x). + now apply int_to_nat_le_cancel_r, int_to_nat_le_l. + rewrite int_to_nat_of_nonpos. solve_propholds. easy. +Qed. + +Lemma int_to_nat_le_back x y : + 0 ≤ y → int_to_nat Z N x ≤ int_to_nat Z N y → x ≤ y. +Proof. + intros. rewrite <-(int_to_nat_of_nonneg y) by easy. + transitivity (f (int_to_nat Z N x)). + now apply int_to_nat_le_r. + now apply (order_preserving f). +Qed. + +Lemma int_to_nat_lt_l x y : + 0 ≤ x → x < y → f (int_to_nat Z N x) < y. +Proof. intros. now rewrite int_to_nat_of_nonneg. Qed. + +Lemma int_to_nat_lt_cancel_l x n : + 0 ≤ x → x < f n → int_to_nat Z N x < n. +Proof. intros. now apply (strictly_order_reflecting f), int_to_nat_lt_l. Qed. + +Lemma int_to_nat_lt_r x y : + x < y → x < f (int_to_nat Z N y). +Proof. + intros E1. destruct (int_to_nat_spec y) as [[? E2]|[? E2]]. + now rewrite E2. + rewrite E2, preserves_0. now apply lt_le_trans with y. +Qed. + +Lemma int_to_nat_lt_cancel_r x n : + f n < x → n < int_to_nat Z N x. +Proof. intros. now apply (strictly_order_reflecting f), int_to_nat_lt_r. Qed. + +Lemma int_to_nat_lt x y : + 0 < y → x < y → int_to_nat Z N x < int_to_nat Z N y. +Proof. + intros Ey Exy. destruct (total (≤) 0 x). + now apply int_to_nat_lt_cancel_r, int_to_nat_lt_l. + rewrite int_to_nat_of_nonpos by easy. now apply int_to_nat_pos. +Qed. + +Lemma int_to_nat_lt_back x y : + 0 ≤ y → int_to_nat Z N x < int_to_nat Z N y → x < y. +Proof. + intros. rewrite <-(int_to_nat_of_nonneg y) by easy. + apply le_lt_trans with (f (int_to_nat Z N x)). + now apply int_to_nat_le_r. + now apply (strictly_order_preserving f). +Qed. +End contents.
79 src/theory/integers.v
 @@ -8,73 +8,73 @@ Require Export (* Any two integer implementations are trivially isomorphic because of their initiality, but it's nice to have this stated in terms of integers_to_ring being self-inverse: *) -Lemma to_ring_involutive `{Integers Int} Int2 `{Integers Int2} x : - integers_to_ring Int2 Int (integers_to_ring Int Int2 x) = x. +Lemma to_ring_involutive `{Integers Z} Z2 `{Integers Z2} x : + integers_to_ring Z2 Z (integers_to_ring Z Z2 x) = x. Proof. - rapply (proj2 (@categories.initials_unique' _ _ _ _ _ _ (rings.object Int) (rings.object Int2) _ + rapply (proj2 (@categories.initials_unique' _ _ _ _ _ _ (rings.object Z) (rings.object Z2) _ integers_initial _ integers_initial) tt x). Qed. -Lemma to_ring_unique `{Integers Int} `{Ring R} (f: Int → R) {h: SemiRing_Morphism f} x : - f x = integers_to_ring Int R x. +Lemma to_ring_unique `{Integers Z} `{Ring R} (f: Z → R) {h: SemiRing_Morphism f} x : + f x = integers_to_ring Z R x. Proof. symmetry. pose proof (rings.encode_morphism_and_ops (f:=f)). set (@varieties.arrow rings.theory _ _ _ (rings.encode_variety_and_ops _) _ _ _ (rings.encode_variety_and_ops _) (λ _, f) _). exact (integers_initial _ a tt x). Qed. -Lemma to_ring_unique_alt `{Integers Int} `{Ring R} (f g: Int → R) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x : +Lemma to_ring_unique_alt `{Integers Z} `{Ring R} (f g: Z → R) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x : f x = g x. Proof. now rewrite (to_ring_unique f), (to_ring_unique g). Qed. -Lemma morphisms_involutive `{Integers N} `{Integers N2} (f: N → N2) (g: N2 → N) +Lemma morphisms_involutive `{Integers Z} `{Integers Z2} (f: Z → Z2) (g: Z2 → Z) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x : f (g x) = x. Proof. now apply (to_ring_unique_alt (f ∘ g) id). Qed. -Lemma to_ring_twice `{Integers N} `{Ring R1} `{Ring R2} (f : R1 → R2) (g : N → R1) (h : N → R2) +Lemma to_ring_twice `{Integers Z} `{Ring R1} `{Ring R2} (f : R1 → R2) (g : Z → R1) (h : Z → R2) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} `{!SemiRing_Morphism h} x : f (g x) = h x. Proof. now apply (to_ring_unique_alt (f ∘ g) h). Qed. -Lemma to_ring_self `{Integers N} (f : N → N) `{!SemiRing_Morphism f} x : f x = x. +Lemma to_ring_self `{Integers Z} (f : Z → Z) `{!SemiRing_Morphism f} x : f x = x. Proof. now apply (to_ring_unique_alt f id). Qed. (* A ring morphism from integers to another ring is injective if there's an injection in the other direction: *) -Lemma to_ring_injective `{Integers Int} `{Ring R} (f: R → Int) (g: Int → R) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g}: +Lemma to_ring_injective `{Integers Z} `{Ring R} (f: R → Z) (g: Z → R) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g}: Injective g. Proof. repeat (split; try apply _). intros x y E. rewrite <-(to_ring_self (f ∘ g) x), <-(to_ring_self (f ∘ g) y). unfold compose. now rewrite E. Qed. -Instance integers_to_integers_injective `{Integers Int} `{Integers Int2} (f: Int → Int2) `{!SemiRing_Morphism f}: +Instance integers_to_integers_injective `{Integers Z} `{Integers Z2} (f: Z → Z2) `{!SemiRing_Morphism f}: Injective f. -Proof. apply (to_ring_injective (integers_to_ring Int2 Int) _). Qed. +Proof. apply (to_ring_injective (integers_to_ring Z2 Z) _). Qed. -Instance naturals_to_integers_injective `{Integers Int} `{Naturals N} (f: N → Int) `{!SemiRing_Morphism f} : +Instance naturals_to_integers_injective `{Integers Z} `{Naturals N} (f: N → Z) `{!SemiRing_Morphism f} : Injective f. Proof. split; try apply _. intros x y E. apply (injective (cast N (SRpair N))). - now rewrite <-2!(naturals.to_semiring_twice (integers_to_ring Int (SRpair N)) f (cast N (SRpair N))), E. + now rewrite <-2!(naturals.to_semiring_twice (integers_to_ring Z (SRpair N)) f (cast N (SRpair N))), E. Qed. Section retract_is_int. - Context `{Integers Int} `{Ring Int2}. - Context (f : Int → Int2) `{!Inverse f} `{!Surjective f} `{!SemiRing_Morphism f} `{!SemiRing_Morphism (f⁻¹)}. + Context `{Integers Z} `{Ring Z2}. + Context (f : Z → Z2) `{!Inverse f} `{!Surjective f} `{!SemiRing_Morphism f} `{!SemiRing_Morphism (f⁻¹)}. (* If we make this an instance, then instance resolution will often loop *) - Definition retract_is_int_to_ring : IntegersToRing Int2 := λ R _ _ _ _ _, integers_to_ring Int R ∘ f⁻¹. + Definition retract_is_int_to_ring : IntegersToRing Z2 := λ Z2 _ _ _ _ _, integers_to_ring Z Z2 ∘ f⁻¹. Section for_another_ring. Context `{Ring R}. - Instance: SemiRing_Morphism (integers_to_ring Int R ∘ f⁻¹) := {}. - Context (h : Int2 → R) `{!SemiRing_Morphism h}. + Instance: SemiRing_Morphism (integers_to_ring Z R ∘ f⁻¹) := {}. + Context (h : Z2 → R) `{!SemiRing_Morphism h}. - Lemma same_morphism: integers_to_ring Int R ∘ f⁻¹ = h. + Lemma same_morphism: integers_to_ring Z R ∘ f⁻¹ = h. Proof with auto. intros x y F. rewrite <-F. transitivity ((h ∘ (f ∘ f⁻¹)) x). @@ -84,38 +84,53 @@ Section retract_is_int. End for_another_ring. (* If we make this an instance, then instance resolution will often loop *) - Program Instance retract_is_int: Integers Int2 (U:=retract_is_int_to_ring). + Program Instance retract_is_int: Integers Z2 (U:=retract_is_int_to_ring). Next Obligation. unfold integers_to_ring, retract_is_int_to_ring. apply _. Qed. Next Obligation. apply integer_initial. intros. now apply same_morphism. Qed. End retract_is_int. Section contents. -Context `{Integers Int}. +Context `{Integers Z}. -Global Program Instance: ∀ x y: Int, Decision (x = y) | 10 := λ x y, - match decide (integers_to_ring Int (SRpair nat) x = integers_to_ring Int (SRpair nat) y) with +Global Program Instance: ∀ x y: Z, Decision (x = y) | 10 := λ x y, + match decide (integers_to_ring Z (SRpair nat) x = integers_to_ring Z (SRpair nat) y) with | left E => left _ | right E => right _ end. -Next Obligation. now apply (injective (integers_to_ring Int (SRpair nat))). Qed. +Next Obligation. now apply (injective (integers_to_ring Z (SRpair nat))). Qed. Next Obligation. intros F. apply E. now rewrite F. Qed. -Instance: PropHolds ((1:Int) ≠ 0). +Global Program Instance slow_int_abs `{Naturals N} : IntAbs Z N | 10 := λ x, + match int_abs_sig (SRpair N) N (integers_to_ring Z (SRpair N) x) with + | inl (n↾E) => inl n + | inr (n↾E) => inr n + end. +Next Obligation. + apply (injective (integers_to_ring Z (SRpair N))). + rewrite <-E. apply (naturals.to_semiring_twice _ _ _). +Qed. +Next Obligation. + apply (injective (integers_to_ring Z (SRpair N))). + rewrite rings.preserves_negate, <-E. + now apply (naturals.to_semiring_twice _ _ _). +Qed. + +Instance: PropHolds ((1:Z) ≠ 0). Proof. intros E. apply (rings.is_ne_0 (1:nat)). - apply (injective (naturals_to_semiring nat Int)). + apply (injective (naturals_to_semiring nat Z)). now rewrite rings.preserves_0, rings.preserves_1. Qed. -Global Instance: ZeroProduct Int. +Global Instance: ZeroProduct Z. Proof. intros x y E. - destruct (zero_product (integers_to_ring Int (SRpair nat) x) (integers_to_ring Int (SRpair nat) y)). + destruct (zero_product (integers_to_ring Z (SRpair nat) x) (integers_to_ring Z (SRpair nat) y)). now rewrite <-rings.preserves_mult, E, rings.preserves_0. - left. apply (injective (integers_to_ring Int (SRpair nat))). now rewrite rings.preserves_0. - right. apply (injective (integers_to_ring Int (SRpair nat))). now rewrite rings.preserves_0. + left. apply (injective (integers_to_ring Z (SRpair nat))). now rewrite rings.preserves_0. + right. apply (injective (integers_to_ring Z (SRpair nat))). now rewrite rings.preserves_0. Qed. -Global Instance: IntegralDomain Int := {}. +Global Instance: IntegralDomain Z := {}. End contents.