1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
From Coq Require Import Ring.
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations
MathClasses.interfaces.orders MathClasses.interfaces.integers
MathClasses.orders.semirings MathClasses.theory.shiftl MathClasses.theory.int_pow.
Local Existing Instance pseudo_srorder_semiring.
Section positive_semiring_elements.
Context `{FullPseudoSemiRingOrder R} `{!PropHolds (1 ≶ 0)}.
Add Ring R : (rings.stdlib_semiring_theory R).
(* * Embedding of R₊ into R *)
Global Instance Pos_inject: Cast (R₊) R := @proj1_sig R _.
(* Operations *)
Global Program Instance Pos_plus: Plus (R₊) := λ x y, (`x + `y)↾_.
Next Obligation.
destruct x as [x Hx], y as [y Hy].
now apply pos_plus_compat.
Qed.
Global Program Instance Pos_mult: Mult (R₊) := λ x y, (`x * `y)↾_.
Next Obligation with auto.
destruct x as [x Hx], y as [y Hy].
now apply pos_mult_compat.
Qed.
Global Program Instance Pos_1: One (R₊) := (1 : R).
Next Obligation. now apply lt_0_1. Qed.
(* * Equalitity *)
Local Ltac unfold_equivs := unfold equiv, sig_equiv in *; simpl in *.
Global Instance: Proper ((=) ==> (=) ==> (=)) Pos_plus.
Proof.
intros [x1 Ex1] [y1 Ey1] E1 [x2 Ex2] [y2 Ey2] E2. unfold_equivs.
now rewrite E1, E2.
Qed.
Global Instance: Proper ((=) ==> (=) ==> (=)) Pos_mult.
Proof.
intros [x1 Ex1] [y1 Ey1] E1 [x2 Ex2] [y2 Ey2] E2. unfold_equivs.
now rewrite E1, E2.
Qed.
Instance: Proper ((=) ==> (=)) Pos_inject.
Proof. now repeat intro. Qed.
Global Instance: Injective Pos_inject.
Proof. now repeat (split; try apply _). Qed.
Section shiftl.
Context `{SemiRing B} `{!Biinduction B} `{!ShiftLSpec R B sl}.
Global Program Instance Pos_shiftl: ShiftL (R₊) B | 5 := λ x n,
(`x ≪ n)↾_.
Next Obligation. destruct x. now apply shiftl_pos. Qed.
End shiftl.
End positive_semiring_elements.
Section int_pow.
Context `{DecField R} `{Apart R} `{!FullPseudoSemiRingOrder Rle Rlt}
`{!TrivialApart R} `{∀ x y : R, Decision (x = y)} `{Integers B} `{!IntPowSpec R B ipw}.
Global Program Instance Pos_int_pow: Pow (R₊) B | 5 := λ x n,
(`x ^ n)↾_.
Next Obligation. destruct x. now apply int_pow_pos. Qed.
End int_pow.
|
