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
71
72
73
74
75
76
77
78
79
80
81
82
|
Require Import NPlus.
Require Export ZPlus.
Require Export ZPairsAxioms.
Module NatPairsPlus (Import NPlusModule : NPlusSignature) <: ZPlusSignature.
Module Export IntModule := NatPairsInt NPlusModule.
Open Local Scope NatScope.
Definition plus (x y : Z) := ((fst x) + (fst y), (snd x) + (snd y)).
Definition minus (x y : Z) := ((fst x) + (snd y), (snd x) + (fst y)).
Definition uminus (x : Z) := (snd x, fst x).
(* Unfortunately, the elements of pair keep increasing, even during subtraction *)
Notation "x + y" := (plus x y) : IntScope.
Notation "x - y" := (minus x y) : IntScope.
Notation "- x" := (uminus x) : IntScope.
(* Below, we need to rewrite subtems that have several occurrences.
Since with the currect setoid_rewrite we cannot point an accurrence
using pattern, we use symmetry tactic to make a particular occurrence
the leftmost, since that is what rewrite will use. *)
Add Morphism plus with signature E ==> E ==> E as plus_wd.
Proof.
unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl.
pose proof (plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1
(fst x2 + snd y2) (fst y2 + snd x2) H2) as H.
rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1.
Qed.
Add Morphism minus with signature E ==> E ==> E as minus_wd.
Proof.
unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl.
rewrite plus_comm in H2. symmetry in H2; rewrite plus_comm in H2.
pose proof (NPlusModule.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1
(snd x2 + fst y2) (snd y2 + fst x2) H2) as H.
rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1.
Qed.
Add Morphism uminus with signature E ==> E as uminus_wd.
Proof.
unfold E, plus; intros x y H; simpl.
rewrite plus_comm. symmetry. now rewrite plus_comm.
Qed.
Open Local Scope IntScope.
Theorem plus_0 : forall n, 0 + n == n.
Proof.
intro n; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_0_l.
Qed.
Theorem plus_S : forall n m, (S n) + m == S (n + m).
Proof.
intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_S_l.
Qed.
Theorem minus_0 : forall n, n - 0 == n.
Proof.
intro n; unfold minus, E; simpl. now do 2 rewrite plus_0_r.
Qed.
Theorem minus_S : forall n m, n - (S m) == P (n - m).
Proof.
intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_S_r.
Qed.
Theorem uminus_0 : - 0 == 0.
Proof.
unfold uminus, E; simpl. now rewrite plus_0_l.
Qed.
Theorem uminus_S : forall n, - (S n) == P (- n).
Proof.
reflexivity.
Qed.
End NatPairsPlus.
Module NatPairsPlusProperties (NPlusModule : NPlusSignature).
Module Export NatPairsPlusModule := NatPairsPlus NPlusModule.
Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule.
End NatPairsPlusProperties.
|
