~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Algebra.v -rw-r--r-- 4.9 KiB View raw
5857f238Andrew Miloradovsky .build.yml: continuous integration for SourceHut 7 months ago
                                                                                
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
Ltac super_rewrite t :=
  first [ rewrite t | rewrite <- t ].

Section Magma.

Variable A: Type.
Variable op: A -> A -> A.

Definition is_associative :=
  forall x y z: A, (op x (op y z)) = (op (op x y) z).

Definition is_left_neutral  (e: A) := forall x: A, op e x = x.
Definition is_right_neutral (e: A) := forall x: A, x = op x e.

Lemma uniqueness_of_neutral (a b: A) (la: is_left_neutral a)
                                     (rb: is_right_neutral b): (a = b).
Proof. congruence. Qed.  (* a = a b = b *)

Variable neutral: A.
Definition is_neutral := is_left_neutral neutral
                      /\ is_right_neutral neutral.
Hypothesis neutrality: is_neutral.

Definition opposite (a b: A) := (op a b) = neutral.

Hypothesis associativity: is_associative.

(*
 a b = e, b c = e ==> a = c
=======================================
 a = a e = a (b c) = (a b) c = e c = c
 *)

Lemma left_and_right_inverse (a b c: A) (oab: opposite a b)
                                        (obc: opposite b c): a = c.
Proof. case neutrality. congruence. Qed.

Variable inverse: A -> A.

Definition is_left_inverse  := forall x: A, opposite (inverse x) x.
Definition is_right_inverse := forall x: A, opposite x (inverse x).
Definition is_inverse := is_left_inverse /\ is_right_inverse.

Lemma left_cancellation (li: is_left_inverse)
  (x y z: A) (op_eq: op x y = op x z): y = z.
Proof.
  destruct neutrality as [ln rn].
  rewrite <- (ln y), <- (ln z). rewrite <- (li x).
  rewrite <- associativity, <- associativity.
  rewrite op_eq. trivial.
Qed.

Lemma right_cancellation (ri: is_right_inverse)
  (x y z: A) (op_eq: op x y = op z y): x = z.
Proof.
  destruct neutrality as [ln rn].
  rewrite -> (rn x), -> (rn z). rewrite <- (ri y).
  rewrite -> associativity, -> associativity.
  rewrite op_eq. trivial.
Qed.

Hypothesis invertibility: is_inverse.

Notation "/ x" := (inverse x).

Lemma inverse_of_neutral : / neutral = neutral.
Proof.
  destruct invertibility as [li ri].
  destruct neutrality as [ln rn].
  congruence.
Qed.

Lemma inverse_of_product (a b: A): (/ (op a b)) = (op (/ b) (/ a)).
Proof.
  case invertibility. intros li ri. case neutrality. intros ln rn.
  let lc := left_cancellation in
    rewrite (lc li (op a b) (/ (op a b)) (op (/ b) (/ a))).
  reflexivity. rewrite (ri (op a b)).
  rewrite associativity. rewrite <- (associativity a).
  rewrite ri. rewrite <- rn. rewrite ri. reflexivity.
Qed.

Lemma double_inverse : forall x, / (/ x) = x.
Proof.
  cbv in *.
  destruct invertibility as [li ri].
  destruct neutrality as [ln rn].
  intro.
  apply left_and_right_inverse with (b := / x).
  - cbv.
    rewrite <- inverse_of_product.
    rewrite ri.
    apply inverse_of_neutral.
  - cbv.
    rewrite li.
    reflexivity.
Qed.

Definition is_a_monoid := is_associative /\ is_neutral.
Definition is_a_group := is_a_monoid /\ is_inverse.
Definition is_commutative := forall x y: A, op x y = op y x.
Definition is_abelian_group := is_a_group /\ is_commutative.

End Magma.

(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Require Import Vector.
Require Import ZArith.

Section Direct_Sum.

Let V T d := Vector.t T d.  (* a shorthand *)
Definition Vector_binary_operation T op (d: nat) (a b: V T d): V T d :=
  Vector.rect2 (fun n _ _ => Vector.t T n)
  (nil T) (fun n _ _ rv x y => cons T (op x y) n rv) a b.
Definition Vector_times_left T op (d: nat) (x: T) (v: V T d): V T d :=
  Vector.map (fun y => op x y) v.
Definition Vector_times_right T op (d: nat) (x: T) (v: V T d): V T d :=
  Vector.map (fun y => op y x) v.
(* TODO: one might also prove that *_left and *_right are equivalent,
 * for the case of the operation being commutative, e.g. Z.mul *)

Definition ZVector_plus := Vector_binary_operation Z Z.add.
Definition ZVector_times := Vector_times_left Z Z.mul.

End Direct_Sum.

(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Section Ring.

Variable R: Type.
Variable plus: R -> R -> R.
Variable zero: R.
Variable negative: R -> R.

Hypotheses addition_axioms: is_abelian_group R plus zero negative.

Variable times: R -> R -> R.

Hypothesis distributivity: forall x y z: R,
  ((times x (plus y z)) = (plus (times x y) (times x z))) /\
  ((times (plus x y) z) = (plus (times x z) (times y z))).

Lemma times_zero_left: forall x: R, (times zero x) = zero.
Proof.
case addition_axioms. intros grp com.
case grp. intros mon inv.
case mon. intros assoc neu. intro.
case inv. intros li ri.
assert (rc := right_cancellation R plus zero neu assoc negative ri).
rewrite (rc (times zero x) (times x x) zero). reflexivity.
case (distributivity zero x x). case neu. congruence.
Qed.

Lemma times_zero_right: forall x: R, (times x zero) = zero.
Proof.
case addition_axioms. intros grp com.
case grp. intros mon inv.
case mon. intros assoc neu. intro.
case inv. intros li ri.
assert (lc := left_cancellation R plus zero neu assoc negative li).
rewrite (lc (times x x) (times x zero) zero). reflexivity.
case (distributivity x x zero). case neu. congruence.
Qed.

End Ring.